Email Gateway (Aug 22 2022 at 09:53): Email Gateway (Aug 22 2022 at 09:53):From: Peter Lammich <lammich@in.tum.de>
Hi
I have roughly 100 theory files loaded,
and the IDE grays out every minute or so.
Are there some options to make the IDE more responsive on my machine
(8virtual cores, 16GiB RAM)? Or is the IDE just not suited for those
(medium size) developments?
As a workaround, I could make an even more fine-rained image-hierarchy,
with is cumbersome to work with, especially when doing maintenance or
cleanup tasks, moving lots of stuff around, mostly into library theories
(which would be in the image then)
Email Gateway (Aug 22 2022 at 09:53):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
My settings are
JEDIT_JAVA_OPTIONS="-Xms256m -Xmx4096m -Xss4m”
and I’ve so far been able to work fairly nicely with that on > 60 files, many of them large.
Going from 1GB max heap size to 4GB made a huge difference for jEdit (I had forgotten to set the max heap size on my laptop before and had fairly frequent gray-outs which just turned out to be Java garbage collecting).
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:53):From: Peter Lammich <lammich@in.tum.de>
After writing the mail, I tested
JEDIT_JAVA_OPTIONS="-Xms2048m -Xmx8192m -Xss8m"
ML_OPTIONS="-H 4000 --gcthreads 2"
without really knowing what I am doing.
And it just grayed out again on ~80 files, but recovered after 2
minutes ...
Email Gateway (Aug 22 2022 at 09:53):From: Peter Lammich <lammich@in.tum.de>
I can almost reliably produce a grayout as follows:
1) Load a theory that depends on (roughly) 80 other theories.
2) Check it in the theories buffer (Alternatively, have it open in
another window).
3) Go back to one of the dependent theories, and edit something there.
During editing in step 3, I will, almost surely, get a grayout after a
few seconds ...
I find this really annoying, since it interferes with two very important
use-patterns of mine:
1) Maintenance: Load some theories with some lib changed, and try to
fix the errors, while the rest is, of course, processed in the
background.
2) Working with multiple windows. If one window happens to show an
ancestor theory of what I am currently editing, chances for grayout
increase ...
-- Peter
p.s.: Currentyl using
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m"
ML_OPTIONS="-H 4096 --gcthreads 2"
and the grayouts that I get do not recover within 5 minutes ...
Email Gateway (Aug 22 2022 at 09:54):From: Makarius <makarius@sketis.net>
You have 4 real cores, so you should use them for GC as well. Without
the --gcthreads you should get that already by default, since David
Matthews counts the physical threads, not the logical hyperthreads.
I guess that most of the greyout time is for ML memory management. On the
isabelle-users thread "run-away Isabelle process" started by Elsa Gunter
03-May-2015 there should be more hints what can be done to improve the
situation -- the hardware side-conditions seem to be rather similar.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC