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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev