Jason Gross (May 05 2021 at 15:28): 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?
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.
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...
Emilio Jesús Gallego Arias (May 05 2021 at 18:09):see man opam pin
Emilio Jesús Gallego Arias (May 05 2021 at 18:10):you want a dot in coq.dev ?
Emilio Jesús Gallego Arias (May 05 2021 at 18:10):best is to use --kind tho, otherwise you get surprises quite often
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?
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?
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.
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
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: Nov 29 2023 at 05:01 UTC