Ralf Jung (May 20 2021 at 10:52): 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.
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
Lasse Blaauwbroek (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.
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.
Lasse Blaauwbroek (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.
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)
Lasse Blaauwbroek (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
Lasse Blaauwbroek (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
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!
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)
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
Ralf Jung (May 28 2021 at 07:45):yeah, adding version: "dev" in the git repo opam files worked
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.
Ralf Jung (Jun 05 2021 at 09:21):@Guillaume Melquiond this "once for each package" is exactly what I wanted to avoid :D
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: May 28 2023 at 13:30 UTC