[isabelle-dev] Testing the QuickCheck setup

Lars Hupel hupel at in.tum.de
Mon Aug 6 07:57:45 CEST 2018

Dear list,

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 mailing list