Stream: Coq devs & plugin devs

Topic: Coq ecosystem licensing


view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:25):

but the biggest licensing trouble in our ecosystem right now is probably GPL vs. CECILL-C and CECILL-B. This is to me a time bomb that could explode in our faces in a few years. But Coq itself and its docs will at least not be affected...

view this post on Zulip Paolo Giarrusso (Nov 06 2021 at 18:06):

if that's still an important problem, any chance for CeCILL-B 2.0?

view this post on Zulip Paolo Giarrusso (Nov 06 2021 at 18:09):

(after a few years of latency, of course! I was amazed when EPFL relicensed Scala)

view this post on Zulip Karl Palmskog (Nov 06 2021 at 18:49):

it's at least theoretically possible for them to publish a CECILL-B/C 2.0, and Théo said he was suprised that they hadn't yet. But to my knowledge the conversion from CECILL-B/C "1.0" could not be done by anyone but copyright holders (no "X or later" clause).

view this post on Zulip Karl Palmskog (Nov 06 2021 at 18:52):

CECILL-B/C were also seemingly never submitted to OSI for approval, forcing us to come up with the following convoluted wording for open source licensing in the Coq ecosystem:

use a license that is either approved as an open source license by the OSI, or considered a free software license by the FSF.

(CECILL-B/C are covered by the latter)

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:33):

The license itself has an "X or later" clause.

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:34):

See 12.3 in https://cecill.info/licences/Licence_CeCILL-B_V1-en.html, at least in the English translation

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:35):

Or 12.3 in https://cecill.info/licences/Licence_CeCILL-C_V1-en.html.

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:41):

Actually, is this _enabling_ later versions, or forbidding the use of previous versions/other licenses? How is this clause usually understood?

Any Software distributed under a given version of the Agreement may only be subsequently distributed under the same version of the Agreement or a subsequent version.
Tout Logiciel diffusé sous une version donnée du Contrat ne pourra faire l'objet d'une diffusion ultérieure que sous la même version du Contrat ou une version postérieure.

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:41):

(the latter’s from http://www.cecill.info/licences/Licence_CeCILL-C_V1-fr.html, but doesn’t seem to help)

view this post on Zulip Paolo Giarrusso (Nov 07 2021 at 04:47):

well, main Cecill V1 had the same clause, so hopefully we can find out what happened when V2 was released. But I can’t find an answer in https://cecill.info/faq.en.html.

view this post on Zulip Théo Zimmermann (Nov 08 2021 at 10:17):

I personally understand this as an internal "or later" clause that allows upgrading the license version without asking copyright owners. Therefore, I think that, in the case of CeCILL-B, our best shot is actually at getting a new version published, that would be compatible with the GPL. Given who are the authors, this seems feasible, in theory.


Last updated: Feb 06 2023 at 19:03 UTC