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).