Stream: coq-community devs & users

Topic: open source vs. OSI


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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".

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:27):

we probably also want urge using OSI rather than non-OSI

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 08:27):

Is Unlicense OSI-approved BTW?

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:27):

yes it is (https://opensource.org/licenses/unlicense)

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 08:28):

OK, then I think we can indeed urge using OSI.

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:28):

we may want to comment on documentation licenses as well

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:28):

for example, I would not like to see CC variants that have NoDerivs or NonCommercial

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 08:28):

Well, they wouldn't be free / open source licenses then.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Sep 08 2021 at 08:29):

(The opposite of what Coq has done.)

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:30):

there is a very vocal contingent seemingly who oppose code licenses for documentation

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:30):

for example, the Awesome people don't allow MIT if you want your list listed

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 08 2021 at 08:38):

let's say I'm not thrilled that the Coq Platform is CC0

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Sep 08 2021 at 08:56):

that's not "extremely burdensome"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Sep 08 2021 at 12:01):

because there's no lesser agpl (<- this is a guess)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: Feb 04 2023 at 02:03 UTC