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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and