Re: [isabelle] error: Unable to load header



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.





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