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