Dear Lars,

Testing quickcheck is indeed quite tricky. Do you know which of the quickcheck calls time out? Does it happen only with the random generator or also with exhaustive?


It might be that you have a fairly large set of code equations and the timeout already kicks in during code generation or compilation with PolyML, though. A larger timeout should help there.

Moreover, both statements have two free variables and you rely on the quickcheck generators being able to quickly come up with two different values for them. If you are not to set on the property, you could alternatively use

lemma "x ~= x" for x :: dec

which will definitely fail on the first generated example.

Hope this helps,
Andreas

On 06/08/18 07:57, Lars Hupel wrote:
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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to