[isabelle-dev] Isabelle_10-Sep-2013

[Makarius]

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