Create README.md

[spitters]

@robbertkrebbers Could you please confirm ?

[robbertkrebbers]

In principle I'm fine with this, but I think it's very confusing.

• Licensing information should not be in a README file in some subfolder, it should be in a LICENSE file. The LICENSE in the root should explain what's the LICENSE for all parts of the development, or describe where that information can be found.
• There is a LICENSE file at the root of the repo (with GPL), since it does not explicitly exclude this directory, I believe this directory is therefore also GPL (I think that LICENSE file was already there when I wrote the code in 2010, so my contributions are therefore GPL already, even without my explicit permission).
• I think you said you wanted to relicense under LGPL, so why not change the LICENSE file in the root (provided you have permissions from everyone involved). In general, having separate licenses for different parts of a development is very confusing.
• I gave the permission for WTFPL since it's very liberal and thus compatible with any open source license, allowing you to use my developments under any license that you see fit (now or in the future). I don't think you should actually use WTFPL, but rather a more common license (which could be any).

[robbertkrebbers]

My 2 cents if you want to change the license: make a PR that changes the LICENSE (in the root of the repo) to LGPL. Then ask all contributors to respond to that PR that they agree.

Another 2 cents: if you are going to change the license, I would directly go to something more liberal than LGPL, for example, BSD, so as to avoid re-licensing issues in the future.

[VincentSe]

@robbertkrebbers Completely relicensing CoRN to LGPL or BSD would greatly improve its chances to be accepted and used in Coq platform as the recommended constructive mathematics library. There are 19 contributors holding the copyright, do you know how to reach them all ?

[VincentSe]

@robbertkrebbers @spitters @Zimmi48 Here is the pull request that replace CoRN's license by Coq's license
#99

Can you contact the 19 CoRN's copyright holders to ask them to accept this change ?

[Zimmi48]

I agree with Robert. I recently gave my reasons for being opposed to the use of LGPL in coq-community/templates#34 (comment). I largely prefer the use of GPL (clear requirements) to LGPL (people think it is a rather permissive license when in fact, its requirements are extremely restrictive). I am very sad that it is the de facto licence of the OCaml and Coq ecosystems. I recommend either MIT (very much used, very permissive, similar to BSD) or MPL 2.0 (weak copyleft but very easy to understand contrary to LGPL).

[robbertkrebbers]

There are 19 contributors holding the copyright, do you know how to reach them all ?

I have no idea if it's feasible to contact all of them. Many are not active in academia anymore. Bas may have a better idea if this is feasible at all, or hopeless to start with.

But before pursuing any such an endeavor, I propose you figure out what license you really want.

Also I have to say that I don't quite understand Bas's original plan. Was his intention to only re-license parts of CoRN or the whole of it?

[spitters]

We have contacted a number of key people already, and they are happy to change the license. To avoid having to contact everyone, we could just relicense the parts that do not have GPL and where we have already contacted the contributors. Vincent has shown that those parts are enough.

…

On Tue, Jun 2, 2020 at 5:54 PM Robbert Krebbers ***@***.***> wrote: There are 19 contributors holding the copyright, do you know how to reach them all ? I have no idea if it's feasible to contact all of them. Many are not active in academia anymore. Bas may have a better idea if this is feasible at all, or hopeless to start with. But before pursuing any such an endeavor, I propose you figure out what license you really want. Also I have to say that I don't quite understand Bas's original plan. Was his intention to only re-license parts of CoRN or the whole of it? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#98 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTTDX2T6GTWSDJXAN2DRUUOE3ANCNFSM4NOUCVNQ> .

[robbertkrebbers]

In that case, I suggest making clear in the LICENSE file in the root what parts are available under which license.

[spitters]

@robbertkrebbers as proposed here MIT instead of WTFPL is preferred (as it is more common)
coq-community/manifesto#110

As per the ongoing discussion
#99
, it may be preferable to (re)license the parts where we can easily contact all the authors, and then handle #99 when we know more. The conclusion from #99 is that it has been accepted practice for a very long time in corn to have parts under MIT license.
So, I see no problem doing this for the faster/ files too.

[robbertkrebbers]

@robbertkrebbers as proposed here MIT instead of WTFPL is preferred (as it is more common)
coq-community/manifesto#110

TLDR: MIT is fine.

As I stated in that email, I'm fine with any open source license. I gave explicit permission for WTFPL kind of as a joke, but also since that would allow you to re-license to whatever you like.

PS: What's the reason why MIT is preferred over BSD?

[Zimmi48]

MIT has just become more popular nowadays. GitHub recommends it (cf. https://choosealicense.com) and the FSF prefers it over BSD because BSD has many variations including an old one (4-clause) that was not GPL-compatible.

[robbertkrebbers]

That sounds like a reasonable motivation to prefer MIT. But are there any technical differences between 3-clause BSD and MIT?

[robbertkrebbers]

@spitters I still think the following should be fixed:

Licensing information should not be in a README file in some subfolder, it should be in a LICENSE file. The LICENSE in the root should explain what's the LICENSE for all parts of the development, or describe where that information can be found.

[spitters]

@robbertkrebbers I agree, but I hope we can resolve that as part of the larger discussion in #99

[Zimmi48]

That sounds like a reasonable motivation to prefer MIT. But are there any technical differences between 3-clause BSD and MIT?

The MIT license is equivalent to the 2-clause BSD license. See https://opensource.stackexchange.com/questions/217/what-are-the-essential-differences-between-the-bsd-and-mit-licences.