Ali Caglayan (Mar 27 2021 at 10:33): Ali Caglayan (Mar 27 2021 at 10:33):If I as a coq user modify a file from the stdlib to use in my own project, will I need to include the GNU header at the top?
Guillaume Melquiond (Mar 27 2021 at 10:39):No. However, that makes your work an obvious derivative of Coq's standard library (rather than just linked to it), and thus forces you to license your work as LGPL 2.1 (or GPL 2.1). But that might already be the case, in which case the point is moot.
Michael Soegtrop (Mar 27 2021 at 10:41):Anyway, I don't think it is a good idea to modify the standard library, except for experimentation. Since the standard lib changes, you will end up in a maintenance night mare or be bound to today's version of Coq. If you think something can be enhanced, do a PR.
Ali Caglayan (Mar 27 2021 at 10:41):So the current license in the HoTT library is: https://github.com/HoTT/HoTT/blob/master/LICENSE.txt
Ali Caglayan (Mar 27 2021 at 10:42):Specifically the files in question are just the Hexadecimal and Decimal datatype files that are used for printing and parsing numeral notations.
Ali Caglayan (Mar 27 2021 at 10:42):We replace all of the stdlib anyway
Bas Spitters (Mar 27 2021 at 10:50):@Michael Soegtrop Generally, I agree, but in this case, we use --indices-matter which breaks much of the stdlib.
In the future we'd like to have a version of Coq where HoTT is better integrated, but we're not there yet.
@Ali Caglayan is doing great work improving/simplifying the compilation of HoTT. This should also facilitate the work on HoTT in platform.
Michael Soegtrop (Mar 27 2021 at 10:56):BSD is not compatible with LGPL2, so I would say you have a problem here. It would probably be OK to create a separate standard library derivative which is then LGPL2 and ship this together with your BSD library, but it is not nice from a user's point of view. If it is not much, you might be better off rewriting it from scratch.
Ali Caglayan (Mar 27 2021 at 12:15):@Michael Soegtrop It really isn't much at all, but I am not sure what exactly would be "rewritten". It seems to me that there is only one obvious way to do it.
Here are the two files:
They total around 500 lines of code. They aren't really doing anything nontrivial, just a basic datatype for number notations to work.
Ali Caglayan (Mar 27 2021 at 12:19):So it seems kind of pointless to me to rewrite this as it will end up being the exact same code. I'm not sure what is gained here by doing so. What makes code "rewritten" or "derivative"? I have no idea 0:-)
Ali Caglayan (Mar 27 2021 at 12:22):To see where this issue is cropping up, have a look at:
https://github.com/HoTT/HoTT/pull/1429#discussion_r602563033
At the moment, my PR removes the copyright banner from the file. At what point can I change the file enough for it to be considered rewritten?
Gaëtan Gilbert (Mar 27 2021 at 12:27):you could say it's too trivial to have copyright
or you could ask the authors of those bits of code for a license
Mike Shulman (Mar 27 2021 at 12:28):Legally, I don't think one can "rewrite" something just to remove its license; otherwise you could nullify the copyright of a book by retyping it into your word processor.
Mike Shulman (Mar 27 2021 at 12:29):I expect what Michael meant is to go back to the documentation on numeral notations and create our own code from scratch.
Mike Shulman (Mar 27 2021 at 12:31):I also don't think code that does something substantial, like this, could possibly be considered too trivial to copyright.
Mike Shulman (Mar 27 2021 at 12:33):I notice that the license file https://github.com/HoTT/HoTT/blob/master/LICENSE.txt linked by Ali already says "except for files which contain a specific copyright notice and licencing information". If that's kosher, doesn't it already cover the files in question if we just leave the LGPL2 copyright notice on them?
Stefan Monnier (Mar 27 2021 at 12:34):If it is not much, you might be better off rewriting it from scratch.
A much simpler option is to use the LGPL-2.1 license instead of BSD. It requires no extra work of any kind (BSD already allows relicensing as LGPL-2.1).
Bas Spitters (Mar 27 2021 at 12:39):It would be better to rewrite the stdlib under a more permissive license. See the discussions around the coq-community license. LGPL is problematic for proofs in any case. @Théo Zimmermann has looked into these licensing issues in the past.
https://github.com/coq-community/manifesto
Maybe it's an opportunity for stdlib2 ?
Bas Spitters (Mar 27 2021 at 12:46):E.g. discussion with @Karl Palmskog here
Michael Soegtrop (Mar 27 2021 at 13:02):I have seen some instructions from GNU on how to rewrite Unix in a legally safe way. What I remember from this is e.g. optimize it in a different way. They said the original Unix code is mostly optimized for memory, so if you do something which is optimized for speed, you will end up with a different solution. But the interface of say GNU vs Linus make, sed, awk, you name it is fairly similar. I agree that it might be hard to come up with substantially different code here. But it does not have to be different. If someone writes the same code without having seen the original, it is fine.
Technically what is copyrighted is the result of a human creative act. So an alternative is to write a tactic which automatically creates the code from a spec. Then you can legally claim that it is not the result of a creative act. Well maybe in 10 years ;-)
Bas Spitters (Mar 27 2021 at 13:55):In this case we can perhaps make most progress by asking the authors @Hugo Herbelin @Théo Zimmermann @Pierre Roux to relicense their work under a more permissive license.
It's a pity of this hinders progress on the HoTT library and Coq platform.
Théo Zimmermann (Mar 27 2021 at 13:55):As already expressed above by @Bas Spitters, LGPL 2.1 is not a very nice license. BSD is much better, so I would find it sad to relicense HoTT to LGPL 2.1 for this reason. Instead, I suggest following what @Gaëtan Gilbert said, i.e. track down who are the authors of these particular files and ask them permission to include in HoTT under the BSD license.
Théo Zimmermann (Mar 27 2021 at 13:56):OK, so apparently, @Bas Spitters just did the tracking down. Cool!
Théo Zimmermann (Mar 27 2021 at 13:56):FTR I hereby agree to this inclusion and licensing under the BSD license.
Bas Spitters (Mar 27 2021 at 13:56):Pierre Letouzey and Vincent Laporte are not on Zulip...
Théo Zimmermann (Mar 27 2021 at 13:57):@Vincent Laporte is though.
Bas Spitters (Mar 27 2021 at 13:59):@Michael Soegtrop @Théo Zimmermann do you see a way forward where one could gradually liberate the coq libraries from LGPL and move to one of the recommended licenses?
Théo Zimmermann (Mar 27 2021 at 14:00):I considered proposing one way, based on an idea from https://gplcc.github.io/gplcc/.
Théo Zimmermann (Mar 27 2021 at 14:01):Basically, you add a clause saying that any contributor forward agrees to waive certain obligations from the original license (for their present and past work).
Théo Zimmermann (Mar 27 2021 at 14:02):But there might be issues with contributors who have switched employers.
Théo Zimmermann (Mar 27 2021 at 14:02):And anyway, we would need a specialized lawyer to draft this new clause.
Bas Spitters (Mar 27 2021 at 14:17):@Mike Shulman solution was proposed earlier, and it seems like the best way forward. Explicitly mention in the license file that all work in the repo is under BSD, except those two files which are under LPGL.
Ali Caglayan (Mar 27 2021 at 14:20):But I thought the problem was that the LGPL is incompatible with BSD, so even if we modify BSD to make the exception you describe, we will be breaking the original license...?
Ali Caglayan (Mar 27 2021 at 14:20):Honestly, I am more confused then when I started now :-)
Pierre Roux (Mar 27 2021 at 14:52):For Hexadecimal.v and the small part of Decimal.v I authored, I hereby agree to have them relicensed under the BSD license.
Mike Shulman (Mar 27 2021 at 14:59):One reason it's confusing is that the language of the LGPL thinks it is only being applied to code in a compiled language like C, e.g. "A library means a collection of software functions and/or data prepared so as to be conveniently linked with application programs (which use some of those functions and data) to form executables."
Mike Shulman (Mar 27 2021 at 14:59):Under that definition, it seems debatable to me whether it even can be applied to Coq source code. (-:
Mike Shulman (Mar 27 2021 at 15:03):According to http://www.gnu.org/licenses/gpl-faq.html#IfInterpreterIsGPL, libraries loaded by an interpreter should be considered "dynamically linked" to the code that uses them, and some people say that an LGPL library can be dynamically linked by e.g. BSD code.
Mike Shulman (Mar 27 2021 at 15:05):I guess maybe the question is whether by including these files in the HoTT/Coq repository we are making them part of HoTT/Coq, so that we get infected by their license, rather than keeping them as a part of the Coq stdlib that we link to?
Bas Spitters (Mar 27 2021 at 15:22):Precisely, that is the reason why LGPL is not recommended by the coq-community.
I believe the conclusion we reached before of clearly marking which files come with which license and then "linking" to them is in the spirit of LGPL, to the extend it applies to proofs at all.
Théo Zimmermann (Mar 27 2021 at 18:12):FTR LGPL is not "incompatible" with BSD: it is compatible because you can combine code under the two licenses to form a larger work under the LGPL license.
Théo Zimmermann (Mar 27 2021 at 18:14):Another thing to keep in mind is that LGPL is that the whole "dynamic linking" question is mostly irrelevant for open source software linking to LGPL code because it is only one technical way to abide by the license (and providing the sources is another one).
Théo Zimmermann (Mar 27 2021 at 18:16):Théo Zimmermann said:
FTR LGPL is not "incompatible" with BSD: it is compatible because you can combine code under the two licenses to form a larger work under the LGPL license.
To further clarify what I mean here: both the BSD2 and BSD3 licenses are compatible with the GNU GPL family of licenses. Only the original BSD4 license was not, but it is scarcely used nowadays. In particular, HoTT uses the BSD2 license (2 is the number of clauses, not a version number).
Guillaume Melquiond (Mar 27 2021 at 18:20):Théo Zimmermann said:
Another thing to keep in mind is that LGPL is that the whole "dynamic linking" question is mostly irrelevant for open source software linking to LGPL code because it is only one technical way to abide by the license (and providing the sources is another one).
It is mostly irrelevant for free software, not for open source software. There are a lot of so-called open source licenses that opens the source but do not allow the user to do anything with it (except maybe reading it). Those are wholeheartedly incompatible with the (L)GPL. Remember the early days of Microsoft's open source initiatives. That was some nice PR work.
Théo Zimmermann (Mar 27 2021 at 18:22):@Guillaume Melquiond When I use the term "open source", I mean, according to the definition of the OSD, which is virtually equivalent to the free software definition. I don't mean just "source available".
Théo Zimmermann (Mar 27 2021 at 18:24):I choose between "free software" or "open source software" terminologies if I need to make a philosophical distinction only (software that protects the user's freedom vs software that is developed according to the open source model).
Théo Zimmermann (Mar 27 2021 at 18:26):I should add that I disagree with @Bas Spitters's interpretation that you can put LGPL files inside a BSD library.
Here are the relevant parts of the LGPL (2.1) license that make it different from the GPL:
A program that contains no derivative of any portion of the Library, but is designed to work with the Library by being compiled or linked with it, is called a "work that uses the Library". Such a work, in isolation, is not a derivative work of the Library, and therefore falls outside the scope of this License.
However, linking a "work that uses the Library" with the Library creates an executable that is a derivative of the Library (because it contains portions of the Library), rather than a "work that uses the library". The executable is therefore covered by this License. Section 6 states terms for distribution of such executables.
Michael Soegtrop (Mar 28 2021 at 07:32):Bas Spitters said:
do you see a way forward where one could gradually liberate the coq libraries from LGPL and move to one of the recommended licenses?
I would read the license such that for all INRIA/CNRS employees, INRIA/CNRS itself is the copyright holder and not the individual authors. In the end this depends on what INRIA employees have in their contracts. The "and contributors" I would say applies to non INRIA people like me. Unfortunately Coq is so old that it was not common to have some legal treaties with contributors beyond what the LGPL license requires. So one would have to track down these contributors and/or remove their contributions.
If INRIA itself decides to take such a step, one would start with doing some statistics on GIT and whatever older SCCS was used before.
Bas Spitters (Mar 28 2021 at 09:21):@Théo Zimmermann the copies of the stdlib were introduced in the HoTT library at around 2012/2013.
People have contributed BSD2 code to it since then. So, with your interpretation, the library seems to have been in an inconsistent state for about a decade. I believe something similar happened with math-comp.
We have 150 students for the EPIT HoTT school in a few weeks, @Ali Caglayan 's PR would be quite useful then.
LGPL does not seem to be helping the Coq community...
Théo Zimmermann (Mar 28 2021 at 09:58):@Bas Spitters Don't let these licensing issues stop you: the state after the PR won't be any worse than before. Furthermore, remember that limitations of a license are only relevant if they are actually enforced. You can be pretty certain that no one on the Coq-side is going to sue anyone for not following the license to the letter. And even then, they would have to prove that there was an actual loss due to this.
Théo Zimmermann (Mar 28 2021 at 09:59):These licensing issues really become a problem when companies are involved, because they are shy of taking such bets, which could cost them a lot more.
Théo Zimmermann (Mar 28 2021 at 10:03):@Michael Soegtrop Maxime tried to track down the copyright owners with some Inria lawyer at some point. And it turned out that some French civil servant researchers may hold copyright themselves instead of their employers. But in the case of employees on a contract with Inria like me, the copyright is indeed held by Inria.
Bas Spitters (Mar 28 2021 at 10:11):@Ali Caglayan @Mike Shulman I think the statement by Theo is clear enough to proceed with the PR, isn't it?
Ali Caglayan (Mar 28 2021 at 10:20):So we should just continue as is and ignore licensing?
Michael Soegtrop (Mar 28 2021 at 10:22):I think at some point one should also spend some money for a solid legal expertise on what GPL and LGPL really say for software which is distributed in source form. I looked at it once and it doesn't seem to be a lot.
Michael Soegtrop (Mar 28 2021 at 10:23):I mean it might be that the whole license compatibility matrix looks entirely different for software which is distributed in source form.
Bas Spitters (Mar 28 2021 at 10:26):INRIA should have the competences for this, I think. Aarhus university would, if it would be one of our flagship's projects.
Gaëtan Gilbert (Mar 28 2021 at 10:33):IIUC coq isn't distributed only in source form, eg the debian package has .vo files
Bas Spitters (Mar 28 2021 at 10:33):@Ali Caglayan we make a best effort. State clearly in the LICENSE file that (only) those files around under LGPL and that the implications of LPGL on Coq source files is unclear to us. We could distribute them in a separate repo and link to them, but the authors do not seem to think that this burden on the users of the HoTT library would be warranted.
Ali Caglayan (Mar 28 2021 at 12:03):@Bas Spitters So the text in our license already seems to cover files which have their own copyright notice. Does this mean we just need to keep the copyright notice for those two files?
Michael Soegtrop (Mar 28 2021 at 12:23):Gaëtan Gilbert said:
IIUC coq isn't distributed only in source form, eg the debian package has .vo files
One could have different licenses for different forms of distributions, e.g. offer a way to compile from sources if this has legal advantages for someone. Also it might make a difference if the sources are delivered with the binaries. In the end we use the binaries more as a cache than as a method to obscurify the sources.
But I am not a lawyer. It s hard to say if a "binary delivery" is one which includes binaries or one which includes only binaries.
Stefan Monnier (Mar 28 2021 at 13:38):I think the intention behind the LGPL is sufficiently clear to be able to interpret it for a use case such as Coq: it's OK to use it in code which uses a license incompatible with that of LGPL under the condition that the end user can replace the LGPL code with some other version of it (e.g. to fix bugs, add new features, you name it). Clearly this can only be applicable if the new version is compatible with the old (i.e. the LGPL doesn't say that you should be able to plug in any random code and it should still work ;-). So I think it's applicable to systems with dependent types, although the dependent types may impose more stringent constraints. In the case where the Coq code is turned into an executable via extraction, the constraints shouldn't be significantly tighter than for non-dependently typed code.
In any case, I still fail to see a serious problem with the solution of converting the BSD code to LGPL (other than some vague expressions of dislikes).
Stefan Monnier (Mar 28 2021 at 13:41):IOW, the only real and concrete problem I see here is that some people dislike the LGPL ;-)
Michael Soegtrop (Mar 28 2021 at 14:05):Stefan said:
IOW, the only real and concrete problem I see here is that some people dislike the LGPL ;-)
The problem is more that taking LGPL code into another development and modifying it there (as discussed here) usually requires that this development also has a LGPL compatible license. And the main reason scientifically interested people have a problem with that is that GPL/LGPL2 and GPL/LGPL3 are incompatible, so there is no legal way to take and modify LGPL2 and LGPL3 source code into the same development. This can severely restrict scientific and other progress. Of cause one can link one program to both LGPL2 and LGPL3 libraries, but one cannot take modified sources.
IMHO LGPL and GPL was perfectly fine until the FSF managed to mess things up by making GPL2 and GPL3 incompatible.
Théo Zimmermann (Mar 28 2021 at 14:45):IOW, the only real and concrete problem I see here is that some people dislike the LGPL ;-)
I dislike it because it's one of the most complex license to understand (and I think I understand it). A testimony is the number of questions people ask about it, trying to understand all the corner cases. I don't have the same issue with the GPL licenses. It's really the "Lesser" clauses that make the whole thing utterly complicated. When weak copyleft licenses are wanted, I'd advise MPL 2.0 which is way simpler to abide by technically speaking. It's true though that the MPL 2.0 does not protect the user's freedom as well (in theory) but does the LGPL provide actual gains in practice?
Théo Zimmermann (Mar 28 2021 at 14:49):@Stefan And watch out that you are misusing the term "incompatible license" (if we take the meaning that the FSF puts behind that word as a reference). Saying that you can combine programs under two licenses (even if it doesn't leave you the choice of the license to apply to the larger work) amounts to say that these licenses are compatible. See https://www.gnu.org/licenses/gpl-faq.html#WhatIsCompatible
Guillaume Melquiond (Mar 28 2021 at 14:55):Théo Zimmermann said:
does the LGPL provide actual gains in practice?
We did sell some licenses to Flocq. Had Flocq been using the MPL or BSD licenses, I am pretty sure we would not have sold them. (The sell price was really low, but that is besides the point. It was more of a political statement: "If you want to use Flocq in closed source software, you pay.")
Stefan Monnier (Mar 28 2021 at 16:30):The LGPL has its share of downsides, but Michael's and Théo's counter arguments seem to confirm my claim that there is no "real and concrete" problem with it here, and since it's the license with which we have to live for the foreseeable future, the easiest is to go along with it.
Théo Zimmermann (Mar 29 2021 at 08:15):Guillaume Melquiond said:
Théo Zimmermann said:
does the LGPL provide actual gains in practice?
We did sell some licenses to Flocq. Had Flocq been using the MPL or BSD licenses, I am pretty sure we would not have sold them. (The sell price was really low, but that is besides the point. It was more of a political statement: "If you want to use Flocq in closed source software, you pay.")
I see. But I was actually asking about actual gains in terms of freedom.
Enrico Tassi (Mar 29 2021 at 08:55):LGPL lets you use a library in a proprietary software at the price of giving back fixes or improvements to that library only. If you measure the "freedom" of a license as the inverse of the constraints it puts, then of course there are licenses which are more free, but it is not that clear that these licenses are better at fostering a community or a piece of software. To me, a piece of software that is free but does not work properly, or is lagging too much behind the standards, is not making anyone's life better or "more free". Maybe copyleft is not the best way to convince clients of the library to give back, but the objective is quite reasonable to me, and the deal quite fair.
Bas Spitters (Mar 29 2021 at 09:03):I believe one of the current problems with LPGL is that we do not have a consensus on how it applies to Coq code.
E.g. the meaning of 'linking'.
Enrico Tassi (Mar 29 2021 at 09:24):Why would .v files be different than, say, .py files, with respect to that?
Bas Spitters (Mar 29 2021 at 09:42):@Enrico Tassi I don't know there would be a difference, but see the unclarity in the discussion above.
Guillaume Melquiond (Mar 29 2021 at 12:16):I don't think the situation with linking is that bad. On the contrary, Coq makes it so that it is even more in the spirit of the LGPL than what the license was originally designed for. Indeed, terms that end with Qed are, by the logic of Coq, freely exchangeable (universes notwithstanding). So, that really follows the original spirit of the LGPL, which is that one can freely link to a library as long as one could reasonably replace this library with a homegrown one.
Now, there is the issue of the Defined terms, which are akin to inline template code in C++ and one of the reasons the LGPL is sometimes deemed to not be suitable for modern programming languages. Here, the simple fact of writing a library with the same interface presumably infringes on the copyright of the original library, as far as the Defined terms are concerned. So, it really depends on whether these transparent terms are deemed trivial enough to not be copyrightable, in which case the LGPL still applies perfectly to Coq libraries.
Michael Soegtrop (Mar 29 2021 at 12:17):@Enrico Tassi : do you have a reference on what LGPL means for Python files?
Enrico Tassi (Mar 29 2021 at 12:18):No, I was just suggesting to look at what more widespread languages do. AFAIK "import" mean link.
Stefan Monnier (Mar 29 2021 at 12:31):I see. But I was actually asking about actual gains in terms of freedom.
Not being able to use it willy-nilly in proprietary code is a "gain in terms of freedom".
Bas Spitters (Mar 29 2021 at 13:20):@Stefan I believe full names are preferred here. What's your background in Coq?
Théo Zimmermann (Mar 29 2021 at 13:26):This is Stefan Monnier (https://www.iro.umontreal.ca/~monnier/), one of the former maintainers of Emacs and also a contributor to Proof General.
Bas Spitters (Mar 29 2021 at 13:50):Hi @Stefan Monnier , glad to see you here :-)
I guess the emacs background explains your understanding of the (L)GPL issues.
Michael Soegtrop (Mar 29 2021 at 13:53):@Stefan Monnier: I agree that copyleft licenses are desirable. Again my argument against GPL / LGPL is the major havoc the incompatibility between GPL2 and GPL3 caused. There are many good open source projects which suffer from this. To give an arbitrary example: there is a GNU library for handling major CAD file formats which is GPL3. And there is a GPL2+ CAD tool which uses a geometry library which is GPL2 (without + for historic reasons and this can't be changed because former contributors are not available) and for this reason can't use the GPL3 GNU CAD file import library. Where is the advantage for anybody in that?
Everything would be perfect, if there wouldn't be the GPL2/GPL3 incompatibility. I understand the argument of the FSF that everything should migrate to GPL3, but there are projects which use GPL2 without + libraries and are stuck. In essence the major fault of the FSF was to not upfront include a term in GPL2 which would have made it equivalent to GPL2+.
Of cause later one is always smarter, so one can't really blame the FSF for that. But the damage to the copyleft world is done, and I think this is what drives people away from copy left towards permissive licenses.
Stefan Monnier (Mar 29 2021 at 14:05):I have no intention to defend the LGPLv2 -vs- GPLv3 mess up [ But I do strongly suspect that this is not the main reason that drives some people away from copyleft. ] I'm only talking about the immediate case under discussion, where clearly the easiest solution is to convert the BSD code to LGPL, and that it does not suffer from any clear and concrete problems (since I don't count lack of popularity as a problem). IOW it's the pragmatic thing to do.
Théo Zimmermann (Mar 29 2021 at 14:35):FWIW Coq is not truly stuck on the LGPL 2.1 license since there exists an upgrade path from LGPL 2.1 to GPL 3:
- You may opt to apply the terms of the ordinary GNU General Public License instead of this License to a given copy of the Library. To do
this, you must alter all the notices that refer to this License, so that they refer to the ordinary GNU General Public License, version 2, instead of to this License. (If a newer version than version 2 of the ordinary GNU General Public License has appeared, then you can specify that version instead if you wish.) Do not make any other change in these notices.
Should we choose then to migrate Coq and all its ecosystem to GPL3? No, of course! And I say this as someone who thinks that for many pieces of software, GPL3 (or even AGPL3) is the most appropriate license.
Last updated: Sep 28 2023 at 11:01 UTC