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