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 ! :)
do you have COQBIN set as an env variable?
For weird reasons scripts need to use
COQBIN/foo so I dunno, a slash is missing
Gosh now I feel stupid. This is my .zprofile :
export OPAMROOT="$XDG_DATA_HOME/opam" export COQBIN="$OPAMROOT/default/bin"
/, 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...)
David JULIEN has marked this topic as resolved.
Last updated: Feb 04 2023 at 01:03 UTC