Stream: Coq Platform devs & users

Topic: Coq platform 8.12.0+beta1 released


view this post on Zulip Michael Soegtrop (Sep 18 2020 at 16:16):

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.

view this post on Zulip Karl Palmskog (Sep 18 2020 at 16:33):

@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

view this post on Zulip Michael Soegtrop (Sep 18 2020 at 17:44):

@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):

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.

view this post on Zulip Karl Palmskog (Sep 18 2020 at 17:47):

sure, it doesn't need to be advertised, but to me downloading local opam package definitions and using a script is kind of weird

view this post on Zulip Karl Palmskog (Sep 18 2020 at 17:59):

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

view this post on Zulip Michael Soegtrop (Sep 18 2020 at 18:43):

The first step is anyway merging the patches upstream.

view this post on Zulip Théo Zimmermann (Sep 19 2020 at 10:02):

@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.

view this post on Zulip Théo Zimmermann (Sep 19 2020 at 10:03):

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.

view this post on Zulip Théo Zimmermann (Sep 19 2020 at 10:07):

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).

view this post on Zulip Karl Palmskog (Sep 19 2020 at 14:27):

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).

view this post on Zulip Théo Zimmermann (Sep 19 2020 at 16:25):

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).

view this post on Zulip Karl Palmskog (Sep 19 2020 at 17:46):

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