Stream: Coq devs & plugin devs

Topic: opam pin does not work with a git url


view this post on Zulip Jason Gross (Sep 11 2024 at 16:47):

Does anyone know why opam pin add coq 'https://github.com/SkySkimmer/coq.git#test-minimizer-general-tycon' -y would install the tip of Coq master? Cf https://github.com/JasonGross/coq-tools/issues/217#issuecomment-2344119969

view this post on Zulip Karl Palmskog (Sep 11 2024 at 16:49):

hmm, did you explicitly say it's a git repo? -k git

view this post on Zulip Gaëtan Gilbert (Sep 11 2024 at 16:50):

may need something like git+https instead of just https to be able to specify the branch using #

view this post on Zulip Jason Gross (Sep 11 2024 at 16:52):

Ooh, good catch, it's probably me forgetting git+https

view this post on Zulip Jason Gross (Sep 11 2024 at 17:01):

Oh, I bet what's happening is that pinning coq to git doesn't change coq-core et al, and all get treated as version "dev" so "= version" doesn't constrain them

view this post on Zulip Jason Gross (Sep 11 2024 at 17:01):

(git+https didn't work any better)

view this post on Zulip Karl Palmskog (Sep 11 2024 at 17:03):

@Jason Gross if you consistently pin all of coq-core, coq-stdlib the same way as coq before you pin coq, it should work

view this post on Zulip Yann Leray (Sep 11 2024 at 17:15):

You can also not mention the package name in the pin, and it will pin all packages defined in the repository

view this post on Zulip Jason Gross (Sep 11 2024 at 17:17):

Ooh, I'll try that, thanks

view this post on Zulip Emilio Jesús Gallego Arias (Sep 11 2024 at 17:19):

Try to use opam 2.2 if you can; has many fixes w.r.t. pinning

view this post on Zulip Jason Gross (Sep 11 2024 at 17:41):

I'm using whatever is in the coq.dev docker image

view this post on Zulip Karl Palmskog (Sep 11 2024 at 18:26):

as can be seen here this Docker image uses opam 2.2.1 (bumped from 2.2.0 two days ago)


Last updated: Oct 13 2024 at 01:02 UTC