On 06.12.2012 14:20, Makarius wrote:
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.
[...]
So this seems to mean JVM memory ...
Yes, I was talking about JVM memory (which is shown in the lower right
corner of jEdit).
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'll keep this in mind for the next time it happens.
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
