[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)

[Makarius]

On Tue, 13 Sep 2011, Lars Noschinski wrote:

>> . Reduced CPU performance requirements, usable on machines with few
>> cores.
>> 
>> . 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 
sessions.)

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


 	Makarius