On 2023-04-22 11:30:48 +0200, Jochen Sprickerhof wrote:
> 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).
>
> 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:
>
> $ 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
Both why3 and frama-c have been rebuilt after the last ocaml ABI change.
>From a quick between a build now and from the last why3, the following
packages changed (that appear to be relevant):
libcairo2-ocaml-dev (= [-0.6.2+dfsg-1+b1),-] {+0.6.4+dfsg-1),+}
ocaml (= [-4.13.1-3),-] {+4.13.1-4),+}
ocaml-base (= [-4.13.1-3),-] {+4.13.1-4),+}
ocaml-compiler-libs (= [-4.13.1-3),-] {+4.13.1-4),+}
ocaml-findlib (= [-1.9.3-1),-] {+1.9.6-1+b1),+}
ocaml-interp (= [-4.13.1-3),-] {+4.13.1-4),+}
ocaml-nox (= [-4.13.1-3),-] {+4.13.1-4),
So either the change in ocaml caused the ABI to change and we probably
need to rebuild the world of ocaml packages, or the ABI of why3 is
influenced by libcairo2-ocaml-dev but is missing the proper
dependencies.
Adding the OCaml maintainers to the loop to check the situation. But
overall this sounds liek a bug that we want to have fixed properly and
not paper over with a couple of rebuilds.
Cheers
--
Sebastian Ramacher
