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

Bug#1012061: marked as done (coq breaks coquelicot autopkgtest: Compiled library Coquelicot.Rcomplements makes inconsistent assumptions over library Coq.Init.Ltac)



Your message dated Thu, 02 Jun 2022 05:37:58 +0000
with message-id <E1nwdWw-000FDy-Ig@fasolo.debian.org>
and subject line Bug#1012061: fixed in coquelicot 3.2.0-4
has caused the Debian Bug report #1012061,
regarding coq breaks coquelicot autopkgtest: Compiled library Coquelicot.Rcomplements 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.)


-- 
1012061: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1012061
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
Source: coq, coquelicot
Control: found -1 coq/8.15.1+dfsg-2
Control: found -1 coquelicot/3.2.0-2
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 coquelicot 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
coquelicot             from testing    3.2.0-2
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/coquelicot/22188156/log.gz

File "./BacS2013.v", line 24, characters 0-112:
Error:
Compiled library Coquelicot.Rcomplements (in file /usr/lib/ocaml/coq/user-contrib/Coquelicot/Rcomplements.vo) makes inconsistent assumptions over library Coq.Init.Ltac

autopkgtest [11:12:10]: test examples

Attachment: OpenPGP_signature
Description: OpenPGP digital signature


--- End Message ---
--- Begin Message ---
Source: coquelicot
Source-Version: 3.2.0-4
Done: Julien Puydt <jpuydt@debian.org>

We believe that the bug you reported is fixed in the latest version of
coquelicot, 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 1012061@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 coquelicot 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: Thu, 02 Jun 2022 07:10:00 +0200
Source: coquelicot
Architecture: source
Version: 3.2.0-4
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Closes: 1012061
Changes:
 coquelicot (3.2.0-4) unstable; urgency=medium
 .
   * Re-upload because of ABI breakage. (Closes: #1012061)
Checksums-Sha1:
 16c87168968764894d327b220b32ef4984b1a784 2048 coquelicot_3.2.0-4.dsc
 dbc551d3ab396f274458dc9bb95ff6b69e4a2e74 2244 coquelicot_3.2.0-4.debian.tar.xz
 75c6b2658f0b36c7072129d47a277e20afe4170e 6764 coquelicot_3.2.0-4_source.buildinfo
Checksums-Sha256:
 66d93e47035a8510e7c074a193bfd606b4386c319adfb52e7a4be12e5805af80 2048 coquelicot_3.2.0-4.dsc
 573d6f8731cd8dee3034c326aabf7687874df818842b9c15bbc62ae287697170 2244 coquelicot_3.2.0-4.debian.tar.xz
 c81b61c8c23151c252aece20d9c3600c080960320335db2bd0cfb7cf500d5636 6764 coquelicot_3.2.0-4_source.buildinfo
Files:
 06d03f3882b62fe64d01dd9ad5bb0d19 2048 ocaml optional coquelicot_3.2.0-4.dsc
 7c56151c47c25b5a6ad7829ff7fb64d4 2244 ocaml optional coquelicot_3.2.0-4.debian.tar.xz
 6a37c44936e4fc8e88fdde910cff2596 6764 ocaml optional coquelicot_3.2.0-4_source.buildinfo

-----BEGIN PGP SIGNATURE-----

iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmKYRjwSHGpwdXlkdEBk
ZWJpYW4ub3JnAAoJEATFO9f+AwVRADMQAJZXX9y0fNtGlwGCkcJkBTn2eRrLf7c0
aKhp7F9caF14tXQV7coRK2KBinmrF0lxOwhjeOM8H5iPH9ieS4V7o8nBJTGq2SyH
/mDR/QwmoCyFh4E51kASptaXsO1GkFwLaOBdRrjvmDjzjqsEYJBVollTgTpNGt3t
eQP5fe/QBVqBO1zrXQevAZoogxQ1ceJvHadzF0jhu9hvaPiARqCawMbkm6ppxR/v
2z3Im5e6uQDGSwbRcuuz7W2eDCenzzq3B8thvvQsCKdiwUjbUMuSO3eCXGG+8owU
s40hUmdCslIhwD06nqVfXhhgN35vKnzqeoo0hsFLidYSvn+A7MPON1AnwrBuHBjD
dyMVgeYRlazerDqz4N6astIp1yymkd+NJ2swbGKVYDNUpyeNpWHihxwTQaqII/hv
wj5oWauNIGhlv1COFmb5F2nDm1yckQrsV060KHAXaTqtY0OEt3vwzRC4/9hJ5XsU
5Fl/5OWRpP8Xb122h89f1DpB58G0SStUKuvXfly0p/UCFZqy5i6VobQ/G9wb9uTR
DTwiLm9dTykV0CSqAviUvo+hcV/vg2nNBHWbvGAOH1UbzDUm7Dkel66rdMfgqokY
lORJoOpndJSRQFsj6Qdjio72JxqOt7i0ptZCMmTqZ7xaGNQv9IOIeo6DUQXWA5zJ
ligk8hPxIwWj
=QatF
-----END PGP SIGNATURE-----

--- End Message ---

Reply to: