On Tue, Dec 20, 2005 at 11:30:02AM +0100, Samuel Mimram wrote: > 1. Coq upstream has agreed to put a license on the documentation > (reproduced at the end of the mail). This would close #294865. Since it > was not written by a lawyer, upstream has asked me if I could get > comments on it. So I'd be glad if you could tell me if you see any > obvious flaw in it.
See below. > Of course, I don't expect it to be DFSG-free. Of course, we have to comment here that we think it is a bad idea. Why is Coq free software? I like to think that it is so that if Pr Przwalsky really thinks Coq should do something differently, but the Coq team disagrees (that's why Coq does it the way it does, after all) can fork Coq into Kogut, and Coq and Kogut will stand publicly in free competition, and the best one will win for the best interest of humanity in general and the French public / nation in particular (the French public is the ones paying for Coq). But now, if the documentation can't be forked with Coq, what's the situation? Kogut has an unfair disadvantage, because its documentation sucks and Coq has all this very nice documentation. So what happens if people continue using Coq and not Kogut? - If Coq is really better than Kogut, then Pr Przwalsky will say (and honestly think) that it is only because Coq has better documentation, that Kogut is inherently better, but he doesn't have the resources to rewrite all documentation. But he has the resources to change Coq's documentation to become a good Kogut doc. The Coq team is then deprived of the fame and public adoration that's rightly theirs: they are right, but it is not clear to the face of the world because of thus unfair advantage thingy. - If Kogut is really better, then we have made humanity (and the French public) a disservice. They are stuck with an inferior system for bad reasons. Am I wrong? > 2. The coq tarball contains LGPL and GPL files (which are both > linked together when building coq). I've always thought that if I > extract an LGPL file from the tarball then I can use it as > LGPL. However upstream has told me that he was told that it was not > the case (all files in the tarball should should be considered as > GPL, because they were distributed with GPL files, thus being part > of the sources of a GPL program). Who's right? If this is the intention of the person creating or distributing the tarball, she can make it so, but it is not the default situation. The tarball compiler (I mean the person that put all the files together in a consistent collection) can assert a "compilation copyright" (that is a copyright over the whole tarball because of his work in putting it together). The license over this compilation can be the GPL, and then you have to obey the GPL on everything you take out of the tarball. The tarball distributor can also decide to relicense the LGPL-covered files under the GPL - a clause of the LGPL permits him to do that. He then removes the header in the file saying "permission to distribute, derivative works, etc under the conditions of the LGPL version 2.1 or any later version published by the FSF" and replaces it with "permission to distribute, derivative works, etc under the conditions of the GPL version 2 or any later version published by the FSF". That particular copy of the file is GPLed, then, not LGPLed. What _is_ automatic is that if you combine these two files in any way (you past the two sources in one file, you compile them separately to object files and link them together, ...) then the result is GPLed. Putting them together in a tarball is not IMHO combination of the two, but "mere aggregation". > ---------------------------------------------------------------------- > The Coq system versions 7 and 8 are copyright (c) 1999-2005 The Coq > development team, Institut National de Recherche en Informatique et en > Automatique (INRIA), Centre National de la Recherche Scientifique > (CNRS) and University Paris Sud, all rights reserved. > > The Coq Reference Manual is copyright (c) 1999-2005 The Coq development > team, Institut National de Recherche en Informatique et en Automatique > (INRIA), Centre National de la Recherche Scientifique (CNRS) and > University Paris Sud. > > The Coq Reference Manual may be reproduced and distributed in whole or > in part, subject to the following conditions: > > * The copyright notice above and this permission notice (including the > internet address of the original source) must be preserved complete > on all complete or partial copies. > > * The distribution of any derivative work of the Coq Reference Manual, > to the exception of translation from English for academic non > commercial purpose, must be approved by the authors in writing to > [EMAIL PROTECTED] (or to one of the contact address available > on the site coq.inria.fr). One could call the selection of a part of the manual for "distribution in part" a derivative work. You intend to permit this without approval, right? So add it to the exceptions. > * If you distribute the Coq Reference Manual in part, instructions for > obtaining the complete version must be included, and a means for > obtaining a complete version provided. What is the intention? That if I put a part on my website or in print I have to provide the whole in _some_ (possibly other) way or is a pointer to http://coq.inria.fr/doc/ enough? > * Small portions may be reproduced as illustrations for reviews or > quotes in other works without this permission notice if proper > citation is given. It is good to let that paragraph there, but you are aware that the law gives people this right even if you don't want people to have this right, right? -- Lionel -- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
