-
Notifications
You must be signed in to change notification settings - Fork 40
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Licensing needs to be clarified #266
Licensing needs to be clarified #266
Comments
@ejgallego if you want my opinion, I think the whole thing (code, documentation, etc.) should be dual licensed under LGPL-2.1-or-later and GPL-3.0-or-later. If this can't be done, e.g., because some code comes from Coq itself, then I think the whole thing should be LGPL-2.1-only. |
Hi folks, indeed the current licensing situation is not good, thanks for bringing the issue into my attention. I can't think about this today, but added to my todo list. |
@SnarkBoojum I will first most of the issues, I think at this point I only have one question. LGPL2.1 does allow you to also pick GPL2.1 and GPL3+ , by virtue of its clause 3, so I guess that indeed I should just write LGPL2.1 and not LGPL2.1+, right? In fact, this is how the whole thing works, when you build sertop, the whole of it (which includes Coq) becomes GPL3 thanks to this licensing provision in LGPL2.1 IIUC. Is my reasoning correct? |
Yes, it is also my understanding that you can combine files under LGPL 2.1 and files under GPL 3+ and the overall thing is GPL 3+. |
In fact you can combine or even relicense the whole of Coq to GPL 3 if you want, if I read the clause correctly. |
Well, I just know that when several license assignments apply to the same file (from the main LICENSE file, from the top of the file itself and from below in the file itself), that's just very confusing! |
@SnarkBoojum , what is the tool to check that LICENSE format is correct? |
The sentence lines 21 and 22 of LICENSE looks strange: shouldn't the start read "In some cases," ? The tool to check the LICENSE file is named 'lintian'. Thanks for the clarification! |
Thanks, fixed! Let me know if we need further fixes, I want to release today as the Coq Platform is waiting for a release hence the quick merge. I agree the wording was confusing, Coq and its derivatives are already GPL 3 if desired, I think now the file looks simpler. The reason the jsCoq are GPL / AGPL 3 is to avoid people putting them as a service. I am familiar with Debian licensing procedure (subscribed to debian-devel for more than a decade) , there should be no problem getting SerAPI in Debian.
Oh, I didn't think lintian for checking the license file, unfortunately I wasn't able to run it in the repos as is, not sure what the right set of options is. If you can run it and send me the report I'll try to fix the problem. |
Ok, I finally packaged all deps for coq-serapi in Debian ; unfortunately, the licensing is still pretty... fuzzy. Here are special notices:
Here is my current debian/copyright for the would-be package I don't feel confident to submit yet:
|
@ejgallego just to flag up that as per discussion on Zulip, this issue is preventing packaging of coq-lsp on Debian. |
Thanks for the reminded, I didn't have time to work on this. I'll push an update to update a couple of things:
(*) The historical reason I did copy some code from JS libs is that back in 2016, |
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers - Move JS files to its own util files (can be also removed in favor of `base` these days)
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers - Move JS files to its own util files (can be also removed in favor of `base` these days)
I guess only 8.19+0.19.0 will be fixed? In that case, I guess I'll be able to rework my serapi packaging just after I'll have made the transition to Coq 8.19 in Coq. |
Hi @SnarkBoojum , I'm happy to fix also older versions; lack of time is a problem tho. But I need to release a new 8.18 version. |
Coq 8.18 is in Debian and I think I'll start wondering about packaging coq 8.19 in about a week so that's why I'm interested in 8.19+0.19.0 - it would fit into my Debian work schedule. |
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers to a single uniform header - Move JS file to its own file, note that on license.
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers to a single uniform header - Move JS file to its own file, note that on license.
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by Julien - Fix file headers to a single uniform header - Move JS file to its own file, note that on license.
CHANGES: - [serlib] Support `btauto` Coq plugin (@ejgallego, rocq-archive/coq-serapi#362) - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n, rocq-archive/coq-serapi#375, fixes rocq-archive/coq-serapi#371) - [general] Make licensing clearer (@ejgallego, @palmskog, @SnarkBoojum, rocq-archive/coq-serapi#361, closes rocq-archive/coq-serapi#266)
CHANGES: - [serlib] Support `btauto` Coq plugin (@ejgallego, rocq-archive/coq-serapi#362) - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n, rocq-archive/coq-serapi#375, fixes rocq-archive/coq-serapi#371) - [general] Make licensing clearer (@ejgallego, @palmskog, @SnarkBoojum, rocq-archive/coq-serapi#361, closes rocq-archive/coq-serapi#266)
I found two remaining unclear things:
That shouldn't prevent me from packaging for Debian, so I'll work on it ; here is the debian/copyright file of the would-be package:
|
Thanks @SnarkBoojum , fixed in |
I'm working on packaging coq-serapi for Debian, and things are pretty annoying:
I don't think a package for the code as-is stands any chance to enter Debian -- the question of licensing & copyright assignment is taken too seriously to accept such contradictory informations.
Can you clarify matters in the code then close this issue?
The text was updated successfully, but these errors were encountered: