Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <4928.9410110928@frogland.inmos.co.uk>
Subject: Re: little things that make HOL unfriendly....
To: reetz@ira.uka.de (reetz)
Date: Tue, 11 Oct 1994 10:28:13 +0100 (BST)
Cc: windley@leopard.cs.byu.edu, hol2000@leopard.cs.byu.edu
In-Reply-To: <"i80fs2.ira.245:11.10.94.08.56.43"@ira.uka.de> from "reetz" at Oct 11, 94 09:56:36 am
Content-Type: text
Content-Length: 1883

reetz has said:
> Here is another little thing:
> loading a library requires being in draftmode in case the
> library has some theories, making them being parent of
> the current theory or whatever. Here's an example which I couldn't
> solve it nicely: after starting hol, I wanted to build a
> version for our site where certain, often needed libraries are
> preloaded, i.e. load_library within the started hol and use
> save_hol ... However, one has to be in draftmode, as already said,
> so I needed to create a new theory for that version :-(
> IMHO not so important, but not so elegant.

HOL theories form a tree ... if you are loading libraries which 
contain theories themselves then you need a new root node
to the tree as subsequent theories need to know whether they
are relative to the original HOL theory base or the new one
augmented by several libraries.

> another little thing:
> I was never successfull in extending an already closed theory.
> If I wanted to add a new definition, I needed to rebuild it all,
> which more or less often meant blocking a SPARC10 for almost an hour
> :-( However, that can be my fault and somebody else was successfull
> in doing that.

I think the problem here is that HOL maintains a global name
space for constants. Adding definitions can cause problems
as consider a theory TH1 which has as parents TH2 and TH3.
If indenpendently new definitions are added to TH2 and TH3
which each define the same name then there will be a clash
in TH1. If constants were identified by a pair of defining theory
and name then this might be less of a problem.


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."