Problème de licenses avec COQ

[Samuel Mimram <samuel.mimram@ens-lyon.fr>]

Bonjour,

Je m'intéresse au packaging Debian de la version 8.0 de COQ.

Malheureusement ceci est impossible en l'état actuel du projet étant
donné le flou qui semble y avoir en ce qui concerne les licenses.

La license générale du projet semble être la LGPL (du moins le seul
texte de license qu'elle semble contenir (LICENSE) est la LGPL et c'est
ce qui est indiqué sur le site). Si la majorité des fichiers de COQ font
bien mention de la LGPL ça n'est pas le cas pour tous :
- un certain nombre, non négligeable, d'entre eux est sous GPL [1] ;
- deux mli portent encore la mention de la Q Public License [2] alors
que les ml correspondant sont sous GPL (ces fichiers sont issus de
cameleon qui est sous GPL) ;
- d'autres encore, dont certains de taille assez conséquente, ne portent
pas de mention de license dans leur header [3].

Je ne suis pas un spécialiste en la matière cependant il me semble que
tout cela est illegal ou du moins inconsistent ce que rend les licenses 
nulles et nous empèche d'intégrer la nouvelle version de COQ à Debian.

Le principal problème est celui des fichiers sous GPL [1]. En effet, la
GPL est une license sous copyleft fort qui stipule que tout programme
dérivé doit lui-même être sous GPL [4] et ne peut donc être utilisé dans
un programme sous LGPL qui n'est pas compatible avec la GPL car plus
permissive. Le fait d'être lié ou d'utiliser du code d'une librairie GPL
est considéré comme faire un produit dérivé.
De plus -- c'est un problème annexe -- vous auriez dû distribuer le
texte de la GPL avec le code sous GPL.

Le problème des fichiers sous QPL [2] se ramène au précédent car d'une
part c'est le même cas de figure, et d'autre part ces fichiers sont
maintenant licensés sous GPL.

Le fait que de très nombreux fichiers ne contiennent pas de license ni
de copyright est un problème moins important ; on peut en effet
considérer que l'ensemble du projet est sous LGPL et que implicitement
les fichiers sans copyright le sont aussi. Il serait néanmoins mieux de
le préciser dans chaque header ou du moins de dire explicitement (dans
le fichier COPYRIGHT par exemple) que le projet entier est sous LGPL [5].

Il serait donc fortement souhaitable que vous vous mettiez en accord
avec les licences du code que vous utilisez. Pour ce faire, je vois deux 
principales
options :
1. passer tout le code sous GPL ;
2. s'arranger avec les auteurs des sources sous GPL utilisées pour avoir
des dérogations.

Je vous remercie par avance pour votre aide et votre coopération.

Codialement,

Samuel.



[1] Liste des fichiers sous GPL:

./contrib/jprover/jall.ml
./contrib/jprover/jtunify.ml
./contrib/romega/ROmega.v
./contrib/romega/ReflOmegaCore.v
./contrib/romega/const_omega.ml
./contrib/romega/g_romega.ml4
./contrib/romega/refl_omega.ml
./contrib/xml/acic.ml
./contrib/xml/acic2Xml.ml4
./contrib/xml/cic.dtd
./contrib/xml/cic2acic.ml
./contrib/xml/doubleTypeInference.ml
./contrib/xml/doubleTypeInference.mli
./contrib/xml/proof2aproof.ml
./contrib/xml/proofTree2Xml.ml4
./contrib/xml/theoryobject.dtd
./contrib/xml/unshare.ml
./contrib/xml/unshare.mli
./contrib/xml/xml.ml4
./contrib/xml/xml.mli
./contrib/xml/xmlcommand.ml
./contrib/xml/xmlcommand.mli
./contrib/xml/xmlentries.ml4
./ide/utils/configwin.ml
./ide/utils/configwin_html_config.ml
./ide/utils/configwin_ihm.ml
./ide/utils/configwin_keys.ml
./ide/utils/configwin_messages.ml
./ide/utils/configwin_types.ml
./ide/utils/okey.ml

Vraisemblablement sous GPL (aucune mention dans les headers cependant) :

./contrib/jprover/jall.mli
./contrib/jprover/jlogic.ml
./contrib/jprover/jlogic.mli
./contrib/jprover/jprover.ml4
./contrib/jprover/jterm.ml
./contrib/jprover/jterm.mli
./contrib/jprover/jtunify.mli
./contrib/jprover/opname.ml
./contrib/jprover/opname.mli


[2] Liste des fichiers sous QPL :

./ide/utils/configwin.mli
./ide/utils/okey.mli

[3] Liste des fichiers sans license :

./dev/Makefile.common
./dev/Makefile.devel
./dev/Makefile.dir
./dev/Makefile.subdir
./config/Makefile.template
./config/giveostype.ml
./config/Makefile.template
./config/giveostype.ml
./contrib/cc/README
./contrib/correctness/examples/extract.v
./contrib/correctness/preuves.v
./contrib/extraction/test/custom/Ranalysis
./contrib/extraction/test/custom/Adalloc
./contrib/extraction/test/custom/Euclid
./contrib/extraction/test/custom/List
./contrib/extraction/test/custom/ListSet
./contrib/extraction/test/custom/Lsort
./contrib/extraction/test/custom/Map
./contrib/extraction/test/custom/Mapcard
./contrib/extraction/test/custom/Mapiter
./contrib/extraction/test/custom/R_Ifp
./contrib/extraction/test/custom/R_sqr
./contrib/extraction/test/custom/Rbasic_fun
./contrib/extraction/test/custom/Raxioms
./contrib/extraction/test/custom/Rbase
./contrib/extraction/test/custom/Rdefinitions
./contrib/extraction/test/custom/Reals.v
./contrib/extraction/test/custom/Rfunctions
./contrib/extraction/test/custom/Rgeom
./contrib/extraction/test/custom/Rlimit
./contrib/extraction/test/custom/Rseries
./contrib/extraction/test/custom/Rsigma
./contrib/extraction/test/custom/Rtrigo
./contrib/extraction/test/custom/ZArith_dec
./contrib/extraction/test/custom/fast_integer
./contrib/extraction/test/Makefile
./contrib/extraction/test/Makefile.haskell
./contrib/extraction/test/addReals
./contrib/extraction/test/e
./contrib/extraction/test/extract
./contrib/extraction/test/extract.haskell
./contrib/extraction/test/hs2v.ml
./contrib/extraction/test/make_mli
./contrib/extraction/test/ml2v.ml
./contrib/extraction/test/v2hs.ml
./contrib/extraction/test/v2ml.ml
./contrib/funind/tacinv.ml4
./contrib/funind/tacinvutils.ml
./contrib/funind/tacinvutils.mli
./contrib/interface/ascent.mli
./contrib/interface/blast.ml
./contrib/interface/blast.mli
./contrib/interface/centaur.ml4
./contrib/interface/ctast.ml
./contrib/interface/dad.ml
./contrib/interface/dad.mli
./contrib/interface/debug_tac.ml4
./contrib/interface/debug_tac.mli
./contrib/interface/history.ml
./contrib/interface/history.mli
./contrib/interface/line_parser.ml4
./contrib/interface/line_parser.mli
./contrib/interface/name_to_ast.ml
./contrib/interface/name_to_ast.mli
./contrib/interface/parse.ml
./contrib/interface/paths.ml
./contrib/interface/paths.mli
./contrib/interface/pbp.ml
./contrib/interface/pbp.mli
./contrib/interface/showproof.ml
./contrib/interface/showproof.mli
./contrib/interface/showproof_ct.ml
./contrib/interface/translate.ml
./contrib/interface/translate.mli
./contrib/interface/vernacrc
./contrib/interface/vtp.ml
./contrib/interface/vtp.mli
./contrib/interface/xlate.ml
./contrib/interface/xlate.mli
./contrib7/correctness/preuves.v
./contrib7/interface/AddDad.v
./contrib7/interface/Centaur.v
./contrib7/interface/vernacrc
./contrib7/romega/ROmega.v
./contrib7/romega/ReflOmegaCore.v
./ide/utils/editable_cells.ml
./ide/utils/uoptions.ml
./ide/utils/uoptions.mli
./tactics/leminv.mli
./test-suite/failure/Case1.v
./test-suite/failure/Case10.v
./test-suite/failure/Case11.v
./test-suite/failure/Case12.v
./test-suite/failure/Case13.v
./test-suite/failure/Case14.v
./test-suite/failure/Case15.v
./test-suite/failure/Case16.v
./test-suite/failure/Case2.v
./test-suite/failure/Case3.v
./test-suite/failure/Case4.v
./test-suite/failure/Case5.v
./test-suite/failure/Case6.v
./test-suite/failure/Case7.v
./test-suite/failure/Case8.v
./test-suite/failure/Case9.v
./test-suite/failure/ClearBody.v
./test-suite/failure/cases.v
./test-suite/failure/check.v
./test-suite/failure/clashes.v
./test-suite/failure/coqbugs0266.v
./test-suite/failure/ltac1.v
./test-suite/failure/ltac2.v
./test-suite/failure/ltac3.v
./test-suite/failure/ltac4.v
./test-suite/failure/params_ind.v
./test-suite/failure/universes-buraliforti.v
./test-suite/failure/universes-sections1.v
./test-suite/failure/universes-sections2.v
./test-suite/failure/universes.v
./test-suite/failure/universes2.v
./test-suite/ideal-features/Case3.v
./test-suite/ideal-features/Case4.v
./test-suite/ideal-features/Case8.v
./test-suite/kernel/inds.mv
./test-suite/modules/Nametab.v
./test-suite/modules/Demo.v
./test-suite/modules/Przyklad.v
./test-suite/modules/Nat.v
./test-suite/modules/PO.v
./test-suite/modules/Tescik.v
./test-suite/modules/fun_objects.v
./test-suite/modules/grammar.v
./test-suite/modules/ind.v
./test-suite/modules/mod_decl.v
./test-suite/modules/modeq.v
./test-suite/modules/modul.v
./test-suite/modules/obj.v
./test-suite/modules/objects.v
./test-suite/modules/pliczek.v
./test-suite/modules/plik.v
./test-suite/modules/sig.v
./test-suite/modules/sub_objects.v
./test-suite/output/Arith.v
./test-suite/output/Cases.v
./test-suite/output/Coercions.v
./test-suite/output/Fixpoint.v
./test-suite/output/Implicit.v
./test-suite/output/InitSyntax.v
./test-suite/output/Intuition.v
./test-suite/output/Nametab.v
./test-suite/output/RealSyntax.v
./test-suite/output/Remark2.v
./test-suite/output/Sum.v
./test-suite/output/TranspModtype.v
./test-suite/output/ZSyntax.v
./test-suite/output/implicits.v
./test-suite/success/Case1.v
./test-suite/success/Case10.v
./test-suite/success/Case11.v
./test-suite/success/Case12.v
./test-suite/success/Case13.v
./test-suite/success/Case14.v
./test-suite/success/Case15.v
./test-suite/success/Case16.v
./test-suite/success/Case17.v
./test-suite/success/Case2.v
./test-suite/success/Case5.v
./test-suite/success/Case6.v
./test-suite/success/Case7.v
./test-suite/success/Case9.v
./test-suite/success/CaseAlias.v
./test-suite/success/Cases.v
./test-suite/success/CasesDep.v
./test-suite/success/Conjecture.v
./test-suite/success/DHyp.v
./test-suite/success/Decompose.v
./test-suite/success/Destruct.v
./test-suite/success/DiscrR.v
./test-suite/success/Discriminate.v
./test-suite/success/Fourier.v
./test-suite/success/Funind.v
./test-suite/success/Generalize.v
./test-suite/success/Hints.v
./test-suite/success/Inductive.v
./test-suite/success/Injection.v
./test-suite/success/Inversion.v
./test-suite/success/LetIn.v
./test-suite/success/MatchFail.v
./test-suite/success/Mod_ltac.v
./test-suite/success/Mod_params.v
./test-suite/success/Mod_strengthen.v
./test-suite/success/NatRing.v
./test-suite/success/Omega.v
./test-suite/success/PPFix.v8
./test-suite/success/Print.v
./test-suite/success/Projection.v
./test-suite/success/Record.v
./test-suite/success/Reg.v
./test-suite/success/Remark.v
./test-suite/success/Rename.v
./test-suite/success/Require.v
./test-suite/success/Scopes.v
./test-suite/success/Simplify_eq.v
./test-suite/success/Try.v
./test-suite/success/cc.v
./test-suite/success/coercions.v
./test-suite/success/coqbugs0181.v
./test-suite/success/evars.v
./test-suite/success/if.v
./test-suite/success/implicit.v
./test-suite/success/import_lib.v
./test-suite/success/import_mod.v
./test-suite/success/ltac.v
./test-suite/success/options.v
./test-suite/success/refine.v
./test-suite/success/setoid_test.v
./test-suite/success/univers.v
./theories/Logic/Hurkens.v
./theories/Logic/ProofIrrelevance.v
./theories7/Logic/Hurkens.v
./theories7/Logic/ProofIrrelevance.v
./tools/coqdoc/coqdoc.sty
./tools/coqdoc/style.css
./tools/coq-sl.sty
./tools/coq.el

[4] Paragraphe 2. b) de la GPL :

« You must cause any work that you distribute or publish, that in whole
or in part contains or is derived from the Program or any part thereof,
to be licensed as a whole at no charge to all third parties under the
terms of this License. »

[5] Extrait de http://www.fsf.org/licenses/gpl-howto.html :

« Whichever license you plan to use, the process involves adding two
elements to each source file of your program: a copyright notice (such
as "Copyright 1999 Linda Jones"), and a statement of copying permission,
saying that the program is distributed under the terms of the GNU
General Public License (or the Lesser GPL). »

--
Samuel Mimram

samuel.mimram@ens-lyon.fr