[isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

On 12/09/2013 19:25, Makarius wrote:
> On Thu, 12 Sep 2013, René Thiemann wrote:
>
>> I noticed that on my machines I often get an "Insufficient memory" error.
>>
>> Building Check-DPP ...
>> poly(59646,0xacc9fa28) malloc: *** mmap(size=134217728) failed (error
>> code=12)
>> *** error: can't allocate region
>> *** set a breakpoint in malloc_error_break to debug
>> Fail "Insufficient memory":
>> /Users/rene/.isabelle/Isabelle_10-Sep-2013/heaps/polyml-5.5.0_x86-darwin/Check-DPP
>>
>> Check-DPP FAILED
>>
>> To be more precise, when using
>>
>> ML_OPTIONS="--minheap 1000"
>>
>> I did not get the error under Isabelle2013, but under
>> Isabelle_10-Sep-2013, it often fails with setting. Fortunately, using
>>
>> ML_OPTIONS="--minheap 3000"
>>
>> mostly works, but it is still annoying, since with this setting, I
>> cannot start two Isabelle sessions in parallel. Does someone else
>> notice increased memory consumption / crashes?
>
> There is definitely some continous bloat factor with every new release,
> although David Matthews was usually ahead of most big applications in
> recent years.  In fact he is about to release Poly/ML 5.5.1 pretty soon,
> so a quick test with some repository version of Poly/ML might help (e.g.
> SVN 1843).

I would suggest trying with the --stackspace option e.g.
ML_OPTIONS='--stackspace 500'
The Fail exception with "Insufficient space" arises in a number of 
places such as when trying to fork a thread.  This requires memory 
outside the ML heap.  The stackspace option keeps some space free from 
the ML heap for these purposes.

I would guess that this is when running the X86/32 version rather than 
X86/64.  Is that correct?

David