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...@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.Ltac
make: *** [Makefile:10: success/NumberScopes.vo] Error 1make: Leaving directory '/tmp/autopkgtest-lxc.1xnd4upm/downtmp/build.b30/src/tests'
autopkgtest [11:12:08]: test command1
OpenPGP_signature
Description: OpenPGP digital signature
