[isabelle-dev] Isabelle_10-Sep-2013

[René Thiemann]

Dear all,

first of all, thanks Makarius for taking care of the new release.

Here are my first comments: 
After changing to Isabelle_10-Sep-2013, most of the theories could easily be adapted.
However, 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?

Here are the details of my machine:

MacOS X 10.8.4, 2 x 2.8 Ghz Quad-Core Intel Xeon, 6 GB RAM

I noticed a similar phenomenon on my laptop with the following setup:

MacOS X 10.8.4, 2.2 Ghz Intel Core i7, 8 GB RAM

Cheers,
René

IsaFoR: a2136da2b517
AFP: 5c7a1374860e