Jean-Marie Madiot (Aug 30 2020 at 14:06): 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 ?)
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.
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
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
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.mdsomething like:cardan3.v: permissive custom license, see file header
But it does need to be a standard open source license, in the file header?
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.
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.
Karl Palmskog (Aug 30 2020 at 14:29):since custom licenses are always hairy, perhaps @Théo Zimmermann could comment as well
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.
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).
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: Jun 06 2023 at 23:01 UTC