Bug#1145675: libcoq-micromega-plugin: Missing ocaml/coq dependencies
Adrian Bunk <[email protected]>
| Newsgroups | gmane.linux.debian.devel.ocaml |
|---|---|
| Message-ID | <178775652477.3564649.15496850413477652595.reportbug__24533.4389664762$1787756609$gmane$org@localhost> |
Package: libcoq-micromega-plugin
Version: 1.1.1-1
Severity: serious
Tags: ftbfs patch
Control: affects -1 src:ssreflect
https://buildd.debian.org/status/fetch.php?pkg=ssreflect&arch=amd64&ver=2.6.0-3%2Bb1&stamp=1787752532&raw=0
...
ROCQ compile algebra/binnums.v
File "./algebra/binnums.v", line 2, characters 0-51:
Error:
Compiled library micromega_plugin.PosDef (in file /usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/micromega_plugin/PosDef.vo) makes inconsistent assumptions over library Corelib.Init.Prelude
make[4]: *** [Makefile.coq:815: algebra/binnums.vo] Error 1
Fix:
--- rocq-micromega-plugin-1.1.1/debian/control 2026-07-27 22:07:30.000000000 +0300
+++ rocq-micromega-plugin-1.1.1/debian/control 2026-07-27 22:07:30.000000000 +0300
@@ -21,7 +21,7 @@
Package: libcoq-micromega-plugin
Architecture: any
-Depends: ${misc:Depends}
+Depends: ${misc:Depends}, ${ocaml:Depends}, ${coq:Depends}
Recommends: coq
Provides:${coq:Provides}
Description: Semi-decision procedures for arithmetic in Rocq