Stream: SerAPI

Topic: coq-serapi licensing


view this post on Zulip Julien Puydt (Dec 15 2021 at 07:41):

Though understanding the licensing might prove difficule, as the LICENSE file is a little unclear.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 using my own

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:25):

So LGPL is not an option for me

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:55):

That's fine to me

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:56):

Otherwise they could just make software closed

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:57):

I guess by users you mean people making derivative software

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:57):

as indeed GPL places no restriction on use

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:57):

otherwise it wouldn't be a free license

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 12:57):

But my software is scientific software, so derivatives must be open source too

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 13:12):

Ok that's fine

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 13:13):

they can't already do it

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 26 2022 at 13:14):

how is this not: "software using your software"?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 26 2022 at 13:17):

how can a CECILL-C project linking with a LGPL project be a problem?

view this post on Zulip Théo Zimmermann (May 26 2022 at 13:17):

Oh, there's no problem with linking obviously.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:00):

I'm fine with people using the software as they want

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:01):

Linking is not derivative

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:02):

but for other softwares we are developing that's relevant

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:03):

And I'm OK with that

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:04):

Oh I see I wrote "using", sorry that was a big typo

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:04):

corrected in my original post

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:04):

I meant using as in making derivate products

view this post on Zulip 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.

view this post on Zulip 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-serapi repo 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:17):

that's the reason it is not used in GPL 3

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:18):

If I understood the format correctly, to everything not covered by Files:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:27):

Again that only can be decided in court

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (May 26 2022 at 14:28):

or in any case, they consider the current state of legal analysis to point towards this

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:29):

I don't know what people may consider

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:30):

that's up to them and their legal team

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:43):

But I think the GPL covers that well

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:46):

Yes

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:48):

To be explicit about it

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:48):

linking can or can not make a derivative work

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:48):

so it is open to interpretation

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:49):

LGPL removes this ambiguity

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:49):

most famous case is Nvidia kernel modules

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:49):

which led to the introduction of GPL-only symbols

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:49):

and in the end, to Nvidia open-sourcing their drivers

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 14:52):

as they intent is the compiler can be used to compile propietary software

view this post on Zulip 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]

view this post on Zulip 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". I take that as my current best approximation.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:11):

but people who want to write LGPL/MIT/BSD libraries do not.

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:12):

nevermind, Karl already said it

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:36):

Agreed; that’s the issue.

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:37):

Actually, wait.

view this post on Zulip 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]

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:38):

The problem is about people who want to write software using your code

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:41):

not that I have an extremely concrete use-case in mind

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:41):

that seems excessive?

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:42):

hm, not sure what are the “changes for the linking”

view this post on Zulip Karl Palmskog (May 26 2022 at 17:42):

you may want to integrate code that does the linking to SerAPI with the project itself

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:50):

I guess you are right, but is that indeed settled law, or are there corner cases?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 26 2022 at 17:55):

(consider my last comment as fourth-hand knowledge)

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 26 2022 at 17:57):

from what I recall, the concept of derivative work has a long history in copyright law

view this post on Zulip 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

view this post on Zulip Karl Palmskog (May 26 2022 at 18:00):

LGPL talks specifically about linking. I already acknowledged GPL does not mention linking.

view this post on Zulip Paolo Giarrusso (May 26 2022 at 18:01):

and linking is just one technique to implement derivative works; sockets are another.

view this post on Zulip 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”.

view this post on Zulip Karl Palmskog (May 26 2022 at 18:02):

the difference here is that the socket does not even use the source code. 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)

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:05):

Yes using sertop it is not bound by serapi license

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (May 26 2022 at 18:06):

It is bound, but GPL usually does not constrain that…

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:06):

I mean by serapi license

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:06):

indeed

view this post on Zulip 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

view this post on Zulip 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…

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:10):

Likely, who knows what a judge would decide?

view this post on Zulip Karl Palmskog (May 26 2022 at 18:10):

that will depend on, I think, whether you actually look at SerAPI source code or not

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:10):

Hehe

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:10):

indeed, the intent is clear

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:10):

I mean, my intent

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:11):

Yeah APIs are a different animal

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:11):

That's why if you are linking to use I don't care

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (May 26 2022 at 18:22):

Alectryon uses sertop and is thus unaffected by SerAPI license currently

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:24):

That's FSF view sorry

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:24):

which I'm not sure it is

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:24):

Because using a python API doesn't require linking

view this post on Zulip Paolo Giarrusso (May 26 2022 at 18:25):

but as you said, the GPL does not mention linking

view this post on Zulip Karl Palmskog (May 26 2022 at 18:25):

well, my view is very close to the FSF view

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:25):

In no way Alectyron is a derived thing of SerAPI

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:26):

However it chooses to communicate

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:31):

just that the result is GPL

view this post on Zulip 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...

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:32):

Then they got bigger problems than us

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:34):

Python is interpreted so where is the linking?

view this post on Zulip Paolo Giarrusso (May 26 2022 at 18:34):

as you argued, that is not very relevant?

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:34):

yeah

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:35):

for example if Alectryon uses PyCoq normally, that is not a problem

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:35):

however it can subclass a public API

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:35):

then, that part is a derived work and should be GPL

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 18:35):

I think LGPL / GPL is really moot these days

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 26 2022 at 18:39):

anyway, that is just to exemplify that to many people, GPL vs. LGPL is not moot...

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:47):

do you have a link?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:54):

which is normal

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:54):

often the whole firmware was under GPL

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:56):

busybox FAQ page seems very clear on that

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:57):

as per GPL

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:59):

and in this case the application can't function without the database

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 21:59):

and it is still not a derivative work

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:00):

music is very interesting in this aspect

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:00):

when a song is a derivative of another

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:00):

nobody dared to go against nvidia because they were afraid they would lose

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:01):

the GPL symbol hack that was a good hack

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:02):

the nvidia case was well beyond money

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:02):

yeah suing Debian makes not a lot of sense

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:03):

so you can keep doing what you want

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:03):

as you get an approval

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:05):

Why is that a pain?

view this post on Zulip Enrico Tassi (May 26 2022 at 22:05):

Keeping the punny name, is not bringing us anything either.

view this post on Zulip Enrico Tassi (May 26 2022 at 22:06):

Because it is more constraining

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:06):

How is it more constraining?

view this post on Zulip Enrico Tassi (May 26 2022 at 22:06):

So you have to understand why and how

view this post on Zulip Enrico Tassi (May 26 2022 at 22:06):

You have to explain you boss all that

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:07):

GPL doesn't forbid linking

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:08):

Yes actually see my comment above, this is more about future projects

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:08):

SerAPI is mostly same license as Coq

view this post on Zulip Enrico Tassi (May 26 2022 at 22:08):

Ok then exchange constrained with just different. The boss will ask different how ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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_

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:14):

What would you choose?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:19):

Interpreters are indeed in a complex position, they are basic building blocks

view this post on Zulip Enrico Tassi (May 26 2022 at 22:20):

IMO licensing as a lever (as GPL was) is no more actual.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 26 2022 at 22:23):

So avoiding pain for the user seem more important to foster free software.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:24):

Actually nvidia cited a reason to be able to use GPL-only symbols

view this post on Zulip Enrico Tassi (May 26 2022 at 22:24):

They just want more success and less pain for GPU users, which are apparently many

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:25):

I don't know

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:26):

all drivers can be in tree (and many are MIT)

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (May 26 2022 at 22:27):

Gotta sleep really, nice chat

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:28):

Chrome is not open source I understand, v8 is MIT

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:28):

good night, me too

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:28):

actually it is a good question if MIT is working good for V8

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:28):

given what Apple is doing

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:28):

but yes, long and interesting chat

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:29):

ciao

view this post on Zulip Emilio Jesús Gallego Arias (May 26 2022 at 22:30):

Umm, webkit is hybrid MIT / LGPL

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (May 26 2022 at 22:32):

If Coq is your base, better be there, IMO.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Théo Zimmermann (May 27 2022 at 09:26):

BTW, it appears that PyCoq is missing a license entirely, which is even more problematic.

view this post on Zulip Karl Palmskog (May 27 2022 at 10:04):

@Théo Zimmermann it has a license in pycoq.opam

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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"?

view this post on Zulip 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).

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:11):

What's dynamic linking in the LGPL sense?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:12):

6.b)

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:12):

?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:12):

Yes it does ensure that, but we are talking about the GPL

view this post on Zulip Emilio Jesús Gallego Arias (May 27 2022 at 14:12):

the GPL says nothing about linking

view this post on Zulip Paolo Giarrusso (May 27 2022 at 14:14):

Ah, I was talking about the LGPL. Its prologue also explains the difference with the GPL:

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC