Email Gateway (Oct 10 2020 at 01:12): Email Gateway (Oct 10 2020 at 01:12):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am using Ubuntu 18.04. I am finding that the ML heap seems to be limited to 16G and I need to use
a bit more. I haven't really been able to find a comprehensible description of how to do this in
the documentation I have looked at, so I attempted to follow the settings reported in the Jenkins
nightly build logs, which seem to use --maxheap 20G. I put the following in ~/.isabelle/etc/settings:
ML_PLATFORM="x86_64-linux"
ML_SYSTEM="polyml-5.8.2"
ML_OPTIONS="-H 4000 --maxheap 20G"
However, when I start Isabelle/JEdit I get the message shown below. How can I get around this?
Thanks for any help.
-- Gene Stark
Value of --maxheap option must not exceeed 16Gbytes
-H <Initial heap size (MB)>
--minheap <Minimum heap size (MB)>
--maxheap <Maximum heap size (MB)>
--gcpercent <Target percentage time in GC (1-99)>
--stackspace <Space to reserve for thread stacks and C++ heap(MB)>
--gcthreads <Number of threads to use for garbage collection>
--debug <Debug options: checkmem, gc, x>
--logfile <Logging file (default is to log to stdout)>
--exportstats <Enable another process to read the statistics>
Debug options:
checkmem <Perform additional debugging checks on memory>
gc <Log summary garbage-collector information>
gcenhanced <Log enhanced garbage-collector information>
gcdetail <Log detailed garbage-collector information>
memmgr <Memory manager information>
threads <Thread related information>
gctasks <Log multi-thread GC information>
heapsize <Log heap resizing data>
x <Log X-windows information>
sharing <Information from PolyML.shareCommonData>
locks <Information about contended locks>
rts <General run-time system calls>
saving <Saving and loading state; exporting>
HOL CANCELLED
Unfinished session(s): HOL, Pure
Return code: 1
Session build failed -- prover process remains inactive!
Email Gateway (Oct 10 2020 at 16:57):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
After reading various of the Isabelle settings and start-up scripts, and also some trial and error,
I found that the following in my settings file produced the behavior I wanted:
ML_SYSTEM="polyml-5.8.1-20200228"
ML_HOME=$ISABELLE_HOME/contrib/$ML_SYSTEM/x86_64-linux
ML_OPTIONS="--maxheap 20G"
ML_PLATFORM="x86_64-linux"
I don't have any idea whether this is the "right" way of doing it, though.
Email Gateway (Nov 07 2020 at 21:14):From: Makarius <makarius@sketis.net>
Did it work out for you? 20G for x86_64 is not so much, compared to 16G for
x86_64_32 (where everything is more compact).
Note that the minimum setup works like this:
* $ISABELLE_HOME_USER/etc/settings:
ML_OPTIONS="--maxheap 20G"
* $ISABELLE_HOME_USER/etc/preferences:
ML_system_64 = true
If you have Isabelle/jEdit running, you can edit ML_system_64 in the Plugin
Options dialog; on shutdown the preferences will be saved/overwritten.
Makarius
Email Gateway (Nov 07 2020 at 22:14):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Thanks for the reply.
Yes, it did work out. I was able to process the session in a reasonable amount of time
with a heap limit of 20-22G. The 16GB heap under x86_64_32 was no longer cutting the mustard.
I replaced my existing 2x4GB DRAM with 2x8GB, to get a total of 32GB, which maxes out this
motherboard. It is a stretch to run Isabelle/JEdit on this system with a heap limit of more
than about 22GB, because Java takes a few GB itself and thrashing starts to set in when the
heap reaches the maximum.
I did notice that the "cold start" time on x86_64 was slower than on x86_64_32. Perhaps this
is because I didn't bother to set the minimum heap size.
If I start feeling rich due to all the money I am saving by not going anywhere or doing anything
during the pandemic, I will build an i9 system to replace this 6-year-old i5 and put more memory
on it. But I am not there yet.
Last updated: Apr 20 2024 at 08:16 UTC