Stream: Coq users

Topic: ✔ opam install on MacOS fails to install coq_makefile


view this post on Zulip Jason Gross (Aug 02 2021 at 01:21):

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?

view this post on Zulip Paolo Giarrusso (Aug 02 2021 at 13:42):

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.

view this post on Zulip Jason Gross (Aug 02 2021 at 14:41):

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...

view this post on Zulip Paolo Giarrusso (Aug 02 2021 at 14:55):

(FWIW that repo seems private)

view this post on Zulip Paolo Giarrusso (Aug 02 2021 at 14:56):

also wonder what's the opam switch setup

view this post on Zulip Jason Gross (Aug 03 2021 at 08:55):

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

view this post on Zulip Notification Bot (Aug 03 2021 at 08:55):

Jason Gross has marked this topic as resolved.


Last updated: Feb 09 2023 at 00:03 UTC