Email Gateway (Aug 23 2022 at 08:16): Email Gateway (Aug 23 2022 at 08:16):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear all,
I've posted <https://stackoverflow.com/q/59931542/5135870> the following
question on Stackoverflow and there I received the suggestion of
bringing it here. Thanks in advance for any help.
I've been working on an Isabelle 2019 session which has grown a bit
large, and at some point I wasn't able to build it anymore using
isabelle build in my 8G RAM machine. Nevertheless, when I open the main
theory file using jEdit (running isabelle jedit -d .), the session is
built with no problems.
/How can I tune the building process so it works as smoothly as the
graphical interface?//
/
Next, I give some more details.
The main symptom is that the Poly/ML process stalls at some point; it
doesn't really fail but does not terminate within a reasonable amount of
time (~20min, when a successful build would take 3' in my computer).
Amidst of the development, adjusting using ML_OPTIONS to "--minheap
5500" was enough to solve this, but afterwards we decided to split the
session in two (no more code added, just a change in the ROOT file) and
after that no further adjustment solved the issue. On the other hand, a
machine with 16G RAM builds with no problem without any further setting.
Later, I checked the options used by jEdit; those relevant (I believe)
are --minheap 500 --gcthreads 0 (the last being a default). I tried
with these with no success. I also noted that the build command has a
distinct --eval Command_Line.tool0 (fn () => (Build.build
"/tmp/isabelle-pedro/buildNNNNNNNNNNNNN")) option, where NNNNNNNNNNNNN
are some numbers.
Finally, I found a post concerning some old behavior of Poly/ML that
might be related:
https://polyml.inf.ed.ac.narkive.com/wb7p8r1B/heap-does-not-grow-up-to-maxheap.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:17):From: Christian Weinz <christian.weinz@stud.uni-goettingen.de>
Dear Pedro,
I've also had and still have ongoing problems with high memory usage of
Isabelle. The data Isabelle keeps in memory apparently has exploitable
redundancy, and transparently compressing it has solved my memory
problem for now wherever I was able to do so. I accomplish that using
zram in linux.
Picking a higher level theory in the dropdown menu in the panel
"Theories" has helped me reducing the memory usage, too. Note that
changing the selection does not take effect directly. I restart
Isabelle for it to take effect.
Does anybody other ways of working with Isabelle on memory constraints
machines?
Best,
Christian
Email Gateway (Aug 23 2022 at 08:21):From: Makarius <makarius@sketis.net>
Add more memory?
Isabelle is a high-end IDE and requires resources above average. As a
rule of thumb:
(1) small examples: 2 cores, 8 GB
(2) regular applications: 4 cores, 16 GB
(3) big applications: 8 cores, 32 GB
It also helps a lot to have proper SSD storage instead of old-style HD.
All of this is mid-range hardware and available rather cheaply.
Makarius
Email Gateway (Aug 23 2022 at 08:21):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Thank you very much for your reply, Makarius.
I only want to emphasize the point that actually the IDE works fine in
my laptop, but the build process is the one that doesn't.
So, either building the session does more things than what the IDE does
while verifying its theories, or there are some parameters that are
optimized when called from the IDE. That I would like to figure out.
Best regards,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
El 4/2/20 a las 16:42, Makarius escribió:
Email Gateway (Aug 23 2022 at 08:22):From: Makarius <makarius@sketis.net>
There are many differences of PIDE processing (e.g. in Isabelle/jEdit)
vs. batch builds via "isabelle build". Notably, the latter also uses
more parallelism: you may experiment with "isabelle build -o threads=1"
to see if it becomes more stable.
Poly/ML heap management depends on many side-conditions, depending on
total memory and overall timing. You can add something like this in
$ISABELLE_HOME_USER/etc/settings to experiment with it:
ML_OPTIONS="--minheap 1000 --maxheap=4000"
Both sides might require non-obvious adjustments towards the top or the
bottom, to work in such a low-memory situation.
Makarius
Email Gateway (Aug 23 2022 at 08:22):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 5/2/20 a las 04:26, Makarius escribió:
Thank you very much. This setting (using one thread) solved the issue.
For two threads, I tried several combinations of heap limits but none of
them worked. Nevertheless, it seems that the PIDE is using two threads.
Best,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Email Gateway (Aug 23 2022 at 08:23):From: Makarius <makarius@sketis.net>
Yes, both PIDE and build are using multiple threads by default, but the
overall profile of the parallel application comes out quite differently. E.g.
in PIDE proofs are only parallel in terminal positions (e.g. 'by').
You can also try this:
isabelle build -o parallel_proofs=0
I.e. multithreading is enabled, but proofs are not forked.
What is the timing output in your application of "isabelle build" with
threads=1 vs. parallel_proofs=0?
Makarius
Email Gateway (Aug 23 2022 at 08:23):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
El 6/2/20 a las 06:52, Makarius escribió:
Yes, both PIDE and build are using multiple threads by default, but the
overall profile of the parallel application comes out quite differently. E.g.
in PIDE proofs are only parallel in terminal positions (e.g. 'by').You can also try this:
isabelle build -o parallel_proofs=0
It also worked.
I.e. multithreading is enabled, but proofs are not forked.
What is the timing output in your application of "isabelle build" with
threads=1 vs. parallel_proofs=0?threads=1:
0:03:41 elapsed time, 0:03:36 cpu time, factor 0.98
parallel_proofs=0:
0:03:02 elapsed time, 0:03:47 cpu time, factor 1.25
So, this seems to be the right setting for me.
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html>
Last updated: Apr 25 2024 at 20:15 UTC