[isabelle-dev] Testing the QuickCheck setup

[Lars Hupel]

Hi Andreas,

thanks, you're making some good points.

> 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?

No, it fails on all of them.

> 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.

I'll apply both changes, in the hope that it makes it more robust.

Cheers
Lars