Julien Puydt (Dec 15 2021 at 07:41): Julien Puydt (Dec 15 2021 at 07:41):Though understanding the licensing might prove difficule, as the LICENSE file is a little unclear.
Karl Palmskog (Dec 15 2021 at 08:46):to my knowledge one can license the whole library under GPL-3.0, but parts are dual licensed. The test cases were derived from real code under various licenses, but we believe the fragments are so small they fall under fair use, and the test cases are anyway not installed together with the library.
Emilio Jesús Gallego Arias (Dec 15 2021 at 23:34):@Julien Puydt please file a bug with the problems, we'll address them ASAP
Karl Palmskog (May 26 2022 at 12:16):@Emilio Jesús Gallego Arias regarding SerAPI licensing, please consider using LGPL of some form consistently. We already have a lot of problems with regular GPL in other projects due to its incompatibility with CECILL-B and CECILL-C.
Karl Palmskog (May 26 2022 at 12:17):Théo recently spelled out some of the issues here: https://github.com/coq-community/apery/issues/10
Emilio Jesús Gallego Arias (May 26 2022 at 12:25):Thanks @Karl Palmskog , I do have a constraint tho, I'd like a license that doesn't allow closed-source software making derivatives of my own
Emilio Jesús Gallego Arias (May 26 2022 at 12:25):So LGPL is not an option for me
Karl Palmskog (May 26 2022 at 12:46):if you do full GPL (or full copyleft), then you also don't permit people with permissive open source licenses to use your software
Emilio Jesús Gallego Arias (May 26 2022 at 12:55):That's fine to me
Emilio Jesús Gallego Arias (May 26 2022 at 12:56):Otherwise they could just make software closed
Emilio Jesús Gallego Arias (May 26 2022 at 12:57):I guess by users you mean people making derivative software
Emilio Jesús Gallego Arias (May 26 2022 at 12:57):as indeed GPL places no restriction on use
Emilio Jesús Gallego Arias (May 26 2022 at 12:57):otherwise it wouldn't be a free license
Emilio Jesús Gallego Arias (May 26 2022 at 12:57):But my software is scientific software, so derivatives must be open source too
Karl Palmskog (May 26 2022 at 13:11):let's be clear that nobody who uses a permissive, open source license will change their license just to be able to link against SerAPI. So full copyleft everywhere in SerAPI means no such projects in the Coq ecosystem can directly use (link with) SerAPI.
Emilio Jesús Gallego Arias (May 26 2022 at 13:12):Ok that's fine
Emilio Jesús Gallego Arias (May 26 2022 at 13:13):they can't already do it
Emilio Jesús Gallego Arias (May 26 2022 at 13:13):even if my licensing is messed up, it was never the intention serapi was lgpl
Karl Palmskog (May 26 2022 at 13:14):but it sounds like you don't really want an open souce or free software license at all. It's trivial to set up a domain socket or similar and communicate with sertop or similar, even for closed-source software.
Karl Palmskog (May 26 2022 at 13:14):how is this not: "software using your software"?
Théo Zimmermann (May 26 2022 at 13:16):Karl Palmskog said:
Emilio Jesús Gallego Arias regarding SerAPI licensing, please consider using LGPL of some form consistently. We already have a lot of problems with regular GPL in other projects due to its incompatibility with CECILL-B and CECILL-C.
With respect to the incompatibilities with GPL of CeCILL-B and C, I think that the problems also exist and are exactly the same with LGPL.
Théo Zimmermann (May 26 2022 at 13:17):IMHO GPL being the default strong copyleft license in the wild, it's not the problem of the authors using it that some people are using incompatible licenses.
Karl Palmskog (May 26 2022 at 13:17):how can a CECILL-C project linking with a LGPL project be a problem?
Théo Zimmermann (May 26 2022 at 13:17):Oh, there's no problem with linking obviously.
Karl Palmskog (May 26 2022 at 13:18):right, and our whole discussion here is about who should be able to link, at least in my view
Emilio Jesús Gallego Arias (May 26 2022 at 14:00):I'm fine with people using the software as they want
Emilio Jesús Gallego Arias (May 26 2022 at 14:01):But if they modify it, or build derivative products, I want them to provide the same rights I provided to them to their users
Emilio Jesús Gallego Arias (May 26 2022 at 14:01):Linking is not derivative
Emilio Jesús Gallego Arias (May 26 2022 at 14:01):I will look into Cecill vs GPL problems, but I guess the solution is to dual-license
Emilio Jesús Gallego Arias (May 26 2022 at 14:02):Anyways for SerAPI the issue is moot, as it will hopefully upstreamed to Coq almost in full
Emilio Jesús Gallego Arias (May 26 2022 at 14:02):but for other softwares we are developing that's relevant
Emilio Jesús Gallego Arias (May 26 2022 at 14:03):Karl Palmskog said:
how is this not: "software using your software"?
This is software using my software and it is totally fine the user is not open source, as the GPL clearly states
Emilio Jesús Gallego Arias (May 26 2022 at 14:03):And I'm OK with that
Emilio Jesús Gallego Arias (May 26 2022 at 14:04):Oh I see I wrote "using", sorry that was a big typo
Emilio Jesús Gallego Arias (May 26 2022 at 14:04):corrected in my original post
Emilio Jesús Gallego Arias (May 26 2022 at 14:04):I meant using as in making derivate products
Karl Palmskog (May 26 2022 at 14:11):if the plan is to upstream most of it, great. But until then, with full-GPL-everywhere, linking with serlib or anything else from the coq-serapi repo in OCaml will automatically force GPL on the linking library - I would express this as: GPL considers mere linking as derivative.
Emilio Jesús Gallego Arias (May 26 2022 at 14:13):Karl Palmskog said:
if the plan is to upstream most of it, great. But until then, with full-GPL-everywhere, linking with serlib or anything else from the
coq-serapirepo in OCaml will automatically force GPL on the linking library - I would express this as: GPL considers mere linking as derivative.
Reading the license file I don't see full GPL everywhere, what is the problematic point?
Where does the GPL use the word linking?
Karl Palmskog (May 26 2022 at 14:14):GPL doesn't use linking, so this means everything linking to a GPL'd library is considered a derivative work. LGPL to me is about excepting mere linking from forming a derivative work
Karl Palmskog (May 26 2022 at 14:16):Reading the license file I don't see full GPL everywhere, what is the problematic point?
But you want to make the licensing consistent, right? Now, it's mix of some parts being GPL, some not-precisely-defined stuff being also under LGPL
Emilio Jesús Gallego Arias (May 26 2022 at 14:17):Karl Palmskog said:
GPL doesn't use linking, so this means everything linking to a GPL'd library is considered a derivative work. LGPL to me is about excepting mere linking from forming a derivative work
How does it mean that, if the word linking doesn't even appear in the license?
"linking" is a very technical term, not a legal term
Emilio Jesús Gallego Arias (May 26 2022 at 14:17):that's the reason it is not used in GPL 3
Emilio Jesús Gallego Arias (May 26 2022 at 14:17):Karl Palmskog said:
Reading the license file I don't see full GPL everywhere, what is the problematic point?
But you want to make the licensing consistent, right? Now, it's mix of some parts being GPL, some not-precisely-defined stuff being also under LGPL
What's unprecise in the LICENSE file?
Karl Palmskog (May 26 2022 at 14:18):example, what does the LGPL here extend to: https://github.com/ejgallego/coq-serapi/blob/v8.15/LICENSE#L5
Emilio Jesús Gallego Arias (May 26 2022 at 14:18):If I understood the format correctly, to everything not covered by Files:
Karl Palmskog (May 26 2022 at 14:20):if GPL did not extend over any kind of linking, why would there be a need for something like the GPL linking exception? The LGPL license singles out linking because it's a very common form of reuse.
Emilio Jesús Gallego Arias (May 26 2022 at 14:24):@Karl Palmskog that's a hotly debated topic actually, but not very interesting to me. Ultimately, the license talks about derivative works, and only a jurisprudence can establish what that means in practice.
Emilio Jesús Gallego Arias (May 26 2022 at 14:25):Indeed, the origins of the linking exception was to reassure people that linking would be fine.
Emilio Jesús Gallego Arias (May 26 2022 at 14:26):Given the current state of PL tech, what linking means is very confusing, so I prefer for my own projects the notion of derivative work
Emilio Jesús Gallego Arias (May 26 2022 at 14:26):for example, using the derivers in SerAPI to build your own derivers, is a derived work I think
Emilio Jesús Gallego Arias (May 26 2022 at 14:27):if you link but actually you are just using the public API, I don't see how that's wrong
Emilio Jesús Gallego Arias (May 26 2022 at 14:27):Again that only can be decided in court
Karl Palmskog (May 26 2022 at 14:27):but maybe we can then agree that most people will consider mere linking against GPL'd libraries (e.g., in OCaml) as forming a derivative work?
Karl Palmskog (May 26 2022 at 14:28):or in any case, they consider the current state of legal analysis to point towards this
Emilio Jesús Gallego Arias (May 26 2022 at 14:29):I don't know what people may consider
Emilio Jesús Gallego Arias (May 26 2022 at 14:30):that's up to them and their legal team
Emilio Jesús Gallego Arias (May 26 2022 at 14:30):I guess if they have a reason to try to do closed source using research open source software, they got a legal team too
Emilio Jesús Gallego Arias (May 26 2022 at 14:37):For me the intention of the license is very clear (which actually, author intent has a lot of weight on court)
"If you wanna modify or make a derivate of this research software, you gotta release the code"
GPL is a tested, good approximation, while not perfect of course
Emilio Jesús Gallego Arias (May 26 2022 at 14:38):I already had people violating my license of Coq-related projects and I'm not happy
Emilio Jesús Gallego Arias (May 26 2022 at 14:41):I'm open to any license choice, as long as closed-source software can't be made where the project is substantial. Note that I'm very happy with commertial uses, for example, but these should be framed in an open source way for the research components
Emilio Jesús Gallego Arias (May 26 2022 at 14:42):All of these projects were done with public funding so it is only fair
Emilio Jesús Gallego Arias (May 26 2022 at 14:43):As these are really protocols, it is also fine to me that the processing of the data they extract can remain propietary
Emilio Jesús Gallego Arias (May 26 2022 at 14:43):But I think the GPL covers that well
Emilio Jesús Gallego Arias (May 26 2022 at 14:44):If we had stuff such as libgcc etc... indeed, then licensing LGPL would make sense I think
Emilio Jesús Gallego Arias (May 26 2022 at 14:45):So to be clear again, the intent is that propietary use is totally fine, propietary forking not
Emilio Jesús Gallego Arias (May 26 2022 at 14:45):I think we don't have components where GPL would forbid propietary use, but if that would be the case then LGPL makes sense
Karl Palmskog (May 26 2022 at 14:46):I'm sure that's the intent, but the intent of the license author will normally also be taken into account. For example, the LGPL 3.0 is formulated as an exception to GPL 3.0, it's not a standalone license.
Emilio Jesús Gallego Arias (May 26 2022 at 14:46):Yes
Emilio Jesús Gallego Arias (May 26 2022 at 14:46):If a use case would require a linking exception I'd consider adding it
Karl Palmskog (May 26 2022 at 14:47):the gist of the argument with linking is: why did the license author of GPL-3.0 bother with writing a license with that's formulated as an exception to GPL-3.0 (LGPL-3.0), if linking was already not enough to create a derivative work?
Emilio Jesús Gallego Arias (May 26 2022 at 14:48):To be explicit about it
Emilio Jesús Gallego Arias (May 26 2022 at 14:48):linking can or can not make a derivative work
Emilio Jesús Gallego Arias (May 26 2022 at 14:48):so it is open to interpretation
Emilio Jesús Gallego Arias (May 26 2022 at 14:49):LGPL removes this ambiguity
Emilio Jesús Gallego Arias (May 26 2022 at 14:49):most famous case is Nvidia kernel modules
Emilio Jesús Gallego Arias (May 26 2022 at 14:49):which led to the introduction of GPL-only symbols
Emilio Jesús Gallego Arias (May 26 2022 at 14:49):and in the end, to Nvidia open-sourcing their drivers
Emilio Jesús Gallego Arias (May 26 2022 at 14:52):It is very logical than in some use cases such as compiler runtime libs, the license removes this ambiguity
Emilio Jesús Gallego Arias (May 26 2022 at 14:52):as they intent is the compiler can be used to compile propietary software
Karl Palmskog (May 26 2022 at 14:53):sure, but as per above, it's also to permit more permissive licenses [in the software being compiled]
Karl Palmskog (May 26 2022 at 15:01):for the record, the FSF's view is that "[linking code with GPL'd code] means you must release your program under a license compatible with the GPL (more precisely, compatible with one or more GPL versions accepted by all the rest of the code in the combination that you link)". I take that as my current best approximation.
Paolo Giarrusso (May 26 2022 at 17:10):@Emilio Jesús Gallego Arias > I guess if they have a reason to try to do closed source using research open source software, they got a legal team too
Paolo Giarrusso (May 26 2022 at 17:11):but people who want to write LGPL/MIT/BSD libraries do not.
Paolo Giarrusso (May 26 2022 at 17:12):nevermind, Karl already said it
Emilio Jesús Gallego Arias (May 26 2022 at 17:33):I don't see how you can write a derivative of GPL software and have it being MIT?
Paolo Giarrusso (May 26 2022 at 17:36):Agreed; that’s the issue.
Paolo Giarrusso (May 26 2022 at 17:37):Actually, wait.
Karl Palmskog (May 26 2022 at 17:38):MIT-like licenses is one thing. But with GPL-incompatible licenses such as CECILL-C and CECILL-B, it's a violation of GPL to link and the software can't be distributed [if you go with FSF, like I do]
Paolo Giarrusso (May 26 2022 at 17:38):The problem is about people who want to write software using your code
Paolo Giarrusso (May 26 2022 at 17:39):yeah okay — you can write MIT software that uses GPL software, but users do not get to use the combo as MIT only as GPL
Paolo Giarrusso (May 26 2022 at 17:40):@Karl Palmskog I guess a relevant question is, to which extent does GPL prevent use in the math-comp ecosystem?
Paolo Giarrusso (May 26 2022 at 17:41):not that I have an extremely concrete use-case in mind
Karl Palmskog (May 26 2022 at 17:41):for MIT-like licenses, the main concern is that changes for the linking can't be upstreamed (since authors don't want their licenses changed just to link)
Paolo Giarrusso (May 26 2022 at 17:41):that seems excessive?
Paolo Giarrusso (May 26 2022 at 17:42):hm, not sure what are the “changes for the linking”
Karl Palmskog (May 26 2022 at 17:42):you may want to integrate code that does the linking to SerAPI with the project itself
Paolo Giarrusso (May 26 2022 at 17:42):of course if you write MIT code, I think anybody can upstream it to a GPL codebase, they’ll keep the original notice but the combination will be GPL
Karl Palmskog (May 26 2022 at 17:46):I specifically mean upstreaming SerAPI library based code to an MIT-like codebase. Essentially, to not have licensing problems, one will be forced to keep the "bundling" code between SerAPI and the codebase in some third location, and avoid any distributing together with CECILL-C/B and the like.
Karl Palmskog (May 26 2022 at 17:47):however, doing the exact same integration over a domain socket and the sertop program avoids all that hassle.
Paolo Giarrusso (May 26 2022 at 17:50):I guess you are right, but is that indeed settled law, or are there corner cases?
Karl Palmskog (May 26 2022 at 17:51):according to the FSF, it's settled. But according to Wikipedia, GPL vs. linking has never been decided in any court.
Paolo Giarrusso (May 26 2022 at 17:53):I mean, it is strange that linking-through-a-socket differs from linking in ways that matter to the law.
Karl Palmskog (May 26 2022 at 17:53):but even if some US court decided on it, European countries are not likely to accept this ruling in any specific form, and vice versa
Paolo Giarrusso (May 26 2022 at 17:54):right, but IIUC this has not been settled in court because everybody who gets sued agrees with the FSF
Karl Palmskog (May 26 2022 at 17:55):my view is that the GPL is a product of the C era of computing, where you have to compile something to use it.
Paolo Giarrusso (May 26 2022 at 17:55):(consider my last comment as fourth-hand knowledge)
Karl Palmskog (May 26 2022 at 17:56):I think nowadays, there's far less difference between "using a program" and "linking with a program"
Karl Palmskog (May 26 2022 at 17:57):but I think the real legal battle, if any, will be about what is considered a derivative work, and at what time
Karl Palmskog (May 26 2022 at 17:57):from what I recall, the concept of derivative work has a long history in copyright law
Paolo Giarrusso (May 26 2022 at 17:59):I think Emilio is right, and the GPL and LGPL does not seem to talk of linking but of derivative works except in examples
Karl Palmskog (May 26 2022 at 18:00):LGPL talks specifically about linking. I already acknowledged GPL does not mention linking.
Paolo Giarrusso (May 26 2022 at 18:01):and linking is just one technique to implement derivative works; sockets are another.
Paolo Giarrusso (May 26 2022 at 18:01):An “Application” is any work that makes use of an interface provided by the Library, but which is not otherwise based on the Library. Defining a subclass of a class defined by the Library is deemed a mode of using an interface provided by the Library.
A “Combined Work” is a work produced by combining or linking an Application with the Library. The particular version of the Library with which the Combined Work was made is also called the “Linked Version”.
Karl Palmskog (May 26 2022 at 18:02):the difference here is that the socket does not even use the source code or compiled libraries directly. It only uses the program. I think it's very hard to argue sertop interaction is restricted by GPL (you run the program, send it input, get output)
Emilio Jesús Gallego Arias (May 26 2022 at 18:05):Yes using sertop it is not bound by serapi license
Emilio Jesús Gallego Arias (May 26 2022 at 18:06):the thing is that linking allows you to do way more than just using
Paolo Giarrusso (May 26 2022 at 18:06):It is bound, but GPL usually does not constrain that…
Emilio Jesús Gallego Arias (May 26 2022 at 18:06):I mean by serapi license
Emilio Jesús Gallego Arias (May 26 2022 at 18:06):indeed
Emilio Jesús Gallego Arias (May 26 2022 at 18:07):If you link just to do that kind of use IMHO you are fine
Paolo Giarrusso (May 26 2022 at 18:09):but if I reimplement the SerAPI API by wrapping SerAPI via a socket? The use is fine, but my source code is clearly derivative work…
Emilio Jesús Gallego Arias (May 26 2022 at 18:10):Likely, who knows what a judge would decide?
Karl Palmskog (May 26 2022 at 18:10):that will depend on, I think, whether you actually look at SerAPI source code or not
Emilio Jesús Gallego Arias (May 26 2022 at 18:10):Hehe
Emilio Jesús Gallego Arias (May 26 2022 at 18:10):indeed, the intent is clear
Emilio Jesús Gallego Arias (May 26 2022 at 18:10):I mean, my intent
Emilio Jesús Gallego Arias (May 26 2022 at 18:10):if you are a user (like in Coq) you do what you want, but if you are building a derivative, then you gotta share your code back
Karl Palmskog (May 26 2022 at 18:10):reverse engineering has been tested in court and was allowed in several high-profile cases. Per Google vs. Oracle, APIs can be reimplemented without copyright entering the picture.
Emilio Jesús Gallego Arias (May 26 2022 at 18:11):Also nvidia has been linking to GPL code for ages and nothing happened to them
Emilio Jesús Gallego Arias (May 26 2022 at 18:11):Yeah APIs are a different animal
Gaëtan Gilbert (May 26 2022 at 18:11):Karl Palmskog said:
reverse engineering has been tested in court and was allowed in several high-profile cases. Per Google vs. Oracle, APIs can be reimplemented without copyright entering the picture.
Wasn't that decision based on fair use which is case by case?
Emilio Jesús Gallego Arias (May 26 2022 at 18:11):That's why if you are linking to use I don't care
Paolo Giarrusso (May 26 2022 at 18:12):we cannot predict the judge’s output, all that we can anticipate is when one needs a lawyer and how expensive it is
Karl Palmskog (May 26 2022 at 18:12):“Google’s copying of the API to reimplement a user interface, taking only what was needed to allow users to put their accrued talents to work in a new and transformative program, constituted a fair use of that material,” the Supreme Court ruled in a 6-2 opinion
from here
Paolo Giarrusso (May 26 2022 at 18:13):and if the client code is open source, they need to decide whether they’re willing to use your code or the license risks are too high.
Paolo Giarrusso (May 26 2022 at 18:21):going from theory to practice, alectryon (MIT licensing) seems to use Coq-serapi — so what is the effective license of Alectryon?
Karl Palmskog (May 26 2022 at 18:22):Alectryon uses sertop and is thus unaffected by SerAPI license currently
Emilio Jesús Gallego Arias (May 26 2022 at 18:23):Even if it would use PyCoq , it is 100% a user so they are free to use their license
Karl Palmskog (May 26 2022 at 18:24):but if Alectryon is ever ported to PyCoq (which would likely increase performance a ton), it would have to switch to GPL, according to FSF
Emilio Jesús Gallego Arias (May 26 2022 at 18:24):Karl Palmskog said:
but if Alectryon is ever ported to PyCoq (which would likely increase performance a ton), it would have to switch to GPL, according to FSF
That's your view, not mine as the author of PyCoq
Emilio Jesús Gallego Arias (May 26 2022 at 18:24):That's FSF view sorry
Emilio Jesús Gallego Arias (May 26 2022 at 18:24):which I'm not sure it is
Emilio Jesús Gallego Arias (May 26 2022 at 18:24):Because using a python API doesn't require linking
Paolo Giarrusso (May 26 2022 at 18:25):but as you said, the GPL does not mention linking
Karl Palmskog (May 26 2022 at 18:25):well, my view is very close to the FSF view
Emilio Jesús Gallego Arias (May 26 2022 at 18:25):In no way Alectyron is a derived thing of SerAPI
Emilio Jesús Gallego Arias (May 26 2022 at 18:26):However it chooses to communicate
Karl Palmskog (May 26 2022 at 18:28):if I was advising Clement (which I'm not), I'd split off any PyCoq support for Alectryon to a separate repo/package
Paolo Giarrusso (May 26 2022 at 18:29):even if Emilio is right, the problem above applies: is this safe enough to not cause trouble? Courts will not come into play, but more careful clients will — both Debian packagers and commercial users of Alectryon
Karl Palmskog (May 26 2022 at 18:29):if Alectryon itself works independently of PyCoq and does not even have the PyCoq integration code, it's hard to make the claim Alectryon itself is a derived work.
Karl Palmskog (May 26 2022 at 18:30):yes, everything would be aimed towards making other people comfortable that Alectryon indeed does not violate GPL
Paolo Giarrusso (May 26 2022 at 18:30):I agree with Karl that is safer. What Emilio says might be true, but how safe would others feel if Clement skipped this extra work?
Paolo Giarrusso (May 26 2022 at 18:31):and as Karl said in the beginning, this means that open-source consumers might feel they have to do extra work just because serapi uses GPL.
Emilio Jesús Gallego Arias (May 26 2022 at 18:31):There is no problem anyways in having a MIT package derive from a GPL package
Emilio Jesús Gallego Arias (May 26 2022 at 18:31):just that the result is GPL
Emilio Jesús Gallego Arias (May 26 2022 at 18:32):I am not familiar with Python stuff, but I'd be shocked if actually using a Python library viralizes licenses...
Emilio Jesús Gallego Arias (May 26 2022 at 18:32):Then they got bigger problems than us
Paolo Giarrusso (May 26 2022 at 18:34):it would be strange if GPL and LGPL were the same for Python etc — at least, I would wonder why there is no GPL+ for this case (like with AGPL)
Emilio Jesús Gallego Arias (May 26 2022 at 18:34):Python is interpreted so where is the linking?
Paolo Giarrusso (May 26 2022 at 18:34):as you argued, that is not very relevant?
Emilio Jesús Gallego Arias (May 26 2022 at 18:34):yeah
Emilio Jesús Gallego Arias (May 26 2022 at 18:35):for example if Alectryon uses PyCoq normally, that is not a problem
Emilio Jesús Gallego Arias (May 26 2022 at 18:35):however it can subclass a public API
Emilio Jesús Gallego Arias (May 26 2022 at 18:35):then, that part is a derived work and should be GPL
Emilio Jesús Gallego Arias (May 26 2022 at 18:35):I think LGPL / GPL is really moot these days
Paolo Giarrusso (May 26 2022 at 18:36):the client writes (1) source code (2) that is potentially so tightly coupled that it is inevitably derived work
Paolo Giarrusso (May 26 2022 at 18:36):even if you were right, I think many open-source people would balk at relying on this.
Karl Palmskog (May 26 2022 at 18:38):maybe Paolo can ask how industry would feel about switching Coq from LGPL to GPL (this is something the Coq core team could do tomorrow, I believe, i.e., say that all future changes will be GPL only)
Paolo Giarrusso (May 26 2022 at 18:38):by this logic, for instance, wouldnt serapi be fine as-is? Yet @Julien Puydt is objecting for Debian.
Karl Palmskog (May 26 2022 at 18:39):anyway, that is just to exemplify that to many people, GPL vs. LGPL is not moot...
Enrico Tassi (May 26 2022 at 21:45):From my one (and only one) law class, I do recall a big discovery, leading to a more relaxed heartbeat, that laws (and licenses) have to be interpreted by humans. Indeed many of them start by explaining principles, and then tons of legaleese to justify salaries.
In that respect I find the difference between LGPL and GPL crystal clear. Even if to just use a software you have to meld it into yours, you are good to go; if you change it you got to share. IMO derivative work is way less clear to me: e.g. if alectryon can't possibly run the coq backend without serapi, how can this backenf not be a derivative work? (the backend for Lean, it is surely not, I m really taling about the coq one).
IMO picking LGPL makes this question moot. I wouldn't bet my money on GPL for that. Busybox has been used for ages as a lever to convince companies to release (or stop selling) their code, which for sure was not linked with busybox. Was it a derivative work?
Emilio Jesús Gallego Arias (May 26 2022 at 21:47):Enrico Tassi said:
IMO picking LGPL makes this question moot. I wouldn't bet my money on GPL for that. Busybox has been used for ages as a lever to convince companies to release (or stop selling) their code, which for sure was not linked with busybox. Was it a derivative work?
Oh that's news to me, Busybox has been very proactive about companies releasing the code of their busybox implementation, but I've never heard they forced any company to release their propietary stuff
Emilio Jesús Gallego Arias (May 26 2022 at 21:47):do you have a link?
Emilio Jesús Gallego Arias (May 26 2022 at 21:48):(by the way Alectryon runs the Coq backend without SerAPI fine, with less functionality, but that's moot anyways as SerAPI does mostly share Coq's license LGPL)
Enrico Tassi (May 26 2022 at 21:51):IMO LGPL is in a sense more clear. Why didn't the author chose GPL? Well, because he didn't want to block any user, but still get back improvements.
GPL was a deliberate smart hack to try to get more free software, not to keep the free one free, which seems what you want Emilio.
Emilio Jesús Gallego Arias (May 26 2022 at 21:52):LGPL arose because of libgcc which a special case. I'm not sure I understand that last part sorry, but IIRC GPL was designed for both.
Enrico Tassi (May 26 2022 at 21:53):IIRC busybox has always been used to obtain the sources of the entire firmware of, say, plug computers. Nobody ever cares about the code adding one more option to httpd.
Emilio Jesús Gallego Arias (May 26 2022 at 21:53):To keep the one free, I don't have my copy of "Free as in Freedom" at hand but I recall Richard mentioning how propietary companies did took MIT code and they didnt' contribute back, which got him super frustated
Emilio Jesús Gallego Arias (May 26 2022 at 21:54):Enrico Tassi said:
IIRC busybox has always been used to obtain the sources of the entire firmware of, say, plug computers. Nobody ever cares about the code adding one more option to httpd.
Only the parts of the software that were under GPL
Emilio Jesús Gallego Arias (May 26 2022 at 21:54):which is normal
Emilio Jesús Gallego Arias (May 26 2022 at 21:54):often the whole firmware was under GPL
Emilio Jesús Gallego Arias (May 26 2022 at 21:54):but I know no record of a company that was forced to release anything non GPL using busybox, if there is such a case I'm very interested to read bout it
Enrico Tassi (May 26 2022 at 21:55):Nope, a firmware is a collection of stuff. How can all it be GPL. But can it run without busybox?
Enrico Tassi (May 26 2022 at 21:56):I'm not saying the argument holds to my ears of geek, but did to the ears of these companies lawyers
Emilio Jesús Gallego Arias (May 26 2022 at 21:56):Likely not. But I know no case of busybox license used to release non-GPL software, unless voluntary
Emilio Jesús Gallego Arias (May 26 2022 at 21:56):busybox FAQ page seems very clear on that
Emilio Jesús Gallego Arias (May 26 2022 at 21:57):a firmware image is mere "bundling" which doesn't force the release of components
Emilio Jesús Gallego Arias (May 26 2022 at 21:57):as per GPL
Enrico Tassi (May 26 2022 at 21:57):Oh, if alectryon can provide coq documentation without serapi with an equal result, it is surely not a derivative work.
Emilio Jesús Gallego Arias (May 26 2022 at 21:58):It is a derivate work as an application using a database is a derivate work of the database
Emilio Jesús Gallego Arias (May 26 2022 at 21:59):and in this case the application can't function without the database
Emilio Jesús Gallego Arias (May 26 2022 at 21:59):and it is still not a derivative work
Emilio Jesús Gallego Arias (May 26 2022 at 22:00):derivative is a notion that goes beyond software, it belongs to the realm of copyright
Emilio Jesús Gallego Arias (May 26 2022 at 22:00):music is very interesting in this aspect
Emilio Jesús Gallego Arias (May 26 2022 at 22:00):when a song is a derivative of another
Emilio Jesús Gallego Arias (May 26 2022 at 22:00):IANAL but I'd bet that LGPL vs GPL would have little weight in court, again c.f. nvidia
Emilio Jesús Gallego Arias (May 26 2022 at 22:00):nobody dared to go against nvidia because they were afraid they would lose
Emilio Jesús Gallego Arias (May 26 2022 at 22:01):and there would be jurisprudence on actually "linking with GPL is Ok, if your product is reasonable independent"
Emilio Jesús Gallego Arias (May 26 2022 at 22:01):so FSF can say all they want, but they were actually afraid as they deemed the risk for too long
Enrico Tassi (May 26 2022 at 22:01):Court is for getting money out of some enyity. Nobody would ever sue Debian since it has little money (lawyers told me so).
Emilio Jesús Gallego Arias (May 26 2022 at 22:01):the GPL symbol hack that was a good hack
Emilio Jesús Gallego Arias (May 26 2022 at 22:02):the nvidia case was well beyond money
Emilio Jesús Gallego Arias (May 26 2022 at 22:02):yeah suing Debian makes not a lot of sense
Emilio Jesús Gallego Arias (May 26 2022 at 22:03):court is often for getting money, but of course many times is about setting precedent
Emilio Jesús Gallego Arias (May 26 2022 at 22:03):so you can keep doing what you want
Emilio Jesús Gallego Arias (May 26 2022 at 22:03):as you get an approval
Enrico Tassi (May 26 2022 at 22:04):IMO this thread is alike the reaming business. Not using LGPL (the one of Coq) or more permissive licenses is just a pain for users and, concretely, will never bring you anything.
Emilio Jesús Gallego Arias (May 26 2022 at 22:05):Why is that a pain?
Enrico Tassi (May 26 2022 at 22:05):Keeping the punny name, is not bringing us anything either.
Enrico Tassi (May 26 2022 at 22:06):Because it is more constraining
Emilio Jesús Gallego Arias (May 26 2022 at 22:06):How is it more constraining?
Enrico Tassi (May 26 2022 at 22:06):So you have to understand why and how
Enrico Tassi (May 26 2022 at 22:06):You have to explain you boss all that
Emilio Jesús Gallego Arias (May 26 2022 at 22:06):Yes I don't understand the point where GPL is more constrainting than LGPL
Emilio Jesús Gallego Arias (May 26 2022 at 22:07):GPL doesn't forbid linking
Enrico Tassi (May 26 2022 at 22:07):This is why I made COQ-ELPI LGPL from the start: meant to used with Coq, why make things more complicated
Emilio Jesús Gallego Arias (May 26 2022 at 22:08):Yes actually see my comment above, this is more about future projects
Emilio Jesús Gallego Arias (May 26 2022 at 22:08):SerAPI is mostly same license as Coq
Enrico Tassi (May 26 2022 at 22:08):Ok then exchange constrained with just different. The boss will ask different how ...
Emilio Jesús Gallego Arias (May 26 2022 at 22:08):the libgcc story is funny, an a bit anacronic, and it is due to the way quotation works in literary and partitions work in copyright
Emilio Jesús Gallego Arias (May 26 2022 at 22:09):we are talking about the 80s, where judges knew the copyright from where they knew
Emilio Jesús Gallego Arias (May 26 2022 at 22:09):so libgcc was considered a "quotation" due to the way linking worked, to start with, _there was no dynamic linking_
Emilio Jesús Gallego Arias (May 26 2022 at 22:10):so there was a legal risk back in the day, but I guess that's too lawyer technical
Enrico Tassi (May 26 2022 at 22:13):If I had to start a new prover, I may chose a different license. I don't love LGPL. But for a derivative work of Coq it is just simpler to pick the same, or an DWTFYW one like MIT.
Emilio Jesús Gallego Arias (May 26 2022 at 22:14):What would you choose?
Emilio Jesús Gallego Arias (May 26 2022 at 22:14):Yes for a derivative work of Coq LGPL is good, tho GPL is not so bad
Emilio Jesús Gallego Arias (May 26 2022 at 22:15):if you have external components, they combine to GPL I understand (should check carefully)
Enrico Tassi (May 26 2022 at 22:18):It depends. If I target the industry, MIT. This is why Lua for example picked it, because a big client was the industry and they preferred to please that audience. If it was a CAT drawing one with a JS UI, I'd consider affero & co. After all, I'd be doing that only for fun.
Emilio Jesús Gallego Arias (May 26 2022 at 22:19):Interpreters are indeed in a complex position, they are basic building blocks
Enrico Tassi (May 26 2022 at 22:20):IMO licensing as a lever (as GPL was) is no more actual.
Enrico Tassi (May 26 2022 at 22:21):You pick GPL as a statement, but it won't make more free software than picking MIT imo.
Enrico Tassi (May 26 2022 at 22:23):So avoiding pain for the user seem more important to foster free software.
Enrico Tassi (May 26 2022 at 22:24):Take you NVIDIA example. I don't think they are releasing their crap to comply, finally, to GPL.
Emilio Jesús Gallego Arias (May 26 2022 at 22:24):Maybe you are right, I was feeling the exact opposite, I'm worried about MIT proliferation, that could destroy the hard to win gains we had
Emilio Jesús Gallego Arias (May 26 2022 at 22:24):Actually nvidia cited a reason to be able to use GPL-only symbols
Enrico Tassi (May 26 2022 at 22:24):They just want more success and less pain for GPU users, which are apparently many
Emilio Jesús Gallego Arias (May 26 2022 at 22:25):that's a side effect of free software, but if Linux was MIT, where would we be today?
Emilio Jesús Gallego Arias (May 26 2022 at 22:25):I don't know
Emilio Jesús Gallego Arias (May 26 2022 at 22:25):Enrico Tassi said:
They just want more success and less pain for GPU users, which are apparently many
Yes, so that makes the GPL a good choice?
Emilio Jesús Gallego Arias (May 26 2022 at 22:26):Moreover thanks to GPL linux avoided a stable API, as they can refactor in large scale
Emilio Jesús Gallego Arias (May 26 2022 at 22:26):all drivers can be in tree (and many are MIT)
Enrico Tassi (May 26 2022 at 22:26):I think GPL worked as a non conflict agreement in days where companies were not understanding the benefits of open development. Today I'm not so sure it would make such a difference. Is Chrome GPL?
Enrico Tassi (May 26 2022 at 22:27):Gotta sleep really, nice chat
Emilio Jesús Gallego Arias (May 26 2022 at 22:28):Chrome is not open source I understand, v8 is MIT
Emilio Jesús Gallego Arias (May 26 2022 at 22:28):good night, me too
Emilio Jesús Gallego Arias (May 26 2022 at 22:28):actually it is a good question if MIT is working good for V8
Emilio Jesús Gallego Arias (May 26 2022 at 22:28):given what Apple is doing
Emilio Jesús Gallego Arias (May 26 2022 at 22:28):but yes, long and interesting chat
Emilio Jesús Gallego Arias (May 26 2022 at 22:29):and moreover so far real license stuff is untested in court, except for Java and Linux with the BSD trools
Emilio Jesús Gallego Arias (May 26 2022 at 22:29):ciao
Emilio Jesús Gallego Arias (May 26 2022 at 22:30):Umm, webkit is hybrid MIT / LGPL
Enrico Tassi (May 26 2022 at 22:31):Chromium is, not very different. My point is that BASE stuff is much better open. Linux is base, chrome/v8 is. Being in the base, what Nvidia is doing, is more important than keeping code to yourself.
Enrico Tassi (May 26 2022 at 22:32):If Coq is your base, better be there, IMO.
Enrico Tassi (May 26 2022 at 22:33):We can argue if the L in LGPL is important or not, but deviating from the base you target surely is.
Théo Zimmermann (May 27 2022 at 09:24):Emilio Jesús Gallego Arias said:
I am not familiar with Python stuff, but I'd be shocked if actually using a Python library viralizes licenses...
What shocks me is people deciding to use GPL but using terms like "viral" that were invented to discredit the free software movement. Also, while I agree that the limits of what a derivative work is are not so clear, I also find surprising that someone who would disagree with the opinion of the FSF on the matter would still choose the GPL license (written by the FSF) for their work (and hope that people would understand that linking is OK despite what is written almost everywhere on the internet, and in particular on the most authoritative site on the GPL, the FSF one).
Théo Zimmermann (May 27 2022 at 09:26):BTW, it appears that PyCoq is missing a license entirely, which is even more problematic.
Karl Palmskog (May 27 2022 at 10:04):@Théo Zimmermann it has a license in pycoq.opam
Emilio Jesús Gallego Arias (May 27 2022 at 10:51):@Théo Zimmermann yes that's an unfortunate term, I should have said "just using a Python library makes the user a derived work"
The opinion of the FSF needs update IMO, as the original LGPL was in the context of static linking, using copyright law, we could compare literally quoting on a paper, vs using a reference, as to understand dynamic vs static linking. When you use dynamic linking over an API, it seems too broad to claim the user is a derived work: someone could reimplement the API with a different license so unless you can copyright the API, you got a weak case, and FSF claims have not stood in court yet (quite the opposite). It may be written all over the internet, but so far nobody has won a case on that IIUC.
In fact, _GPL symbols in Linux had to use a "quotation trick" as to try to enforce this restriction using quite outdated copyright law for our purposes.
FSF also recommends against using LGPL in new libraries. PyCoq is at alpha stage so please bear with us, it will get a proper metadata soon and before its first release.
Karl Palmskog (May 27 2022 at 11:03):I think it's well known that FSF recommends the regular GPL since they don't want free software to be combined/linked with proprietary software, i.e., their recommendation is rooted in their view that any linking requires full GPL'ing of everything.
Paolo Giarrusso (May 27 2022 at 13:21):the "well-known" thing is IIRC more complex — but the default is as Karl says; I recall exceptions such as "if you write a filesystem in another OS and port it to Linux, then it might not be a derived work despite linking".
Paolo Giarrusso (May 27 2022 at 13:38):Emilio Jesús Gallego Arias said:
Thanks Karl Palmskog , I do have a constraint tho, I'd like a license that doesn't allow closed-source software making derivatives of my own
So LGPL is not an option for me
Actually, can we revisit this? The LGPL forbids closed-source derivatives alright
Paolo Giarrusso (May 27 2022 at 13:39):Emilio Jesús Gallego Arias said:
Linking is not derivative
if you want to allow non-GPL code to link with yours, it seems LGPL matches your intent better?
Emilio Jesús Gallego Arias (May 27 2022 at 13:42):@Paolo Giarrusso I'm ok with propietary code using these tools. What's the relationship of linking vs derivative. How do you define "linking"?
Paolo Giarrusso (May 27 2022 at 14:08):I’d say that in Python (like in Coq), you essentially only have “dynamic linking” in the LGPL sense (since users can always patch the LGPL component and run the combination).
Emilio Jesús Gallego Arias (May 27 2022 at 14:11):What's dynamic linking in the LGPL sense?
Paolo Giarrusso (May 27 2022 at 14:11):I find the preamble of LGPL 2.1 pretty enlightening on intent: https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
Emilio Jesús Gallego Arias (May 27 2022 at 14:12):6.b)
Emilio Jesús Gallego Arias (May 27 2022 at 14:12):?
Paolo Giarrusso (May 27 2022 at 14:12):Re dynamic linking, this is the core goal: > Although the Lesser General Public License is Less protective of the users' freedom, it does ensure that the user of a program that is linked with the Library has the freedom and the wherewithal to run that program using a modified version of the Library.
Emilio Jesús Gallego Arias (May 27 2022 at 14:12):Yes it does ensure that, but we are talking about the GPL
Emilio Jesús Gallego Arias (May 27 2022 at 14:12):the GPL says nothing about linking
Paolo Giarrusso (May 27 2022 at 14:14):Ah, I was talking about the LGPL. Its prologue also explains the difference with the GPL:
Paolo Giarrusso (May 27 2022 at 14:14):When a program is linked with a library, whether statically or using a shared library, the combination of the two is legally speaking a combined work, a derivative of the original library. The ordinary General Public License therefore permits such linking only if the entire combination fits its criteria of freedom. The Lesser General Public License permits more lax criteria for linking other code with the library.
Paolo Giarrusso (May 27 2022 at 14:15):If you’re asking how I define linking for Python, running a Python interpreter using two libraries is using their dynamic linking.
Last updated: May 31 2023 at 09:01 UTC