Rob Arthan wrote:
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?

(I'm not sure if that was a question for Roger or me.) For me, an example is extending proof support for Z sequences. This involves significant changes to the structure ZSequences1 and associated theory in dtd107 and imp107. There are likely to be changes for knock-on effects but I haven't got that far yet.

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.

For changes to the OPP code base like above, a baseline version of the OPP source really needs to be in the repository. There is no intention to be redistributing OPP, just making the changes available, however someone would get everything in the repository when cloned. What do you think of that set up?

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

Thanks for explaining that. I think it is important to clarify you interpretation on the ProofPower licence web page and in the LICENCE file. Unless stated, nobody will ever really know. For example, it wasn't clear whether you take Larry Wall's position on object code too. Under GPL, someone can pass on a binary release of OpenProofPower, as long as they (offer to) provide the source. Can they provide a proprietary child database or is that within your definition of shrink-wrapping?


Proofpower mailing list

Reply via email to