Your message dated Wed, 01 Jun 2022 13:34:00 +0000
with message-id <e1nwou4-000imk...@fasolo.debian.org>
and subject line Bug#1012060: fixed in coq-bignums 8.15.0-3
has caused the Debian Bug report #1012060,
regarding coq breaks coq-bignums autopkgtest: Compiled library
Bignums.BigN.BigN makes inconsistent assumptions over library Coq.Init.Ltac
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ow...@bugs.debian.org
immediately.)
--
1012060: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1012060
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Source: coq, coq-bignums
Control: found -1 coq/8.15.1+dfsg-2
Control: found -1 coq-bignums/8.15.0-1
Severity: serious
Tags: sid bookworm
User: debian...@lists.debian.org
Usertags: breaks needs-update
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
OpenPGP_signature
Description: OpenPGP digital signature
--- End Message ---
--- Begin Message ---
Source: coq-bignums
Source-Version: 8.15.0-3
Done: Julien Puydt <jpu...@debian.org>
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 1012...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Julien Puydt <jpu...@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 ftpmas...@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
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-ma...@lists.debian.org>
Changed-By: Julien Puydt <jpu...@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-----
--- End Message ---
