[Fwd: Résumé discussion licence de Coq]
Hello,
COQ licensing problems might be very soon resolved (cf. the forwarded
message). I think that the code should not change very much, only the
licenses should be there and consistent.
Is any one volunteering to begin COQ's packaging (I cannot do that
myself before at least two weeks because I only have a modem
connection)? This can be done on the current distribution and there
should be only very few modifications (if any) to have it working with
the new COQ source code.
It would be a good thing to have it done quickly in order to be sure
that COQ 8.0 will be part of sarge.
Thanks,
Samuel.
-------- Original Message --------
Subject: Résumé discussion licence de Coq
Date: Tue, 18 May 2004 18:11:24 +0200 (MET DST)
From: Hugo Herbelin <hugo.herbelin@inria.fr>
To: coqdev@pauillac.inria.fr, Guillaume.Rousseau@inria.fr
CC: samuel.mimram@ens-lyon.fr, lionel@mamane.lu
Un petit mot pour donner un bilan de la discussion que nous avons
eue avec le responsable aux relations industrielles de l'INRIA Futurs,
Guillaume Rousseau.
Combiner du GPL et du LGPL
--------------------------
Confirmation de l'analyse de Lionel Mamame que l'intégration de code
LGPL et de code GPL est compatible. Le binaire résultant est alors
GPL.
La présence de code GPL dans les sources de Coq n'interdit pas à un
utilisateur extérieur de distribuer sous forme binaire du code
provenant de Coq, mais il devra se séparer des répertoires sous GPL,
c'est-à-dire à l'heure actuelle, les répertoires
- ide/utils
(à moins qu'un volontaire ne réécrive le code ou s'arrange avec
Maxence)
- contrib/jprover (en fait les 2 fichiers principaux)
- contrib/xml
(mais j'ai cru comprendre que Claudio était d'accord
pour le passer dans la licence principale de Coq)
[Il semble bien que, contrairement à ce qu'annoncé par Samuel,
romega est en LGPL 2.1]
Choisir LGPL, GPL ou une autre licence pour Coq ?
-------------------------------------------------
À partir du moment où GPL et LGPL sont compatibles, le plus simple
est de garder la licence actuelle, càd LGPL. D'autres licences sont
plus libérales (et mieux rédigées, selon Guillaume) mais 1) il
faudrait les étudier 2) il faudrait en théorie que la décision de
changer de licence soit approuvée par l'ensemble des contributeurs,
passés et présents.
Le statut des .v, des .vo, et du code extrait
---------------------------------------------
Il serait probablement opportun d'expliciter dans le fichier
décrivant la licence le statut du code extrait
- Typiquement, si JProver, GPL, est utilisé (dans Set) pour
construire une preuve dont un programme est extrait, ce dernier
peut-il être considéré comme (partiellement) dérivé de JProver, et
donc imposer sa licence à tout programme utilisant ce code extrait ?
- Similairement (cf message de Lionel), du code extrait de la biblio
standard, LGPL, peut-il imposer à tout programme utilisant ce code
extrait d'être LGPL à son tour ?
Je ne sais pas comment cela se dirait, peut-être quelque chose comme
« Le procédé de transformation par Coq des fichiers vernaculaires (.v)
en fichiers vernaculaires objets (.vo) doit être compris comme un
procédé de compilation et lesdits fichiers vernaculaires objets
doivent ainsi être compris comme des bibliothèques compilées » ?
Mise à jour de l'archive et du site web
---------------------------------------
Nous mettrons l'archive à jour d'ici quelques jours (quand nous aurons
le temps).
- Mise à jour des 2 fichiers QPL ce qui les rend GPL.
- Mise à jour du fichier COPYRIGHT.
- Mise à jour du fichier CREDITS récapitulant notamment les licences et
application automatique de la licence principale choisie aux
fichiers qui n'ont pas d'en-tête explicite (LGPL).
Nous expliciterons sur le site Web que la licence des fichiers de Coq
est celle choisie par l'équipe de développement (LGPL), hors quelques
contributions périphériques sous licence GPL.
Le statut de contrib/interface
------------------------------
Yves Bertot a écrit:
Je suis favorable à ce que ce code soit
mis sous la licence la plus permissive possible, mais certains des
fichiers sont en fait engendrés à partir de spécification venant de
pcoq (les fichiers vtp.ml et ascent.mli). Faudra-t-il que pcoq passe
sous licence GPL également?
La licence de pcoq a l'air très libérale et ne semble pas interdire
de cohabiter avec du GPL ou LGPL, donc en mettant les fichiers vtp.ml,
ascent.mli sous licence pcoq, il ne devrait pas y avoir de problèmes,
non ?
Mais après tout, Lemme est l'auteur tant de pcoq que de ces
fichiers, donc je suppose que vous pouvez choisir la licence que vous
voulez quelque soit la manière dont vous avez produit les fichiers .ml,
non ?
Reply to: