Sorry for the slow response.
I have thought quite a bit about this, but these days such
cogitations don't always go anywhere useful.
On Thursday 30 Aug 2012 21:58, Rob Arthan wrote:
> On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:
> > and a number of cases where identifiers which I had
> > been using are now used in MathsEgs theories which are
> > in my ancestry these include Tree TREE Pair
> Were you using these names for things of your own?
> If so,
> then perhaps this would be solved if the underlying
> names of constants were prefixed with the theory name.
> What I am considering in this area is an option
> controlled by a flag (say "structured_HOL_namespace"),
> which I would turn on towards the end of the HOL build,
> whereby the HOL parser would do this for you. When you
> define constant "xyz" in theory "abc", the underlying
> name would be "xyz.abc" and "abc" would be introduced as
> an alias for that. And likewise for types. This
> behaviour would be optional and language-specific (e.g.,
> you wouldn't want it for Z, and you might not want it in
> HOL). Would that have saved you any trouble?
I don't think my problems with the new version of maths_egs
are of any concern, and don't for me motivate changes.
I do think changes in this area are desirable but I would
say that my own prime motivation would be to move to a
situation in which proof tools can make use of results
obtained in other proof tools, i.e. the motivations for
OpenTheory and my "X-Logic".
I think being able to eliminate junk from theories is
something which would help in that enterprise, and as it
happens it would probably would also help to mange the above
kind of problem.
I think that probably would involve using compound constant
names, at least behind the scenes, not necessarily in front
of the children.
But I'm not keen on the use of the ProofPower aliasing
mechanism to manage the use of simple names.
A key feature I think is simply to be able to hide names, or
project a theory according to a signature, but also it would
be nice to be able to rename on import.
I am inclined now to think that it might have been a mistake
to automatically inherit all the ancestry when adding a
This connects with the discussion about conservative
extension, since it represents an alternative way of
obtaining the kind of abstraction which "new_specification"
provides, and possibly somewhat superior in that the details
are all there, but not actually "exported".
Putting it in that context, the idea that the structured
namespace is something you opt into at some point seems to
me doubtfull, though you might want it to default to
behaviour which is backward compatible, i.e. if the local
names are all globally unique then they will all get
correctly resolved as at present.
However, once you put it in this context, then you are
really looking at a bigger problem in which concensus across
theorem provers is essential.
Personally, I think that shouldn't just be HOL provers, and
as you know I advocate importing results even if proofs
cannot be imported.
As an example of what ideally might be possible, classical
arithmetic is standard, no two provers should disagree about
what is true (though they will differ about what they can
prove), so exchange across any tool which is sound for first
order arithmetic should be possible in that domain.
All that of course is much more than you wanted to get into,
and for my money you can safely do nothing here if your
concern is just the occasional rework that people might have
to do when you change maths_egs.
> > (probably the most
> > disruptive) and some identifiers consisting of or
> > starting with subscripted "D".
> Really - I can't find any identifiers that start with a
> subscripted character in the MathsEgs theories.
The theory is topology which now contains some names which
are the same as names you put into a bit of differential
geometry you did for me way back.
> > I have not yet considered a new way of building
> > contribs. I feel that making MathsEgs build OK on the
> > development system would not be productive in the
> > absence of a little more clarity about how a contrib
> > system would be expected to work.
> I had a discussion with Anthony Fox about how they do
> things in HOL4 and that has given me some more ideas on
> this. I think it is actually completely orthogonal to
> how the ProofPower code is organised.
I got confused when you issues the trial reorganisation and
tried to build maths_egs out of the RCS, which didn't work,
but it did build in the normal way of course.
> In HOL4, the contents of a theory are exported to and
> imported from text files. So if you have code associated
> with a theory that you want to export to users of the
> theory, you put that in a separate file and let users
> load that file. As ML doesn't have separate compilation,
> such code has to be provided as source. To make things
> easier for the user, HOL4 has its own make function,
> HOLmake, that automatically figures out dependencies
> between a set of things you want to bring together and
> loads them in the right order. Given that we don't have
> HOLmake and we don't allow export and import from files,
> this suggests to me that a contrib offering should
> comprise ML source to build the theory and provide any
> supporting ML functions etc.
Which is of course what maths_egs does, and my own stuff
based on that makefile.
> Here is one possible set of conventions. The source of a
> contrib offering, XYZ, comprises a directory containing
> doc files together with a (UN*X) make file. The make
> file has a target that build a database called XYZ, that
> contains the contrib theories and associated ML and a
> minimal set of dependencies. Users who want to start
> from the contrib offering can just create children of
> the database. The make file also has a target that
> creates the ML source from the doc files and
> concatenates them into an appropriate order to give a
> single source file XYZ.ML (not XYZ.sml, since this will
> typically not be directly derived from a single .doc
> file). A built contrib offering would comprise the .doc
> files plus PDF of those (and/or DVI?) plus the database
> XYZ and the source file XYZ.ML.
I don't understand why you are proposing this departure from
the pattern set by maths_egs.
> It would also be useful to maintain a ref to a list of
> strings identifying the loaded contrib offerings. This
> would be managed at the head and tail of XYZ.ML via
> access functions that allow it to be interrogated and
> extended. At the head we would have code to check that
> all the dependencies are satisfied and to report on
> anything that is missing (or you could be cleverer and
> attempt to load the missing dependencies - so this would
> be a bit like a mini-HOLmake, in which the contrib
> provider has to declare the dependencies). At the tail
> would be code to add the new contrib name to the list.
> The contrib directories could be organised as a tree
> with an initial contrib at the top that defines the list
> of loaded offerings and includes tools for working with
> As regards ML conventions, I would suggest that we don't
> mandate the rigid packaging of things into structures
> with signature constraints that ProofPower itself
> follows, but do encourage people at least to collect all
> the external interfaces into structures so that they can
> be accessed if the plain name is accidentally recycled.
> How does that sound? Is it definite enough for you to
> consider making a start?
It seems to me more of a departure from present practise
than I would have thought necessary.
A question to answer is, what's wrong with just recommending
that contribs follow the pattern set by maths_egs.
I think there is only one problem, so long as there are not
many contribs around and that is that to build more than one
independent contrib into the same database you would have to
hack one of the makefiles.
This would be fixed if the makefiles consulted an environment
variable to see whether they should build into an existing
If there were more contribs around then the next step would
be to manage the dependencies between them in some way,
I'm a little surprised to see you hoping for me to
contribute any signficant amount of scripting, since my
scripting skills are very basic and my standards are very
poor. If I did do anything non-trivial you would probably
feel compelled to completely rewrite it!
One the reorganisation of the ProofPower build system I
don't have a clear view of your objectives.
Are you aiming to make it more like the usual opensource
arrangement whereby others can contribute by accessing the
repository directly, and in much the same manner as you do
(except that you control what changes actually go into the
I would have thought that this could be done without any
radical changes to the organisation, its more a question of
making the repository available and devising a protocol
between you and other contributors for coming to agreements
about what changes from them you are iikely to accept.
Not that I have any experience of working in such a way.
I no only the kind of arrangement under which ProofPower was
But I don't really see why that old fashioned method could
not work in a distributed context, especially with the new
Proofpower mailing list