dm at prolingua.co.uk
Fri Sep 13 11:22:42 CEST 2013
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
>> *** error: can't allocate region
>> *** set a breakpoint in malloc_error_break to debug
>> Fail "Insufficient memory":
>> 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.
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?
More information about the isabelle-dev