[isabelle-dev] Towards the next release

[Gerwin Klein]

On 19/04/2012, at 4:26 AM, Florian Haftmann wrote:
> I think it is very important to differentiate here into more detail.
> There is not »the« code generator setup but a layered one:
> a) Registering a record, its projections and quality on the record as an
> executable program fragment
> b) Provided support for all those funny quickcheck generators.
[..]
> What happens in b) is much more ambitious, and if this is really a
> bottleneck, an option like »record_quickcheck« could do the job.
> 
> But I think before to settle here it is important to have more detailed
> benchmarks about records which separates figures for a) and b).
[..]

I've done the measurements now, using time as a somewhat poor substitute for memory, but it's still indicative I think.

The results for a 500 field record with plain Isabelle2009-1 as 100% base line are:

no code generator setup at all (fastest): 140% runtime
code generator, but no quickcheck:        166% runtime
plain Isabelle rev 940953b0:              201% runtime

So, you're right that the bulk is in the quickcheck setup, but just the code generator alone is still significant.

Since the number of users for this switch is going to be fairly close to 1 for the foreseeable future, I'll implement just the drastic off-switch, not the staged variant. I don't think that the case where you do want to generate code for gigantic records, but don't want the quickcheck setup is going to occur any time soon. If against all odds it does occur, we can reconsider and add a second option.

None of this should ever be visible for normal users with normal records. The default is still the full setup with everything.

Cheers,
Gerwin