Wolfgang Jeltsch (Feb 23 2023 at 00:14): Wolfgang Jeltsch (Feb 23 2023 at 00:14):Limiting memory usage of Isabelle in order to not have it hang my computer has already been discussed in another topic (which, annoyingly enough, can’t be be marked as unresolved anymore). However, I had to find out that the solution proposed there by @Jan van Brügge doesn’t work for me, as it relies on a newer version of cgroup (older versions apply limits only to the process directly started, not the processes started by that process). That said, isn’t it possible to pass some option to Poly/ML to have it using a smaller heap or whatever? Not sure whether Poly/ML is the offender, but I would think so.
Mathias Fleury (Feb 23 2023 at 06:08):you can tell poly/ml what maximal heap size you want. In your settings file ($ISABELLE_HOME/etc/settings):
ML_OPTIONS="--max-heap 10G"
I mostly used that to set the minimum size to a larger value, but I stopped doing that at some point…
Mathias Fleury (Feb 23 2023 at 06:11):At that point you might also want to tune the java options:
ISABELLE_TOOL_JAVA_OPTIONS="-Xms4g -Xmx32g -Xss16m"
ML_OPTIONS="--minheap 4G --maxheap 32G"
(taken from https://isabelle.in.tum.de/website-Isabelle2022/dist/doc/system.pdf, just above 2.7)
Last updated: Apr 30 2024 at 04:19 UTC