Email Gateway (Aug 07 2023 at 11:19): Email Gateway (Aug 07 2023 at 11:19):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!
I have a machine with 8 GB RAM, and running Isabelle/VSCode alongside
such software as Firefox apparently gets me into issues like too much
swapping. I have the impression that Poly/ML is adapting its maximum
heap size to the total amount of RAM rather than some notion of
available RAM, and therefore I want to manually limit its heap size.
To this end, I have tried to set the --max-heap option, but it seems
that this option is ignored. Concretely, I have the following in
~/.isabelle/Isabelle2022/etc/settings:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms64m -Xmx512m -Xss2m"
ML_OPTIONS="--max-heap 768M"
While the Java-related options seem to be taken into account when
Isabelle/VSCode is run, the heap size limitation for ML doesn’t seem to
have any effect. Right now, ps -eO rss | grep polyml gives the
following output:
203686 1497964 S ? 00:20:29 /home/wolfgang/Software/isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux/poly -q --max-heap 768M --gcthreads 0 --exportstats --eval (PolyML.SaveState.loadHierarchy ["/home/wolfgang/Software/isabelle/heaps/polyml-5.9_x86_64_32-linux/Pure", "/home/wolfgang/Software/isabelle/heaps/polyml-5.9_x86_64_32-linux/HOL"]; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ ": HOL\n"); OS.Process.exit OS.Process.failure) --eval Options.load_default () --eval Isabelle_Process.init ()
203724 6512 S ? 00:00:36 /home/wolfgang/Software/isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux/poly -q --use src/Pure/ML/ml_statistics.ML --eval ML_Statistics.monitor 203686 0.5
As can be seen, there is a Poly/ML process that did receive the option
--max-heap 768M but nevertheless takes about 1.5 GB of RAM.
How can I effectively limit the amount of RAM that Poly/ML will use?
All the best,
Wolfgang
Email Gateway (Aug 07 2023 at 18:40):From: Thomas Sewell <tals4@cam.ac.uk>
You might be able to use the shell builtin "ulimit -v" to set the maximum virtual memory available to children.
I have used that to prevent various things, including SMT solvers, from choking my system. I don't quite recall whether PolyML handles it gracefully or not, but I'd recommend giving it a try.
Good luck,
Thomas.
Email Gateway (Aug 07 2023 at 19:28):From: Makarius <makarius@sketis.net>
On 07/08/2023 13:13, Wolfgang Jeltsch wrote:
I have a machine with 8 GB RAM, and running Isabelle/VSCode alongside
such software as Firefox apparently gets me into issues like too much
swapping.
If it is just one machine, and not a larger installation of many machines,
then the easiest way is to upgrade RAM to 16GB or 32GB.
Seriously. I have recently refurbished several really old machines (concerning
SSD and RAM), and the materials are ridiculously cheap.
So just look up your hardware model on the Net and order to correct RAM
modules: maximum possible size.
I have the impression that Poly/ML is adapting its maximum
heap size to the total amount of RAM rather than some notion of
available RAM, and therefore I want to manually limit its heap size.
ML_OPTIONS="--max-heap 768M"
Isn't the option called --maxheap?
If you pass unknown options to the poly process, they end up as command-line
arguments to the ML program, i.e. are effectively ignored.
Makarius
Email Gateway (Aug 08 2023 at 12:06):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Yes, you’re absolutely right: it’s --maxheap, not --max-heap. Thanks
for pointing this out: this was really helpful.
All the best,
Wolfgang
Last updated: Apr 29 2024 at 04:18 UTC