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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
