License of coq documentation
[Please keep Hugo and I in CC, we're not subscribed to the list]
I have two questions for you.
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. Of course, I don't expect it to be DFSG-free.
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?
Thanks very much.
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
firstname.lastname@example.org (or to one of the contact address available
on the site coq.inria.fr).
* 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.
* Small portions may be reproduced as illustrations for reviews or
quotes in other works without this permission notice if proper
citation is given.
The Coq Reference Manual is available in
* html format, online at http://coq.inria.fr/doc and as a tarball at
* PostScript or PDF format at ftp://ftp.inria.fr/INRIA/coq/current/doc.