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