Re: [isabelle] How do I set --maxheap greater than 16G on Linux?



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.



On 10/9/20 9:12 PM, Eugene W. Stark wrote:
> 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!
> 
> 
> 





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