[isabelle-dev] Towards the next release

[Gerwin Klein]

On 12/04/2012, at 7:02 PM, Makarius wrote:
> we need to get to a more concrete release schedule.  Presently I would like to aim for late May, which means we need to start consolidating and converging about now.
> 
> Are there any further big things in the pipeline?

There are two small things from the NICTA side in the pipeline (should be in by end of April):

- Tom would like to add a tactic for bit-wise proofs on machine words, based on Sacha's and his work a while back. This is one is ready, I'll push it to the test board later and add it to the repository if everything works.

- 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 

I'm currently in favour of 4, because the limit is very specialised and will only really occur for records that are somehow automatically generated in which case the code generator setup is very unlikely to make sense. Options 1 and 3 would require adding syntax/configuration names which is not really worth it. Option 2 threads yet another obscure parameter through a rather large package. 

I'm open to other ideas/comments/feedback, though.

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.

Cheers,
Gerwin