rene.thiemann at uibk.ac.at
Thu Sep 12 17:14:37 CEST 2013
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
To be more precise, when using
I did not get the error under Isabelle2013, but under Isabelle_10-Sep-2013, it often fails with setting.
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
More information about the isabelle-dev