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
[EMAIL PROTECTED]
-- To UNSUBSCRIBE, email to [EMAIL PROTECTED] with a subject of "unsubscribe". Trouble? Contact [EMAIL PROTECTED]
