Replace CoRN's license by Coq's license #99
Conversation
|
For the reasons I gave in the related PR, I think that if an effort is made to relicense CoRN, the goal should be a more permissive license than LGPL. |
|
@Zimmi48 Because CoRN |
|
Fortunately, it doesn't work like this. But you are perfectly illustrating my point on the LGPL being a complex license to understand. (I can come back to this and write a—long—explanation if you wish.) |
|
@Zimmi48 Who is interpreting the license now ? You say that LGPL is complicated so we should avoid it, but eventually CoRN imports files from the standard library. If there is a problem with LGPL, by using the MIT license you would wrongly let CoRN users assume more permissions than they actually have. What I propose is much simpler : one license for both Coq and CoRN. |
I am. But I'm relatively confident in my interpretation of standard open source licenses based on my experience reading about them and discussing them.
Let us be specific. No open source license (be it MIT, LGPL or GPL) places any restriction on how you can use a piece of software. Software licenses that do place restrictions on usage (like CompCert's Non-Commercial License) are non-free and non-open source. Open source licenses restrict how you may redistribute the software or a derivative. For instance, with a copyleft license (like the LGPL) you may not distribute a binary version without also making the sources available, and if you create a derived version, you may be bound by the same restrictions. If I distribute Coq + CoRN, of course, I am bound by the terms of Coq's license. However, if I distribute only CoRN, I am only bound by the terms of CoRN's license. So it makes a difference.
I agree that what you propose is very simple. However, my point (which was previously raised by @robbertkrebbers) is that if you go through the burden of relicensing CoRN, you may as well go one step further and choose a more permissive license. If some day, Coq's standard library itself is relicensed under a more permissive license (which would be difficult but not impossible), it would be sad to have to conduct again the same relicensing process for CoRN. Choosing a permissive license that allows relicensing (like MIT or BSD) now guarantees against such issue. |
@Zimmi48 Great, let's keep it simple. This is complicated enough already.
This is not happening, you know it as much as I do. |
Well, I don't know it, so I wonder how you can be so sure.
Well in any case, I'd oppose to relicensing to LGPL-2.1-only. At the very least, make this LGPL-2.1-or-later. |
|
@Zimmi48 The option to use a later version of the license is already given in each file By the way, that means we need to modify all the files, replacing "GNU General Public License" by "GNU Lesser General Public License". I do not know how to modify |
That's correct. And "version 2" should become "version 2.1".
You only need to change two lines: Lines 75 to 77 in 9db8c9e The identifier should become Then files can be regenerated using: (cf. https://github.com/coq-community/templates/blob/master/README.md) But it would be best to merge #97 before doing this. Can you answer my question over there? |
|
@Zimmi48 Is it good now with meta.yml modified and the templates regenerated ? |
|
Note that you probably had a slightly outdated version of the templates, leading to the (spurious) change to |
|
@Zimmi48 I regenerated the templates and |
|
This time it is the Nix builds which are failing because of the changes to |
|
@Zimmi48 Now branch master builds, but not the previous branches |
|
Cf. my comment just above. |
Replace license notices Update meta.yml
Would it make sense to have multi-licensing? This seems to be considered in some situations. More generally, why one licence for the whole repository, rather than one (or more) licence per file (if not per Coq declaration). If the problem is a problem of compatibility, we could treat it with the same kind of granularity as we treat e.g. option |
|
Multi licensing could be a possibility, but there doesn't seem to be a reason to go for LGPL, over MIT/BSD. |
|
Thinking at this licensing issue, there is something I still don't understand. Here, we are only talking about source code, while combining license is about building binaries, right? For instance, according to GPL's FAQ What is the difference between “mere aggregation” and “combining two modules into one program”?, two binaries which interact through a communication channel rather than being linked together can be combined whatever the license of the other is if one is GLP. So, having Coq source code in different licenses such as GPL, LGPL or MIT seems to be no problem. The burden is put on who wants to make a binary executable out of the code having different licenses: they will have to make the components whose licenses are incompatible to communicate over a channel rather than by linking. Is this interpretation correct? And if yes, is this constraint put on who wants to create a binary out of Coq code so critical? One may also wonder whether distributing source code should satisfy that the licenses of every code present in the distributed archive have to be compatible. Still according to the GPL FAQ above, it is ok to put side by side a GPL program with a distinct program having any other license on the same CD-ROM. So, it is a fortiori ok to do so for the sources of the programs (and we actually already do it for the platform). TL;DR: From the Coq point of view, I don't see problems with incompatible licenses other than forcing people interested in producing binaries to have the incompatible binaries in separate processes, and, for compatible licenses, to adopt the license resulting of this compatible match. The remaining questions are then "political". Do we want to force people possibly producing binaries (such as a certified compiler with a floating point component) to have these libraries communicating over a channel rather than being linked? In practice, it is not even sure that it matters, since the executable part of CoRN, which is the part liable to be linked in a binary, is already MIT. Then, the actual licence incompatibilities I know regarding real numbers are with Flocq and Coquelicot, but, since there are less developers involved here, it may be easier to change the license of these packages, say, from LGPL 3 to LGLP 2 or any later version so that any combination of code related to real or floating-point numbers become acceptable as part of a same binary. |
|
If someone wants to build a certified piece of software they may be interesting to depend on more than one Coq library. If they do so, then they create a derivative work of the various libraries they picked. If these libraries' licenses are not compatible, they won't be able to do so. It's as simple as this. Discussing workarounds like having two independent programs communicate on a textual channel doesn't make sense in a software verification context IMHO. Furthermore, no, combining is not just about binaries. If it were, then programs in interpreted languages wouldn't be submitted to the same kind of constraints than the rest. It would also mean that people could write proprietary code that depends on a GPL'd library and distribute the two side by side (as source code) and put whatever restrictions they want on the code they wrote. |
|
Corn has had MIT code in the fast/ directory since 2007. |
|
@Zimmi48, I'm concerned by the current CoRN situation but I don't have a strong experience with licenses, my apologies. My feeling, especially after Abhishek asked his license question recently on Coq-Club, was that there was no clear consensus on what a software license should exactly imply in the context of formal proofs. Is there some jurisprudence to rely on? So, regarding the MIT-licensed part of CoRN, should we consider that it is a non-sense to have part of the MIT-licensed directory of CoRN to depend on the part of CoRN marked as GPL without being itself GPL? |
No, I believe that it is OK to put some part of the code under a more permissive (and GPL-compatible) license, as long as it is clear to everyone that the "larger work" resulting from the combination of the two differently-licensed parts is GPL licensed. |
|
Then, what is the problem in distributing the GPL 2 part of CoRN, the MIT part of CoRN, and the LGPL 2.1 stdlib as part of a same repository? The constraint is only on who wants to "combine" the different parts? As for the case of the platform, is it ok to distribute an archive which contains both GPL 2 and LGPL 3, even though they are incompatible? |
There is no problem at all. It's just that if one wanted at some point to move some CoRN code to the Coq repository, it wouldn't be possible if that code is under GPL. Furthermore, managing several licenses in a single repository creates more maintenance burden (you cannot easily move code between the various parts) and more confusion for the users.
Yes, this is not a problem. In this case, it would really be considered as side-by-side distribution, pretty similarly to your earlier CD-ROM example. Of course, problems arise if users want to use several libraries that are incompatible license-wise in a single project, so this should still be a concern for the platform maintainers. In practice, I don't know of any such examples since CoRN is the only Coq library I know which is under GPL and it is not under GPL-2-only, it is under GPL-2-or-later as testified by the headers of those files under GPL. |
Ah right. I looked at the main LICENCE file which says GPL 2, and I did not see the "or later" in each file.
This is exactly the kind of things which confuses me. Since we are only talking about files with full source information, where is the limit between "side-by-side" and a "single project"? This seems to be rather a matter of convention. We could organize things as CoRN-A and CoRN-B, or Platform-CoRN and Platform-Flocq, or Platform-CoRN-A, Platform-Corn-B and Platform-Flocq. It seems in last analysis to be only about how "people" perceive things as going together or not. Am I missing something? Similarly, if it is ok to have both MIT-licensed and GPL-licensed code in the CoRN library, why couldn't it be possible to mix licenses also in the Coq repository? |
Ultimately, yes, interpreting law, contracts and licensing is about how people perceive things. However, there is a key difference here between distributing a set of packages in a single bundled and creating a project that needs to import two libraries to be evaluated. Only the later kind is an example of a "larger work".
The only limitation would be the one that we, as Coq maintainers, choose to impose. I would personally be OK with accepting that clearly defined and limited components are put under a more permissive license (in fact that was the case for |
I can understand this, but how much does this matter in practice if it can just be instead two repositories or a repository of repositories? By the way, is the licence of camlp5 LGPL-compatible for instance? For instance, to be extreme, why don't we attach license to theorems (as proposed above), reflecting what the contributor of the theorem intends. As far as I understood, this is actually what basically happened to CoRN. If I understood correctly, mostly nobody cared about a license, except two persons. When CoRN was already quite big and had still no license, one proposed to use GPL and the others agreed because they did not care. But another (more recent) contributor (then followed by a group of developers) used MIT for his (their) own work. Told otherwise, as soon as what matters is source code, which is the case for us, if we would not want to do politics regarding how this source code might eventually be used, we may also welcome contributors as they are and accept any license for any (distinct) contribution. (I'm not saying that we don't want to do politics though!) |
|
@herbelin your description of the history is correct. In fact, I'm aware of only one strong GPL proponent, who has since long left academia. |
FYI, the license of camlp5 is what is known as 3-clause BSD (BSD3 for short and BSD-3-Clause in the SPDX classification) and yes, it is compatible with the (L)GPL licenses.
Most people have no idea what licenses entail, and as I explained above, the more licenses you get, the more complicated you make the life of both users and maintainers. Of course, in an extreme world like the one you propose, one would develop additional tools to make license management bearable and would actually limit the choice of licenses to have a gradation but no equivalent and incompatible licenses. Anyway, the most reasonable approach which a lot of people support today is that it's good to consolidate an open source community around a single open source license (see the first proposition of https://choosealicense.com/). Unfortunately, the historically preferred license of the OCaml (and thus Coq) communities have been LGPL-2.1(-only) which as I've explained somewhere else is a technically complex license that is not the best suited for Coq (nor OCaml) libraries. Given that the community is far from united around this license anyway, I think it make sense to start actively promoting other licenses such as the permissive (and very popular) MIT license or the weak copyleft (but simpler to understand than LGPL) MPL-2.0.
But will this author agree to relicense their work under a more permissive license? Otherwise, this whole relicensing enterprise is bound to be never complete. |
|
He seems to have disappeared from the internet. There are no papers
describing substantial contributions to the corn library.
…On Mon, Aug 3, 2020 at 2:34 PM Théo Zimmermann ***@***.***> wrote:
By the way, is the licence of camlp5 LGPL-compatible for instance?
FYI, the license of camlp5 is what is known as 3-clause BSD (BSD3 for short and BSD-3-Clause in the SPDX classification) and yes, it is compatible with the (L)GPL licenses.
For instance, to be extreme, why don't we attach license to theorems (as proposed above), reflecting what the contributor of the theorem intends.
Most people have no idea what licenses entail, and as I explained above, the more licenses you get, the more complicated you make the life of both users and maintainers. Of course, in an extreme world like the one you propose, one would develop additional tools to make license management bearable and would actually limit the choice of licenses to have a gradation but no equivalent and incompatible licenses. Anyway, the most reasonable approach which a lot of people support today is that it's good to consolidate an open source community around a single open source license (see the first proposition of https://choosealicense.com/). Unfortunately, the historically preferred license of the OCaml (and thus Coq) communities have been LGPL-2.1(-only) which as I've explained somewhere else is a technically complex license that is not the best suited for Coq (nor OCaml) libraries. Given that the community is far from united around this license anyway, I think it make sense to start actively promoting other licenses such as the permissive (and very popular) MIT license or the weak copyleft (but simpler to understand than LGPL) MPL-2.0.
@spitters
I'm aware of only one strong GPL proponent, who has since long left academia.
But will this author agree to relicense their work under a more permissive license? Otherwise, this whole relicensing enterprise is bound to be never complete.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub, or unsubscribe.
|
|
Does this mean that you would remove his code from CoRN? |
You are inverting the situation. Actually, it is the GPL of CoRN that "forces" the combination of Coq and CoRN to be GPL, under two different possible mechanisms (any person distributing such a combination can choose which mechanism to use). Under section 6 of the LGPLv2.1, one is allowed to link an LGPL-covered work (such as Coq and/or its "theories" standard library) with any other work (such as CoRN), and redistribute the combination, with some quite weak conditions on the licence of the "other work". The GPL fulfils these weak conditions. In effect, the license of the result of the combination of Coq and CoRN is the GPL. ("Obviously" if one takes out Coq without CoRN from the combined work distributed under section 6, then that copy of Coq can be used and redistributed under the LGPL.) This is the same mechanism that allows a closed-source program, distributed as binary executable code only, to link dynamically against an LGPL-covered library. Or a free-as-in-free-speech / open source software under a GPL-incompatible license to do the same. Another path for this specific case is that LGPL section 3 allows any person having a copy of Coq to redistribute that copy under the GPL. Then you have a GPL Coq and a GPL CoRN, and the combination is covered by the GPL. That path is specific to GPL, it doesn't work for any other license. |
To guard against such issue, no need to relicense to a non-copyleft license. You only need to change the license of CoRN to "Lesser GPL v2.1 or later, or, at your option, the license of the Coq standard library (theories directory as of time of writing)". Provided all copyright holders agree, that is not more work than relicensing to "Lesser GPL v2.1 or later". In other words, "Lesser GPL v2.1 or later, with the added permission that you can also choose the same licence as the Coq Standard Library (theories directory)". In effect the copyright holders say they trust the Coq copyright holders to make good choices in the future, and delegate to them collectively together (not individually) the power to relicense CoRN. A more complicated setup which works in other scenarios is to give that power to an identified institution or group of persons... The Free Software Foundation, the Radboud University, the group "Bas Spitters and Robbert Krebbers and Herman Geuvers", the CNRS, the NWO or whatever the copyright holders collectively choose. I don't think that is a good setup for CoRN, but if that's what other people want, I'm willing to consent to a reasonable identified institution or group of people. |
Well, this harks back to the question "why is CoRN under the GPL in the first place?" and the related "why is Coq under the Lesser GPL, rather than MIT/BSD/..."? For me, it is linked to a certain view of scientific progress and the role you have (and I had at the time) as academics. That things are done incrementally, by standing on the shoulder of giants, and we add the common pot of humanity's advancement and knowledge. And whether, or not, people should be allowed to make use of that common pot without contributing back their work to that same common pot. That used to be "obvious"; Newton and Leibnitz never had to worry whether someone making improvements on the calculus the developed would use the improved calculus for personal gain, but forbid others from further improving the improved calculus. Bohr and Heisenberg didn't have to worry that people making refinements to their Copenhagen interpretation of quantum mechanics would forbid other people to make further refinements. The idea would have seemed outlandish, bizarre and just not possible. We now live in a world where that is not obvious anymore. And thus, as far as we intend our work to be in an ecosystem of "common pot", we have to use mechanisms like copyleft to express that. There is a strong copyleft (the GPL) and a weak copyleft (the Lesser GPL). The argument, which is being made, that CoRN would be better served by being under a weak copyleft doesn't mean we to throw away the baby with the bathwater and abandon all expression of the common pot ecosystem, going all the way to no copyleft at all. Secrecy of knowledge is so abhorrent to humanity and progress of humanity, that about a century (and a half?) ago, when secrecy of new ideas was a concrete problem, leading to loss of progress when people died, humanity devised a system, and agreed to make sacrifices, to entice inventors of new ideas to make them public, through the patent system: give the inventor a temporary monopoly on usage of his idea, in exchange for making the idea public. That was the basic deal. Under the same basic position (abhorrence of secret of ideas leading to progress), we use copyleft to discourage secrecy. |
OK, thanks. Following @lmamane's comments, I would like to add two comments. To mitigate the situation, it is probably worth to replace the discussion in an historical context which changed in the last 20 years. At some time, part of the academic world was pretty irritated by the closed attitude of some big software companies (as witnessed by critical books and posts at this time). That justified, in reaction to these attitudes, to strongly defend strict copyleft policies. Some of these companies learnt from it and started to support open source software (e.g. acquiring GitHub), reducing this feeling of a conflict between proprietary and open source software. On the other side, the emergence of startups in domains close to us, and sometimes from colleagues, contributed to the idea that it is legitimate for such startups to protect their source, at least temporary, so that they can simply live from their work. Another aspect whose impact on the current ways of thinking I'm not able to quantify is the role of "permissive" approaches to licensing such as the one defended by the widely spreaded interpreted language Python. My second comment is a question: do we have a clear idea of the impact of a license in our field? At the technical level, I see at least two situations where an entity might want to keep a Coq development secret.
In the latter, I neglect the moral aspect. If the intent of the author of the strong copyleft license is to force works depending on it to be released with sources, it might be unwelcome to bypass this intent and be (morally) dommageable to release without sources. On the other side, the strong copyleft might be considered too constraining for who wants to release executables without releasing the sources and move them to rely on other, more permissive, dependencies. Yet on another side, good ideas kept secret do not remain secret for long. For instance, proprietary spreadsheets or word processors did not so much prevent the development of open-source similar softwares. Proprietary drivers did not significantly prevent developing open-source versions of these drivers. This is a question of time, and a natural swing of the pendulum, which we can see in other situations (e.g. the current reactions to an excess of tracking of internet users). At the end, my feeling is that what really matters is not the technical impacts but the moral impact (and a regular attention that no actors abuse their power). Back to the PR, I see that several people would feel more comfortable with sending the message of a more permissive license, either MIT-like, or LGPL 2.1, or "Lesser GPL v2.1 or later, or, at your option, the license of the Coq standard library (theories directory as of time of writing)". Do we then try to go for the latter, which after all seems reasonable? Then, an appropriate mail to CoRN developers could be prepared. |
|
Thanks Hugo for the careful response. I believe it's accurate. |
|
Which contributors are missing, or more relevantly, for which parts of CoRN do we not have permission yet? |
|
I think I have something to add about H.Herbelin's comment : if you extract a software from whatever source files in a language Foo to sources in a Bar language -- then the sources in the Bar language are not the sources from your project. So if you release a final product which links against a GPL software, any user can ask you for the sources, and you can't give only the Bar-language ones -- you will have to provide the Foo-language ones. |
For better interactions with other Coq libraries, use the same license as Coq, which is LGPL 2.1. This pull request replaces CoRN's LICENSE file by Coq's LICENSE file and changes the license notice in each file, replacing "GNU General Public License" by "GNU Lesser General Public License" and "version 2 of the License" by "version 2.1 of the License".
To each copyright holder: please write in this pull request that you accept this modification of the license, applicable immediately after this pull request is merged into CoRN's repository. Please state your full name next to your github user name, so that it is easier to identify yourselves.