[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#1012060: marked as done (coq breaks coq-bignums autopkgtest: Compiled library Bignums.BigN.BigN makes inconsistent assumptions over library Coq.Init.Ltac)

Your message dated Wed, 01 Jun 2022 13:34:00 +0000
with message-id <E1nwOU4-000ImK-UD@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 owner@bugs.debian.org
immediately.)


-- 
1012060: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1012060
Debian Bug Tracking System
Contact owner@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-ci@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

Attachment: OpenPGP_signature
Description: OpenPGP digital signature


--- End Message ---
--- Begin Message --- 
Source: coq-bignums
Source-Version: 8.15.0-3
Done: Julien Puydt <jpuydt@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 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)


-----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-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-----

--- End Message ---
Reply to: