[isabelle-dev] Quickcheck Examples

[Florian Haftmann]

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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