Re: [isabelle] build process

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.