Dear Coq Team & Users,
I just tagged the 8.12.0+beta1 release of the Coq platform. See (https://github.com/MSoegtropIMC/coq-platform/releases) for details.
It would be great if this could be tested a bit until Monday. I want to make an anoucement on Coq-Club on Monday.
@Théo Zimmermann : I think it would be fine to move this over to the Coq repo group - the main work is done and further work should follow a usual PR + review scheme.
@Michael Soegtrop hmm, wouldn't it make sense to host your OPAM repository using GitHub Pages? This way, at least Linux users wouldn't need to download anything to test, just add this repo via OPAM
@Karl Palmskog : I would still use the script on Linux. There are a few things one needs to take care of (on Mac it is the same):
opam init --reinit)
I would say the number of ways in which this can go wrong is quite large and the resulting errors will be subtle - that's the reason d'être for the script. Still one can have a virtual opam package, but I wouldn't advertise it - more for experts. Also I try to keep the setup procedure and usage of the resulting platform as consistent as possible - stuff like switch names and so on.
sure, it doesn't need to be advertised, but to me downloading local opam package definitions and using a script is kind of weird
moreover, until we find a solution for Docker images, one could use the regular Docker images and hook into a publicly hosted opam repo for the 8.12 platform in CI
The first step is anyway merging the patches upstream.
@Michael Soegtrop I was very surprised to read "It is not yet decided if also Windows and Mac installers will be created. The main issue here is not technical but some unresolved questions on license compatibility of binary distributions." and I would appreciate that you remove this claim before advertising the platform more widely.
First, I am pretty sure of my interpretation of "larger work" vs "mere aggregation" but of course I'm open to having this confirmed by the FSF first.
Second, providing binary installers for Windows and Mac (and also hopefully for the most common Linux distributions) was the whole point of developing the platform in the first place. If we were really blocked on licensing issues (which I strongly think we won't), then we would simply need to include fewer packages in the first tier for which we would provide binary installers (basically just include packages under GPL3-compatible licenses).
I'm also curious about the rationale for the new license for the Platform. Personally, I don't think CC-0 is a good choice when there is a significant program/automation component (e.g., the scripts). For the Coq automation templates, we consciously chose the Unlicense for this reason (it has an MIT-like fallback, and is approved by OSI, which CC-0 is not).
The rationale given by @Michael Soegtrop was "this is the license of the opam-repository" (see https://github.com/ocaml/opam-repository/blob/master/COPYING). That being said, and quite unfortunately, the opam-coq-archive itself is licensed under LGPL 2.1 (https://github.com/coq/opam-coq-archive/blob/master/LICENSE).
but the opam-repository archive is pure data, no? This is not the case here.
Also, it actually seems the Coq opam archive data is MIT: https://github.com/coq/opam-coq-archive/blob/master/released/LICENSE
Last updated: Jan 30 2023 at 12:03 UTC