Stream: Coq devs & plugin devs

Topic: How to install Coq 8.16.0?


view this post on Zulip Yannick Forster (Sep 06 2022 at 14:51):

The announcement that 8.16.0 was tagged mentions that package managers should start working on upgrading their packages. I would assume that - at least in general - this includes installing the tagged Coq version. Now my question is: How do I install Coq 8.16.0? I know how to do it once there is an opam package, but the PR is not yet merged. I read INSTALL.md and build-system.dune.md, but nothing of this seems to give me a state where coqcis in my path

view this post on Zulip Guillaume Melquiond (Sep 06 2022 at 14:58):

You can use the one tracking branch 8.16 in the Coq repository, which is a good enough approximation:

opam remote add core-dev https://coq.inria.fr/opam/core-dev
opam install coq=8.16.dev

view this post on Zulip Théo Zimmermann (Sep 06 2022 at 15:15):

FYI "package managers" is directed toward people maintaining packaging of the Coq system, so to distinguish from "package maintainers" who are people maintaining Coq packages (Coq plugins and libraries). I would expect that package maintainers can wait for the opam package to be available, or use the 8.16+rc1 version, or use the solution provided by Guillaume above.

view this post on Zulip Julien Puydt (Sep 06 2022 at 15:24):

Here is a transition tracker for coq 8.16.0 in Debian ; it should turn green progressively.

view this post on Zulip Julien Puydt (Sep 06 2022 at 15:27):

(In fact, according to this, the coq line would already be green if the S390X architecture had more available builders.)

view this post on Zulip Karl Palmskog (Sep 06 2022 at 18:05):

opam package PR for 8.16.0 is merged now, so I guess in a couple of hours it should be out via opam update. Best option for people who can't wait is still core-dev opam repo.

view this post on Zulip Karl Palmskog (Sep 06 2022 at 18:06):

I think we need to add some big fat warning to regular users to not try installing from source, but just wait for the Coq package (opam, debian, etc.) or even better, the Platform release

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:07):

Théo's answer has solved the issue for me in the sense that I now understand what was meant by "package managers"

view this post on Zulip Yannick Forster (Sep 07 2022 at 12:08):

But yes, maybe a copy-pastable message the release manager can post to the dev channels mentioning that an opam package is on its way and that regular users / package maintainers should definitely wait for that would be great

view this post on Zulip Guillaume Melquiond (Sep 07 2022 at 12:21):

Actually, I would not recommend that package maintainers wait for the actual release. I would recommend them to test the release-candidate packages as soon as humanly feasible. (That is, opam install coq=8.16+rc1 for 8.16.) But obviously, if they never got to test the release candidate before the actual release, they might just as well wait a few more hours for the new opam packages to be made available.

view this post on Zulip Michael Soegtrop (Sep 07 2022 at 12:21):

@Yannick Forster : for packages in Coq Platform I post issues which include information on how to build a close approximation of the planned release. I usually have some additional local opam patches to make things work like weakening version restrictions of packages or providing packages pinned to specific commits. Usually I update Coq Platform main weekly during release time - this time was tough because I was moving homes (still have > 100 packaged boxes ...) but it should have been good enough for most purposes.

You can also use opam directly and just download and register the Coq Platform opam patch repos under (https://github.com/coq/platform/tree/main/opam - there are also some docs there).

If this method does not work for you, I would like to know what is missing, so that I can improve.

For me it is important that all packages converge to a common point.


Last updated: Feb 01 2023 at 15:04 UTC