Source: why3 Control: found -1 why3/1.5.1-1 Severity: serious Tags: sid bookworm User: debian-ci@lists.debian.org Usertags: breaks Dear maintainer(s),With a recent upload of why3 the autopkgtest of frama-c fails in testing when that autopkgtest is run with the binary packages of why3 from unstable. It passes when run with only packages from testing. In tabular form:
pass fail
why3 from testing 1.5.1-1
frama-c from testing 20220511-manganese-1.3
all others from testing from testing
I copied some of the output at the bottom of this report. The message
seems serious enough (to my eyes) that you'd want to prevent this on
partial upgrades and during dist-upgrades. Does why3 (version in
unstable) really break the version of frama-c in testing? Then adding a
*versioned* Breaks might be a good idea. Maybe the failure isn't as bad
as it looks, then please just close this bug report (but be warned, why3
might migrate then, while the fixed frama-c seems stuck).
Currently this regression is blocking the migration of why3 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=why3 https://ci.debian.net/data/autopkgtest/testing/amd64/f/frama-c/28047266/log.gz [kernel] User Error: cannot load plug-in 'frama-c-wp': cannot load module Details: implementation mismatch on Why3[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input. autopkgtest [20:18:19]: test eva
Attachment:
OpenPGP_signature
Description: OpenPGP digital signature