[isabelle-dev] Quickcheck Examples

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Feb 24 18:26:59 CET 2012

Hi Lukas,

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.
> http://isabelle.in.tum.de/repos/isabelle/rev/f462e49eaf11)

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.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120224/4cf9bfb4/attachment.sig>

More information about the isabelle-dev mailing list