Re: [isabelle] build process


the "build" script, as far as I can tell, puts the heaps into the "$ISABELLE_HOME/heaps/" directory. isatool on the other hand puts them into "~/isabelle/heaps". I also run several versions of Isabelle which leads to confusion about which heaps go with which version. The solution I use is to make a directory "~/isabelle/etc" and in there make a file called "settings", which contains the following:


Isabelle automatically looks in this directory for this file when it starts up and makes Isabelle use the heaps into the "$ISABELLE_HOME/heaps" directory. This should allow you to remove "~/isabelle/heaps" directory and either rerun the build script, or use isatool to remake your heap files; from now on the heap files used will correspond to the version of isabelle you run. The heaps will be inside "$ISABELLE_HOME/heaps".

hope this helps,

Jeremy Dawson wrote:
Martin Ellis wrote:
On Wednesday 07 March 2007 06:25, Jeremy Dawson wrote:

I've made some (rather trivial) changes to a Pure source file,
and rebuilt HOL (which includes rebuilding Pure, and I had thought that
HOL is built on top of Pure).
But when I run Pure, I see the effects of the changes,
when I run HOL I don't.

Perhaps when you rebuilt HOL, it did not build 'on top of' the right Pure image? You could try checking there's not more than one copy of Pure
or HOL lying around, and then rebuilding HOL - and see if that has any

There might be a copy in your home directory, and a copy in the actual Isabelle install directory. The one in your home directory is supposed to
take precedence, if I recall correctly.

At least, I've had similar confusion caused by having more than one copy of
an image before.


Thanks Martin, for your help on this.  This is almost what the problem was.

I seem to have a rather weird collection of directories and heap locations:

jeremy at scooter:~/isabelle/heaps$ du
132     ./Isabelle_30-Nov-2006/polyml-4.1.4_x86-linux/log
77364   ./Isabelle_30-Nov-2006/polyml-4.1.4_x86-linux
77368   ./Isabelle_30-Nov-2006
4       ./polyml-4.1.4_x86-linux
364     ./Isabelle_11-Feb-2007/polyml-4.1.4_x86-linux/log
76308   ./Isabelle_11-Feb-2007/polyml-4.1.4_x86-linux
76312   ./Isabelle_11-Feb-2007
153688  .
jeremy at scooter:~/isabelle/heaps$

Is this the way it's meant to be?

I've also found that the build command places the HOL and Pure files in ~/Isabelle_11-Feb-2007/heaps/polyml-4.1.4_x86-linux

whereas getting into the source directories for Pure and HOL, and running isatool make (which someone else suggested I try), puts HOL and Pure files in ~/isabelle/heaps/Isabelle_11-Feb-2007/polyml-4.1.4_x86-linux

And the one that gets built by ./build isn't the one that gets used.

Thanks again for your help


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