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.



Proofpower mailing list

Reply via email to