Michael Soegtrop (Sep 28 2022 at 08:36): Michael Soegtrop (Sep 28 2022 at 08:36):@Karl Palmskog : yes makes sense - law is not logic in the end.
@Théo Zimmermann : I think a question we should discuss is if Coq Platform should be CC0 or something else. As I said historically I decided for CC0 because the OCaml opam repo is CC0 and originally there was a lot of copying of files hence and forth between the OCaml opam repo and Coq platform local opam patch repo. But this is not the case any more.
Karl Palmskog (Sep 28 2022 at 08:40):@Michael Soegtrop I think we agree 100% that the database part of the Platform (e.g., opam package definitions) should be CC0, so as easily copy stuff back and forth with OCaml opam repo. Where your opinion and mine diverge is w.r.t. the scripts (which are not likely to be used upstream). I think Unlicense would be better there, for the reasons discussed above. But maybe you want to open a Platform issue about it [or is there one?], and we accumulate pros and cons and eventually make a decision there.
Théo Zimmermann (Sep 28 2022 at 09:35):IMHO if we change the license of the scripts only, then I would even recommend switching to MIT. Having two different public domain dedications in a single repositories would raise more questions than it would help I think.
Théo Zimmermann (Sep 28 2022 at 09:37):Another solution is to use the Unlicense for everything because CC0 and Unlicense anyway allow you to copy-paste stuff without tracing where it comes from and thus there is no problem with the back and forth copying between the two repositories as long as both are dedicated to the public domain.
Karl Palmskog (Sep 28 2022 at 09:38):OK, if we know switching back-and-forth between CC0 and Unlicense works, then that's fine with me to make the whole repo Unlicense. Also fine with MIT for everything.
Théo Zimmermann (Sep 28 2022 at 09:40):MIT for everything would be problematic though.
Théo Zimmermann (Sep 28 2022 at 09:40):I only recommended MIT as an option for the scripts part since there are no back and forth copying for them.
Michael Soegtrop (Sep 28 2022 at 12:43):Regarding Coq Platform: since I have both a local repo for OCaml opam (origin is CC0) and Coq opam (origin is LGPL2.1) I don't think there is a proper solution (short of assuming that opam packages are not "work" in the sense of copy right law, since they are an effect of rules and the nature of things and not of creativity) except giving these sub repos the same license as the main repos. Then we anyway have 2 licenses and it doesn't matter much if the rest is then one of these or a 3rd one - I tend to MIT then.
Notification Bot (Sep 28 2022 at 12:44):A message was moved here from #Miscellaneous > CC0 for software by Théo Zimmermann.
Karl Palmskog (Sep 28 2022 at 12:44):@Michael Soegtrop as I mentioned before, the Coq opam archive data is MIT: https://github.com/coq/opam-coq-archive/blob/master/released/LICENSE
Are you referring to scripts from the Coq opam repo that are LGPL-2.1? I don't think we are using any of them in the Platform.
Michael Soegtrop (Sep 28 2022 at 13:57):@Karl Palmskog - ah yes, sorry, I somehow read over this.
So the conclusion is to make it MIT except for the OCaml opam patch repo?
Karl Palmskog (Sep 28 2022 at 14:03):Théo didn't want to make the data MIT - just the scripts, at most.
Michael Soegtrop (Sep 28 2022 at 14:34):I think @Théo Zimmermann referred to the OCaml opam patch repo, which I would keep as CC0. I don't see a good reason to make the Coq opam repo something else than MIT, when the main repo is MIT.
Théo Zimmermann (Sep 28 2022 at 15:05):Indeed. I agree with your conclusion @Michael Soegtrop. MIT is a good license choice for everything but the OCaml opam patch repo.
Michael Soegtrop (Sep 29 2022 at 07:16):OK, then I create an issue for the re licensing - fortunately the list of contributors is still small.
Théo Zimmermann (Sep 29 2022 at 08:43):@Michael Soegtrop You do not need to ask for permission to relicense from CC0 to another license, because CC0 already gives you permission.
Karl Palmskog (Sep 29 2022 at 08:48):this is essentially where the fight is between copyleft and permissive: FSF encourages people to relicense projects with permissive licenses under GPL. In for example OpenBSD camp, some consider this antisocial behavior [but allowed by licenses]
Théo Zimmermann (Sep 29 2022 at 08:55):FSF encourages people to relicense projects with permissive licenses under GPL
Does it? I think the FSF would never support creating a fork of an active open source project just to move it under GPL. Then, if it's the current main maintainers decision, this is different of course.
Karl Palmskog (Sep 29 2022 at 08:58):they don't go that far, but this doesn't land well with BSD hackers:
Contributing to an existing project
[...]
One case where using a different license can be justified is when you make major changes to a work under a non-copyleft license. If the version you've created is considerably more useful than the original, then it's worth copylefting your work, for all the same reasons we normally recommend copyleft.
Karl Palmskog (Sep 29 2022 at 08:58):https://www.gnu.org/licenses/license-recommendations.html#contributing
Karl Palmskog (Sep 29 2022 at 09:01):if people followed this to the letter, probably a ton of conflict (e.g., due to MathComp situation, Coq ecosystem would suffer)
Théo Zimmermann (Sep 29 2022 at 09:01):Karl Palmskog said:
they don't go that far, but this doesn't land well with BSD hackers:
Contributing to an existing project
[...]
One case where using a different license can be justified is when you make major changes to a work under a non-copyleft license. If the version you've created is considerably more useful than the original, then it's worth copylefting your work, for all the same reasons we normally recommend copyleft.
Right. Well, permissive licenses precisely exist to allow people creating new projects from them to do whatever they want, so this can certainly sound offensive or antisocial, but this is nothing compared to doing the same under a proprietary license, which for some reason, will be perceived by some as less offensive.
Théo Zimmermann (Sep 29 2022 at 09:02):Karl Palmskog said:
if people followed this to the letter, probably a ton of conflict (e.g., due to MathComp situation, Coq ecosystem would suffer)
Sure, but that's because the main problem with copyleft licenses is not in fact that they are copyleft but that they are complex licenses that are often incompatible with each other.
Théo Zimmermann (Sep 29 2022 at 09:03):So you still get issues even in ecosystems where everyone wants to stay under open source licenses.
Karl Palmskog (Sep 29 2022 at 09:04):right. And even problems related to public domain (I think in most of Europe one has to go with the fallback license of CC0 or Unlicense rather than relinquishing copyright, but maybe hasn't been tested)
Last updated: Jun 03 2023 at 04:30 UTC