Bug#977258: libssreflect-coq: ABI break by coq binNMU

[Stéphane Glondu <glondu@crans.org>]

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 :
>> Compiled library mathcomp.ssreflect.ssreflect (in file /usr/lib/coq/user-contrib/mathcomp/ssreflect/ssreflect.vo) makes inconsistent assumptions over library Coq.Init.Ltac
> [...]
> I think this package should depend on "libcoq-ocaml-<Hash>",
> because "coq-<CoqVer>+<OCamlVer>" is insufficient for binNMUs.

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,

-- 
Stéphane