Re: [isabelle] error: Unable to load header



On Thu, 19 Jan 2012, Christian Sternagel wrote:

Unable to load header:
$HOME/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux/Name

This is the Poly/ML runtime system complaining about the heap image. I've seen this occasionally -- it means that the writing of the heap image left it somehow in a bad state. It is particulary frequent on x86-cygwin with big heaps and little memory.


$ isabelle version
Isabelle2011-1: October 2011

$ isabelle tty
val it = (): unit
val commit = fn: unit -> bool
Welcome to Isabelle/HOL (Isabelle2011-1: October 2011)

x86_64-linux (Fedora 16)

ISABELLE_USEDIR_OPTIONS=-M 2 -q 2

ML_PLATFORM=x86_64-linux
ML_HOME=/usr/local/Isabelle2011-1/contrib/polyml/x86_64-linux
ML_SYSTEM=polyml-5.4.0
ML_OPTIONS=-H 400

It sometimes helps to tweak the initial heap size, say -H 800 or -H 2000.

You can also try the current polyml-5.4.1, which is packaged in the Isabelle way in http://www4.in.tum.de/~wenzelm/test/polyml-5.4.1.tar.gz -- David Matthews made many improvements in the heap management between 5.4.0 and 5.4.1.

If the problem persists and is clearly reproducible we should tell David Matthews about it.


	Makarius





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