Stream: Coq devs & plugin devs

Topic: Platform tagging for 8.14


view this post on Zulip Michael Soegtrop (Sep 22 2021 at 15:37):

@Guillaume Melquiond : I did a first pick for 8.14 - actually a lot of packages which point to a commit hash in Coq CI do have a tag which compiles with 8.14+rc1. I will send everybody a reminder that now would be the time to release a new tag in case they want to, but I think for the time being we should use working existing tags in Coq CI.

If you want I can do a PR vs v8.14 to adjust the packages to the same version I currently have in Coq platform.

For Coq Platform packages which don't have a working tag, I created upstream issues. There is a combined tracker issue on Coq Platform here: https://github.com/coq/platform/issues/139.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 17:58):

thanks to Erik, we now have an 8.14 Docker image with 8.14+rc1 that all platform projects could test against in CI. Would be nice if we could advertise this somehow.

view this post on Zulip Karl Palmskog (Sep 22 2021 at 17:59):

I'm guessing there's also a Nix package in the works, which would provide even more testing options.

view this post on Zulip Théo Zimmermann (Sep 22 2021 at 18:41):

Yeah, the Nix package has been basically ready ever since the 8.14+rc1 was set, but it hasn't been merged yet because of a strange CI build error: https://github.com/NixOS/nixpkgs/pull/138274 :cry:

view this post on Zulip Karl Palmskog (Sep 22 2021 at 18:44):

I foresee a Terminator-like man-vs.-machine perpetual struggle in the future: developers against nit-picky & fault-prone CI

view this post on Zulip Théo Zimmermann (Sep 22 2021 at 18:57):

That's something which Nix was supposed to avoid by making builds more reproducible. Not yet reproducible enough apparently :face_palm:

view this post on Zulip Michael Soegtrop (Sep 23 2021 at 12:16):

I just wanted to let you know that I finished creating tag request issues for all packages which don't have a tag compatible with 8.14.rc1 and "are you happy with our pick?" issues for all packages which do have a tag which works with 8.14+rc1. For projects hosted on github there is an overview here: (https://github.com/coq/platform/issues/139) but I also created tickets for all other projects (all hosted on INRIA gitlab).

view this post on Zulip Michael Soegtrop (Sep 23 2021 at 17:32):

Things are converging - I got in various updates today (see my latest PR).

What is missing are equations, unicoq, mtac2, elpi and hierarchy-builder.


Last updated: Oct 21 2021 at 20:02 UTC