[isabelle-dev] Towards the next release

[Florian Haftmann]

Hi all,

> - I would like to add a size limit to records beyond which no code generator setup is performed. The main reason is that on sizes > 200 fields or so, the setup does not make any sense, but consumes very large amounts of memory (and time). Switching it off gets rid of almost all of the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit:
>  1) as an option available the user at record definition time
>  2) as an option/flag to the internal record definition function only
>  3) as a configuration option
>  4) as a compile time constant 
> 
> There is a third small thing that I will discuss separately with Florian: there is a bug in the code generator setup in Isabelle2011-1 somewhere in generating narrowing lemmas. It is triggered for records with more than ~530 fields where it constructs a lemma of the form  "f ty = g a b .. aa ab .. tw tx ty tz .." where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version.

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.

I would strongly recommend not to sacrifice a) for a »optimisiation«
(once I had something similar in the datatype package and it produced a
lot of pain); basically, it uses theorems which are »almost there« anyway.

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).
Commenting out ensure_random_record and ensure_exhaustive_record in
function add_code coulde make a good start.

Also note that most of the quickcheck addons are by Lukas, not me ;-)

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/20120418/785797ad/attachment.sig>