Stream: Coq devs & plugin devs

Topic: opam package split


view this post on Zulip Ralf Jung (May 20 2021 at 10:52):

FWIW, I am not sure that it was a good idea to split the Coq opam package. I just tried to opam pin add coq.dev -k git git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213 and that failed, saying

The following dependencies couldn't be met:
  - coq → coq-core
      unknown package

Pinning the Coq package to a particular git version just got a lot harder.

view this post on Zulip Ralf Jung (May 20 2021 at 10:56):

looks like the full command sequence now is

opam pin add -k git coq-core.dev git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213 -n
opam pin add -k git coq-stdlib.dev git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213 -n
opam pin add coq.dev -k git git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213

this will also download the git repo 3 times

view this post on Zulip Lasse (May 20 2021 at 11:02):

Part of the reason for the original error is that the package split is not yet in the opam-coq-archive. Once they are there, the error should go away. But I think you still have to do two pins, because pinning is not transitive. So if you pin coq, that does not automatically pin coq-core and coq-stdlib to the same commit.

view this post on Zulip Ralf Jung (May 20 2021 at 11:24):

yeah, as you say -- if the packages were in the repo, this would have been worse: the pin would have succeeded but not taken effect, since the -core/-stdlib packages would not have been pinned.

view this post on Zulip Lasse (May 20 2021 at 11:38):

Note that if you navigate to your local copy of Coq's git repo, checkout the correct commit and run opam install ., all packages will be automatically pinned and installed.

view this post on Zulip Ralf Jung (May 20 2021 at 12:02):

yeah but that's not really helpful for what I am doing (this is for CI of some Coq-using project)

view this post on Zulip Lasse (May 20 2021 at 12:03):

Oh, and additionally, you can also just run the following command to pin everything
opam pin add git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213

view this post on Zulip Lasse (May 20 2021 at 12:05):

If you do not want to install all packages such as coq-doc you can run the following:

opam pin add git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213 --no-action
opam install coq

view this post on Zulip Ralf Jung (May 20 2021 at 12:11):

Lasse said:

Oh, and additionally, you can also just run the following command to pin everything
opam pin add git+https://github.com/coq/coq#f16b7c75bcc8651e43ec1f0c8ae6744748665213

ah, that's interesting, I did not know one can pin a git repo like that. it doesn't entirely fit the structure of our CI but this is good to know, thanks!

view this post on Zulip Ralf Jung (May 28 2021 at 07:39):

@Lasse I started integrating this git repo pinning into our CI, and like it a lot. There is just one problem: do you know how I can control the version opam will choose for these packages? I'd like it to be dev, but when I do this in a new empty switch it picks some random-looking version (might be the highest version that exists in any of the registered repositories)

view this post on Zulip Ralf Jung (May 28 2021 at 07:42):

ah, looks like I can possibly set that in the target repo... that#s less control than the other kind of pinning but might work out

view this post on Zulip Ralf Jung (May 28 2021 at 07:45):

yeah, adding version: "dev" in the git repo opam files worked

view this post on Zulip Guillaume Melquiond (May 28 2021 at 07:51):

You should also be able to specify it at opam pin time: opam pin add coq.dev git+https... --no-action. Obviously, you need to do it once for each package, but since no action is performed, this does not matter much.

view this post on Zulip Ralf Jung (Jun 05 2021 at 09:21):

@Guillaume Melquiond this "once for each package" is exactly what I wanted to avoid :D

view this post on Zulip Ralf Jung (Jun 18 2021 at 06:52):

Pinning multiple packages this way is indeed very convenient, but what about unpinning? Currently it looks like I need to list all the packages explicitly there -- not very convenient...


Last updated: Oct 16 2021 at 02:03 UTC