coq-library-undecidability
coq-library-undecidability copied to clipboard
uds-psl
Consider changing to a permissive or weak copyleft license
To enable easier reuse of this library, please consider changing its license to a permissive license like MIT or a weak copyleft license like MPL-2.0.
The issue with strong copyleft such as CeCILL-2.1 is that clients of the library will need to change their licenses to a strong copyleft license like CeCILL-2.1 itself or GPL, which they may not be prepared to do.
Changing this library to a permissive or weak copyleft license is (at least currently) a prerequisite for addressing https://github.com/uds-psl/coq-library-fol/issues/2
Thanks a lot Karl for bringing this up!
I'm in favour of changing the library to the weakest license possible: MIT. In the end, we want as many people as possible to use our library :) @DmxLarchey @mrhaandi, do you have opinions on this?
@palmskog (cc @yforster @mrhaandi)
Would a license like CeCILL B (targeted for libraries) be more convenient wrt to the issue you raise?
@DmxLarchey CeCILL-B is definitely a step in the right direction for reuse compared to CeCILL-2.1, but the problem with it is that it's incompatible with GPL, as stated by the Free Software Foundation themselves:
The CeCILL-B is a free software license. It is incompatible with the GPL because it has requirements that are not present in the GPL. The credit requirements in section 5.3.4 exceed those of the GPL. It also has a strange requirement that you use your “best efforts” to get third parties to agree “to comply with the obligations set forth in this Article.” Please do not release software under this license.
What this means in practice is that if someone has a library licensed under say GPL-2 or GPL-3 and they use your library, then they can't legally distribute the resulting .vo files. You can see some advice from @zimmi48 on CeCILL-C/B licensing for another project here.
CeCILL-B is definitely a step in the right direction for reuse compared to CeCILL-2.1
Given the reason that you provide in the rest of your message, I think we could even debate if CeCILL-B would really represent a step in the right direction.
Despite the appeal that they may have (my first open source project was initially published under a CeCILL license), the CeCILL licenses may be considered as an aborted experiment. Only the CeCILL v2 license is an acceptable (and OSI-approved) open source license, but it is a copyleft license, so it may not be suitable for a library aiming at getting the broadest audience. The fact that only the basic CeCILL license got a v2 update, but not the -B and -C variants shows a lack of commitment from the French public institutions that created these licenses to support them in the long run.
Given the reason that you provide in the rest of your message, I think we could even debate if CeCILL-B would really represent a step in the right direction.
I guess I should have been more precise. I think it's a step in the right direction based on the empirical evidence that CeCILL-B based projects can have many users (see MathComp). At a personal level, I also find strong copyleft licenses for Coq projects very difficult to abide by - almost any mode of "use" of a Coq project can be argued to create a derived work, due to conflation of compile-time and runtime. So I'm personally more inclined to reuse a CeCILL-B project than a GPL-3.0 or CeCILL-2.1 project, even when taking the GPL-incompatibility of CeCILL-B into account.
I'm in favour of changing the library to the weakest license possible: MIT. In the end, we want as many people as possible to use our library :)
I agree.
I am also Ok to move to a more permissive license. However, it seems to me that the MIT license does not imply that the user has to provide the source code of the modified software code, but only the copyright notice. Do I understand this well?
From my point of view, if I provide open source software, I ask for its derivatives to be open source as well. The only case I could accept the software I did write not available as source code is when it is included as a library w/o any modification, hence simple reference to the original file is enough.
In the usual parlance around open source licenses, permissive means that there is no requirement for derived works to be open source if they are distributed (but they may have to include a copyright notice, like in MIT). This applies to CeCILL-B as well, which is considered a permissive license but with some quirks around the notices.
If you want to control the license derived works are distributed under and still be open source, then this kind of license is called weak or strong copyleft. The former is represented by LGPL variants (2.1, etc.) and MPL-2.0, and the latter by GPL variants (2.0, etc.) and CeCILL-2.1. As I argued above, strong copyleft often makes it unfeasible for people to even use a Coq library, since they will typically need to relicense their own projects.
Weak copyleft as in MPL-2.0 at least allows clients of a library to keep their existing licenses, but they will have to distribute any modifications of the library under the library's license. So it sounds like you want a weak copyleft license, @DmxLarchey.
In Coq-community, we consistently recommend MPL-2.0 over LGPL for those who prefer weak copyleft due to the length and complexity of (abiding by) LGPL.
Ok @palmskog, sorry for the confusion around my non-standard use of the word permissive. I am ok to move to MPL-2.0. Would there be any trouble to distribute the code under a dual license, ie MPL-2.0 and CeCILL v2? Perhaps it would not make sense.
For me this implies modifying headers of a lot of files so I rather not repeat the work several times. @yforster and @mrhaandi would you be ok with such a move. In that case, I would only migrate the current living branch, namely the coq-8.17 branch.
In that case, I would only migrate the current living branch, namely the
coq-8.17branch.
For migration, I'd suggest the master branch, which will be coq-8.18 (I guess we are waiting for metacoq).
Would there be any trouble to distribute the code under a dual license, ie MPL-2.0 and CeCILL v2?
@DmxLarchey to my knowledge, dual licensing MPL-2.0 and CeCILL-2.1 does not lead to any immediate legal issues. However, dual licensing in general can be confusing to users, not least since the rights and obligations may be different depending on the license they choose. So my general recommendation would be to only use a single license.
My understanding is that MIT and MPL are relatively similar, but the difference is that if somebody changes our code, they have to publish this code under MPL license again. Using our code works under any license though.
I'm happy with that, so I'm all for changing to MPL.
As Andrej suggests, better do it on the master branch. And thanks for mentioning that we're missing a coq-8.18 branch - I started the creation of one for MetaCoq.
For future reference, here is a list of the most recommended open source licenses, in a gradation from the strongest copyleft (AGPL 3.0) to the most permissive (Unlicense): https://choosealicense.com/licenses/
This screenshot of this page shows that MPL 2.0 and MIT are not that far, but there are still several differences. By comparing the colored dots, you can notice that MPL 2.0 additionally includes a "patent grant" (this is systematic in longer-form modern licenses), imposes to disclose sources and keep the same license (only when modifying existing files) and restricts trademark use:
I can open a new issue about this, but would obviously be helpful with a release/tag under the new license (that library users can depend on). Not necessarily now, but at some later point.
My understanding is that the master branch where the license change occured is going to be the basis for the coq-8.18 release. This one will certainly get tagged. Possibly we could insist on the license change in the remarks about this release.