[isabelle-dev] Isabelle_10-Sep-2013

[René Thiemann]

Dear David,

>>> I would guess that this is when running the X86/32 version rather than X86/64.
>> 
>> Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode.
>> 
>> Here is my current setup:
>> 
>> ISABELLE_BUILD_OPTIONS=""
>> 
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
>> ML_SYSTEM="polyml-5.5.0"
>> ML_OPTIONS="--minheap 1000 --stackspace 5000"
>> 
> 
> You definitely don't want a value as large as 5000.
> 
> I think the exception may be occurring with PolyML.shareCommonData. This needs memory outside the heap to hold some tables.  If there is a lot of live data in the heap these tables can be large and if the heap is taking up most or all of the available virtual memory, a particular problem in 32-bit mode, you may get the above message and exception.  Is that possible in this case?  

Most of the time, it indeed appears after the theories have been processed, and the heap-file is being generated.
(e.g., I never get the error with "isabelle build Check-DPP", only if I build the heapfile with "isabelle build -b Check-DPP")

Moreover, I now tested a bit the 64-bit version of poly, and there the error does not occur, even without specifying ML_OPTIONS.
For me, this looks like the most sensible solution.

> It is safe to handle the exception and continue; it's just that the sharing process will not be complete so that the heap will be bigger than it might otherwise be.
I see.

Thanks for your helpful comments,
René