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
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
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
take precedence, if I recall correctly.
At least, I've had similar confusion caused by having more than one
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
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
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
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