[isabelle-dev] Quickcheck Examples

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

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)

Maybe we could also get performance measurements for the new session?

I hope it facilitates maintenance nevertheless.
Although if Quickcheck fails (or does not terminate) after some changes, 
this usually indicates that there is some flaw in the code generation setup.
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.


Lukas