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


Proofpower mailing list

Reply via email to