Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10

[Jochen Sprickerhof]

Control: tag -1 - moreinfo

Hi Sebastian,

* Sebastian Ramacher <sramac...@debian.org> [2023-04-22 11:10]:

On 2023-04-21 21:35:21 +0200, Jochen Sprickerhof wrote:

Package: release.debian.org
Severity: normal
User: release.debian....@packages.debian.org
Usertags: binnmu
X-Debbugs-Cc: w...@packages.debian.org
Control: affects -1 + src:why3 src:frama-c

Hi release team,

can you please binNMU why3 to pick up the new ABI:

nmu why3_1.5.1-1+b1 . ANY . unstable . -m "Rebuild with new OCaml ABI"

And afterwards frama-c needs a rebuild against the new why3:

nmu frama-c_20220511-manganese-3-10 . ANY . unstable . -m "Rebuild with new OCaml 
ABI (Closes: #1033701)"

why3 installs perfectly fine in both bookworm and unstable. Why is this
needed? We are past the point of doing transitions (especially
uncoordinated ones).

$ apt-cache show libwhy3-ocaml-dev | grep Provides
Provides: libwhy3-ocaml-dev-mzlf3

And frama-c-base depends exactly on that:

apt-cache show frama-c-base | grep -o "libwhy3-ocaml-dev[^,]*"
libwhy3-ocaml-dev-mzlf3

But rebuilding the package in testing generates a different hash:

$ sbuild -d testing why3 | grep Provides
Provides: libwhy3-ocaml-dev-2bt20


Cheers Jochen

I don't know enough OCaml but rebuilding why3 and frama-c on top fixes frama-c and thus #1033701 for me. My understanding is that dh-ocaml uses some hash to track the ABI of a library and encodes into a virtual package: So I assume this is not a new transition but a missing rebuild for an old transition.

signature.asc
Description: PGP signature