copyleft

Stream: general

[Kenny Lau]

I notice that in @**Johan Commelin**'s sset branch, every newly created file has a copyleft notice on the top:

/-
Copyleft 2020 Johan Commelin. No rights reserved.
Authors: Johan Commelin
-/

However, I could not find any copyleft notice in mathlib. What do people think about copyleft?

[Scott Morrison]

I think we decided to stick with the current copyright notice.

[Scott Morrison]

No one particularly objected to copyleft, and indeed it seems everyone was very happy with an even more permissive licence than what we have now.

[Scott Morrison]

But uniformity is its own virtue.

[Bryan Gin-ge Chen]

Some recent discussion here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.233223.20homogeneous/near/205261936

[Yury G. Kudryashov]

E.g., with the same license on all files we can move code around more easily. Though I'm still not sure whether we should add (c) Microsoft to a file when we move a lemma from a file that is used to be in core to another file.

[Chris Wong]

I'm not a lawyer, but I'm pretty sure "copyleft" means "using copyright as a means to subvert itself", a la GPL. Not the "public domain" that "no rights reserved" would imply

[Chris Wong]

I'm also wary of being "clever" with licensing. e.g. some companies ban WTFPL, despite it being free in principle, as the wording is too vague. So it's safer to stick to standards here

[Mario Carneiro]

That's why I prefer multiply-licensed CC0 / WTFPL / PD. I offer all these options, and the user is allowed to pick whichever license they prefer. The result is that you get the max of all three permissions, and companies that are worried about WTFPL can receive it under a different license

[Yury G. Kudryashov]

We can't relicense MS code anyway...