Pierre Rousselin (Sep 18 2023 at 08:12): Pierre Rousselin (Sep 18 2023 at 08:12):(Again sorry if this is very naive, I'm still not very comfortable with opam). I tried to install mathcomp-analysis and failed because Hierarchy Builder won't be installed. Here is the error message. I tried with Coq 8.16.1, Coq 8.17.1 and Coq.8.18.1 and OCaml 4.14.1.
⬇ retrieved coq-hierarchy-builder.1.5.0 (cached)
[ERROR] The compilation of coq-hierarchy-builder.1.5.0 failed at "make build".
#=== ERROR while compiling coq-hierarchy-builder.1.5.0 ========================#
# context 2.1.3 | linux/x86_64 | ocaml.4.14.1 | https://coq.inria.fr/opam/released#2023-09-17 19:30
# path ~/.opam/coq.8.16.1/.opam-switch/build/coq-hierarchy-builder.1.5.0
# command ~/.opam/opam-init/hooks/sandbox.sh build make build
# exit-code 2
# env-file ~/.opam/log/coq-hierarchy-builder-1325516-b0befe.env
# output-file ~/.opam/log/coq-hierarchy-builder-1325516-b0befe.out
### output ###
# Warning: in file structures.v, library elpi is required
# [...]
# [module-not-found,filesystem,default]
# COQC structures.v
# File "./structures.v", line 18, characters 0-30:
# Error: Cannot find a physical path bound to logical path
# elpi with prefix elpi.
#
# make[2]: *** [Makefile.coq:838: structures.vo] Error 1
# make[2]: *** [structures.vo] Suppression du fichier « structures.glob »
# make[1]: *** [Makefile.coq:409: all] Error 2
# make[1] : on quitte le répertoire « /home/pierre/.opam/coq.8.16.1/.opam-switch/build/coq-hierarchy-builder.1.5.0 »
# make: *** [Makefile:97: this-build] Error 2
It seems elpi is not installed, which is weird since HB depends on it. Did opam install it? (the log is cut)
Pierre Rousselin (Sep 18 2023 at 08:16):Yes:
$ opam install elpi
[NOTE] Package elpi is already installed (current version is 1.16.10).
opam install coq-elpi
Pierre Rousselin (Sep 18 2023 at 08:20):$ opam install coq-elpi
[NOTE] Package coq-elpi is already installed (current version is 1.16.0).
Here is my opam list
opam_list.txt
Enrico Tassi (Sep 18 2023 at 08:22):coqc -where
ls `coqc -where`/user-contrib
The list of packages is OK, but maybe your opam root is broken. Did you tamper with it? (eg run make install by hand on a coq project)
Pierre Rousselin (Sep 18 2023 at 08:24):$ coqc -where
/home/pierre/.opam/coq.8.16.1/lib/coq
$ ls $(coqc -where)/user-contrib
elpi Ltac2
Enrico Tassi said:
The list of packages is OK, but maybe your opam root is broken. Did you tamper with it? (eg run make install by hand on a coq project)
I don't think so. Are there commands to check this?
Enrico Tassi (Sep 18 2023 at 08:26):echo 'From elpi Require Import elpi.' | coqtop
$ echo 'From elpi Require Import elpi.' | coqtop
Welcome to Coq 8.16.1
Coq < [Loading ML file coq-elpi.elpi ... done]
Hum, so here it works... I really don't know what opam does wrong.
Any COQ* env variable which could mislead opam?
Enrico Tassi (Sep 18 2023 at 08:28):export| grep COQ
Pierre Rousselin (Sep 18 2023 at 08:28):hmm... maybe
Pierre Rousselin (Sep 18 2023 at 08:30):Indeed... I had COQBIN defined... I'm so stupid, sorry.
Pierre Rousselin (Sep 18 2023 at 08:30):works now. Thanks and sorry again.
Notification Bot (Sep 18 2023 at 08:30):Pierre Rousselin has marked this topic as resolved.
Last updated: Sep 15 2024 at 13:02 UTC