Re: [isabelle] Insufficient memory when building heap image
On Fri, 28 Sep 2012, Manuel Eberl wrote:
Also, if I load all these theories by hand by importing them in a theory
and loading that theory in Proof General, everything seems to work, but
when I do "isabelle usedir" with an appropriate ROOT.ML file, I get this
insufficient memory exception.
Traditionally, Proof General runs things with slightly different options,
such as quick_and_dirty and reduced parallel proof checking, so there can
be easily a difference to batch mode.
I am trying hard not to repeat these mistakes and consequent confusion in
the current interactive document model, the one that is used for
Isabelle/jEdit. So after a few more rounds of refinements, and when Proof
General is forgotten, such issues should no longer occur.
The reason for that is that, apparently, "Isabelle usedir" uses up to
6.5 GiB of memory (tested on a 64 bit system), but the computer with
which I normally work runs a 32 bit system, so I only have 4 GiB per
You need to find out where the resources are going, i.e. which part of
your application burns them. You may try this in plain "isabelle tty"
which is a bit closer to batch mode than the Proof General interaction
Alternatively, you can ignore the problem and use current polyml-5.5.0
from here: http://isabelle.in.tum.de/components/polyml-5.5.0.tar.gz
This is the brand-new Poly/ML release, with greatly improved heap
management (parallel garbage collection and online sharing of values).
It is able to run much larger Isabelle applications even in 32bit mode.
To use the above polyml-5.5.0 component in Isabelle2012, add something
like this to your $ISABELLE_HOME_USER/etc/settings:
Then rebuild the required images as usual via Isabelle2012/build.
This archive was generated by a fusion of
Pipermail (Mailman edition) and