Dear All,

Many thanks to Roger for making pp-contrib happen.

For reasons that I do not understand, the following reply to Phil's last post arrived in the mailing list with "** SPAM **" in the subject line. It is in the archive, but I expect it won't have got to many subscribers. So I am trying again.

On 12/04/2010 16:19, Phil Clayton wrote:
Roger Bishop Jones wrote:
Perhaps one directory for "maths_eq"-like contributions, one for
contributions in the form of patches:

What kind of patches are you envisaging? Do you have any examples in mind?

Personally, I am happy with GPL (2 or 3).

Well, so far it looks like GPL3 on google with mercurial.

GPL 3 would rule out the ProofPower code base as that is GPL 2.  GPL 2
and 3 are 'incompatible':
So, whilst ProofPower is GPL 2, my preference would actually be GPL 2.
(Note ProofPower does not specify "any later version" regarding GPL.)

That would be about redistribution. You won't be redistributing OpenProofPower on pp-contrib. I am considering the "any later version" option, but don't consider it a big issue at the moment because I don't think anybody will want to do redistribute OpenProofPower other than perhaps as a freestanding whole so that it can be freely combined with other GPL 2 and GPL 3 offerings regardless of which I use.

In fact, this may be an issue for the sort of contributions you are
talking about too.  On the one hand, one could view ProofPower like a
compiler that processes theories and these theories could be viewed as
works in their own right, so they could have whatever licence the
author wants.  On the other hand, one could view these theories as ML
programs that make calls to the ProofPower library of ML functions so
would need to be available under GPL 2:
That does not stop them also being made available under a 'compatible'
licence, i.e. one that is upstream from GPL 2 in the following diagram:

Under the latter interpretation, which is probably the right one, I
don't think it would be possible to make the contributions available
under GPL 3 as it stands.

Please bear in mind that an open source licence is simply a public statement that the copyright holder won't take legal action against users of their software who haven't bought a licence but do conform with a given set of rules. It isn't a contract. It is the copyright holder who is going to assess conformance with the rules and decide whether to take action against a user. If that every happened, then no doubt a court would take the terms of the open source licence into account.

In this case, the copyright holder is Lemma 1 and my position is essentially like that of Larry Wall on Perl scripts and the GPL (see That means that I will always take your first interpretation for scripts that are distributed separately from OpenProofPower. I would be very happy to make a similar public statement about this to clarify the position and would it make it clear that distributing theory scripts under GPL3 is OK. The only thing I really want to prevent is someone shrink-wrapping OpenProofPower inside their own packaging and selling the result (i.e., unlike Perl, I definitely don't want to use something like the Artistic Licence).

On google you can have a different licence for documentation, one of
the creative commons licences. Does anyone think that would be a good

I don't know much about the creative commons licence - what are the
benefits and drawbacks for documentation?
I don't understand the distinctions you are making here, and think
that I need to.

 Whilst the
 Subversion working copy is local to a machine, without
 visibility of the repository I couldn't see the log of
 previous commits, ...

I'm not convinced that the problems you are experiencing reflect what
would happen if we had a properly set up subversion repository.

For this I think you need to have the repository on a server which
runs a subversion service.  Having a repository which is visible
across the network by other means is not the same.
I have a subversion repository at, but cannot provide a
general service because is on a virtual host so all
access to the repository has to be through my username.

Sorry, all I was saying is that when one doesn't have access to the
Subversion repository (for whatever reason), any operation that
requires access to the Subversion repository won't work, which
includes various operations that I would do normally during the course
of development, e.g. looking at the previous log messages or previous
revisions or making commits.

I am with Phil on this one. Using subversion is a pain if you are on the move, say. Even with 100% access to the server, you typically end up with a check-out of everything you have ever worked on lying round on your local filestore, you end up with a configuration which takes up as much space as the distributed model but doesn't put that space to very good use.
Wherever the repository is, or however it is set up, if you don't have
access, you can get stuck.  Whilst a repository on Google Code would
be quite accessible, I do a lot of development on the move and
wouldn't even want to be dependent on an internet connection.

With a distributed VCS, you have your own local repository, so access
is not a problem.

Also I don't understand your commit problem, why was it desirable to
have a series of commits rather than just one?

If I'm making three separate changes that are totally unrelated, it's
better for these to be separate commits, in my view.  For example, it
is easier for people to understand the changes if they're separated
out. Also, it would allow someone else to pull one of the changes into
their development without having to get all three.

Well you and Rob are both against subversion so we can do Mercurial
at google or Git at sourceforge, unless anyone prefers some other host.

I think Rob prefers Mercurial, which I'm quite happy with too.
I do prefer the look of Mercurial.

Both of these are blocked for Cuba, Iran, Libya, North Korea, Sudan,
Syria, does anyone think that important?

I haven't heard of anyone working on ProofPower in these countries...
I would be happy to make source tarballs of pp-contrib releases available via the ProofPower website from time to time, so that it would be available world-wide. (I am assuming that we will want to make tarballs available.)



Proofpower mailing list

Reply via email to