Hi, the build of coq currently fails on non-native architectures due to the missing shared library file dllcoqperf_stubs.so [1]: dh_install: warning: Cannot find (any matches for) "/usr/lib/sparc64-linux-gnu/ocaml/5.3.0/stublibs/dllcoqperf_stubs.so" (tried in ., debian/tmp) dh_install: warning: libcoq-core-ocaml missing files: /usr/lib/sparc64-linux-gnu/ocaml/5.3.0/stublibs/dllcoqperf_stubs.so dh_install: error: missing files, aborting This can be fixed by making the installation of this file conditional with the help of the dh-exec package: diff -Nru debian.orig/control debian/control --- debian.orig/control 2025-11-10 10:59:00.000000000 +0100 +++ debian/control 2026-02-16 09:34:05.257704960 +0100 @@ -11,6 +11,7 @@ Build-Depends: debhelper-compat (= 13), dh-coq, + dh-exec, dh-ocaml, dh-python, ocaml-dune, diff -Nru debian.orig/libcoq-core-ocaml.install.in debian/libcoq-core-ocaml.install.in --- debian.orig/libcoq-core-ocaml.install.in 2025-08-21 15:13:46.000000000 +0200 +++ debian/libcoq-core-ocaml.install.in 2026-02-16 09:33:20.257429872 +0100 @@ -1,6 +1,7 @@ +#!/usr/bin/dh-exec @OCamlStdlibDir@/coq-core/META @OCamlStdlibDir@/rocq-runtime/META @OCamlDllDir@/dllcoqrun_stubs.so -@OCamlDllDir@/dllcoqperf_stubs.so +[amd64 arm64 armhf i386 ppc64el riscv64 s390x] @OCamlDllDir@/dllcoqperf_stubs.so @OCamlStdlibDir@/rocq-runtime/dev/ml_toplevel/include* # *.cmo and *.cmxs files are added by debian/rules Also, make sure that debian/libcoq-core-ocaml.install.in is mode 0755 (executable). Thanks, Adrian
Hi, OK, this doesn't work as expected as debian/rules messes with the file as well. Let's use this approach then:--- debian/rules.orig 2025-09-16 23:56:00.000000000 +0200 +++ debian/rules 2026-02-16 10:19:08.882267610 +0100 @@ -60,6 +60,10 @@ find debian/tmp$(OCAML_STDLIB_DIR)/rocq-runtime -regextype posix-awk \ -regex '.*\.(a|cmi|cmo|cmt|cmti|cmx|cmxa|ml|mli|o])$$' \ >> debian/libcoq-core-ocaml-dev.install + # remove dllcoqperf_stubs.so for non-native architectures + ifeq (,$(filter amd64 arm64 armhf i386 ppc64el riscv64 s390x), $(DEB_HOST_ARCH))) + sed -i '/.*dllcoqperf_stubs.so/d' debian/libcoq-core-ocaml-dev.install + endif override_dh_gencontrol: for u in $(PACKAGES); do \ Attaching a patch. Adrian
Hi, Small correction, there was a typo:--- debian/rules.orig 2025-09-16 23:56:00.000000000 +0200 +++ debian/rules 2026-02-16 10:49:34.185373014 +0100 @@ -60,6 +60,10 @@ find debian/tmp$(OCAML_STDLIB_DIR)/rocq-runtime -regextype posix-awk \ -regex '.*\.(a|cmi|cmo|cmt|cmti|cmx|cmxa|ml|mli|o])$$' \ >> debian/libcoq-core-ocaml-dev.install + # remove dllcoqperf_stubs.so for non-native architectures +ifeq (,$(filter amd64 arm64 armhf i386 ppc64el riscv64 s390x, $(DEB_HOST_ARCH))) + sed -i '/.*dllcoqperf_stubs.so/d' debian/libcoq-core-ocaml-dev.install +endif override_dh_gencontrol: for u in $(PACKAGES); do \ Adrian
Hi, OK, maybe I should test my patches properly. Here's a tested one:--- debian/rules.orig 2025-09-16 23:56:00.000000000 +0200 +++ debian/rules 2026-02-16 12:54:36.219191624 +0100 @@ -60,6 +60,10 @@ find debian/tmp$(OCAML_STDLIB_DIR)/rocq-runtime -regextype posix-awk \ -regex '.*\.(a|cmi|cmo|cmt|cmti|cmx|cmxa|ml|mli|o])$$' \ >> debian/libcoq-core-ocaml-dev.install + # remove dllcoqperf_stubs.so for non-native architectures +ifeq (,$(filter amd64 arm64 armhf i386 ppc64el riscv64 s390x, $(DEB_HOST_ARCH))) + sed -i '/.*dllcoqperf_stubs.so/d' debian/libcoq-core-ocaml.install +endif override_dh_gencontrol: for u in $(PACKAGES); do \ Sorry for that! Adrian
Hi, Le lundi 16 février 2026 à 13:02 +0100, John Paul Adrian Glaubitz a écrit : thanks for your help, I'll commit that to my packaging. An upload will have to wait until my tools stop misbehaving (#1122524), but the change will be ready to roll. Cheers, J.Puydt
Hello, Bug #1128189 in coq reported by you has been fixed in the Git repository and is awaiting an upload. You can see the commit message below and you can check the diff of the fix at: https://salsa.debian.org/ocaml-team/coq/-/commit/c7afde82030fde633c1eb7d981d866cd9e110b06 (this message was generated automatically) -- Greetings https://bugs.debian.org/1128189
Hi Julian, Great, thanks a lot! And sorry for the many iterations of this fix, I wasn't in the best mood this week. Adrian
We believe that the bug you reported is fixed in the latest version of
coq, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 1128189@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Julien Puydt <jpuydt@debian.org> (supplier of updated coq package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@ftp-master.debian.org)
Format: 1.8
Date: Fri, 10 Jul 2026 10:22:15 +0200
Source: coq
Binary: coq libcoq-core libcoq-core-ocaml libcoq-core-ocaml-dev rocqide
Architecture: source amd64
Version: 9.2.0+dfsg-1
Distribution: experimental
Urgency: medium
Maintainer: Julien Puydt <jpuydt@debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Description:
coq - proof assistant for higher-order logic (toplevel and compiler)
libcoq-core - proof assistant for higher-order logic (theories)
libcoq-core-ocaml - runtime libraries for Coq
libcoq-core-ocaml-dev - development libraries and tools for Coq
rocqide - proof assistant for higher-order logic (gtk interface)
Closes: 1128189 1128515
Changes:
coq (9.2.0+dfsg-1) experimental; urgency=medium
.
* Fix non-native platform compilation
thanks to John Paul Adrian Glaubitz (Closes: #1128189).
* Remove Benjamin Barenblat from Uploaders (Closes: #1128515).
* New upstream release.
* Rewrite d/watch.
* Bump standards-version to 4.7.4.
Checksums-Sha1:
2bea7b2e98b0baa4f36c6d114ad7804328fa0cce 2499 coq_9.2.0+dfsg-1.dsc
651b3d3858235f80e2aeb62ab57ce0b8081cce16 3946088 coq_9.2.0+dfsg.orig.tar.xz
c9fe4f599b6e49c92ed1ddb03191266c163bbf54 23724 coq_9.2.0+dfsg-1.debian.tar.xz
5a94f667ceb56a46d68850187b04a40f2f594860 17086 coq_9.2.0+dfsg-1_amd64.buildinfo
755a2d202ec0654594bf6741a6a70011fee8d59c 41143764 coq_9.2.0+dfsg-1_amd64.deb
cd726abfa59a0ce49d50c004ee1dc8e926128206 55434592 libcoq-core-ocaml-dev_9.2.0+dfsg-1_amd64.deb
b2179131b031eb671c33f7dcc4584f633f818a9f 25713812 libcoq-core-ocaml_9.2.0+dfsg-1_amd64.deb
0afeba87fd810a899c42ff2ba83db4ba2d71778a 1153152 libcoq-core_9.2.0+dfsg-1_amd64.deb
7724e9e329b4890337fb8b876a94bc4ce4db7908 1941608 rocqide_9.2.0+dfsg-1_amd64.deb
Checksums-Sha256:
8ec05acd85ad7c1a48730f8aeddfa58097c3ec8f864055ccc8adf99c3f0a0e81 2499 coq_9.2.0+dfsg-1.dsc
6d04561edb60ef68f5cf73c6f6fdb25c31cf6bf0c96f01fd0861f0c99a9c49db 3946088 coq_9.2.0+dfsg.orig.tar.xz
70fb1351fe0b0945eeb5ce07a9a55448f2ad1b81da2739db8de9072a9c3ce411 23724 coq_9.2.0+dfsg-1.debian.tar.xz
2937c9452403a2b382017c1d6013ddec39dac3f203693014ea99a979627248c6 17086 coq_9.2.0+dfsg-1_amd64.buildinfo
2be0691cc0285d354f206f0723730183319d29b0488b4038dd77732e7a15a866 41143764 coq_9.2.0+dfsg-1_amd64.deb
0bc26c1329a1f0a3b4e33d9b812375fcbe427272f112c4a12da0bf4459dc210d 55434592 libcoq-core-ocaml-dev_9.2.0+dfsg-1_amd64.deb
9958a5572017c1aa1292a99d8461eae5e693e822099a757e3d89987a197c5847 25713812 libcoq-core-ocaml_9.2.0+dfsg-1_amd64.deb
1c3de252c5270a63899daac7c6b435bb01dd3404e1659510314b889e1fb63d2f 1153152 libcoq-core_9.2.0+dfsg-1_amd64.deb
d4b4d26db5c457d86dbca57df4ea3ac89f08c4cea680fd8f4a4205f01ed2b1b8 1941608 rocqide_9.2.0+dfsg-1_amd64.deb
Files:
8b195bbd632d4d986bc99ff7ca4abde5 2499 math optional coq_9.2.0+dfsg-1.dsc
a33dfe089575d328913178abf6c5b41a 3946088 math optional coq_9.2.0+dfsg.orig.tar.xz
4f7f94d34632366bd492726f0daaa999 23724 math optional coq_9.2.0+dfsg-1.debian.tar.xz
86a27553aa9c283da5e2690662a023c0 17086 math optional coq_9.2.0+dfsg-1_amd64.buildinfo
326074c4df88b995214671bceba1ce26 41143764 math optional coq_9.2.0+dfsg-1_amd64.deb
815875daa3d5e75bc6352b2d97a6b380 55434592 ocaml optional libcoq-core-ocaml-dev_9.2.0+dfsg-1_amd64.deb
02630fbf99783d57332d3a7b7a18d3b1 25713812 ocaml optional libcoq-core-ocaml_9.2.0+dfsg-1_amd64.deb
586763c9cf32874155c4373ade04eef1 1153152 math optional libcoq-core_9.2.0+dfsg-1_amd64.deb
f31e8bfa5cf53a23e481155aa1dda918 1941608 math optional rocqide_9.2.0+dfsg-1_amd64.deb
-----BEGIN PGP SIGNATURE-----
iQJNBAEBCgA3FiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmpQrWYZHGp1bGllbi5w
dXlkdEBsYXBvc3RlLm5ldAAKCRAExTvX/gMFUeIwD/0dWJu2R/VlpxuiWGiVcDjS
xukjMwHi/pxXgmmn+pal/dgTrwtvwx94sy5OM83HkEYtP9NtztMI+CcScIk1LuiM
y+3RVyjyyKjzur70EC2iNrO8eAyFroVBfjWtEnk7SD8Y4BKKWqk61MgJuktVzoMQ
ob8ZI9jj5G4J5k9r0g/wyb6XXK4haj6kbyl72Hj868upKMBzo0rERWaRB2nIv1lq
p8jEwXsu1DvgohYIN+VlPW7QpbWvAafvAw+FnQm5AnLHWXHjje9DV7EZTeNwd5Zf
VTqtFE7nZiMYmyGUO1xYHnrg6QTeWhhWsmwMeolFo/ZQNXOxOint4nBGLoLc+EDX
727NPWF6SoxqQn0F8a1abMO/luRO/UuOhb1klr7jj2o58/kxMT12vUCJ9kBdTwRX
FaGmsbkn01PRWDEAnV7wwKe8vrd/LOiezJLJorp8FgmXbaCibXgohhe3JQbTiRrB
imHnY9pp4j4a6UsS1V6pTlnyHAqKYFOFwGsouiWDAEzkK4n/3Y50XizsGZp7ZDeY
dIrFSkZmvqiMjPodY1bDFRXviXmM1i7DJ1/mrWIuz5qg7+fwO2kbWemZADHjsWI8
IsFfRQWL8lxpQRAaoa1vaXXYa9IsF9l73GG+06n2UM8R4TeLuQ2fzeIATjGb6I0G
VtV1hmWkbLe4xYHiB5uIww==
=7rCk
-----END PGP SIGNATURE-----