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 <hugo.herbelin@inria.fr> À : samuel.mimram@ens-lyon.fr (Samuel Mimram) Cc : barras@pauillac.inria.fr (Bruno Barras), Christine.Paulin@lri.fr (Christine Paulin), marche@lri.fr, Yves.Bertot@inria.fr, filliatr@pauillac.inria.fr (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 samuel.mimram@ens-lyon.fr 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"
Attachment:
pgp1qPnW3VqMk.pgp
Description: PGP signature