On Monday 12 Apr 2010 16:19, Phil Clayton wrote:

> That sounds flexible enough.  Does this all go into one
>  repository?  (I don't know what is possible or most
>  suitable using Mercurial on google code.)

Well I don't know enough about mercurial so I am relying on 
Rob to say if we are proposing something that won't work.

With svn, (which also I lack experience in) the issue is 
where you split trunk from branches, and the google 
repository comes with these set up at the top level.
I assume they will do the same with mercurial.
I think that would be OK because I would guess that we are 
going to fork for each new release of ProofPower, and 
presumably that would have to be done for all three kinds of 
contribution.
 
> >> 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.)

Yes it has to be the same as ProofPower so if GPL3 is not 
compatible with GPL2 we'd better stick to GPL2.
Perhaps Rob could comment on why he doesn't allow GPL3?

> 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.htm
> l#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-c
> ompatible-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.

For my purpose it is necessary to stick with the ProofPower 
licence because my contrib would contain variants on 
ProofPower facilities obtained by editing ProofPower source 
code.  (e.g. unifying forward chaining).

However, I don't think your interpretation of the licencing 
requirement for contributions which don't do that is 
correct.  I think the discussions address the cases where 
you are actually linking in libraries which are then 
distributed as part of your product.
So long as you don't incorporate or distribute software you 
are not bound by its,licence terms (as far as distributing 
software which uses it, though of course someone using the 
contrib would need to comply with the ProofPower licence).
But that's by the by since I agree that we do need GPL2.
In any case the patches are derived works, and your proposed 
use of the entire code base certainly would be!
  
> > 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 think they are more liberal licences and there is more 
flexibility.
However, in the present context, unless ProofPower were to 
adopt this procedure then it wouldn't be possible to use 
proofpower documentation in a contribution, so we had better 
just stick with GPL2.

We would have to change the licence if ProofPower does, this 
seems to be possible.

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

Of course.
I was reconciling myself to the idea that life grinds to a 
halt when your connection goes down, but I'm sure you are 
right to want to minimise the disruption.

My inclination then is to set up the project on Google with
the name pp-contrib (assuming that's available) and then 
sketch out in the project wiki a proposed modus operandum
for comments, and then we can try it out, perhaps with 
maths_eqs and something from me.

If I set it up initially perhaps interested parties could 
join the project and have a look around see whether they hae 
any comments on the setup.

Roger Jones







_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to