Stream: Coq Platform devs & users

Topic: CECILL licenses and (L)GPL compatibility


view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:07):

Is there any clarity on the compatibility of the various CECILL licenses with more conventional ones? CECILL got an update with explicit GPL compatibility, but I haven’t seen such clarifications for e.g. CECILL-C or CECILL-B

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:08):

so, while CECILL-B and CECILL-C are meant to be _comparable_ with BSD and LGPL, I’m not sure if they’re actually compatible with their analogues.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:10):

(IIRC, there’s a path to relicense any such work under CECILL 2.0 and then under GPL, but it’s very non-straightforward, and I don’t see a way to get to e.g. LGPL)

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:10):

https://www.gnu.org/licenses/license-list.en.html#CeCILL-B (and CECILL-C just below)

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:13):

doesn’t that forbid distributing the Coq platform, or at least combining CECILL-B,C and GPL code?

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:14):

for the main CECILL license, this was fixed by releasing an update

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:14):

the Coq platform is to me not a "combined/derived work", we don't fork the code and modify it. It's essentially just joint distribution. I have a hard time seeing that if I put FreeBSD and a Linux distribution on the same DVD, the whole DVD falls under the GPL.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:16):

so what is forbidden by the incompatibility?

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:16):

and why did CECILL people not release updates to CECILL-B and -C?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:17):

basically, if you set up a project licensed under the GPL, I guess you can't use any CECILL-B or CECILL-C libraries in that project (bye, MathComp).

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:18):

but also if I just want my project to be GPL-compatible

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:21):

I guess so. Personally, let's just say that GPL-compatibility for my projects is not something I lose sleep over. It just means that someone copies my code and imposes tons of annoying extra conditions for other people using that copy.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:21):

“this license is sort-of BSD-style, so you can do pretty much anything with it, except use it in (L?)GPL code” sounds like a licensing nightmare.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:22):

fair enough, I guess — to me “GPL-incompatible” is a bit like anti-classical :-)

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:23):

(that is, it forbids something that I don’t plan to do myself, but that feels like it should be legal)

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:25):

I wonder how Infotheo manages these conundrums: https://github.com/affeldt-aist/infotheo/#license

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:28):

IANAL, but I thought that GPL-incompatibility is only problematic when you want to publish a binary?

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:29):

You can always put some GPL code that depends on a GPL-incompatible library, the only thing you don't have the right to is to compile a binary and distribute the result, or am I mistaken?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:29):

@Pierre-Marie Pédrot from https://www.gnu.org/licenses/gpl-faq.html#WhatDoesCompatMean

[GPL compatibility means] you can combine code released under the other license with code released under the GNU GPL in one larger program.

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:30):

Define "combine"

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:30):

A strict reading would prohibit you to have GPL incompatible code on the same hard drive as a GPL one

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:31):

Looking at the infotheo link, I wonder if they have a solution

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:31):

It's certainly true that some combinations are allowed

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:31):

I think "combine" comes from "combined work" which I believe has some US legal definition

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:32):

Linking [name of your program] statically or dynamically with other modules is making a combined work based on [name of your program]. Thus, the terms and conditions of the GNU General Public License cover the whole combination.

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:32):

Coq proofs are not quite programs.

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:33):

I personally have no idea what it means to "link" code in the Coq world.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:33):

I've seen people argue that "Require" counts as "dynamic linking".

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:33):

otherwise, if it counted as static linking, I think we are all screwed by Coq's LGPL license (which makes non-dynamic-linking contingent on being GPL'd or LGPL'd)

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:34):

oh sure

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:35):

but my point was that Require should count as (dynamic) linking

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:35):

but it would be surprising if there was no linking at all, e.g., would it count as using an API? This seems optimistic

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:36):

If I had to take a position, I'd believe that Requiring is the closest thing we have to dynamic link.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:36):

so, haven’t we already a plausible case that infotheo cannot be distributed?

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:37):

As a binary, most definitely.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:38):

your quote mentions dynamic linking, and if Require counts (which is plausible), we’re done.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:38):

IIRC I had found a potential fix, since CECILL licenses have clauses for relicensing and upgrading.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:39):

but exercising those clauses required sacrificing quite a few goats

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:39):

so does anyone want be the bringer of bad news and open an issue? I was honestly hoping to have infotheo in the Coq platform, but if the project itself can't be distributed as a binary, you can't put it in a Docker container and so on.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:41):

from my notes: to relicense CECILL-B software, you must add a contribution under the CeCILL-v1 license, to redistribute the whole thing under CeCILL-v1 (under CeCILL-B 5.3.5), then use CeCILL-v1 upgrade clause (12.2) to upgrade to CeCILL-v2, and finally use CeCILL-v2 5.3.4 to upgrade to GPL.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:42):

IANAL, and those clauses have some side conditions, but they _don’t_ involve “contact all contributors”

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:43):

ah, the next step in automation, auto-relicensing -- a bot will add a dummy CeCILL-v1 commit to MathComp, add redistribution/licensing boilerplate, build it, then build infotheo

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:43):

ROTFL

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:44):

this is like where all those bots make PRs, then another bot merges and another bot celebrates with a meme

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 11:44):

anyway, this is why it’d have been better to have a v2 of CECILL-B and CECILL-C

view this post on Zulip Karl Palmskog (Sep 05 2020 at 11:45):

Our future: https://twitter.com/gabro27/status/1173547934132178944

So this just happened: - a bot found a vulnerability in a dependency - a bot sent a PR to fix it - the CI verified the PR - a bot merged it - a bot celebrated the merge with a GIF https://github.com/buildo/react-components/pull/1367 https://twitter.com/gabro27/status/1173547934132178944/photo/1

- Gabriele Petronella (@gabro27)

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:46):

Dafuq.

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 11:46):

The singularity is around the corner...

view this post on Zulip Karl Palmskog (Sep 05 2020 at 12:04):

licensing issues are perhaps the top GitHub issues to report if you are a jerk who likes to appear to be clever. Not much knowledge about code required, developers will inevitably find them super-annoying, and may even have to take them really seriously. Also, relatively high chance of distracting people from getting work done and sowing uncertainty and doubt among users/developers.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 12:09):

I can already see the software engineering paper (maybe already written?): "Our technique found 2000+ potential licensing issues among popular open source projects on GitHub, which our tool duly reported as GitHub issues containing the full legal and technical background [...] responses were regrettably not positive from most project developers."

view this post on Zulip Pierre-Marie Pédrot (Sep 05 2020 at 12:11):

Legalism is a plague. As a reasonably nice citizen, I break the law literally several times per day. Am I going to be tortured for eternity in the hell of business lawyers if I mistakenly compile infotheo on my computer?

view this post on Zulip Karl Palmskog (Sep 05 2020 at 12:17):

I see it as yet another tool in the toolbox of state, law enforcement, big corporations, etc. They can go after you for these things if it becomes salient for another reason, e.g., to pressure you to sign some document.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 12:20):

my contribution to legalism is (I guess) to force/suggest that people pick some SPDX identifier, rather than writing random silly letter combinations under "license". It's not completely clear what is worse in the long run...

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 13:07):

I doubt math-comp authors would sue somebody, but a company (no matter its size) would take a risk in using such software.

view this post on Zulip Paolo Giarrusso (Sep 05 2020 at 13:10):

to be clear, I only looked into CECILL-B because of some code I was using in my academic project, not because of something I’m using industrially

view this post on Zulip Karl Palmskog (Sep 05 2020 at 13:22):

secret industry Coq project confirmed!

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 14:24):

So how about a Ph.D. thesis to formalize licenses in Coq :-)

view this post on Zulip Karl Palmskog (Sep 05 2020 at 14:33):

it's already ongoing to formalize legal documents, although copyright law may be even harder than tax code: https://twitter.com/_protz_/status/1223263479873921024

My student Denis wrote a formal semantics for the French tax code, complete with Coq proof of soundness and SMT queries to uncover unfair tax hikes. PL for fiscal justice! https://blog.merigoux.ovh/en/2019/12/20/taxes-formal-proofs.html

- Jonathan Protzenko (@_protz_)

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 14:36):

A while back I looked into Grammatical Framework - it might work quite well with Coq. Is is a parser for natural languages with (mildly) dependently typed grammars.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 14:44):

you might be already aware of the autoformalization work by Kaliszyk and Urban? For example: https://arxiv.org/abs/1912.02636

view this post on Zulip Karl Palmskog (Sep 05 2020 at 14:46):

bottom line: it doesn't work that well yet. But Szegedy at Google seemingly thinks autoformalization is the way forward (https://link.springer.com/chapter/10.1007/978-3-030-53518-6_1)

view this post on Zulip Karl Palmskog (Sep 05 2020 at 16:15):

Karl Palmskog said:

licensing issues are perhaps the top GitHub issues to report if you are a jerk who likes to appear to be clever. Not much knowledge about code required, developers will inevitably find them super-annoying, and may even have to take them really seriously. Also, relatively high chance of distracting people from getting work done and sowing uncertainty and doubt among users/developers.

if anyone was wondering, this was a sarcastic comment, and I do think licensing issues should be reported. In my opinion, the best way to avoid licensing discussions is to use and work with projects that have simple and permissive licenses, as often as possible.

view this post on Zulip Michael Soegtrop (Sep 05 2020 at 17:06):

@Karl Palmskog regarding the language processing links: I am more a fan of rigid meaning definitions with GF than of machine learning - machine learning can get it arbitrarily wrong - with GF you can clearly define what you mean with certain language constructs. Of cause GF will always lead to a rather restricted language, but it can be a reasonable subset of the language which has a well defined meaning in a given domain like software licenses.

view this post on Zulip Karl Palmskog (Sep 05 2020 at 17:55):

@Michael Soegtrop did you see Hales's summary on controlled natural languages? https://jiggerwit.wordpress.com/2019/06/20/an-argument-for-controlled-natural-languages-in-mathematics/

Sounds like something along those lines. I'm sure people have already tried at high abstraction level for licenses, e.g., all those summaries of Creative Commons licenses.

view this post on Zulip Bas Spitters (Sep 05 2020 at 19:22):

Michael Soegtrop said:

A while back I looked into Grammatical Framework - it might work quite well with Coq. Is is a parser for natural languages with (mildly) dependently typed grammars.

GF came out of the early work in agda and logical frameworks. So, indeed it is not far from Coq.

view this post on Zulip Bas Spitters (Sep 05 2020 at 19:33):

About CNL, the declarative mode in Coq was recently removed IIRC
https://link.springer.com/chapter/10.1007/978-3-540-68103-8_5

Here's the connection between GF and agda/alfa
https://cth.altocumulus.org/~hallgren/Alfa/Tutorial/GFplugin.html

view this post on Zulip Michael Soegtrop (Sep 19 2020 at 17:58):

@Karl Palmskog , @Théo Zimmermann : the majority of the work of the Coq platform is fixing opam packages - the scripts are not a big deal. I also do not want to hinder e.g. teachers in creating platform variants together with packages which have an uncommon license. In the end it is not enough code to really worry about it. As I said, 90% of the effort is writing opam patches.

Reagrding the binary installer: the expressed opinion of the FSF is that the CECILL-B and CECILL-C licenses are incompatible with any variant of GPL license, which means they are incompatible with the Coq standard library. As I read this one can't distribute Mathcomp and Coq-interval with the Coq standar dlibrary in binary form. Also as I read this .vo files are technically similar to object files and it is obvious that e.g. the matchcomp .vo files are statically linked to the coq standard library.

I think the easiest solution would be if Mathcomp and Coq-Interval would change their license to the respective GPL license they are a variant of. If this cannot be done, one has to study the license conditions very carefully.It might be OK as long as we do not change anything in MathComp or Coq-Interval - that is only deliver plain absolutely unmodified tags, but I am not sure if this is sufficient. An interesting question is e.g. if a delivery containing both source and binary is a source or a binary delivery in terms of the GPL.

All I am saying is that these things need to be clarified before we do a binary release and it might actually get a bit tricky.

Of cause I can delay any annoucement until we have discussed this.

view this post on Zulip Karl Palmskog (Sep 19 2020 at 18:54):

that distributing binaries where there is dynamic linking between LGPL and non-LGPL parts leads to problems whenever the non-LGPL parts are GPL-incompatible would be complete news to me

view this post on Zulip Karl Palmskog (Sep 19 2020 at 18:56):

the reason there are problems with distributing binaries for Infotheo (GPL-licensed) with MathComp (CECILL-B) is at least clear, since GPL needs everything to be GPL-compatible all the time. But LGPL as well? This would make LGPL and GPL observationally equal in my view.

view this post on Zulip Enrico Tassi (Sep 19 2020 at 20:33):

https://cecill.info/licences.fr.html says GPL is compatible with Cecill-*
Do you have a pointer?

view this post on Zulip Enrico Tassi (Sep 19 2020 at 20:42):

Coq and the stdlib are LGPL, which do not require derivative works to be under the same license. I mean, Coq could be linked in a proprietary software. I'm pretty sure it can be put in a bundle with Cecille licensed software, how is the platform different from Debian, Ubuntu, RHL... (I know nothing about Compcert, I'm only concerned about mathcomp).

view this post on Zulip Karl Palmskog (Sep 19 2020 at 20:56):

@Enrico Tassi CECILL (without "-B" or "-C"), version 2, is indeed compatible with GPL explicitly, but to my knowledge no Coq project uses CECILL v2. "-B" and "-C" are claimed by FSF to not be compatible with GPL: https://www.gnu.org/licenses/license-list.en.html#CeCILL-B

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:00):

Paolo came up with a rather ingenious way to convert any CECILL-B or CECILL-C project to GPL without changing the project upstream, but it requires actually changing the project locally: https://coq.zulipchat.com/#narrow/stream/237663-coq-community-devs.20.26.20users/topic/CECILL.20licenses.20and.20%28L%29GPL.20compatibility/near/209174197

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:01):

I think we rather definitively established that using this conversion path is the only way one could legitimately co-distribute MathComp with Infotheo as .vo files (the latter is GPL-3)

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:05):

but bottom line for the projects originally discussed, my analysis disagrees with Michael's: I believe there is no obstacle to co-distribute .vo files for Coq Stdlib (LGPL) and MathComp-* (CECILL-C or CECILL-B)

view this post on Zulip Enrico Tassi (Sep 19 2020 at 21:30):

I'm sure all math comp devs would be happy to ease the distribution of MC if there was a real need by bumping the license. I'm not a big fan of cecill, but the incompatibility argument of GNU (you said FSF, not exactly the same thing) is, hem, not very fundamental and reasonably easy to comply to. 5.3.4 is essentially requiring to credit the original authors and put some stuff online. In these cases I suggest we do a reality check: did anyone claim this incompatibility in a court (because a website does not really count as a source of legislation, in any law systems I've heard of)? Also, would an entity ever start a lawsuit to obtain some credits to be put online (if they are not yet)? Lawsuits are for money, if there are no money to gain and no software to "free" (this is not my opinion, is what real lawyers told a bunch of Debian people worried of distributing software with problematic licenses).

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:33):

basically, Paolo's conversion path ("-B or -C" to full GPL) is something that could be done by anyone, at any time, from any revision of MathComp.

I think most people consider FSF to be the ultimate authority on what is compatible with GPL or not (they have some very experienced copyright lawyers on staff). But probably, -B/-C vs. GPL has not been tested in court.

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:36):

I'd be willing to take a bet that the Debian legal team will go with FSF's interpretation of CECILL-B/CECILL-C compatibility with GPL. Hence, they would not want to package MathComp together with Infotheo. So we are basically discussing and operating in the shadow of the law, regardless of what the law says.

view this post on Zulip Karl Palmskog (Sep 19 2020 at 21:40):

regarding "GNU says" vs. "FSF says":

This page is maintained by the Free Software Foundation's Licensing and Compliance Lab.

view this post on Zulip Michael Soegtrop (Sep 19 2020 at 21:47):

The whole license stuff is indeed quite annoying - in the end it is all source and nobody wants to take any rights of anybody and still we are having issues.

My summary line: I haven't though this through (had to many technical issues up to now) and before we do a binary release we have to think this through and document the rationale.

I think worst case we have the option to deliver certain pieces as source and compile them on the machine of the user if needed.

view this post on Zulip Théo Zimmermann (Sep 20 2020 at 09:46):

The whole relicensing plan of @Paolo Giarrusso is way over complicated. CeCILL is one of these licenses which has an "or-later" clause by default:

12.3 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.

You don't have to modify the software to distribute it under the new version of CeCILL which is compatible with the GPL. Furthermore, you don't have to go further than this. GPL-compatibility is GPL-compatibility. Why would you ever need to relicense to the (L)GPL itself?
And yes, if that helps we could ask the math-comp maintainers themselves to upgrade the license version in the repository.

EDIT: no in fact, he was right, because only the main (GPL-like) CeCILL license has a v2 version.

view this post on Zulip Théo Zimmermann (Sep 20 2020 at 09:47):

Anyway, I agree that certain questions may need to be clarified but I'd like to avoid any public announcement that because of these questions we might never provide a binary installer for the platform.

view this post on Zulip Théo Zimmermann (Sep 20 2020 at 09:48):

Furthermore, it's not like these questions do not already apply to the Windows installer. So it would be pretty inconsistent to announce this, and release 8.12.1 with the usual Windows installer with add-ons just a few days later.

view this post on Zulip Michael Soegtrop (Sep 20 2020 at 16:27):

@Théo Zimmermann : OK, I will remove this message and just say "we are working on it".

Regarding the licensing stuff I suggest the following:

I would appreciate it if someone could help with the first two points above.

view this post on Zulip Michael Soegtrop (Sep 20 2020 at 16:40):

@Théo Zimmermann : I adjusted the ReadMe and also changed the beta1 tag to the new commit. Can you please check if this is OK now?

view this post on Zulip Théo Zimmermann (Sep 20 2020 at 20:25):

@Michael Soegtrop You haven't yet removed or adjusted the sentence "It is not yet decided if also Windows and Mac installers will be created. The main issue here is not technical but some unresolved questions on license compatibility of binary distributions." from the release notes (https://github.com/coq/platform/releases/tag/v8.12.0%2Bbeta1). Did you intend to do this as well?

view this post on Zulip Michael Soegtrop (Sep 20 2020 at 21:24):

@Théo Zimmermann : ah yes sorry - I thought you meant the similar comment in the ReadMe. I now also adjusted the release text.

view this post on Zulip Enrico Tassi (Sep 23 2020 at 09:13):

Théo Zimmermann said:

The whole relicensing plan of Paolo Giarrusso is way over complicated. CeCILL is one of these licenses which has an "or-later" clause by default:

12.3 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.

You don't have to modify the software to distribute it under the new version of CeCILL which is compatible with the GPL. Furthermore, you don't have to go further than this. GPL-compatibility is GPL-compatibility. Why would you ever need to relicense to the (L)GPL itself?
And yes, if that helps we could ask the math-comp maintainers themselves to upgrade the license version in the repository.

I did bring up the topic at the MathComp meeting, but we did not even discuss it, because MC is under CeCILL-B (which is not CeCILL) and there is no version 2 of CeCILL-B. CeCILL-B is BSD-like, while CeCILL is GPL-like. For sure I can't upgrade CeCILL-B to v2 because there is no such a thing, and we are not "upgrading" a BSD license to a GPL one. I'm lost in this conversation.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 09:44):

Thanks for the feedback and sorry for the confusion then. I'll look into it more closely.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 09:51):

Enrico Tassi said:

https://cecill.info/licences.fr.html says GPL is compatible with Cecill-*

In fact, this claim is only made for the main (CeCILL v2) license, so this is consistent with the info on the FSF website.

view this post on Zulip Notification Bot (Sep 23 2020 at 09:57):

This topic was moved here from #coq-community devs & users > CECILL licenses and (L)GPL compatibility by Théo Zimmermann

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:12):

So I tried to read everything again and I have to agree that the situation is seriously messed up.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:19):

Regarding the CeCILL-B / GPL incompatibility which affects infotheo, the simplest solution to me would be a relicensing of infotheo. If the authors are few enough they can decide the relicensing together to any license. If they really wish to keep the strong copyleft aspect they could relicense to CeCILL v2 (which is compatible with math-comp's license and also with the GPL). But relicensing to a permissive license would be even better.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:20):

[Off-topic]: We should really discuss if we wish to include strong-copyleft-licensed libraries in the platform.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:23):

Regarding whether math-comp license would be incompatible with stdlib's license LGPL v2.1 and whether Require counts as dynamic linking or not: LGPL does not mandate dynamic linking and basically the dynamic linking clause does not apply if you provide the source code for everything. So no, I really don't think there are any issues with math-comp + stdlib binary distribution.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:27):

Finally, I am really surprised that the concerns raised by the FSF regarding the GPL-incompatibility of CeCILL-B and -C and the fact that these licenses were never OSI-approved did not concern the French institutions that created this family of licenses enough to publish a new version for those as well.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:27):

Maybe someone should write to Inria management about this...

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:30):

Oh but in fact, that's interesting: CeCILL-B and -C were published at the same date as CeCILL v2 (in 2006). Why were there never OSI-approved, I have no idea.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 10:37):

@Théo Zimmermann so you’re also wishing for a V2 of the B and C variants? Thanks for confirming

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 10:47):

Yes, despite all the trouble that the FSF has created for everyone, CeCILL arrived much later and only added to the mess. FSF is the leading authority regarding GPL-compatibility and GPL is the historic and most used copyleft license, so also the license every other free software license should be compatible with. It would really be a shame if Inria and its partners did not fix the mess they made despite having the power. But the fact that there was no release for the last 14 years (despite the FSF note which probably is quite ancient) does not give me high hopes.

view this post on Zulip Enrico Tassi (Sep 23 2020 at 11:29):

The legit part of considering writing a new GPL license is that the big fat warning "this comes as is, your problem" is not really valid in Europe, IIRC. You can't give someone a drink of yours, tell him "use at your own risk", and be clean if the drink was poison. So that clause is not valid. From this to going the full distance of writing another license is another story, and doing it without chatting with FSF enough to make it compatible, well, it's as silly as it sounds.

Anyway, I take the massage that MC wise, licensing is not problematic for the platform.

@Paolo Giarrusso what @Théo Zimmermann suggests, is that the -B variant is already as good as a V2 (well, there was no V1, but since its only version was released at the same time of the v2, it is likely not to contain any problematic section).

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 11:40):

Agreed that it's legit. Too bad they didn't talk with the FSF first indeed.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 11:41):

But I'm not saying that the -B variant doesn't contain the problematic section, the description of the FSF regarding this problematic section is precisely about the -B and -C variants.

view this post on Zulip Karl Palmskog (Sep 23 2020 at 11:43):

@Enrico Tassi what might be appropriate from the MathComp side: add a big fat warning somewhere in the documentation not to license a project that uses MathComp under the GPL - even if it hasn't been established in court that "-B" is incompatible with GPL, that FSF says it's incompatible should scare everyone away from using MC+GPL nevertheless

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 11:46):

@Enrico Tassi If you happen to be willing to track down all copyright owners, a relicensing of math-comp under "your choice of CeCILL-B or BSD3" or whatever permissive license you wish (BSD3 is just the most similar) would be great for the ecosystem.

view this post on Zulip Enrico Tassi (Sep 23 2020 at 12:07):

Hum, the problem is that the copyright owners are Microsoft and Inria. In particular that license was picked at the time of the join lab.

I guess I'll go for the warning with a pointer to https://www.gnu.org/licenses/gpl-faq.html#GPLIncompatibleLibs (btw you can use GPL, but you have to write down an exception).

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 12:36):

Karl Palmskog said:

I'd be willing to take a bet that the Debian legal team will go with FSF's interpretation of CECILL-B/CECILL-C compatibility with GPL. Hence, they would not want to package MathComp together with Infotheo. So we are basically discussing and operating in the shadow of the law, regardless of what the law says.

It's worse than this. They seem to consider that CeCILL-B is not a free software license, so this would jeopardize any packaging attempt of the platform into Debian (see https://github.com/coq/coq/issues/9281), although it was already discussed at the time that there is a trivial upgrade path (to CeCILL-C) that allows to get rid of this clause (see the e-mail sent to the mailing list by the author of this issue).

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 13:50):

And to clarify: I wasn’t wishing for a GPL-ed math-comp, and my “license hack” wasn’t meant as a good idea, and I’d hope something simpler is possible.

view this post on Zulip Paolo Giarrusso (Sep 23 2020 at 13:52):

But if the CeCILL authors acknowledged FSF’s concerns enough to create a CeCILL-V2, it’s even more unfortunate that -B and -C don’t have compatibility clauses.

view this post on Zulip Enrico Tassi (Sep 23 2020 at 14:34):

Théo Zimmermann said:

It's worse than this. They seem to consider that CeCILL-B is not a free software license, so this would jeopardize any packaging attempt of the platform into Debian (see https://github.com/coq/coq/issues/9281), although it was already discussed at the time that there is a trivial upgrade path (to CeCILL-C) that allows to get rid of this clause (see the e-mail sent to the mailing list by the author of this issue).

This time you are stretching it too much. What the FSF qualifies as free software (or GPL compatible) is not what Debian considers as free (that is DFSG). As I wrote in the issue there, Debian accepted CeCILL-B software before. The license has been considered DFSG compliant by the authoritative Debian team (which is not the debian-legal mailing list: there is no professional lawyer on debian-legal, just in case you were mislead by the name of the list, it's just a place where certain discussions start and hopefully where they stay...).

What the GPL incompatibility may prevent is to package and redistribute infoteo without having its license to be amended (via an exception, or by adding to the GPL the funny redistribution "via a website" clause that is in CeCILLE). In that respect I see the relevance for the platform. Also changing MC license would fix that, but I'm afraid it is not the easiest of options.

The email sent by Benjamin to debian-legal got no answer. He proposed the upgrade path, but nobody acknowledged it was possible AFAICT.

view this post on Zulip Karl Palmskog (Sep 23 2020 at 14:38):

for extra clarity, Infotheo is currently not even a candidate to join the Platform (although I personally would like for it to join, if legal issues can be resolved). My main use of it was to illustrate potential legal issues the platform could be subject to as it grows.

view this post on Zulip Théo Zimmermann (Sep 23 2020 at 15:20):

Thanks for clarifying that it is considered DFSG compliant. FSF does make the distinction between free and GPL compatible, but I wasn't talking about this.

view this post on Zulip Reynald Affeldt (Oct 08 2020 at 02:28):

I am one of the authors of infotheo which is mentioned as part of the problem but I actually missed most of this conversation. I have now contacted the other authors to inform them and to look for a solution.

view this post on Zulip Reynald Affeldt (Oct 08 2020 at 02:29):

(It looks like I was not "subscribed" to the stream actually. I am not sure what it means but that would maybe explained why I did not see the conversation.)

view this post on Zulip Reynald Affeldt (Oct 13 2020 at 13:53):

affeldt-aist said:

I am one of the authors of infotheo which is mentioned as part of the problem but I actually missed most of this conversation. I have now contacted the other authors to inform them and to look for a solution.

fwiiw, we agreed on relicensing to LGPL

view this post on Zulip Bas Spitters (Oct 13 2020 at 14:00):

MIT or MPL 2 is recommended over LGPL:
https://github.com/coq-community/manifesto

view this post on Zulip Reynald Affeldt (Oct 13 2020 at 14:02):

(yes, I did see that, still...)

view this post on Zulip Bas Spitters (Oct 13 2020 at 14:08):

I missed the discussion. Do you disagree, or was LGPL the best compromise?

view this post on Zulip Reynald Affeldt (Oct 13 2020 at 14:12):

Maybe the latter (I am not the only ingredient in the decision process). No disagreement with the manifesto anyway.

view this post on Zulip Karl Palmskog (Oct 13 2020 at 16:01):

at least we are near-100% LGPL is GPL-compatible, and quite-near-100% it can be distributed together in binary form with CECILL-B/C, so altogether a big improvement!


Last updated: Jan 29 2023 at 19:02 UTC