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

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: http://www.gnu.org/licenses/quick-guide-gplv3.html#new-compatible-licenses 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 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).

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

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 rbjones.com, but cannot provide a general service because rbjones.com 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