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

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

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