Stream: Coq devs & plugin devs

Topic: opam install cannot find directory?


view this post on Zulip Jason Gross (May 05 2021 at 15:28):

What does it mean when opam pin add coq.8.13.1 fails with Error: Could not retrieve /home/runner/work/fiat-crypto/fiat-crypto/coq.8.13.1?

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 16:13):

hard to know opam's black magic, I'd say the first thing to look into is if the right --kind argument for opam pin was used.

view this post on Zulip Jason Gross (May 05 2021 at 16:42):

What's --kind? The full log is at https://github.com/mit-plv/fiat-crypto/runs/2503870392, btw. Does coq.8.13.1 not make sense? I think it worked fine when I did opam pin add coq 8.13.1, but opam pin add coq dev does not work...

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 18:09):

see man opam pin

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 18:10):

you want a dot in coq.dev ?

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 18:10):

best is to use --kind tho, otherwise you get surprises quite often

view this post on Zulip Jason Gross (May 05 2021 at 18:46):

What should I be passing to --kind? version? http? git? And perhaps the instructions at https://coq.inria.fr/opam-using.html suggesting opam pin add coq 8.13.1 should be updated to include --kind? Or is it not necessary there?

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 19:06):

If you want to pin the version only, then pass the version kind, not?

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 19:07):

Maybe it should be updated, the problem with omitting kind is that then the kind of pin that opam will select will depend on what the contents of pwd are, env variables, and a bunch of other factors.

view this post on Zulip Emilio Jesús Gallego Arias (May 05 2021 at 19:08):

This is new in opam 2.0 so you will find plenty of examples omitting it, but in fact it was added to resolve the problems in Opam 1.2 pin, but for compat opam pin still tries to guess the kind if the arg is not present

view this post on Zulip Paolo Giarrusso (May 07 2021 at 23:08):

+1 for updating instructions, opam should just stop guessing since it never seems to guess the right thinu


Last updated: Oct 16 2021 at 01:03 UTC