Stream: Coq Platform devs & users

Topic: License for the platform charter and documentation


view this post on Zulip Bas Spitters (Aug 06 2020 at 11:21):

@Michael Soegtrop Do you want to change the license of platform to MPL-2.0, as per the coq community manifesto:
https://github.com/coq-community/manifesto

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:21):

@Bas Spitters the manifesto repo itself and the documentation it contains is CC-0. For documentation, we don't recommend MPL-2.0. And I think the scripts in the platform repo are due to earlier licensing (which was due to code owned by Michael's earlier employer)

view this post on Zulip Bas Spitters (Aug 06 2020 at 11:25):

I'm referring to this:
"The Coq platform setup scripts and the selection of packages are licensed LGPL 2.1+."
https://github.com/MSoegtropIMC/coq-platform/

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:26):

I think this is the reason for LGPL2-1+ for the scripts:

# Released to the public by Intel under the
# GNU Lesser General Public License Version 2.1 or later
# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:27):

but nevertheless I think it could be made clear that the platform charter text and so on is under something less onerous than LGPL (@Théo Zimmermann can perhaps comment)

view this post on Zulip Théo Zimmermann (Aug 06 2020 at 11:28):

That's a good point.

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:29):

also, the Platform opam repo metadata should ideally also be under something different than LGPL

view this post on Zulip Théo Zimmermann (Aug 06 2020 at 11:31):

What is the license for the main opam repo metadata?

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:33):

hm, the Coq opam repo is LGPL-2.1-unknown (only), so I guess the metadata is too

view this post on Zulip Théo Zimmermann (Aug 06 2020 at 11:34):

Coq developers have been consistently using this license without even taking the time to think about it sigh

view this post on Zulip Karl Palmskog (Aug 06 2020 at 11:39):

looks like the OCaml people were way ahead: https://github.com/ocaml/opam-repository/commit/dc4bef160b6b77fc8845470643846b9d72ab446e (it's CC0 these days)

view this post on Zulip Michael Soegtrop (Aug 06 2020 at 15:20):

I picked LGPL 2.1 mostly for compatibility with Coq itself. If this is considered an issue I can likely soon remove the remaining parts of the script - the main reason I still keep parts of the old Windows build script is that GTK3 is outdated on Cygwin. I wanted to update it before the release and/or add facilities for Cygwin patch packages. What is a little bit of work to redo is the Windows Cygwin outer setup script. I will change the license as soon as nothing from the old Windows setup script remains.

view this post on Zulip Karl Palmskog (Aug 06 2020 at 17:38):

personally, I think it may still make sense to license the Coq Platform code and the Coq Platform metadata (including documentation) differently. Having a very permissive license for the latter is really important, I think. The code will have a much smaller audience

view this post on Zulip Michael Soegtrop (Aug 09 2020 at 17:16):

Karl Palmskog said:

personally, I think it may still make sense to license the Coq Platform code and the Coq Platform metadata (including documentation) differently. Having a very permissive license for the latter is really important, I think. The code will have a much smaller audience

Yes I will change the license. Actually the Coq platform is not that much code or metadata. Most of the work is to test things, produce fixes and get this merged upstream. If I manage to merge everything upstream, the remaining coq platform code and metadata is not much. So I don't care much what license it has.

Btw.: I managed to replace the scripts from the old Windows installer with opam - pretty much all of the functionality of my old scripts is covered by opam, like doanloading and caching sources, expanding and patching them, building and installing stuff, book keeping installed files, ... . Interestingly opam is not OCaml centric - one can use it as well to manage / build other stuff. One issue I had is that I need to compile gtksourceview from sources on Windows. I just created a simple opam file and it does the trick. I have only one very simple remaining package - than I can delete most of the script.


Last updated: Jan 29 2023 at 19:02 UTC