Re: [isabelle] Isabelle2013-2-RC1 available for testing



On Mon, 25 Nov 2013, René Thiemann wrote:

- changing the method of (intro TrueE) does not stop the system from evaluation (comsuming 100% of CPF and eating > 4 GB of RAM)

2 x 2.8 Ghz Quad-Core Intel Xeon
6 GB RAM

ML_PLATFORM="x86_64-darwin"
ML_HOME="/Applications/Isabelle2013-2-RC1.app/Isabelle/contrib/polyml-5.5.1-1/x86_64-darwin"
ML_SYSTEM="polyml-5.5.1-1"
ML_OPTIONS="-H 500"

Just another side remark, before I look more closely how Isabelle/Scala can terminate Isabelle/ML processes more reliably.


Above you are using x86_64-darwin with its unbounded address space, because polyml-5.5.1 on x86-darwin sometimes cannot allocate heap space for IsaFoR, as we know already.

The good news is that David Matthews has improved this after the Poly/ML 5.5.1 release, and he will make another release soon.

Then you can also use x86-darwin for your application, which limits the poly process to comfortable 2-3 GB. This is sufficient in practice, due to the online sharing of immutable values on the ML heap that David Matthews is doing for us.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.