Karl Palmskog (Sep 08 2021 at 08:18): Karl Palmskog (Sep 08 2021 at 08:18):something annoying I (re)discovered recently: CECILL-B and CECILL-C are not OSI approved. This means we probably can't require OSI-approved licenses in coq-community and have to be lax about what "open source" means. Also, we have repos that need to be CC-0, like Awesome Coq.
Théo Zimmermann (Sep 08 2021 at 08:22):AFAICT, they are all considered as "free license" according to FSF (https://www.gnu.org/licenses/license-list.html).
Théo Zimmermann (Sep 08 2021 at 08:22):Therefore, I suppose the criterion can be "OSI-approved open source license or free software license according to the FSF".
Karl Palmskog (Sep 08 2021 at 08:23):OK, that's at least better than what we now (just "open source" with implicit link to OSI, which we are not following)
Karl Palmskog (Sep 08 2021 at 08:27):we probably also want urge using OSI rather than non-OSI
Théo Zimmermann (Sep 08 2021 at 08:27):Is Unlicense OSI-approved BTW?
Karl Palmskog (Sep 08 2021 at 08:27):yes it is (https://opensource.org/licenses/unlicense)
Théo Zimmermann (Sep 08 2021 at 08:28):OK, then I think we can indeed urge using OSI.
Karl Palmskog (Sep 08 2021 at 08:28):we may want to comment on documentation licenses as well
Karl Palmskog (Sep 08 2021 at 08:28):for example, I would not like to see CC variants that have NoDerivs or NonCommercial
Théo Zimmermann (Sep 08 2021 at 08:28):Well, they wouldn't be free / open source licenses then.
Théo Zimmermann (Sep 08 2021 at 08:29):And the usual recommendation is: use the same license for your documentation as for your source code.
Théo Zimmermann (Sep 08 2021 at 08:29):(The opposite of what Coq has done.)
Karl Palmskog (Sep 08 2021 at 08:30):there is a very vocal contingent seemingly who oppose code licenses for documentation
Karl Palmskog (Sep 08 2021 at 08:30):for example, the Awesome people don't allow MIT if you want your list listed
Karl Palmskog (Sep 08 2021 at 08:32):I think it's nice that the totality of hydra-battles is MIT, but I hope Pierre is clear about what that means
Karl Palmskog (Sep 08 2021 at 08:35):also, I think we should enforce that all repos must have an explicit license, no matter if it's just metadata or automation, e.g., https://github.com/coq-community/coq-performance-tests-plots-history lacks LICENSE or similar
Karl Palmskog (Sep 08 2021 at 08:37):it's also doubtful if CC0 works in all jurisdictions, in some sense this is the problem the Unlicense solves
Karl Palmskog (Sep 08 2021 at 08:38):let's say I'm not thrilled that the Coq Platform is CC0
Karl Palmskog (Sep 08 2021 at 08:40):I honestly think we can recommend the Unlicense for "stuff you just copy", since you don't have this burden of including any attribution
Karl Palmskog (Sep 08 2021 at 08:54):a recent concern from industry are all these extremely burdensome AGPL-like licenses, this one for example. It would be good to have them explicitly excluded.
Gaëtan Gilbert (Sep 08 2021 at 08:56):that's not "extremely burdensome"
Karl Palmskog (Sep 08 2021 at 08:57):text is basically a word mountain that you will have to pay a lawyer to interpret and varies from jurisdiction to jurisdiction
Karl Palmskog (Sep 08 2021 at 08:58):AGPL at least has been around for a while and has had legal people look at it
Karl Palmskog (Sep 08 2021 at 09:01):figuring out what "interacting with [stuff] remotely through a computer network" means legally in Europe vs US is likely to take man-months of legal work
Théo Zimmermann (Sep 08 2021 at 11:54):Do you have any idea why people are using custom licenses in this case instead of just AGPL?
Gaëtan Gilbert (Sep 08 2021 at 12:01):because there's no lesser agpl (<- this is a guess)
Michael Soegtrop (Sep 08 2021 at 12:04):let's say I'm not thrilled that the Coq Platform is CC0
@Karl Palmskog : the main reason why Coq Platform is CC0 is that the opam repos are CC0 (see https://github.com/ocaml/opam-repository/blob/master/COPYING) and the main work in Coq Platform is traditionally to patch opam packages and integrate them upstream, although this is usually not visible in a release version of the platform (which is just a bunch of scripts). The main work of the Coq Platform actually goes into the opam repos. So it does make sense to use the same license as opam repos.
Karl Palmskog (Sep 08 2021 at 12:23):@Michael Soegtrop but you're adding scripts on top of that, right? So Unlicense would make more sense to me. The Coq opam archive data is MIT btw: https://github.com/coq/opam-coq-archive/blob/master/released/LICENSE
Michael Soegtrop (Sep 08 2021 at 12:35):Yes, but the scripts are really not that much and one can discuss if it is really a work independent of opam. Beyond the work on opam packages I see Coq Platform more as publishing a book in a nicer cover.
Last updated: Jun 06 2023 at 22:01 UTC