Dear maintainer(s),

With a recent upload of coq the autopkgtest of coq-bignums fails in
testing when that autopkgtest is run with the binary packages of coq
from unstable. It passes when run with only packages from testing. In
tabular form:

                        pass            fail
coq                    from testing    8.15.1+dfsg-2
coq-bignums            from testing    8.15.0-1
all others             from testing    from testing

I copied some of the output at the bottom of this report.

Currently this regression is blocking the migration of coq to testing
[1]. Due to the nature of this issue, I filed this bug report against
both packages. Can you please investigate the situation and reassign the
bug to the right package?

More information about this bug and the reason for filing it can be found on
https://wiki.debian.org/ContinuousIntegration/RegressionEmailInformation

Paul

[1] https://qa.debian.org/excuses.php?package=coq

https://ci.debian.net/data/autopkgtest/testing/amd64/c/coq-bignums/22188155/log.gz

make: Entering directory
'/tmp/autopkgtest-lxc.1xnd4upm/downtmp/build.b30/src/tests'
coqc success/NumberScopes.v
File "./success/NumberScopes.v", line 7, characters 0-33:
Error:
Compiled library Bignums.BigN.BigN (in file
/usr/lib/ocaml/coq/user-contrib/Bignums/BigN/BigN.vo) makes inconsistent
assumptions over library Coq.Init.Ltac

make: *** [Makefile:10: success/NumberScopes.vo] Error 1
make: Leaving directory
'/tmp/autopkgtest-lxc.1xnd4upm/downtmp/build.b30/src/tests'
autopkgtest [11:12:08]: test command1

We believe that the bug you reported is fixed in the latest version of
coq-bignums, which is due to be installed in the Debian FTP archive.

A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 1012060@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Julien Puydt <jpuydt@debian.org> (supplier of updated coq-bignums package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
Format: 1.8
Date: Wed, 01 Jun 2022 15:07:56 +0200
Source: coq-bignums
Architecture: source
Version: 8.15.0-3
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Closes: 1012060
Changes:
 coq-bignums (8.15.0-3) unstable; urgency=medium
 .
   * Bump standards-version to 4.6.1.
   * Upload will fix ABI breakage. (Closes: #1012060)
Checksums-Sha1:
 3f3df1fa8f34290851f93292fa6a7ad840e78471 2188 coq-bignums_8.15.0-3.dsc
 4224f702671ead7e36d91a98cdf65f06e79c1b1a 1844 coq-bignums_8.15.0-3.debian.tar.xz
 95b32356f7cb5e2abc83a635c5be588d2f1ac79c 6730 coq-bignums_8.15.0-3_source.buildinfo
Checksums-Sha256:
 012c705a48514c5b398a7bac6644173277bc3d0bc215b0811849abc0a956ad42 2188 coq-bignums_8.15.0-3.dsc
 0ab9add4884ce2cedf6e4eee484445258c69cfca7bd73a6430ed0d6c51982fc8 1844 coq-bignums_8.15.0-3.debian.tar.xz
 2f62f8c8af0f15e8d9498ca7bec0039e73bab63cc111d57a7c912703f39bcdac 6730 coq-bignums_8.15.0-3_source.buildinfo
Files:
 0ffaf398963e9f5430c7bdd3bdecd07d 2188 ocaml optional coq-bignums_8.15.0-3.dsc
 f971acc8efcfd3e5b5a88ae8a113abc1 1844 ocaml optional coq-bignums_8.15.0-3.debian.tar.xz
 815bdcb172af7c328cdbac5d4c4bc408 6730 ocaml optional coq-bignums_8.15.0-3_source.buildinfo
-----BEGIN PGP SIGNATURE-----

iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmKXZWISHGpwdXlkdEBk
ZWJpYW4ub3JnAAoJEATFO9f+AwVRRCoP/AirUfC8O/+lOXZrHbNcNJL4fQ2/9sVt
SIAe2dIRhk+6P9I/zzkqLhkoHwhVw+INGuyyX02BTLIftzVb5aUYba65UjKWzlOA
qx3Sw0YE/BtrTTnzwG6XG9YzzULCGq298ikrzMmQoaVHNTaTFlrIEatoLjIkxKIt
s1EYP//hw8E+RghCgQmnLXnRJjAJaTFGP8bNFZIMlKrmSnfr0s4mkI2HG0ZTd32r
kBR7VArsUcB9OCKHfOTGNCEh26NM+AWQVopmVrOGdDRnTo8hgNxvd4PrmiYFs/LW
sCxDy8lYzCL8xOE9MikzSRn3c2UyQNCI7ytrmqCglWKpAjuuYgjJ+aPihxTwqmr+
UZ0Zbw0/oo+xezC6ZW9DbEOISw4JYH9OkZTCVLXjcTbCO7jOZAxhDEWWKosaocLh
GJgjJnc1+WlBvS49StF3mML7V5UXjxGinGlVPNiZ+w2CaraJ7+yBLw3aq/cZY5xm
WGbtzBsuXBrvXA/fizwaQDoedeVlntCuTO/OIaJ7dyy3gclM9Z7sRK/+KWEQxaxR
kGZs/NUbcqlBDN1WZL9FbK+WSaax7kl1tfyT+PiCE4uFrXH3SD+IfAj7S98vYs5g
Bdt58ypbWcLmGxwvsPDeBEPOpFRDSRYN+aZGnKQ79Z9GBEuiX9xd22SBZuOUehYG
f858EKY+DUQh
=XQhJ
-----END PGP SIGNATURE-----

Hi,

letting the packages all migrate will solve the issue.

And when dh-coq will have cleared NEW, such issues will be a thing of
the past.

Cheers,

J.Puydt