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