@Michael Soegtrop we should start asking people to make tags for 8.14 BTW.
@Théo Zimmermann : yes indeed - I will create the tickets tomorrow.
it's amazing that we finally have an incentive model for getting maintainers to tag compatible releases... I'm not sure if people realize the very hard coordination problems behind this that the community has been struggling with for years
@Karl Palmskog : as I keep saying: the work behind Coq Platform is not the bunch of scripts but the required coordination work.
yeah, the platform might be described as a multi-year, continuous technical lobbying effort (which produces useful artifacts along the way)
@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.
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.
I'm guessing there's also a Nix package in the works, which would provide even more testing options.
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:
I foresee a Terminator-like man-vs.-machine perpetual struggle in the future: developers against nit-picky & fault-prone CI
That's something which Nix was supposed to avoid by making builds more reproducible. Not yet reproducible enough apparently :face_palm:
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).
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: Dec 07 2023 at 06:38 UTC