[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
makarius at sketis.net
Tue Sep 20 21:20:49 CEST 2011
On Tue, 13 Sep 2011, Lars Noschinski wrote:
>> . Reduced CPU performance requirements, usable on machines with few
>> . Reduced memory requirements due to pruning of unused document
>> versions (garbage collection).
> As some data point: I was able to load HOL/Probability/Probability.thy
> (using HOL-Image), but needed my whole memory for this (6GiB).
In the meantime I have investigated this a little bit. It seems that
HOL-Probability requires quite some memory even in minimalistic batch mode
-- approx. 2GB on my 4GB machine. With Isabelle/jEdit one needs further
600 MB for the editor process and the same (and more) for the fully
persistent document state within ML. So it adds up to something > 4 GB
such that it becomes infeasible to edit the full session live on a "small"
laptop with "only" 4 GB.
Most other Isabelle example sessions are less bulky, and can be loaded
comfortably into the Prover IDE with its persistent document model
(MicroJava, Bali, Auth etc.) -- all on my plain Mac Book Pro from 2 years
ago: 2 cores, 4 GB.
I have also made some further experiments with AFP on a solid workstation
with 8 cores and 32 GB: editing Flyspeck is quite comfortable using only 4
GB for the Poly/ML heap. (Disposing old 'types' commands throughout the
theories was an easy job of a few minutes.)
What is also fun is to load many sessions into the same prover process.
This works because fully qualified file names are used to identify the
"document nodes" in PIDE parlance, although the theory namespace itself is
still flat. (This would affect cross-imports between the loaded
There are some limits to this madness: overloading the Poly/ML process
with 5-10 big sessions -- using tons of GBs heap space -- sometimes makes
the ML runtime system crash in a hard way. Probably in the same way
isatest occasionally crashes. Interestingly, I have seen the JVM get into
trouble much earlier concerning heap usage -- beyond 2 GB it can get quite
More information about the isabelle-dev