Stream: Coq devs & plugin devs

Topic: Change of manual license for DFSG compatibility


view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 14:59):

Didn't we change the documentation license at some point to please the Debian folks? I might have dreamt that...

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:00):

I think there was a long discussion of the Debian manual licensing woes as an issue, but not sure it concluded with a license change

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:01):

indeed, still open: https://github.com/coq/coq/issues/8774 -- the proposed change was to CC BY-SA 3.0, but didn't go through (yet)

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 15:04):

Oh, it's worse than that according to the issue: the license was changed to something that turned out to be not DFSG-compatible. Mamma mia...

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:05):

well, I was talking about the new change after the first change turned out to be soured

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 15:05):

yep, yep. we should definitely do something about that though...

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:10):

I generally agree with Théo though that the ideal is the same license for code and docs. But there is a whole community of people who absolutely will not accept code licenses for documentation, even if it's permissive like MIT. And then there are people like me, who don't like CC licenses at all for anything...

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 15:11):

even CC-0 or CC-BY?

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:11):

I really really don't like CC-0, mostly because it's not even clear it works in most of the world

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:12):

CC-BY is probably OK legally, but then one might as well call it code and use the usual permissive code licenses that enforce attribution

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 15:15):

In France you can't abandon your moral rights on a creation, so CC-0 has to be taken "up to the local rights" but then this apply for virtually any license. You can always create a micronation that forbids the GPL or judge that some license is incompatible with \<insert the local ideology of your place of living\>

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:16):

but how do you know it will be taken "up to", and not just be declared invalid overall?

view this post on Zulip Pierre-Marie Pédrot (Nov 06 2021 at 15:17):

because that's the intended meaning of the license, fuck the common law and embrace Roman law

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:18):

I like civil law too, but the "up to" feels like a big assumption, and then one might as well use the Unlicense which has an explicit fallback, and is also OSI approved (unlike CC-0, which was rejected)

view this post on Zulip Karl Palmskog (Nov 06 2021 at 15:20):

anyway, CC-BY-SA-3.0 is at least better than the current "Open Documentation License", or whatever it's called


Last updated: Feb 05 2023 at 19:29 UTC