Bas Spitters (Aug 06 2020 at 11:21): 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
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)
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/
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
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)
Théo Zimmermann (Aug 06 2020 at 11:28):That's a good point.
Karl Palmskog (Aug 06 2020 at 11:29):also, the Platform opam repo metadata should ideally also be under something different than LGPL
Théo Zimmermann (Aug 06 2020 at 11:31):What is the license for the main opam repo metadata?
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
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
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)
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.
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
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: Jun 03 2023 at 03:01 UTC