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
Finally, I suspect you weren't using opam v1, just setup-ocaml V1?
I'd extend logs to show the
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
Jason Gross has marked this topic as resolved.
Last updated: Feb 09 2023 at 00:03 UTC