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

Reply via email to