Stream: coq-community devs & users

Topic: ✔ [fixed][opam] compilation regression ?

view this post on Zulip David JULIEN (Oct 19 2021 at 14:43):

Hi folks! I'm running into trouble installing coq plugins through opam.
I installed two plugins flawlessly two weeks ago, and opam/dune do not seem to have been changed on my distros since then.

Though yesterday morning I wanted to install another plugin, only to be greeted with

[ swytch: ~ ] $ opam install coq-itree
...
[ERROR] The compilation of coq-ext-lib failed at "/home/swytch/.local/share/opam/opam-init/hooks/sandbox.sh build make -j3 theories".

#=== ERROR while compiling coq-ext-lib.0.11.4 =================================#
# context     2.0.8 | linux/x86_64 | ocaml-system.4.11.2 | https://coq.inria.fr/opam/released#2021-10-17 11:30
# path        ~/.local/share/opam/default/.opam-switch/build/coq-ext-lib.0.11.4
# command     ~/.local/share/opam/opam-init/hooks/sandbox.sh build make -j3 theories
# exit-code   2
# env-file    ~/.local/share/opam/log/coq-ext-lib-30386-ad8886.env
# output-file ~/.local/share/opam/log/coq-ext-lib-30386-ad8886.out
### output ###
# /home/swytch/.local/share/opam/default/bincoq_makefile -f _CoqProject -o Makefile.coq
# make: /home/swytch/.local/share/opam/default/bincoq_makefile: No such file or directory
# make: *** [Makefile:10: Makefile.coq] Error 127

Thinking something messed up my opam config and since I was attending a lecture, I just removed the opam directory to start from scratch. It was a mistake, since I now cannot install any plugin (not even the two plugins I installed two weeks ago, which were up-to-date)... This happens on both of my machines:

Both configs have coq pinned to 8.13.2, which compiles flawlessly.

None of those packages got updated in last ten days, so I don't know what is causing breakage. gnu-make hasn't been updated since April 2020 either.

I'd be happy to help sorting this out, and can provide more logs too if need be (just tell me how to get them).

Thanks in advance ! :)

view this post on Zulip Gaëtan Gilbert (Oct 19 2021 at 14:47):

do you have COQBIN set as an env variable?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2021 at 14:47):

For weird reasons scripts need to use COQBIN/foo so I dunno, a slash is missing

view this post on Zulip David JULIEN (Oct 19 2021 at 14:58):

Gosh now I feel stupid. This is my .zprofile :

export OPAMROOT="$XDG_DATA_HOME/opam"
export COQBIN="$OPAMROOT/default/bin"

Added a /, and now it works. Nice catch ! I've never had to put a / at the end of those variables so I didn't even think of it -- even more since I was looking for bincoq.

(as to why it used work but doesn't anymore...)

view this post on Zulip Notification Bot (Oct 19 2021 at 21:41):

David JULIEN has marked this topic as resolved.

Last updated: Jun 03 2023 at 17:29 UTC