[isabelle-dev] Testing the QuickCheck setup

[Andreas Lochbihler]

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