Stream: Hierarchy Builder devs & users

Topic: ✔ opam install issue


view this post on Zulip 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

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:15):

It seems elpi is not installed, which is weird since HB depends on it. Did opam install it? (the log is cut)

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:16):

Yes:

$ opam install elpi
[NOTE] Package elpi is already installed (current version is 1.16.10).

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:19):

opam install coq-elpi

view this post on Zulip 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).

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:21):

Here is my opam list
opam_list.txt

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:22):

coqc -where
ls `coqc -where`/user-contrib

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:23):

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)

view this post on Zulip 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

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:25):

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?

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:26):

echo 'From elpi Require Import elpi.' | coqtop

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:27):

$ echo 'From elpi Require Import elpi.' | coqtop
Welcome to Coq 8.16.1

Coq < [Loading ML file coq-elpi.elpi ... done]

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:28):

Hum, so here it works... I really don't know what opam does wrong.
Any COQ* env variable which could mislead opam?

view this post on Zulip Enrico Tassi (Sep 18 2023 at 08:28):

export| grep COQ

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:28):

hmm... maybe

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:30):

Indeed... I had COQBIN defined... I'm so stupid, sorry.

view this post on Zulip Pierre Rousselin (Sep 18 2023 at 08:30):

works now. Thanks and sorry again.

view this post on Zulip Notification Bot (Sep 18 2023 at 08:30):

Pierre Rousselin has marked this topic as resolved.


Last updated: Apr 21 2024 at 01:02 UTC