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

[Paul Gevers <elbrus@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.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