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 ---
- To: submit@bugs.debian.org
- Subject: coq breaks coq-bignums autopkgtest: Compiled library Bignums.BigN.BigN makes inconsistent assumptions over library Coq.Init.Ltac
- From: Paul Gevers <elbrus@debian.org>
- Date: Sun, 29 May 2022 17:33:43 +0200
- Message-id: <8cf9c175-e88f-6437-3873-202726979555@debian.org>
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.gzmake: 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.Ltacmake: *** [Makefile:10: success/NumberScopes.vo] Error 1make: Leaving directory '/tmp/autopkgtest-lxc.1xnd4upm/downtmp/build.b30/src/tests'autopkgtest [11:12:08]: test command1Attachment: OpenPGP_signature
Description: OpenPGP digital signature
--- End Message ---
--- Begin Message ---
- To: 1012060-close@bugs.debian.org
- Subject: Bug#1012060: fixed in coq-bignums 8.15.0-3
- From: Debian FTP Masters <ftpmaster@ftp-master.debian.org>
- Date: Wed, 01 Jun 2022 13:34:00 +0000
- Message-id: <E1nwOU4-000ImK-UD@fasolo.debian.org>
- Reply-to: Julien Puydt <jpuydt@debian.org>
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 ---