[isabelle-dev] Testing the QuickCheck setup
hupel at in.tum.de
Mon Aug 6 07:57:45 CEST 2018
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.
More information about the isabelle-dev