Re: License of coq documentation
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
> coqdev@pauillac.inria.fr (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
Reply to: