Email Gateway (Aug 22 2022 at 19:42): Email Gateway (Aug 22 2022 at 19:42):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
This might not be new to Isabelle2019-RC2, but I thought that I had set a limit
on the size of the ML heap, but it is still exceeding that and sending my system
into thrashing mode.
Contents of my ~/.isabelle/Isabelle2019-RC2/etc/settings
ISABELLE_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
ML_PLATFORM="${ISABELLE_PLATFORM}"
ML_HOME="${POLYML_HOME}/x86_64-linux"
ML_OPTIONS="--maxheap 12000"
ps output showing poly with --maxheap option applied:
gene 18897 75.2 71.7 23475004 17680688 ? Ssl May21 2365:39
/opt/Isabelle2019-RC2/contrib/polyml-5.8/x86_64-linux/poly -q --maxheap 12000 --gcthreads 0 --eval
(PolyML.SaveState.loadHierarchy ["/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/Pure",
"/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/HOL",
"/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/HOL-Library",
"/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/Category3",
"/home/gene/.isabelle/Isabelle2019-RC2/heaps/polyml-5.8_x86_64-linux/MonoidalCategory"]; PolyML.print_depth 0) handle
exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ ": MonoidalCategory\n"); OS.Process.exit
OS.Process.failure) --eval Options.load_default () --eval Isabelle_Process.init ()
Output from "top":
PID USER PR NI VIRT RES SHR S %CPU %MEM TIME+ COMMAND
18897 gene 20 0 22.372g 0.016t 6104 S 127.9 71.6 2367:46 poly
% uname -a
Linux home.starkeffect.com 4.4.0-142-generic #168-Ubuntu SMP Wed Jan 16 21:00:45 UTC 2019 x86_64 x86_64 x86_64 GNU/Linux
Did I not read and follow the proper documentation?
Last updated: Nov 21 2024 at 12:39 UTC