#979756 Please compute ABIs for Coq libraries

Package:
coq
Source:
coq
Description:
proof assistant for higher-order logic (toplevel and compiler)
Submitter:
Nobuhiro Ban
Date:
2022-06-13 23:09:03 UTC
Severity:
wishlist
#979756#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
#979756#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.
#979756#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,
#979756#32
Date:
2022-06-13 23:05:48 UTC
From:
To:
Hi,

the newly uploaded dh-coq does abi key computation and use them for better
deps, and now all coq-related packages use it, so this report can be closed.

Cheers,

J.Puydt