Hello, For non-french speakers: the QPL files have been completely removed from the sources. The code is under LGPL excepting contrib/jprover and ide/utils which are under GPL and are not absolutely necessary to build COQ.
The new archive should be available soon (How much time do we have left
to have it in sarge? I guess we'll have to wait the results of the
votings to know).
Cheers,
Samuel.
Message transmis :
Le : Tue, 29 Jun 2004 15:47:36 +0200 (MET DST)
De : Hugo Herbelin <[EMAIL PROTECTED]>
� : [EMAIL PROTECTED] (Samuel Mimram)
Cc : [EMAIL PROTECTED] (Bruno Barras), [EMAIL PROTECTED]
(Christine Paulin), [EMAIL PROTECTED], [EMAIL PROTECTED], [EMAIL PROTECTED]
(Jean-Christophe Filliatre)
Sujet : Re: [Coqdev] Re: Commentaires sur bug Coq 708
Bonjour,
Coq restera principalement en LGPL avec 2 r�pertoires sous GPL:
- contrib/jprover qui implante une tactique en standard dans Coq
- ide/utils qui ne sert qu'� l'interface graphique CoqIde
Dans notre version de d�veloppement, il n'y a d�sormais plus de code
QPL.
Je ne sais pas que cela veut dire pour l'ex�cutable lui-m�me.
L'ex�cutable ne venant pas avec les sources, je suppose que la
question d'�tre GPL ou LGPL ne s'applique pas.
S'il faut caract�riser le projet de d�veloppement Coq dans son
ensemble, je propose la formulation suivante : Coq est d�velopp� sous
license LGPL � l'exception de 2 contributions auxiliaires qui sont
d�velopp�es en license GPL. L'une de ces contributions est n�cessaire
pour le fonctionnement de l'interface graphique CoqIde mais n'est en
aucun cas n�cessaire au fonctionnement de Coq. La seconde de ces
contributions fait partie de Coq mais peut �tre retir�e de la phase
d'�dition de liens sans effet sur le principe de fonctionnement de
Coq.
Yves Bertot nous transmet l'information que la pr�paration d'une
nouvelle version stable de Debian (la Sarge ?) est en cours. Nous
serions bien s�r ravi d'y voir int�grer la version 8.0 de Coq. Merci
de nous dire (si pas d�j� trop tard) pour quand vous aurez besoin que
nous publions une version de Coq conforme aux principes ci-dessus ?
Cordialement,
Hugo Herbelin
--
Samuel Mimram
[EMAIL PROTECTED]
Whenever the literary German dives into a sentence, that is the last
you are going to see of him until he emerges on the other side of his
Atlantic with his verb in his mouth.
-- Mark Twain "A Connecticut Yankee in King Arthur's Court"
pgpDQWL3tZCqC.pgp
Description: PGP signature
