[isabelle] Isabelle2019-RC2 Does poly really honor --maxheap?



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?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.