On 27/02/17 23:55, Makarius wrote:
On 24/02/17 13:26, Makarius wrote:
We have strange memory management problems with Isabelle.
(1) Poly/ML pre-5.7 requires a bit more heap space (tested for HOL, HOL-Library, HOL-Analysis), especially when running in parallel. This might explain the failure building main HOL on the small macOS machine: it probably runs into a situation where heap compaction no longer works and the ML process interrupts all threads.
Here are some more measurements for the plain HOL build problem on my new MacMini. Current Isabelle/36c650d1a90d it usually works, even on that small macOS 10.12 Sierra machine, but it requires much more memory than usual.
The included a.png vs. b.png illustrate that, but they have been produced on a different machine (macbroy2), which runs Mac OS X 10.9 Mavericks.
Here are the Isabelle settings to reproduce that:
##enable this for "b.png" #init_component "$HOME/.isabelle/contrib/polyml-5.7-20170217"
ML_OPTIONS="-H 500 --gcthreads=2" ISABELLE_BUILD_OPTIONS="threads=2"
The session is then built as follows:
$ isabelle build HOL
The low number of threads is important. With 4 it generally works better.
I've done the same test on a virtual Ubuntu 16.04 with 2 cores + 8 GB, and there is no big difference in heap usage.
I am unsure if this is really a matter of Poly/ML 5.6 vs. 5.7: on Mac OS X, we have seen many heap irregularities in the past few years, i.e. situations where heap compaction does not work anymore and the process is interrupted.
Makarius