Stream: coq-community devs & users

Topic: Licensing requirements


view this post on Zulip Jean-Marie Madiot (Aug 30 2020 at 14:06):

Hello everyone! In order to move to coq-community a list of 100 theorems (repo, website), I need to mention some license information. The purpose of the list is to give coq statements so... do I need to specify the license for each statement? Are the links to each original development enough? Do I need to check that all of the licenses, if they exist, are compatible with coq-community, and if not, do I need to remove the statement and give only the link? (Knowing that sometimes the licensing does change, but maybe only in the good direction.)

In addition, there are some of the proofs on the repository, maybe that's not the correct places for them to be, but I would like to leave them there. To do so I will need to contact the author of this file: it contains the word "license" but is not a regular one, so, I don't think that's enough. Is it? If not, can I tell him to choose any one he likes from https://choosealicense.com/ ? (or https://cecill.info/licences.fr.html ?)

view this post on Zulip Karl Palmskog (Aug 30 2020 at 14:18):

@Jean-Marie Madiot we have some general advice on licensing here: https://github.com/coq-community/manifesto#faq ("What license to choose for a coq-community project?")

There are essentially two different levels of granularities for specifying licenses in coq-community. Either you say that all source (.v files) in the repo are under some license, or you specify the license for each source file. One example of the latter is here: https://github.com/ejgallego/coq-serapi/blob/v8.12/LICENSE

The third option, specifying license for each statement, is to me untenable.

view this post on Zulip Karl Palmskog (Aug 30 2020 at 14:20):

For the specific file you point to, you could just say in LICENSE/LICENSE.md something like:

cardan3.v: permissive custom license, see file header

view this post on Zulip Karl Palmskog (Aug 30 2020 at 14:22):

another (and perhaps better) option is as you say to contact the author and ask him to choose a regular license, we would recommend MIT license in this case: https://spdx.org/licenses/MIT.html

view this post on Zulip Jean-Marie Madiot (Aug 30 2020 at 14:22):

Karl Palmskog said:

For the specific file you point to, you could just say in LICENSE/LICENSE.md something like:

cardan3.v: permissive custom license, see file header

But it does need to be a standard open source license, in the file header?

view this post on Zulip Jean-Marie Madiot (Aug 30 2020 at 14:23):

Karl Palmskog said:

another (and perhaps better) option is as you say to contact the author and ask him to choose a regular license, we would recommend MIT license in this case: https://spdx.org/licenses/MIT.html

ok, I will contact him anyway, so I'll tell him that.

view this post on Zulip Karl Palmskog (Aug 30 2020 at 14:24):

Jean-Marie Madiot said:

But it does need to be a standard open source license, in the file header?

We have no "strict" set of open source licenses, only recommendations (to make it easy for the community to reuse results). At a glance, that license header would qualify as open source to us. So I think it would be fine if we used the custom license for now, and also email the author about switching to MIT, and adjust it later if he approves.

view this post on Zulip Karl Palmskog (Aug 30 2020 at 14:29):

since custom licenses are always hairy, perhaps @Théo Zimmermann could comment as well

view this post on Zulip Théo Zimmermann (Aug 31 2020 at 10:43):

Yes: it makes sense for such a project (a collection of files really) to have licenses per files (in header) or per directory.

view this post on Zulip Théo Zimmermann (Aug 31 2020 at 10:45):

Yes: we can accept this custom license as showing some open source intent but yes, it would be great to contact the author of this file to encourage them to adopt a more widely used license (like MIT) because it would create less legal "risks" for its users (some industrial users are very cautious regarding non-standard licenses).

view this post on Zulip Jean-Marie Madiot (Aug 31 2020 at 19:37):

Thank you both, the author agreed to MIT and he contributed a new proof with his reply :D


Last updated: Feb 05 2023 at 14:02 UTC