Error: The compilation of rocq-hierarchy-builder.1.9.1 failed at "make build".

[fblanqui]

Hi. I get a compilation error with opam with coq 8.19:

    - install atd                       2.16.0   [required by atdgen, atdts]
    - install atdgen                    2.15.0   [required by elpi]
    - install atdgen-runtime            2.16.0   [required by atdgen]
    - install atdts                     2.16.0   [required by elpi]
    - install biniou                    1.2.2    [required by atdgen]
    - install camlp-streams             5.0.1    [required by biniou]
    - install coq-elpi                  2.2.3
    - install coq-fourcolor-reals       1.4.1    [required by coq-hol-light]
    - install coq-hol-light-real-with-N 1.2.0    [required by coq-hol-light]
    - install coq-mathcomp-algebra      2.4.0    [required by coq-fourcolor-reals]
    - install coq-mathcomp-ssreflect    2.4.0    [required by coq-fourcolor-reals]
    - install easy-format               1.3.4    [required by atd]
    - install elpi                      1.19.6   [required by rocq-mathcomp-ssreflect]
    - install menhir                    20240715 [required by elpi]
    - install menhirCST                 20240715 [required by menhir]
    - install menhirLib                 20240715 [required by menhir]
    - install menhirSdk                 20240715 [required by menhir]
    - install ppx_optcomp               v0.15.0
    - install re                        1.12.0   [required by elpi]
    - install rocq-hierarchy-builder    1.9.1    [required by rocq-mathcomp-ssreflect]
    - install rocq-mathcomp-algebra     2.4.0    [required by coq-mathcomp-algebra]
    - install rocq-mathcomp-fingroup    2.4.0    [required by rocq-mathcomp-algebra]
    - install rocq-mathcomp-ssreflect   2.4.0    [required by coq-mathcomp-ssreflect]
    - install stdio                     v0.15.0

#=== ERROR while compiling rocq-hierarchy-builder.1.9.1 =======================#
  # context              2.3.0 | linux/x86_64 | ocaml-option-flambda.1 ocaml-variants.4.13.1+options | https://coq.inria.fr/opam/released#2025-05-12 13:16
  # path                 ~/.opam/4.13.1+flambda/.opam-switch/build/rocq-hierarchy-builder.1.9.1
  # command              /usr/bin/make build
  # exit-code            2
  # env-file             ~/.opam/log/rocq-hierarchy-builder-164-f52c5c.env
  # output-file          ~/.opam/log/rocq-hierarchy-builder-164-f52c5c.out
  ### output ###
  # Warning: in file HB/structures.v, library locker is required
  # [...]
  #          [module-not-found,filesystem,default]
  # COQC HB/structures.v
  # File "./HB/structures.v", line 17, characters 0-30:
  # Error: Cannot find a physical path bound to logical path
  # elpi with prefix elpi.
  # 
  # make[2]: *** [Makefile.coq:848: HB/structures.vo] Error 1
  # make[2]: *** [HB/structures.vo] Deleting file 'HB/structures.glob'
  # make[1]: *** [Makefile.coq:417: all] Error 2
  # make[1]: Leaving directory '/home/coq/.opam/4.13.1+flambda/.opam-switch/build/rocq-hierarchy-builder.1.9.1'
  # make: *** [Makefile:120: this-build] Error 2

[CohenCyril]

I vaguely remember seeing this error somewhere else in my messages recently. @proux01 @erikmd do you have a link to the issue?

[proux01]

I remember we experienced that on the Docker image for Coq 8.19 and MathComp 2.4 (and only that one). I tried to reproduce it locally but was unable to do so. I guess our best bet to understand this woud be to dive into that Docker image but I have no time for it now.

@fblanqui if you're indeed on that Coq 8.19/MC 2.4 combination, you're best short term workaround is probably to either upgrade to Coq 8.20 or downgrade to MC 2.3 (I'd recommend going for 8.20 or even 9.0 if possible, it's a huge improvement performance-wise).

[GenEars]

Hi @proux01, I am using rocq-prover 9.0 and have the same install issue (see below), hence the issue with HB seems elsewhere. Any piece of advice?

[ERROR] The compilation of rocq-hierarchy-builder.1.10.1 failed at "make build".

#=== ERROR while compiling rocq-hierarchy-builder.1.10.1 ======================#
# context     2.4.1 | linux/x86_64 | ocaml.4.13.1 | https://rocq-prover.org/opam/released#2025-10-30 14:37
# path        ~/.opam/default/.opam-switch/build/rocq-hierarchy-builder.1.10.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build make build
# exit-code   2
# env-file    ~/.opam/log/rocq-hierarchy-builder-139961-901a3f.env
# output-file ~/.opam/log/rocq-hierarchy-builder-139961-901a3f.out
### output ###
# [...]
# *** Warning: in file HB/structures.v, library ssrfun is required from root Corelib and has not been found in the loadpath!
# *** Warning: in file HB/structures.v, library elpi is required from root elpi and has not been found in the loadpath!
# *** Warning: in file HB/structures.v, library locker is required from root elpi.apps and has not been found in the loadpath!
# COQC HB/structures.v
# File "./HB/structures.v", line 2, characters 0-45:
# Error: Cannot find a physical path bound to logical path
# ssreflect with prefix Corelib.
# 
# make[2]: *** [Makefile.coq:764 : HB/structures.vo] Erreur 1
# make[1]: *** [Makefile.coq:387 : all] Erreur 2
# make[1] : on quitte le répertoire « ~/.opam/default/.opam-switch/build/rocq-hierarchy-builder.1.10.1 »
# make: *** [Makefile:114 : this-build] Erreur 2

[GenEars]

Hi @proux01. Please forget my previous comment: forcing the reinstall of coq-core.9.0.1 solves the rocq-hierarchy-builder.1.10.1 install issue I have mentioned. Don't ask me why, it just works.