On Mon, 26 Jul 2010, Gerwin Klein wrote:
On 26/07/2010, at 1:35 PM, David Matthews wrote:
Did you rebuild the compiler before you ran with that version (i.e.
make compiler) or use the original compiler?
Maybe you should also try to rebuild the official 5.3.0 version from
source. Theoretically there could be a problem with the compilation from
the Isabelle download site -- it also has some add-on library for SHA1
that is loaded into the RTS at some point.
In the 64bit 5.3 version I noticed normal (< 2G) memory usage while it
was processing everything and then a huge spike at the very end going up
to > 7G (presumably at the commit call at the very end of the session,
but can't really tell).
BTW, the commit is no longer a primitive of Poly/ML 5.x but defined in
Isabelle/lib/scripts/run-polyml like this:
fun commit () = (PolyML.shareCommonData PolyML.rootFunction;
TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\");
PolyML.SaveState.saveState \"$OUTFILE\"; true);
You can also experiment doing only part of the above.
Makarius
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
