[isabelle-dev] Editing large sessions with Isabelle/jEdit

[Makarius]

On Thu, 6 Dec 2012, Lars Noschinski wrote:

> Does this also influence memory usage?

Probably not.  In general one also needs to distinguish ML and JVM 
resources.  David Matthews made Poly/ML 5.5.0 ultra-smart in memory 
management, and the JVM still cannot quite compete.


> In the last weeks, I occasionally had the problem that Isabelle/jEdit 
> sort-of ran out of memory on long-running sessions.

So this seems to mean JVM memory ...

If it is ML nonetheless, I am presently working on some monitoring there. 
The system option ML_statistics already emits raw data on stderr.


> With "sort-of", I mean that the word stopped for a few seconds 
> (apparently for garbage collection). Memory usage then dropped to around 
> 750 of 1000MiB, but filled up very quickly again, even if I was just 
> browsing around, not making any changes (This was with my graph library, 
> which hasn't a current, publicly available copy at the moment. But it is 
> definitely small compared to e.g. Probability).

Did you try to monitor the JVM process already?  I usually use jconsole or 
jvisualvm.  None of them is really good, so I switch back and forth and 
make guesses.


> I might just need to increase the default memory limit of the JVM.

I normally work with something like this on 8 cores + 32 GB physical 
memory (etc/settings):

JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4 
-Dactors.enableForkJoin=false"


It is a bit like ancient Mac OS (until version 6 or 7): before starting an 
application you have to provide a hard limit for its ressource usage.


 	Makarius