Bug#977258: libssreflect-coq: ABI break by coq binNMU
- To: Nobuhiro Ban <ban.nobuhiro@gmail.com>, 977258@bugs.debian.org
- Subject: Bug#977258: libssreflect-coq: ABI break by coq binNMU
- From: Ralf Treinen <treinen@free.fr>
- Date: Mon, 11 Jan 2021 09:50:01 +0100
- Message-id: <X/wROSWS/eSB974Q@seneca.home.org>
- Reply-to: Ralf Treinen <treinen@free.fr>, 977258@bugs.debian.org
- In-reply-to: <CADQnRq7rG5VGnzT4d5FRLcB904Bk1J+d74Zg8=-W3D1EpLBU8w@mail.gmail.com>
- References: <CADQnRq7rG5VGnzT4d5FRLcB904Bk1J+d74Zg8=-W3D1EpLBU8w@mail.gmail.com> <CADQnRq7rG5VGnzT4d5FRLcB904Bk1J+d74Zg8=-W3D1EpLBU8w@mail.gmail.com>
Hello,
On Sun, Dec 13, 2020 at 06:28:01PM +0900, Nobuhiro Ban wrote:
> I cannot use the ssreflect library in my Debian coq env (amd64 testing).
>
> the code:
> > Require Import mathcomp.ssreflect.ssreflect.
>
> gets an error:
>
> > 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 have now recompiled the package (and updated to a newer version), so
it is at least solved for the moment.
> I think this package should depend on "libcoq-ocaml-<Hash>",
> because "coq-<CoqVer>+<OCamlVer>" is insufficient for binNMUs.
I am not sure what exactly has to be done, will have to consult with the
teamm.
-Ralf.
Reply to: