Thanks for those explanations Claudio. > > % rgrep "Q Public" . -l > > ./ide/utils/configwin.mli > > ./ide/utils/okey.mli > > > Those files seem to come from Cameleon which is now licensed under > > the GPL. > > Right. These are QPLed. Thes two files are necessary only to > coqide. Of course coqide is interesting, but it should be a separate > package from the rest of Coq (since it depends on lablgtk). > Thus this does not inhibit packaging the core Coq. Of course it should be a separate package but anyway there's a problem. I think the QPL is a mistake since the corresponding ml are under GPL and the files are now distributed under GPL (see for example [1]). But anyway, the coqide would have to be under GPL which does not seem to be the case (for example coqide.ml is clearly under LGPL). > > What is also very worrying I think is: > > > ./contrib/xml/* > > Right: the COPYRIGHT file states that the licensee is the same as > Coq, but I put the GPL header in the files (I am the main author of > contrib/xml). I am willing to change it if requested to. I think it would be a nice thing to do since the GPL is not compatible with COQ's LGPL. > > ./ide/* [...] > > ./contrib/jprover/jtunify.ml Here is a major legal problem. We could remove those components from the package but I don't think this would be enough to be legally correct. IANAL but COQ is violating some licenses and I think that just not packaging the incriminated parts would not be enough to be able to be in Debian. It is not acceptable to have GPLed code reused in LGPLed code. > > ./tools/coq-inferior.el > > I do not know much about this. It provides emacs modes for Coq. > The author is probably willing to change the licence, but the file > is a modification of an older file that could be GPLed. I should not have put this file in the list of problematic files. To have an emacs-mode under GPL in an LGPL project is correct since COQ is not linked with it. Moreover, RMS advises to put emacs-lisp files under GPL [2]. Another problem is that many files don't have a copyright header [3]. The whole project seems to be under LGPL (at least the only license is in the file LICENSE and is the LGPL and it is stated so on the website). But there should be a clear mention of the copyright in each file [4]: "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)." As a conclusion I would say that COQ can absolutely not be packaged now. COQ's team absolutely has to clarify the situation. I would be glad if you could help. Thank you, Samuel. [1] http://savannah.nongnu.org/cgi-bin/viewcvs/cameleon/cameleon/configwin/configwin.mli?rev=1.9&content-type=text/vnd.viewcvs-markup [2] http://lists.debian.org/debian-legal/2002/debian-legal-200211/msg00217.html [3] Files without 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] http://www.fsf.org/licenses/gpl-howto.html
Attachment:
pgpc67qCMeMpd.pgp
Description: PGP signature