Rob,

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?

Yes.

> 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 
parent.

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.

Yes.
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
> it.
> 
> 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 
database.

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 
issued ProofPower)?
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 
originally developed.
But I don't really see why that old fashioned method could 
not work in a distributed context, especially with the new 
respositories available.

Roger





_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to