Karl Palmskog (Nov 09 2022 at 11:54): Karl Palmskog (Nov 09 2022 at 11:54):Is it possible to:
.vo files) under some open source license?I can't think of an obvious way, due to the CECILL-B/C GPL incompatibility.
Théo Zimmermann (Nov 09 2022 at 14:02):From the top of my head, a strategy would be to distribute the result under GPL-3.0 (possibly GPL-2.0 would be also fine). IIRC CeCILL-B and CeCILL-C allow relicensing to CeCILL (and I think this includes "future versions"), CeCILL allows relicensing to GPL (probably 2.0 is fine) and LGPL 2.1 allows relicensing to GPL 2.0 or 3.0. There might be legal subtleties such as requiring a fourth component that is already under GPL to trigger the various "to GPL" clauses.
Michael Soegtrop (Nov 09 2022 at 14:04):In case the LGPL-2.1 software is copyrighted by an institution (rather than by a possibly unknown set of individuals), you can still go with this section of the LGPL-2.1:
- If you wish to incorporate parts of the Library into other free programs whose distribution conditions are incompatible with these, write to the author to ask for permission. For software which is copyrighted by the Free Software Foundation, write to the Free Software Foundation; we sometimes make exceptions for this. Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally.
An official statement from INRIA that all software published by INRIA under LGPL 2.1 is compatible with the various forms of CECILL - which I guess is the intention of INRIA - would probably help.
Another thing one should do is to ask the FSF what the rules are for software which is distributed in source form and where distributing binaries is just a means to save user time and CO2. I think we take quite a bit if effort to make it easy to compile from sources - especially looking at opam as meta build system and Coq Platform as user friendly wrapper around it. I think the FSF might come to different judgments of what is license wise compatible in case a meta build system exists.
Karl Palmskog (Nov 09 2022 at 14:08):ah, so I guess the relicensing-of-CECILL-B-C path might actually work out, but we seemingly can't use CECILL for the end product
Karl Palmskog (Nov 09 2022 at 14:09):@Michael Soegtrop but isn't this a generic clause that applies to nearly every copyrightable work? If you can track down copyright holders, you can ask for permissions beyond the current license.
Théo Zimmermann (Nov 09 2022 at 14:13):Just FTR, just because software is published by Inria does not mean that Inria has the copyright over all of it. Also, I think assuming Inria has "intentions" is far-stretching things. There is no and never was a general licensing strategy at Inria. Certainly, a beginning of strategy must have existed when they decided to create the CeCILL license, but it obviously died since then.
Karl Palmskog (Nov 09 2022 at 14:15):there was no Inria connection in my question, it was more about understanding some consequences of Coq ecosystem licenses
Théo Zimmermann (Nov 09 2022 at 15:05):Yes, I was answering Michael's suggestions here.
Karl Palmskog (Nov 09 2022 at 15:07):sure, but just wanted to clarify if someone reading the whole thread was thinking this
Michael Soegtrop (Nov 09 2022 at 16:13):@Karl Palmskog : The interesting point is that the FSF says: "if you have issues, talk to us". So it might not be out of the question that something generic around GPL/LGPL and CECILL can be negotiated with the FSF in case there are special conditions like opam. At least one can try.
Théo Zimmermann (Nov 09 2022 at 16:26):No, you are just misunderstanding why they put this clause.
Théo Zimmermann (Nov 09 2022 at 16:26):They say this because the GNU (L)GPL was initially written for programs owned by the FSF.
Théo Zimmermann (Nov 09 2022 at 16:27):So they have clauses like this, but they have no power whatsoever to negotiate anything over code that doesn't belong to them.
Paolo Giarrusso (Nov 09 2022 at 17:35):Why exactly would LGPL object to CeCILL here, any more than it'd object to proprietary software? It seems the user retains their right to patch the LGPL code and build the new product, since you're distributing sources and build scripts
Paolo Giarrusso (Nov 09 2022 at 17:36):IIRC, that's also relevant to @Michael Soegtrop 's question on source/binary distribution: "can the user still patch the LGPL library" is the key test, and "distributing sources" or "dynamic linking" are technical means to that end
Paolo Giarrusso (Nov 09 2022 at 17:39):okay, I guess @Karl Palmskog 's point is that the integration is deep enough that the CeCILL-B/CeCILL-C code is now a derivative work? that seems much stronger than "they all depend on each other"
Paolo Giarrusso (Nov 09 2022 at 17:48):IOW, if we only "assume all three now depend on each other", the non-LGPL code should still be a "work that uses the Library" (LGPL2.1 Sec. 5), so you still get to use LGPL's relaxed rules instead of the GPL ones:
A program that contains no derivative of any portion of the Library, but is designed to work with the Library by being compiled or linked with it, is called a "work that uses the Library".
Karl Palmskog (Nov 09 2022 at 17:52):I was assuming nontrivial changes to the LGPL library to make it use the CECILL library in some way, for example. So it wasn't purely just an unmodified "L" anymore
Karl Palmskog (Nov 09 2022 at 17:56):I think then you have to drop the L part of the license and go full GPL with it, so you get something-with-GPL that integrates with CECILL-B/C
Paolo Giarrusso (Nov 09 2022 at 18:00):I suspect that's oversimplified; clause 2 and 2d allows sticking to LGPL under some conditions.
Paolo Giarrusso (Nov 09 2022 at 18:09):If I Understand Correctly (but I Am Not A Laywer), adding dependencies is allowed, adding _artificial_ dependencies unrelated to functions isn't. Here's a summary from law professor Eben Moglen:
Section 2 continues to require, as LGPLv2.1 §2(d) required, that the Library not be modified to require keys, tokens, tables, or other global non-argument data unrelated to function. This is again stated as a “good faith effort” requirement, but failure to cure on notice is strong evidence of the absence of good faith. Use of GPLv3 terms by removal of the additional permission, as provided for by GPLv3 §7, is the alternate path to compliance.
https://softwarefreedom.org/resources/2014/SFLC-Guide_to_GPL_Compliance_2d_ed.html
Paolo Giarrusso (Nov 09 2022 at 18:11):(and Eben Moglen was FSF general counsel)
Paolo Giarrusso (Nov 09 2022 at 18:16):OTOH, applying clause 2d seems pretty subtle.
Michael Soegtrop (Nov 09 2022 at 18:32):Théo Zimmermann said:
So they have clauses like this, but they have no power whatsoever to negotiate anything over code that doesn't belong to them.
This is not entirely true because the statements of the FSF on what licenses are compatible with FSF licenses are usually taken as definitive and such statements do have a substantial impact on any software using FSF licenses, not only the software of the owned by the FSF.
My point is that these compatibility matrices are done under most general circumstances taking nothing than the legal text of the licenses. Now my question is what happens if one scrutinises the legal text of the licenses with additional hypothesis, say that the software is developed as an open source project or that the software is not about executables but math.
Think if it this way: assume you have a formalisation of all the licenses in Coq. Now you try to prove that certain licenses are compatible and fail. Then you try to prove the same thing but with additional hypothesis about the projects at hand. I think it is quite obvious that the result is not necessarily the same.
I cited this text mostly to point out that the goal of the FSF is to foster open source software and not to be a pain in the *** of researchers who publish their stuff on github anyway and got to quite some length to make it easy to compile. And if the FSF says that they are willing to make exceptions for their own software if it is for the general good of open source SW, it might well be that they are willing to discuss their compatibility judgments with additional conditions on the projects.
Last updated: Dec 07 2023 at 04:02 UTC