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" 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 (probably the most disruptive) and some identifiers consisting of or starting with subscripted "D". 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. 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. 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). So the situation at the moment is that I don't feel there is enough clarity about where we are going to actually do anything at present, though I am more keen than I was last time we talked about this to make a fresh start on my own material, so I would like to move this forward so that I don't have to change twice to fit in. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
