Email Gateway (Aug 08 2022 at 16:22): Email Gateway (Aug 08 2022 at 16:22):From: "M. Baksys" <mb2412@cam.ac.uk>
Dear all,
While working on a decently long proof (currently ~400 lines), I have started
to experience some performance issues on my machine. These issues manifest
themselves by jEdit becoming unresponsive after a few minutes of use and the
message "ML Cleanup" popping up on the bottom right. After this, the said "ML
Cleanup" rarely goes away allowing only for small intervals when the editor is
responsive (and behaving at its usual speed). I have noticed this slowdown
only while working on comparatively longer proofs and my machine is currently
running Windows. Note that during development, I keep the file error-free by
sorry-ing lemmas and statements to be proved, so this should not be an issue.
I would appreciate it a lot if anyone suggested any tips on how to tackle the
issues I've described above. Thanks in advance!
Mantas Baksys
Email Gateway (Aug 09 2022 at 10:20):From: Makarius <makarius@sketis.net>
"ML Cleanup" means that the Poly/ML runtime system is trying to reclaim ML
heap space by garbage collection or aggressive sharing of immutable values.
This indicates a general shortage of memory. The "Monitor" dockable can show
you further details.
How much RAM do you have on this Windows machine? From the description of the
problem, I would guess 4-8 GB, but you need 8-16 GB as a start for reasonable
Isabelle applications. Experts usually have 32-64 GB.
Makarius
Email Gateway (Aug 09 2022 at 10:41):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Mantas,
400 lines is not at all long and I suspect something else is going on. For example, does your development depend on HOL-Analysis? Then it makes a huge difference whether you start it by
isabelle jedit ...
or
isabelle jedit HOL-Analysis ...
In the former case, something like 100 large theories making up HOL-Analysis will be loaded into your session, taking many minutes, and because they are all "live", they'll be using up a lot of memory. In the latter case, a precompiled image will be used; the first time round, it will need to be built but then it will be kept for next time.
Or perhaps your development is loading a bunch of AFP entries. Then what you need is to create an appropriate ROOT file so that you can launch your session with
isabelle jedit -R <session_name>
A precompiled image will be built incorporating all the ancestors of your development, so that nothing needs to be held in memory beyond your 400 lines.
The use of a ROOT file is a technique that everybody will need to learn once they start making extensive use of libraries.
Larry
Last updated: Apr 18 2024 at 08:19 UTC