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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
