Email Gateway (Aug 18 2022 at 18:57): Email Gateway (Aug 18 2022 at 18:57):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear All,
recently (after setting up a new machine) I get the error message
"Unable to load header" when trying to use the code generator on a
previously built heap image.
In the archives of the mailing list I found out that this problem
already occurred earlier... but I did not find an answer.
I create the heap image by:
$ /usr/local/Isabelle2011-1/bin/isabelle usedir -C false -D generated
-s Name Underlying-Heap-Image .
and then try to generate code via:
/usr/local/Isabelle2011-1/bin/isabelle codegen Name Theory \
'some-function in Haskell module_name Some-Module file
"generated/Haskell/"'
But this command results in
Unable to load header:
$HOME/.isabelle/Isabelle2011-1/heaps/polyml-5.4.0_x86_64-linux/Name
Any help is welcome ;)
Details:
$ 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
thanks in advance
chris
Email Gateway (Aug 18 2022 at 18:57):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 18:57):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Hi all,
Just for the protocol: it turned out that I walked right into my own
trap. The error was just due to my own stupidity, but is funny enough to
share ...
The trouble started by reusing a very old IsaMakefile without really
reconsidering what it was meant for. Furthermore, the line below was not
the whole "truth".
/usr/local/Isabelle2011-1/bin/isabelle usedir -C false -D generated -s
Name Underlying-Heap-Image .
The next line of my IsaMakefile was
touch $(ISABELLE_OUTPUT)/Name
So the first line (just meant for document generation) does not build a
heap file at all. And the second line creates an empty "heap image"
(please don't ask me, why on earth this line was contained in my old
IsaMakefile!). No wonder that the header could not be read :D.
Somehow I'm often blind to my own errors... those made by others are
much easier to detect ;)
Sorry for wasting your time.
christian
PS: This is an example how trying to present a problem "nicely" can
completely obfuscate the real cause.
Last updated: Apr 23 2024 at 12:29 UTC