[isabelle-dev] Testing the QuickCheck setup

[Lars Hupel]

Dear list,

I've been trying to test some QuickCheck generators in the CakeML
formalization, like so:

<https://bitbucket.org/isa-afp/afp-devel/commits/c9f0f80df2108eb2772c6b9492e913f9236613db>

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.

Cheers
Lars