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.
you can tell poly/ml what maximal heap size you want. In your settings file ($ISABELLE_HOME/etc/settings):
I mostly used that to set the minimum size to a larger value, but I stopped doing that at some point…
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: Dec 07 2023 at 08:19 UTC