It seems to me that the behavior of opam install coq.8.13.1
has changed between opam v1 and opam v2, such that in opam v2 on MacOS, opam install coq.8.13.1
followed by eval $(opam env)
is not enough to access coq_makefile
. Can others reproduce this behavior? https://github.com/mit-plv/fiat-crypto/runs/3214536848?check_suite_focus=true#step:8:34 What's going on?
coq_makefile
is available alright here on Mac — and opam env
exports the PATH correctly on opam 2.0.8 (and probably .9 but I haven't checked). Some digging showed that script is calling $(HIDE)$(COQBIN)coq_makefile
, not coq_makefile
.
Finally, I suspect you weren't using opam v1, just setup-ocaml V1?
I'd extend logs to show the PATH
, COQBIN
and the results of which coq_makefile
— maybe at different points — to know whether the problem is in opam itself, in the CI scripts, or in the Makefiles.
Hm, I guess you're right. https://github.com/JasonGross/test/runs/3221270692#step:8:21 suggests that the problem is that opam env
is empty...
(FWIW that repo seems private)
also wonder what's the opam switch
setup
Oops, I wanted the repo unlisted rather than private. In any case, the issue seems to be https://github.com/ocaml/setup-ocaml/issues/190, that the GH checkout action somehow clears opam env
Jason Gross has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC