[isabelle-dev] Towards the next release

[Makarius]

On Tue, 17 Apr 2012, Gerwin Klein wrote:

> - 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.

If 3) means "configuration option" in the sense of Config.T, here is the 
canonical 1-liner to make one for a package:

   val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);

You then merely export that in the signature, and use it with Config.get 
in the package implementation, on the context that is already there 
anyway. (For non-localized packages Config.get_global approximates that.)


Concerning performance issues in general, I've recently made a lot of 
measurements.  It seems indeed that the code generator is responsible for 
quite a bit of it, although I did not look any further into its depths. 
Instead I've made some performance tuning for the critical infrastructure 
for localizing big packages with big application.

Moreover, David Matthews is right now reforming the Poly/ML runtime 
system, such that we might see an improvement of an order of magnitude 
soon.  Maybe even a renaissance of 32bit mode for reasonable big 
applications -- if this works for the infamous JinjaThreads is still to be 
seen (right now it cannot be tested because it is still broken in 
AFP/8469825f5d1b).


 	Makarius