I've been trying to test some QuickCheck generators in the CakeML
formalization, like so:
Unfortunately, it seems that they fail occasionally. I've tried
increasing the timeout, but that still seems to be problematic.
Is there a way to make these tests more robust? I don't want to comment
out the checks because much of the QuickCheck setup silently fails if
something is broken; meaning e.g. that Auto QuickCheck just doesn't work
on a proposition where it should work.
isabelle-dev mailing list