#977258 libssreflect-coq: ABI break by coq binNMU

Package:
libssreflect-coq
Source:
ssreflect
Submitter:
Nobuhiro Ban
Date:
2022-07-05 06:39:07 UTC
Severity:
normal
#977258#5
Date:
2020-12-13 09:28:01 UTC
From:
To:
Dear Maintainer,

I cannot use the ssreflect library in my Debian coq env (amd64 testing).

the code:

gets an error:



Additional information

libssreflect-coq 1.11.0-2 is built against coq 8.12.0-3+b2.
(buildd log: https://buildd.debian.org/status/fetch.php?pkg=ssreflect&arch=all&ver=1.11.0-2&stamp=1604474661&raw=0
)

But the current coq version is 8.12.0-3+b3.

I think this package should depend on "libcoq-ocaml-<Hash>",
because "coq-<CoqVer>+<OCamlVer>" is insufficient for binNMUs.

I got the same issue before,
libssreflect-coq 1.11.0-1 (built against coq 8.12.0-3) + coq 8.12.0-3+b1.


Regards,
Nobuhiro Ban
#977258#12
Date:
2021-01-11 08:50:01 UTC
From:
To:
Hello,

I have now recompiled the package (and updated to a newer version), so
it is at least solved for the moment.

I am not sure what exactly has to be done, will have to consult with the
teamm.
#977258#17
Date:
2021-01-11 09:36:12 UTC
From:
To:
clone 977258 -1
reassign -1 coq
severity -1 wishlist
retitle -1 Please compute ABIs for Coq libraries
thanks

Hello,

Le 13/12/2020 à 10:28, Nobuhiro Ban a écrit :

Not exactly. Ideally, a ABI/hash should be computed for each Coq library
(including the standard library), by a to-be-written dh_coq. The ABI
would include versions of OCaml and Coq, but also whatever Coq uses to
assess "assumption consistency".

Note that <Hash> in libcoq-ocaml-<Hash> is arch-specific, so if
ssreflect actually depends on libcoq-ocaml-<Hash>, ssreflect should be
arch:any and not arch:all.


Cheers,
#977258#24
Date:
2022-07-05 06:35:05 UTC
From:
To:
Hi,

since I wrote dh-coq and started using it for all coq-related packages,
we do have an ABI that will avoid future breakages.

Cheers,

J.Puydt