Paolo Giarrusso (Sep 05 2020 at 11:07): 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
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.
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)
Karl Palmskog (Sep 05 2020 at 11:10):https://www.gnu.org/licenses/license-list.en.html#CeCILL-B (and CECILL-C just below)
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?
Paolo Giarrusso (Sep 05 2020 at 11:14):for the main CECILL license, this was fixed by releasing an update
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.
Paolo Giarrusso (Sep 05 2020 at 11:16):so what is forbidden by the incompatibility?
Paolo Giarrusso (Sep 05 2020 at 11:16):and why did CECILL people not release updates to CECILL-B and -C?
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).
Paolo Giarrusso (Sep 05 2020 at 11:18):but also if I just want my project to be GPL-compatible
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.
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.
Paolo Giarrusso (Sep 05 2020 at 11:22):fair enough, I guess — to me “GPL-incompatible” is a bit like anti-classical :-)
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)
Karl Palmskog (Sep 05 2020 at 11:25):I wonder how Infotheo manages these conundrums: https://github.com/affeldt-aist/infotheo/#license
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?
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?
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.
Pierre-Marie Pédrot (Sep 05 2020 at 11:30):Define "combine"
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
Paolo Giarrusso (Sep 05 2020 at 11:31):Looking at the infotheo link, I wonder if they have a solution
Paolo Giarrusso (Sep 05 2020 at 11:31):It's certainly true that some combinations are allowed
Karl Palmskog (Sep 05 2020 at 11:31):I think "combine" comes from "combined work" which I believe has some US legal definition
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.
Pierre-Marie Pédrot (Sep 05 2020 at 11:32):Coq proofs are not quite programs.
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.
Paolo Giarrusso (Sep 05 2020 at 11:33):I've seen people argue that "Require" counts as "dynamic linking".
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)
Paolo Giarrusso (Sep 05 2020 at 11:34):oh sure
Paolo Giarrusso (Sep 05 2020 at 11:35):but my point was that Require should count as (dynamic) linking
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
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.
Paolo Giarrusso (Sep 05 2020 at 11:36):so, haven’t we already a plausible case that infotheo cannot be distributed?
Pierre-Marie Pédrot (Sep 05 2020 at 11:37):As a binary, most definitely.
Paolo Giarrusso (Sep 05 2020 at 11:38):your quote mentions dynamic linking, and if Require counts (which is plausible), we’re done.
Paolo Giarrusso (Sep 05 2020 at 11:38):IIRC I had found a potential fix, since CECILL licenses have clauses for relicensing and upgrading.
Paolo Giarrusso (Sep 05 2020 at 11:39):but exercising those clauses required sacrificing quite a few goats
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.
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.
Paolo Giarrusso (Sep 05 2020 at 11:42):IANAL, and those clauses have some side conditions, but they _don’t_ involve “contact all contributors”
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
Paolo Giarrusso (Sep 05 2020 at 11:43):ROTFL
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
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
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)
Pierre-Marie Pédrot (Sep 05 2020 at 11:46):Dafuq.
Pierre-Marie Pédrot (Sep 05 2020 at 11:46):The singularity is around the corner...
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.
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."
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?
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.
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...
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.
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
Karl Palmskog (Sep 05 2020 at 13:22):secret industry Coq project confirmed!
Michael Soegtrop (Sep 05 2020 at 14:24):So how about a Ph.D. thesis to formalize licenses in Coq :-)
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_) 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.
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
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)
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.
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.
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.
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.
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
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.
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
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.
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?
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).
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
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
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)
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)
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).
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.
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.
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.
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.
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.
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.
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.
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.
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?
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?
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.
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.
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.
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.
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
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.
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.
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.
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.
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.
Théo Zimmermann (Sep 23 2020 at 10:27):Maybe someone should write to Inria management about this...
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.
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
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.
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).
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.
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.
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
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.
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).
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).
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.
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.
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.
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.
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.
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.
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.)
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
Bas Spitters (Oct 13 2020 at 14:00):MIT or MPL 2 is recommended over LGPL:
https://github.com/coq-community/manifesto
Reynald Affeldt (Oct 13 2020 at 14:02):(yes, I did see that, still...)
Bas Spitters (Oct 13 2020 at 14:08):I missed the discussion. Do you disagree, or was LGPL the best compromise?
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.
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: Jun 05 2023 at 10:01 UTC