Bug#1143292: coq-corn: FTBFS: dh_auto_build: error: make -j2 INSTALL="install --strip-program=true" returned exit code 2

Package: src:coq-corn
Version: 8.20.0-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-corn, so that this is still
visible in the BTS web page for this package.

Thanks.

--------------------------------------------------------------------------------
[...]
 debian/rules clean
dh clean --with coq
   debian/rules override_dh_auto_clean
make[1]: Entering directory '/<<PKGBUILDDIR>>'
find . -name "*.aux" -delete
find . -name "*.glob" -delete
find . -name "*.vo*" -delete
rm -f .lia.cache .Makefile.d
rm -f Make Makefile Makefile.conf
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_clean
 debian/rules binary
dh binary --with coq
   dh_update_autotools_config
   dh_autoreconf
   debian/rules override_dh_auto_configure
make[1]: Entering directory '/<<PKGBUILDDIR>>'
./configure.sh
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
   dh_auto_build
	make -j2 INSTALL="install --strip-program=true"
make[1]: Entering directory '/<<PKGBUILDDIR>>'
ROCQ DEP VFILES
ROCQ compile algebra/RSetoid.v
ROCQ compile stdlib_omissions/Pair.v
File "./stdlib_omissions/Pair.v", line 1, characters 15-31:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./algebra/RSetoid.v", line 27, characters 15-33:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./algebra/RSetoid.v", line 29, characters 0-55:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./algebra/RSetoid.v", line 29, characters 0-55:
Warning: Notation "_ ≠ _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./algebra/RSetoid.v", line 85, characters 0-88:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope setoid_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
ROCQ compile tactics/CornTac.v
File "./tactics/CornTac.v", line 22, characters 15-40:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
ROCQ compile tactics/Step.v
ROCQ compile stdlib_omissions/P.v
ROCQ compile algebra/OperationClasses.v
File "./stdlib_omissions/P.v", line 2, characters 15-33:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./stdlib_omissions/P.v", line 2, characters 68-79:
Warning: Loading Stdlib without prefix is deprecated.
Use "From Stdlib Require ZArith_base"
or the deprecated "From Coq Require ZArith_base"
for compatibility with older Coq versions.
[deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
File "./algebra/OperationClasses.v", line 22, characters 15-33:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./stdlib_omissions/P.v", line 2, characters 0-80:
Warning: Library File Stdlib.ZArith.ZArith_base is deprecated
since Stdlib 9.0. use ZArith instead
[deprecated-library-file-since-Stdlib-9.0,deprecated-since-Stdlib-9.0,deprecated-library-file,deprecated,default]
File "./stdlib_omissions/P.v", line 26, characters 33-36:
Warning: Using "..." is deprecated, use "; auto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/P.v", line 26, characters 42-45:
Warning: Using "..." is deprecated, use "; auto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/P.v", line 37, characters 0-42:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
ROCQ compile metric2/Metric.v
ROCQ compile order/PartialOrder.v
File "./metric2/Metric.v", line 23, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./order/PartialOrder.v", line 55, characters 0-76:
Warning: Declaring a scope implicitly is deprecated; use in advance an
explicit "Declare Scope po_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
File "./order/PartialOrder.v", line 65, characters 72-75:
Warning: Using "..." is deprecated, use "; trivial." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./metric2/Metric.v", line 25, characters 0-54:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./metric2/Metric.v", line 25, characters 0-54:
Warning: Notation "_ ≠ _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./metric2/Metric.v", line 26, characters 0-55:
Warning: Notation "_ ≠ _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./metric2/Metric.v", line 26, characters 0-55:
Warning: Notation "_ ≠ _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./metric2/Metric.v", line 212, characters 0-56:
Warning: Implicitly declaring hint databases is deprecated. Please explicitly
create "metric"
[implicit-create-hint-db,deprecated-since-9.2,deprecated,default]
File "./metric2/Metric.v", line 245, characters 0-75:
Warning: Implicitly declaring hint databases is deprecated. Please explicitly
create "metric"
[implicit-create-hint-db,deprecated-since-9.2,deprecated,default]
ROCQ compile util/Container.v
File "./order/PartialOrder.v", line 98, characters 0-37:
Warning: "Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
[deprecated-exact-proof,deprecated-since-9.2,deprecated,default]
File "./order/PartialOrder.v", line 101, characters 0-32:
Warning: "Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
[deprecated-exact-proof,deprecated-since-9.2,deprecated,default]
File "./order/PartialOrder.v", line 104, characters 0-33:
Warning: "Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
[deprecated-exact-proof,deprecated-since-9.2,deprecated,default]
File "./order/PartialOrder.v", line 107, characters 0-37:
Warning: "Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
[deprecated-exact-proof,deprecated-since-9.2,deprecated,default]
File "./order/PartialOrder.v", line 110, characters 0-37:
Warning: "Proof term." is deprecated. Use "Proof. exact term. Qed." instead.
[deprecated-exact-proof,deprecated-since-9.2,deprecated,default]
File "./util/Container.v", line 1, characters 0-54:
Warning: Notation "_ = _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./util/Container.v", line 1, characters 0-54:
Warning: Notation "_ ≠ _" was already used in scope type_scope.
[notation-overridden,parsing,default]
File "./util/Container.v", line 4, characters 0-25:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
ROCQ compile util/PointFree.v
ROCQ compile tactics/DiffTactics1.v
File "./util/PointFree.v", line 1, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
ROCQ compile logic/PropDecid.v
ROCQ compile liouville/RingClass.v
ROCQ compile reals/stdlib/ConstructiveDiagonal.v
File "./liouville/RingClass.v", line 23, characters 22-26:
Warning: Loading Stdlib without prefix is deprecated.
Use "From Stdlib Require Ring" or the deprecated "From Coq Require Ring"
for compatibility with older Coq versions.
[deprecated-missing-stdlib,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 15, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 16, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 17, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 18, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 19, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 20, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 21, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 22, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 23, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
ROCQ compile reals/stdlib/ConstructivePartialFunctions.v
File "./reals/stdlib/ConstructivePartialFunctions.v", line 18, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 19, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 289, characters 12-27:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 289, characters 12-27:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 302, characters 12-27:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 302, characters 12-27:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 20, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 21, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 22, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 23, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 24, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 25, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructivePartialFunctions.v", line 26, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 437, characters 8-23:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 437, characters 8-23:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 562, characters 43-58:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
File "./reals/stdlib/ConstructiveDiagonal.v", line 562, characters 43-58:
Warning: Notation Nat.div_le_mono is deprecated since 8.17.
Use Div0.div_le_mono instead.
[deprecated-syntactic-definition-since-8.17,deprecated-since-8.17,deprecated-syntactic-definition,deprecated,default]
ROCQ compile reals/stdlib/Markov.v
File "./reals/stdlib/Markov.v", line 13, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/Markov.v", line 14, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/stdlib/Markov.v", line 15, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
ROCQ compile reals/fast/LazyNat.v
File "./reals/fast/LazyNat.v", line 22, characters 15-32:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./reals/fast/LazyNat.v", line 111, characters 0-95:
Warning: Implicitly declaring Rewrite hint databases is deprecated. Please
explicitly create "UnLazyNat"
[implicit-create-rewrite-hint-db,deprecated-since-9.2,deprecated,default]
ROCQ compile stdlib_omissions/List.v
ROCQ compile stdlib_omissions/Z.v
File "./stdlib_omissions/List.v", line 1, characters 15-29:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./stdlib_omissions/Z.v", line 2, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./stdlib_omissions/List.v", line 4, characters 2-18:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
File "./stdlib_omissions/List.v", line 15, characters 34-37:
Warning: Using "..." is deprecated, use "; auto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/List.v", line 16, characters 32-35:
Warning: Using "..." is deprecated, use "; auto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/List.v", line 24, characters 16-19:
Warning: Using "..." is deprecated, use "; eauto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/List.v", line 27, characters 18-21:
Warning: Using "..." is deprecated, use "; eauto." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/List.v", line 30, characters 0-30:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated-since-8.10,deprecated,default]
File "./stdlib_omissions/List.v", line 42, characters 14-17:
Warning: Using "..." is deprecated, use "; auto with arith." instead
[deprecated-end-tac,deprecated-since-9.2,deprecated,default]
File "./stdlib_omissions/List.v", line 42, characters 9-17:
Error: No such Hint database: arith.

make[2]: *** [Makefile:815: stdlib_omissions/List.vo] Error 1
make[2]: *** [stdlib_omissions/List.vo] Deleting file 'stdlib_omissions/List.glob'
make[2]: *** Waiting for unfinished jobs....
File "./stdlib_omissions/Z.v", line 4, characters 5-8:
Warning: "From Coq" has been replaced by "From Stdlib".
[deprecated-from-Coq,deprecated-since-9.0,deprecated,default]
make[1]: *** [Makefile:411: all] Error 2
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
dh_auto_build: error: make -j2 INSTALL="install --strip-program=true" returned exit code 2
make: *** [debian/rules:4: binary] Error 25
dpkg-buildpackage: error: debian/rules binary subprocess failed with exit status 2
--------------------------------------------------------------------------------