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