On 24/02/17 13:26, Makarius wrote: > We have strange memory management problems with Isabelle. > > I've been using repository versions of Poly/ML privately during the past > few months, without seeing such problems. Only the official switch in > http://isabelle.in.tum.de/repos/isabelle/rev/42b92fa72a51 exposed that, > ranging from main HOL not building on an underpowered macOS machine to > some big AFP entry not building on an overpowered Linux box. > > For the moment, I have switched the Isabelle setup back to stable > Poly/ML 5.6 (see http://isabelle.in.tum.de/repos/isabelle/rev/18f3d341f8c0). > > I will come back on that when I've investigated the situation further.
I've now spent some time with it. Here are some preliminary observations for Isabelle/002b4c8c366e and AFP/d0bd0f0fe3b2 and Poly/ML 5.6 vs. Poly/ML pre-5.7 (6307085deb18): (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. To address that, I have fine-tuned the defaults for parallel proofs, leading up to Isabelle/05f1b5342298, with some hope that it might improve the situation in general: less waste of CPU and memory on small machines. (2) The big problem is AFP/Iptables_Semantics_Examples. Here is the timing with Poly/ML 5.6 on lxbroy10, an old AMD machine that is relatively slow: Finished Iptables_Semantics_Examples (4:35:13 elapsed time, 23:35:08 cpu time, factor 5.14) With Poly/ML 5.7 it quickly runs into memory problems. See the included PNG images for comparison. That session is definitely quite ambitious, not to say insane. It contains lots of invocations of the "eval" proof method, which means dynamic compilation of ML from HOL specifications, and throwing away the result. My current guess is that it is a problem of compiled ML code that is no longer garbage-collected. Is there a way to measure the size of this persistent ML code? Is there a way to invoke the Poly/ML compiler in interpreted mode via some flag? See also http://isabelle.in.tum.de/repos/isabelle/file/1803a9787eca/src/Pure/ML/ml_compiler.ML#l270 where Poly/ML is invoked in Isabelle/ML. Makarius
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
