Bug#1143295: coq-relation-algebra: FTBFS: findlib error: coq-core.plugins.ltac not found in:

Package: src:coq-relation-algebra
Version: 1.7.11-1
Severity: serious
Tags: ftbfs forky sid

Dear maintainer:

During a rebuild of all packages in unstable, this package failed to build.

Below you will find the last part of the build log (probably the most
relevant part, but not necessarily). If required, the full build log
is available here:

https://people.debian.org/~sanvila/build-logs/202608/

About the archive rebuild: The build was made on virtual machines from AWS,
using sbuild and a reduced chroot with only build-essential packages.

If you cannot reproduce the bug please contact me privately, as I
am willing to provide ssh access to a virtual machine where the bug is
fully reproducible.

If this is really a bug in one of the build-depends, please use
reassign and add an affects on src:coq-relation-algebra, so that this is still
visible in the BTS web page for this package.

Thanks.

--------------------------------------------------------------------------------
[...]
 debian/rules clean
dh clean --with coq,ocaml
   debian/rules override_dh_auto_clean
make[1]: Entering directory '/<<PKGBUILDDIR>>'
make clean
make[2]: Entering directory '/<<PKGBUILDDIR>>'
coq_makefile -f _CoqProject -o Makefile.coq
CLEAN
make[2]: Leaving directory '/<<PKGBUILDDIR>>'
find . -name "*.aux" -delete
rm -f Makefile.coq Makefile.coq.conf .nia.cache
if test -f _CoqProject.orig; then \
  mv _CoqProject.orig _CoqProject; \
fi
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_ocamlclean
   dh_clean
 debian/rules binary
dh binary --with coq,ocaml
   dh_update_autotools_config
   dh_autoreconf
   dh_ocamlinit
   debian/rules override_dh_auto_configure
make[1]: Entering directory '/<<PKGBUILDDIR>>'
cp _CoqProject _CoqProject.orig
./configure --enable-ssr --enable-aac
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_auto_build
	make -j2
make[1]: Entering directory '/<<PKGBUILDDIR>>'
coq_makefile -f _CoqProject -o Makefile.coq
COQPP src/fold_g.mlg
COQPP src/mrewrite_g.mlg
COQPP src/reification_g.mlg
COQPP src/kat_reification_g.mlg
ROCQ DEP VFILES
CAMLDEP src/fold_g.ml
CAMLDEP src/mrewrite_g.ml
CAMLDEP src/reification_g.ml
CAMLDEP src/kat_reification_g.ml
CAMLDEP src/common.ml
CAMLDEP src/fold.ml
CAMLDEP src/mrewrite.ml
CAMLDEP src/reification.ml
CAMLDEP src/kat_dec.ml
CAMLDEP src/kat_reification.ml
OCAMLLIBDEP src/plugins.mlpack
OCAMLLIBDEP src/packed_fold.mlpack
OCAMLLIBDEP src/packed_mrewrite.mlpack
OCAMLLIBDEP src/packed_reification.mlpack
OCAMLLIBDEP src/packed_kat.mlpack
CAMLDEP src/common.mli
*** Error: In file theories/kat_reification.v
           findlib error: coq-core.plugins.ltac not found in:
           src/
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/../rocq-runtime/..
           /usr/local/lib/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/METAS
           required by `coq-relation-algebra.kat'
CAMLDEP src/fold.mli
CAMLDEP src/fold_g.mli
CAMLDEP src/mrewrite.mli
CAMLDEP src/mrewrite_g.mli
CAMLDEP src/reification.mli
CAMLDEP src/reification_g.mli
CAMLDEP src/kat_dec.mli
CAMLDEP src/kat_reification.mli
CAMLDEP src/kat_reification_g.mli
ROCQ DEP VFILES
*** Error: In file theories/kat_reification.v
           findlib error: coq-core.plugins.ltac not found in:
           src/
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/../rocq-runtime/..
           /usr/local/lib/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/METAS
           required by `coq-relation-algebra.kat'
ROCQ DEP VFILES
*** Error: In file theories/kat_reification.v
           findlib error: coq-core.plugins.ltac not found in:
           src/
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/../rocq-runtime/..
           /usr/local/lib/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/METAS
           required by `coq-relation-algebra.kat'
ROCQ DEP VFILES
*** Error: In file theories/kat_reification.v
           findlib error: coq-core.plugins.ltac not found in:
           src/
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/../rocq-runtime/..
           /usr/local/lib/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1
           /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/METAS
           required by `coq-relation-algebra.kat'
make[2]: *** No rule to make target '.Makefile.coq.d', needed by 'theories/common.vo'.  Stop.
make[1]: *** [Makefile.coq:411: all] Error 2
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
dh_auto_build: error: make -j2 returned exit code 2
make: *** [debian/rules:6: binary] Error 25
dpkg-buildpackage: error: debian/rules binary subprocess failed with exit status 2
--------------------------------------------------------------------------------