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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
