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
