search

coq / stdlib2

GNU Lesser General Public License v2.1
39 stars 9 forks source link

Stdlib2 license #1

Closed maximedenes closed 5 years ago

maximedenes commented 6 years ago

As part of the stdlib2 project, I plan to take/adapt code from at least:

So I'll probably stick with LGPL 2.1, but if there's a reason to do otherwise, please let me know.

Zimmi48 commented 6 years ago

Make sure you properly credit the various authors and copy the original licenses somewhere. LGPL 2.1 seems like the only possible choice that's compatible with the three origins you cited. Actually GPL would also be compatible (any version, including GPL 3) but I don't suppose that everyone would be happy with such a choice :laughing:

ppedrot commented 6 years ago

I'm not even sure linking makes any sense in the Coq context, but definitely LGPL 2.1 seems the most sensible choice.

Zimmi48 commented 6 years ago

There are two ways of satisfying LGPL requirements: dynamic linking or providing the source code (under any license, including non-free). So if the first one is not an option in the context of Coq, it still allows the user of the standard library to use whatever license they choose. Which is better than imposing GPL on everyone who does basically anything using Coq.

That being said, if Coq was created today, developers would definitely consider using a lighter license (no copyleft like MIT / BSD / Cecill B or weaker copyleft and much easier to understand with no tricky technical requirements like MPL 2.0). If that was doable, I would think that choosing one of these licenses for Stdlib2 would be preferable. This would be a less daunting task than changing the license for the whole code-base. It would only require tracking down the authors of the parts that are reused.

maximedenes commented 5 years ago

We picked LGPL 2.1, so let's close this.