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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
