On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: > I have now managed to build my theories on the new > ProofPower and MathsEgs. > > I had to modify 13 source files to get them through. > > It seems probable that the changes all resulted from the new > MathsEgs, and primarily were changes to names. > These include the changes to theorems "plus" => "additive"
Those name changes seemed like a necessary rationalisation when I was prettying up this stuff in preparation for my talk at the AIPA workshop at ETAPS. > 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? > (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. > There was only one broken proof (for reasons other than > naming), and I am guessing that the reason was a change in > the behaviour of R_top_anf_tac which now introduces powers > in place of products where possible (it doesn't look like > that was happening before) but I just repaired the proof and > didn't go into detail on what had broken it. Sorry, I forgot to announce the change to real ANF. > > 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. 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. 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. 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? > The first issue in relation to this seems to me to be the > localisation of namespaces. > A contrib system presumably would not work with a single RCS > directory. > I don't actually understand why you could not have separate > RCS directories for each product, together with one for files > common to more than one product. > I suppose the problem is that make would not know where to > go to for the files (and I suppose expects the RCS directory > to be called RCS). I think I will just be forced to do it that way. It would be nice to overhaul the make files in any case. What would probably be best would to invent meaningful names for all the modules, so that the resulting directory structure would look something like what most programmers expect these days. Most modules define exactly one structure and could be named after that structure (after converting extended characters into something more file-system friendly). So dtd/imp/mdt093.doc would become something like dtd-IntegerTheory.doc imp-IntegerTheory.doc and mdt-IntegerTheory.doc. I would retain the dtd/imp/mdt numbering systems for use in the bibliography files so this change would have minimal affect on the internals of any existing .doc files. Regards, Rob. _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
