Opam build fail with Coq 8.18.0 and ocaml 5.1.0

[threonorm]

Hi,

Thanks for your work!

I am having a little issue, it seems coq-deriving is failing for Coq 8.18 and Ocaml 5.1.0:

[ERROR] The compilation of coq-deriving.dev failed at "make -j 11".

#=== ERROR while compiling coq-deriving.dev ===================================#
# context     2.1.5 | linux/x86_64 | ocaml-base-compiler.5.1.0 | https://coq.inria.fr/opam/extra-dev#2024-06-06 11:43
# path        ~/.opam/ocaml5/.opam-switch/build/coq-deriving.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -j 11
# exit-code   2
# env-file    ~/.opam/log/coq-deriving-1309739-e0a4c8.env
# output-file ~/.opam/log/coq-deriving-1309739-e0a4c8.out
### output ###
# [...]
# *** Warning: in file theories/base.v, library structures is required from root HB and has not been found in the loadpath!
# *** Warning: in file theories/ind.v, library structures is required from root HB and has not been found in the loadpath!
# *** Warning: in file theories/instances.v, library structures is required from root HB and has not been found in the loadpath!
# COQC theories/base.v
# File "./theories/base.v", line 1, characters 0-34:
# Error: Cannot find a physical path bound to logical path
# structures with prefix HB.
# 
# make[2]: *** [CoqMakefile:838: theories/base.vo] Error 1
# make[2]: *** [theories/base.vo] Deleting file 'theories/base.glob'
# make[1]: *** [CoqMakefile:409: all] Error 2
# make: *** [Makefile:13: invoke-coqmakefile] Error 2

[arthuraa]

Hi,

Thanks for the report! I am currently traveling and don't have much time to look into this. I should be able to debug this in a week or two. In the meantime, did you make sure that you have all the required dependencies? You seem to be missing Hierarchy Builder, which a transitive dependency of extructures via mathcomp 2.0.0.

[arthuraa]

@threonorm Could you please include the exact commands that you ran to compile the library?