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.
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.
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': http://www.gnu.org/licenses/rms-why-gplv3.html
So, whilst ProofPower is GPL 2, my preference would actually be GPL 2.
(Note ProofPower does not specify "any later version" regarding GPL.)
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:
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.
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.
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
http://dev.perl.org/licenses). 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
Proofpower mailing list