[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Bug#977258: marked as done (libssreflect-coq: ABI break by coq binNMU)

Your message dated Tue, 05 Jul 2022 08:35:05 +0200
with message-id <49817a9ac55427be1bd5ce3bc3b299a56c97463e.camel@gmail.com>
and subject line Using dh-coq fixes those issues
has caused the Debian Bug report #977258,
regarding libssreflect-coq: ABI break by coq binNMU
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
977258: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=977258
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: libssreflect-coq
Version: 1.11.0-2
Severity: grave
Justification: renders package unusable

Dear Maintainer,

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



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


-- System Information:
Debian Release: bullseye/sid
  APT prefers testing-debug
  APT policy: (500, 'testing-debug'), (500, 'stable-debug'), (500,
'testing'), (500, 'stable')
Architecture: amd64 (x86_64)

Kernel: Linux 5.9.0-3-amd64 (SMP w/4 CPU threads)
Kernel taint flags: TAINT_FIRMWARE_WORKAROUND
Locale: LANG=ja_JP.UTF-8, LC_CTYPE=ja_JP.UTF-8 (charmap=UTF-8), LANGUAGE not set
Shell: /bin/sh linked to /bin/dash
Init: systemd (via /run/systemd/system)
LSM: AppArmor: enabled

Versions of packages libssreflect-coq depends on:
ii  coq [coq-8.12.0+4.11.1]  8.12.0-3+b3
ii  libcoq-ocaml             8.12.0-3+b3

libssreflect-coq recommends no packages.

libssreflect-coq suggests no packages.

-- debconf-show failed

--- End Message ---
--- Begin Message --- 
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

--- End Message ---
Reply to: