[isabelle-dev] Towards the next release
gerwin.klein at nicta.com.au
Thu Apr 19 01:32:20 CEST 2012
On 19/04/2012, at 4:26 AM, 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.
It's not an optimisation for us. It's the choice between using Isabelle or not. I'm happy to sacrifice a lot of features for that choice..
> 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.
My feeling is that the problem already occurs in a), but you are right, this needs to be confirmed. I'll measure and see how things go.
Btw, it's easy to reproduce: just make a theory file based on HOL (Main.thy) that defines a record with 600 fields. Run it in Isabelle-2009-1 and the current version for comparison.
> Also note that most of the quickcheck addons are by Lukas, not me ;-)
Sorry, I had just assumed that anything that looks like code generator is in your domain ;-)
More information about the isabelle-dev