[isabelle-dev] Editing large sessions with Isabelle/jEdit
makarius at sketis.net
Thu Dec 6 14:20:09 CET 2012
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
> 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
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4
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.
More information about the isabelle-dev