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:
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#IfLibraryIsGPL
http://www.gnu.org/licenses/old-licenses/gpl-2.0-faq.html#LinkingWithGPL
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.)
Regards
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
