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

Re: [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:



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

[isabelle-dev] Testing the QuickCheck setup

[Lars Hupel]

Dear list,

I've been trying to test some QuickCheck generators in the CakeML
formalization, like so:



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