Email Gateway (Aug 18 2022 at 10:16): Email Gateway (Aug 18 2022 at 10:16):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Can anyone explain the Isabelle build process?
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.
Why could this be?
Any suggestions appreciated.
Jeremy
Email Gateway (Aug 18 2022 at 10:16):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Martin Ellis wrote:
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@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@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
Jeremy
Email Gateway (Aug 18 2022 at 10:17):From: Martin Ellis <m.a.ellis@ncl.ac.uk>
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
effect.
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.
Martin
Email Gateway (Aug 18 2022 at 10:17):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,
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_OUTPUT="$ISABELLE_HOME/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
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,
lucas
Jeremy Dawson wrote:
Last updated: May 03 2024 at 12:27 UTC