Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Dear Sebastian, Le 23/04/2023 à 11:36, Sebastian Ramacher a écrit : ocaml 4.13.1-4 causes the ABI to change for at least why3. Do you expect that the ABI of ther ocaml packages also changes? If so, we should rebuild the ocaml world before the release to not get any surprises if a ocaml package gets a stable update. See also: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1030785 The ABI of ocaml-compiler-libs changed (only on native architectures), with no visible changes in virtual packages, so anything using that is potentially broken. I (thought I) binNMUed all affected packages (there were a lot of them), but missed why3 for some reason. IMHO, the cleanest way to fix the issue for sure is to change the OCaml ABI advertised in the virtual package name. But that means an amount of work similar to an OCaml transition. Do we really work this kind of move at this stage of the freeze? I don't think so. A pretty good approximation to checking that everything is fine is to mass-rebuild everything (as Lucas Nussbaum does regularly), identify the (few, I expect) packages that FTBFS, and binNMU them (+ maybe some of their dependencies). I suspect why3 is special because it embeds modules provided by ocaml in a plugin (dh_ocaml's --nodefined-map is suspicious in this context) but this situation should be rare. Cheers, -- Stéphane
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Hi Stéphane
On 2023-04-22 20:28:34 +0200, Jochen Sprickerhof wrote:
> * Sebastian Ramacher [2023-04-22 16:06]:
> > 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.
>
> I can recreate the old ABI hash by downgrading the src:ocaml packages, i.e.:
>
> > 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-interp (= [-4.13.1-3),-] {+4.13.1-4),+}
> > ocaml-nox (= [-4.13.1-3),-] {+4.13.1-4),
>
> I leave the decision what to do with it to you.
ocaml 4.13.1-4 causes the ABI to change for at least why3. Do you expect
that the ABI of ther ocaml packages also changes? If so, we should
rebuild the ocaml world before the release to not get any surprises if a
ocaml package gets a stable update.
Cheers
--
Sebastian Ramacher
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
* Sebastian Ramacher [2023-04-22 16:06]:
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.
I can recreate the old ABI hash by downgrading the src:ocaml packages,
i.e.:
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-interp (= [-4.13.1-3),-] {+4.13.1-4),+}
ocaml-nox (= [-4.13.1-3),-] {+4.13.1-4),
I leave the decision what to do with it to you.
Cheers Jochen
signature.asc
Description: PGP signature
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
On 2023-04-22 11:30:48 +0200, Jochen Sprickerhof wrote:
> Control: tag -1 - moreinfo
>
> Hi Sebastian,
>
> * Sebastian Ramacher [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
Processed: Re: Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Processing control commands: > tag -1 - moreinfo Bug #1034691 [release.debian.org] nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10 Removed tag(s) moreinfo. -- 1034691: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1034691 Debian Bug Tracking System Contact ow...@bugs.debian.org with problems
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Control: tag -1 - moreinfo Hi Sebastian, * Sebastian Ramacher [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 So I assume this is not a new transition but a missing rebuild for an old transition. Cheers Jochen signature.asc Description: PGP signature
Processed: Re: Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Processing control commands: > tags -1 moreinfo Bug #1034691 [release.debian.org] nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10 Added tag(s) moreinfo. -- 1034691: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=1034691 Debian Bug Tracking System Contact ow...@bugs.debian.org with problems
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
Control: tags -1 moreinfo Hi Jochen 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). Cheers -- Sebastian Ramacher
Bug#1034691: nmu: why3_1.5.1-1+b1 frama-c_20220511-manganese-3-10
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)" Thanks! Jochen
