Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

Sorry for the slow response.
I have thought quite a bit about this, but these days such 
cogitations don't always go anywhere useful.

On Thursday 30 Aug 2012 21:58, Rob Arthan wrote:
 On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote:

  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?

Yes.

 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?

I don't think my problems with the new version of maths_egs 
are of any concern, and don't for me motivate changes.

I do think changes in this area are desirable but I would 
say that my own prime motivation would be to move to a 
situation in which proof tools can make use of results 
obtained in other proof tools, i.e. the motivations for 
OpenTheory and my X-Logic.
I think being able to eliminate junk from theories is 
something which would help in that enterprise, and as it 
happens it would probably would also help to mange the above 
kind of problem.

I think that probably would involve using compound constant 
names, at least behind the scenes, not necessarily in front 
of the children.
But I'm not keen on the use of the ProofPower aliasing 
mechanism to manage the use of simple names.

A key feature I think is simply to be able to hide names, or 
project a theory according to a signature, but also it would 
be nice to be able to rename on import.
I am inclined now to think that it might have been a mistake 
to automatically inherit all the ancestry when adding a 
parent.

This connects with the discussion about conservative 
extension, since it represents an alternative way of 
obtaining the kind of abstraction which new_specification 
provides, and possibly somewhat superior in that the details 
are all there, but not actually exported.

Putting it in that context, the idea that the structured 
namespace is something you opt into at some point seems to 
me doubtfull, though you might want it to default to 
behaviour which is backward compatible, i.e. if the local 
names are all globally unique then they will all get 
correctly resolved as at present.
However, once you put it in this context, then you are 
really looking at a bigger problem in which concensus across 
theorem provers is essential.

Personally, I think that shouldn't just be HOL provers, and 
as you know I advocate importing results even if proofs 
cannot be imported.
As an example of what ideally might be possible, classical 
arithmetic is standard, no two provers should disagree about 
what is true (though they will differ about what they can 
prove), so exchange across any tool which is sound for first 
order arithmetic should be possible in that domain.

All that of course is much more than you wanted to get into, 
and for my money you can safely do nothing here if your 
concern is just the occasional rework that people might have 
to do when you change maths_egs.

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

The theory is topology which now contains some names which 
are the same as names you put into a bit of differential 
geometry you did for me way back.
 
  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.

Yes.
I got confused when you issues the trial reorganisation and 
tried to build maths_egs out of the RCS, which didn't work,
but it did build in the normal way of course.

 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,
 

Re: [ProofPower] ProofPower Update

[Rob Arthan]

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 

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

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

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

On Thursday 09 Aug 2012 10:26, Rob Arthan wrote:

 I plan to make a new ProofPower release shortly. In the
 meantime, if you want the state of the art, I uploaded
 an experimental version built from the latest source.
 You can find this here:
 
 http://www.lemma-one.com/ProofPower/getting/experimental/

It that any different from what you get building from the RCS 
archive in your dropbox?

Can I build MathsEgs from that RCS?

[actually, I just tried but I see that the makefile for 
maths_egs isn't compliant with the pattern used in that 
system (no inst target, and the bld target fails).

VERY MINOR COMMENT

Seems odd that the directory in which one builds is called 
pp and the one in which one installs is ppdev.
Shouldn't it be the other way round?

Roger

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower Update

[Roger Bishop Jones]

Rob,

My theories fail to build on the latest version of maths_egs 
because I have been using R_plus_ops_thm and 
R_plus_group_thm which were in wrk068 but are no longer.

Looks like you have just changed some names, is that right?

Roger Jones

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com