[isabelle-dev] Quickcheck Examples
florian.haftmann at informatik.tu-muenchen.de
Fri Feb 24 18:26:59 CET 2012
Am 24.02.2012 09:09, schrieb Lukas Bulwahn:
> On 02/18/2012 10:18 AM, Florian Haftmann wrote:
>>> How much relative time do the quickcheck examples in HOL-ex take?
>>> According to my feeling time could be high to separate these into a
>>> separate session, to facilitate maintenance.
> I separated the Quickcheck-Examples from HOL-ex into an own session (cf.
thanks a lot.
> The latest performance numbers do not show that the run time reduced, so
> either there is really another bottleneck or my own change has not had
> any effect on the measurements yet?
> (cf. http://isabelle.in.tum.de/devel/stats/at-poly/HOL-ex.png)
Now it had.
> If Library-Codegenerator-Test works, you only know that you get source
> code that compiles correctly.
> With the Quickcheck-Examples session, you know that the source code also
> runs correctly.
On the other hand, Library-Codegenerator-Test is more pervasive.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev