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