On 04/18/2012 08:26 PM, Florian Haftmann wrote:
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.
Undoubtedly, Quickcheck has to produce a few "large terms" for each
record to support them.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
