sbuild (Debian sbuild) 0.91.10 (27 June 2026) on cil.up7.fr +===============================================================================+ | coq-hierarchy-builder 1.10.3-2+ocaml1 (amd64) Tue, 11 Aug 2026 09:38:14 +0000 | +===============================================================================+ Package: coq-hierarchy-builder Version: 1.10.3-2+ocaml1 Source Version: 1.10.3-2+ocaml1 Distribution: trixie-backports-ocaml Machine Architecture: amd64 Host Architecture: amd64 Build Architecture: amd64 Build Type: full I: Unpacking /home/steph/srv/ocaml.debian.net/backports/20260811/ben/rootfs.tar.zst to /var/cache/pbuilder/tmp/tmp.sbuild.SDKrsiVo91... I: Setting up the chroot... I: Creating chroot session... I: Setting up log color... +------------------------------------------------------------------------------+ | Chroot Setup Commands Tue, 11 Aug 2026 09:38:21 +0000 | +------------------------------------------------------------------------------+ /repo/conf/mk-release.sh ------------------------ dpkg-scanpackages: info: Wrote 1281 entries to output Packages file. I: Finished running '/repo/conf/mk-release.sh'. Finished processing commands. -------------------------------------------------------------------------------- I: Setting up apt archive... +------------------------------------------------------------------------------+ | Update chroot Tue, 11 Aug 2026 09:38:54 +0000 | +------------------------------------------------------------------------------+ Ign:1 file:/repo rebuilt InRelease Get:2 file:/repo rebuilt Release [1496 B] Get:2 file:/repo rebuilt Release [1496 B] Ign:3 file:/repo rebuilt Release.gpg Get:4 file:/repo rebuilt/main amd64 Packages [1240 kB] Get:5 http://localhost:9999/debian trixie InRelease [140 kB] Get:6 http://localhost:9999/debian trixie/non-free-firmware amd64 Packages [6884 B] Get:7 http://localhost:9999/debian trixie/non-free amd64 Packages [100 kB] Get:8 http://localhost:9999/debian trixie/main amd64 Packages [9673 kB] Get:9 http://localhost:9999/debian trixie/contrib amd64 Packages [53.8 kB] Fetched 9974 kB in 1s (6770 kB/s) Reading package lists... W: Conflicting distribution: file:/repo rebuilt Release (expected rebuilt but got ) Reading package lists... Building dependency tree... Reading state information... Calculating upgrade... 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. +------------------------------------------------------------------------------+ | Fetch source files Tue, 11 Aug 2026 09:38:58 +0000 | +------------------------------------------------------------------------------+ Local sources ------------- /tmp/tmp.ben.transition-scripts.C57ooJd1Ft/coq-hierarchy-builder_1.10.3-2+ocaml1.dsc exists in /tmp/tmp.ben.transition-scripts.C57ooJd1Ft; copying to chroot +------------------------------------------------------------------------------+ | Install package build dependencies Tue, 11 Aug 2026 09:39:02 +0000 | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff, build-essential Filtered Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff, build-essential dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/build/reproducible-path/resolver-ZpUaMB/apt_archive/sbuild-build-depends-main-dummy.deb'. Ign:1 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ InRelease Get:2 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ Release [609 B] Ign:3 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ Release.gpg Get:4 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ Sources [669 B] Get:5 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ Packages [708 B] Fetched 1986 B in 0s (93.6 kB/s) Reading package lists... Reading package lists... Install main build dependencies (apt-based resolver) ---------------------------------------------------- Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following additional packages will be installed: autoconf automake autopoint autotools-dev bsdextrautils coq debhelper dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libconfig-tiny-perl libcoq-core libcoq-core-ocaml libcoq-elpi libcoq-stdlib libdebhelper-perl libelf1t64 libelpi-ocaml libelpi-ocaml-dev libexpat1 libffi8 libfile-stripnondeterminism-perl libfindlib-ocaml libjson-perl libmagic-mgc libmagic1t64 libmenhir-ocaml-dev libncurses-dev libncurses6 libncursesw6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.13-minimal libpython3.13-stdlib libre-ocaml-dev libreadline8t64 libsexplib0-ocaml libsexplib0-ocaml-dev libstdlib-ocaml libstdlib-ocaml-dev libtool libuchardet0 libunistring5 libxml2 libzarith-ocaml libzstd-dev m4 man-db media-types netbase ocaml ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal python3.13 python3.13-minimal quickjs readline-common sensible-utils tzdata wdiff Suggested packages: autoconf-archive gnu-standards autoconf-doc rocqide | proofgeneral ledit | readline-editor libcoq-core-ocaml-dev why3 coq-doc dh-make git gettext-doc libasprintf-dev libgettextpo-dev gnulib-l10n groff ncurses-doc libtool-doc gfortran | fortran95-compiler gcj-jdk m4-doc apparmor less www-browser ocaml-doc elpa-tuareg camlp4 libmail-box-perl python3-doc python3-tk python3-venv python3.13-venv python3.13-doc binfmt-support readline-doc wdiff-doc Recommended packages: curl | wget | lynx libarchive-cpio-perl libjson-xs-perl libgpm2 ocaml-man libltdl-dev libfindlib-ocaml-dev ledit | readline-editor libmail-sendmail-perl ca-certificates The following NEW packages will be installed: autoconf automake autopoint autotools-dev bsdextrautils coq debhelper dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libconfig-tiny-perl libcoq-core libcoq-core-ocaml libcoq-elpi libcoq-stdlib libdebhelper-perl libelf1t64 libelpi-ocaml libelpi-ocaml-dev libexpat1 libffi8 libfile-stripnondeterminism-perl libfindlib-ocaml libjson-perl libmagic-mgc libmagic1t64 libmenhir-ocaml-dev libncurses-dev libncurses6 libncursesw6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.13-minimal libpython3.13-stdlib libre-ocaml-dev libreadline8t64 libsexplib0-ocaml libsexplib0-ocaml-dev libstdlib-ocaml libstdlib-ocaml-dev libtool libuchardet0 libunistring5 libxml2 libzarith-ocaml libzstd-dev m4 man-db media-types netbase ocaml ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal python3.13 python3.13-minimal quickjs readline-common sbuild-build-depends-main-dummy sensible-utils tzdata wdiff 0 upgraded, 79 newly installed, 0 to remove and 0 not upgraded. Need to get 18.4 MB/237 MB of archives. After this operation, 1067 MB of additional disk space will be used. Get:1 file:/repo rebuilt/main amd64 libcoq-core amd64 9.2.0+dfsg-3+ocaml1 [1153 kB] Get:2 copy:/build/reproducible-path/resolver-ZpUaMB/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [892 B] Get:3 file:/repo rebuilt/main amd64 libstdlib-ocaml amd64 5.4.1-1+ocaml1 [605 kB] Get:4 file:/repo rebuilt/main amd64 ocaml-base amd64 5.4.1-1+ocaml1 [503 kB] Get:5 file:/repo rebuilt/main amd64 libfindlib-ocaml amd64 1.9.8-1+ocaml1 [194 kB] Get:6 file:/repo rebuilt/main amd64 libzarith-ocaml amd64 1.14-4+ocaml1 [110 kB] Get:7 file:/repo rebuilt/main amd64 libcoq-core-ocaml amd64 9.2.0+dfsg-3+ocaml1 [25.8 MB] Get:8 http://localhost:9999/debian trixie/main amd64 libexpat1 amd64 2.7.1-2 [108 kB] Get:9 http://localhost:9999/debian trixie/main amd64 libpython3.13-minimal amd64 3.13.5-2+deb13u3 [863 kB] Get:10 http://localhost:9999/debian trixie/main amd64 python3.13-minimal amd64 3.13.5-2+deb13u3 [2224 kB] Get:11 http://localhost:9999/debian trixie/main amd64 python3-minimal amd64 3.13.5-1 [27.2 kB] Get:12 http://localhost:9999/debian trixie/main amd64 media-types all 13.0.0 [29.3 kB] Get:13 http://localhost:9999/debian trixie/main amd64 netbase all 6.5 [12.4 kB] Get:14 http://localhost:9999/debian trixie/main amd64 tzdata all 2026b-0+deb13u1 [264 kB] Get:15 http://localhost:9999/debian trixie/main amd64 libffi8 amd64 3.4.8-2 [24.1 kB] Get:16 http://localhost:9999/debian trixie/main amd64 libncursesw6 amd64 6.5+20250216-2 [135 kB] Get:17 http://localhost:9999/debian trixie/main amd64 readline-common all 8.2-6 [69.4 kB] Get:18 http://localhost:9999/debian trixie/main amd64 libreadline8t64 amd64 8.2-6 [169 kB] Get:19 http://localhost:9999/debian trixie/main amd64 libpython3.13-stdlib amd64 3.13.5-2+deb13u3 [1959 kB] Get:20 http://localhost:9999/debian trixie/main amd64 python3.13 amd64 3.13.5-2+deb13u3 [757 kB] Get:21 http://localhost:9999/debian trixie/main amd64 libpython3-stdlib amd64 3.13.5-1 [10.2 kB] Get:22 http://localhost:9999/debian trixie/main amd64 python3 amd64 3.13.5-1 [28.2 kB] Get:23 http://localhost:9999/debian trixie/main amd64 sensible-utils all 0.0.25 [25.0 kB] Get:24 http://localhost:9999/debian trixie/main amd64 libmagic-mgc amd64 1:5.46-5 [338 kB] Get:25 http://localhost:9999/debian trixie/main amd64 libmagic1t64 amd64 1:5.46-5 [109 kB] Get:26 http://localhost:9999/debian trixie/main amd64 file amd64 1:5.46-5 [43.6 kB] Get:27 http://localhost:9999/debian trixie/main amd64 gettext-base amd64 0.23.1-2 [243 kB] Get:28 http://localhost:9999/debian trixie/main amd64 libuchardet0 amd64 0.0.8-1+b2 [68.9 kB] Get:29 http://localhost:9999/debian trixie/main amd64 groff-base amd64 1.23.0-9 [1187 kB] Get:30 http://localhost:9999/debian trixie/main amd64 bsdextrautils amd64 2.41-5 [94.6 kB] Get:31 http://localhost:9999/debian trixie/main amd64 libpipeline1 amd64 1.5.8-1 [42.0 kB] Get:32 http://localhost:9999/debian trixie/main amd64 man-db amd64 2.13.1-1 [1469 kB] Get:33 http://localhost:9999/debian trixie/main amd64 m4 amd64 1.4.19-8 [294 kB] Get:34 http://localhost:9999/debian trixie/main amd64 autoconf all 2.72-3.1 [494 kB] Get:35 http://localhost:9999/debian trixie/main amd64 autotools-dev all 20240727.1 [60.2 kB] Get:36 http://localhost:9999/debian trixie/main amd64 automake all 1:1.17-4 [862 kB] Get:37 file:/repo rebuilt/main amd64 libstdlib-ocaml-dev amd64 5.4.1-1+ocaml1 [6476 kB] Get:38 http://localhost:9999/debian trixie/main amd64 autopoint all 0.23.1-2 [770 kB] Get:39 http://localhost:9999/debian trixie/main amd64 libncurses6 amd64 6.5+20250216-2 [105 kB] Get:40 http://localhost:9999/debian trixie/main amd64 libncurses-dev amd64 6.5+20250216-2 [353 kB] Get:41 http://localhost:9999/debian trixie/main amd64 libzstd-dev amd64 1.5.7+dfsg-1 [371 kB] Get:42 http://localhost:9999/debian trixie/main amd64 libtool all 2.5.4-4 [539 kB] Get:43 http://localhost:9999/debian trixie/main amd64 dh-autoreconf all 20 [17.1 kB] Get:44 http://localhost:9999/debian trixie/main amd64 libarchive-zip-perl all 1.68-1 [104 kB] Get:45 http://localhost:9999/debian trixie/main amd64 libfile-stripnondeterminism-perl all 1.14.1-2 [19.7 kB] Get:46 http://localhost:9999/debian trixie/main amd64 dh-strip-nondeterminism all 1.14.1-2 [8620 B] Get:47 file:/repo rebuilt/main amd64 libcompiler-libs-ocaml-dev amd64 5.4.1-1+ocaml1 [39.3 MB] Get:48 http://localhost:9999/debian trixie/main amd64 libelf1t64 amd64 0.192-4 [189 kB] Get:49 http://localhost:9999/debian trixie/main amd64 dwz amd64 0.15-1+b1 [110 kB] Get:50 http://localhost:9999/debian trixie/main amd64 libunistring5 amd64 1.3-2 [477 kB] Get:51 http://localhost:9999/debian trixie/main amd64 libxml2 amd64 2.12.7+dfsg+really2.9.14-2.1+deb13u3 [700 kB] Get:52 http://localhost:9999/debian trixie/main amd64 gettext amd64 0.23.1-2 [1680 kB] Get:53 http://localhost:9999/debian trixie/main amd64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get:54 http://localhost:9999/debian trixie/main amd64 po-debconf all 1.0.21+nmu1 [248 kB] Get:55 http://localhost:9999/debian trixie/main amd64 quickjs amd64 2025.04.26-1 [440 kB] Get:56 http://localhost:9999/debian trixie/main amd64 libjson-perl all 4.10000-1 [87.5 kB] Get:57 http://localhost:9999/debian trixie/main amd64 libconfig-tiny-perl all 2.30-1 [18.9 kB] Get:58 http://localhost:9999/debian trixie/main amd64 wdiff amd64 1.2.2-9 [122 kB] Get:59 file:/repo rebuilt/main amd64 ocaml-interp amd64 5.4.1-1+ocaml1 [7459 kB] Get:60 file:/repo rebuilt/main amd64 ocaml amd64 5.4.1-1+ocaml1 [18.8 MB] Get:61 file:/repo rebuilt/main amd64 ocaml-findlib amd64 1.9.8-1+ocaml1 [595 kB] Get:62 file:/repo rebuilt/main amd64 coq amd64 9.2.0+dfsg-3+ocaml1 [41.3 MB] Get:63 file:/repo rebuilt/main amd64 libdebhelper-perl all 14.3+ocaml1 [77.4 kB] Get:64 file:/repo rebuilt/main amd64 debhelper all 14.3+ocaml1 [934 kB] Get:65 file:/repo rebuilt/main amd64 dh-coq all 0.16+ocaml1 [6920 B] Get:66 file:/repo rebuilt/main amd64 dh-ocaml all 3.8+ocaml1 [201 kB] Get:67 file:/repo rebuilt/main amd64 libsexplib0-ocaml amd64 0.17.0-1+ocaml1 [115 kB] Get:68 file:/repo rebuilt/main amd64 libppx-deriving-ocaml amd64 6.1.3-1+ocaml1 [393 kB] Get:69 file:/repo rebuilt/main amd64 libelpi-ocaml amd64 3.7.2-2+ocaml1 [3395 kB] Get:70 file:/repo rebuilt/main amd64 libmenhir-ocaml-dev amd64 20260209+ds-3+ocaml1 [1006 kB] Get:71 file:/repo rebuilt/main amd64 libocaml-compiler-libs-ocaml-dev amd64 0.17.0-2+ocaml1 [94.0 kB] Get:72 file:/repo rebuilt/main amd64 libppx-derivers-ocaml-dev amd64 1.2.1-4+ocaml1 [16.8 kB] Get:73 file:/repo rebuilt/main amd64 libsexplib0-ocaml-dev amd64 0.17.0-1+ocaml1 [273 kB] Get:74 file:/repo rebuilt/main amd64 libppxlib-ocaml-dev amd64 0.38.0-1+ocaml1 [18.9 MB] Get:75 file:/repo rebuilt/main amd64 libppx-deriving-ocaml-dev amd64 6.1.3-1+ocaml1 [5016 kB] Get:76 file:/repo rebuilt/main amd64 libre-ocaml-dev amd64 1.14.0-2+ocaml1 [1356 kB] Get:77 file:/repo rebuilt/main amd64 libelpi-ocaml-dev amd64 3.7.2-2+ocaml1 [12.1 MB] Get:78 file:/repo rebuilt/main amd64 libcoq-stdlib amd64 9.2.0-1+ocaml1 [20.1 MB] Get:79 file:/repo rebuilt/main amd64 libcoq-elpi amd64 3.5.0-2+ocaml1 [12.8 MB] Preconfiguring packages ... Fetched 18.4 MB in 1s (16.0 MB/s) Selecting previously unselected package libexpat1:amd64. (Reading database ... 11874 files and directories currently installed.) Preparing to unpack .../libexpat1_2.7.1-2_amd64.deb ... Unpacking libexpat1:amd64 (2.7.1-2) ... Selecting previously unselected package libpython3.13-minimal:amd64. Preparing to unpack .../libpython3.13-minimal_3.13.5-2+deb13u3_amd64.deb ... Unpacking libpython3.13-minimal:amd64 (3.13.5-2+deb13u3) ... Selecting previously unselected package python3.13-minimal. Preparing to unpack .../python3.13-minimal_3.13.5-2+deb13u3_amd64.deb ... Unpacking python3.13-minimal (3.13.5-2+deb13u3) ... Setting up libpython3.13-minimal:amd64 (3.13.5-2+deb13u3) ... Setting up libexpat1:amd64 (2.7.1-2) ... Setting up python3.13-minimal (3.13.5-2+deb13u3) ... Selecting previously unselected package python3-minimal. (Reading database ... 12208 files and directories currently installed.) Preparing to unpack .../00-python3-minimal_3.13.5-1_amd64.deb ... Unpacking python3-minimal (3.13.5-1) ... Selecting previously unselected package media-types. Preparing to unpack .../01-media-types_13.0.0_all.deb ... Unpacking media-types (13.0.0) ... Selecting previously unselected package netbase. Preparing to unpack .../02-netbase_6.5_all.deb ... Unpacking netbase (6.5) ... Selecting previously unselected package tzdata. Preparing to unpack .../03-tzdata_2026b-0+deb13u1_all.deb ... Unpacking tzdata (2026b-0+deb13u1) ... Selecting previously unselected package libffi8:amd64. Preparing to unpack .../04-libffi8_3.4.8-2_amd64.deb ... Unpacking libffi8:amd64 (3.4.8-2) ... Selecting previously unselected package libncursesw6:amd64. Preparing to unpack .../05-libncursesw6_6.5+20250216-2_amd64.deb ... Unpacking libncursesw6:amd64 (6.5+20250216-2) ... Selecting previously unselected package readline-common. Preparing to unpack .../06-readline-common_8.2-6_all.deb ... Unpacking readline-common (8.2-6) ... Selecting previously unselected package libreadline8t64:amd64. Preparing to unpack .../07-libreadline8t64_8.2-6_amd64.deb ... Adding 'diversion of /lib/x86_64-linux-gnu/libhistory.so.8 to /lib/x86_64-linux-gnu/libhistory.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libhistory.so.8.2 to /lib/x86_64-linux-gnu/libhistory.so.8.2.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libreadline.so.8 to /lib/x86_64-linux-gnu/libreadline.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libreadline.so.8.2 to /lib/x86_64-linux-gnu/libreadline.so.8.2.usr-is-merged by libreadline8t64' Unpacking libreadline8t64:amd64 (8.2-6) ... Selecting previously unselected package libpython3.13-stdlib:amd64. Preparing to unpack .../08-libpython3.13-stdlib_3.13.5-2+deb13u3_amd64.deb ... Unpacking libpython3.13-stdlib:amd64 (3.13.5-2+deb13u3) ... Selecting previously unselected package python3.13. Preparing to unpack .../09-python3.13_3.13.5-2+deb13u3_amd64.deb ... Unpacking python3.13 (3.13.5-2+deb13u3) ... Selecting previously unselected package libpython3-stdlib:amd64. Preparing to unpack .../10-libpython3-stdlib_3.13.5-1_amd64.deb ... Unpacking libpython3-stdlib:amd64 (3.13.5-1) ... Setting up python3-minimal (3.13.5-1) ... Selecting previously unselected package python3. (Reading database ... 13232 files and directories currently installed.) Preparing to unpack .../00-python3_3.13.5-1_amd64.deb ... Unpacking python3 (3.13.5-1) ... Selecting previously unselected package sensible-utils. Preparing to unpack .../01-sensible-utils_0.0.25_all.deb ... Unpacking sensible-utils (0.0.25) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../02-libmagic-mgc_1%3a5.46-5_amd64.deb ... Unpacking libmagic-mgc (1:5.46-5) ... Selecting previously unselected package libmagic1t64:amd64. Preparing to unpack .../03-libmagic1t64_1%3a5.46-5_amd64.deb ... Unpacking libmagic1t64:amd64 (1:5.46-5) ... Selecting previously unselected package file. Preparing to unpack .../04-file_1%3a5.46-5_amd64.deb ... Unpacking file (1:5.46-5) ... Selecting previously unselected package gettext-base. Preparing to unpack .../05-gettext-base_0.23.1-2_amd64.deb ... Unpacking gettext-base (0.23.1-2) ... Selecting previously unselected package libuchardet0:amd64. Preparing to unpack .../06-libuchardet0_0.0.8-1+b2_amd64.deb ... Unpacking libuchardet0:amd64 (0.0.8-1+b2) ... Selecting previously unselected package groff-base. Preparing to unpack .../07-groff-base_1.23.0-9_amd64.deb ... Unpacking groff-base (1.23.0-9) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../08-bsdextrautils_2.41-5_amd64.deb ... Unpacking bsdextrautils (2.41-5) ... Selecting previously unselected package libpipeline1:amd64. Preparing to unpack .../09-libpipeline1_1.5.8-1_amd64.deb ... Unpacking libpipeline1:amd64 (1.5.8-1) ... Selecting previously unselected package man-db. Preparing to unpack .../10-man-db_2.13.1-1_amd64.deb ... Unpacking man-db (2.13.1-1) ... Selecting previously unselected package m4. Preparing to unpack .../11-m4_1.4.19-8_amd64.deb ... Unpacking m4 (1.4.19-8) ... Selecting previously unselected package autoconf. Preparing to unpack .../12-autoconf_2.72-3.1_all.deb ... Unpacking autoconf (2.72-3.1) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../13-autotools-dev_20240727.1_all.deb ... Unpacking autotools-dev (20240727.1) ... Selecting previously unselected package automake. Preparing to unpack .../14-automake_1%3a1.17-4_all.deb ... Unpacking automake (1:1.17-4) ... Selecting previously unselected package autopoint. Preparing to unpack .../15-autopoint_0.23.1-2_all.deb ... Unpacking autopoint (0.23.1-2) ... Selecting previously unselected package libcoq-core. Preparing to unpack .../16-libcoq-core_9.2.0+dfsg-3+ocaml1_amd64.deb ... Unpacking libcoq-core (9.2.0+dfsg-3+ocaml1) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../17-libstdlib-ocaml_5.4.1-1+ocaml1_amd64.deb ... Unpacking libstdlib-ocaml (5.4.1-1+ocaml1) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../18-ocaml-base_5.4.1-1+ocaml1_amd64.deb ... Unpacking ocaml-base (5.4.1-1+ocaml1) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../19-libfindlib-ocaml_1.9.8-1+ocaml1_amd64.deb ... Unpacking libfindlib-ocaml (1.9.8-1+ocaml1) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../20-libzarith-ocaml_1.14-4+ocaml1_amd64.deb ... Unpacking libzarith-ocaml (1.14-4+ocaml1) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../21-libcoq-core-ocaml_9.2.0+dfsg-3+ocaml1_amd64.deb ... Unpacking libcoq-core-ocaml (9.2.0+dfsg-3+ocaml1) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../22-libstdlib-ocaml-dev_5.4.1-1+ocaml1_amd64.deb ... Unpacking libstdlib-ocaml-dev (5.4.1-1+ocaml1) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../23-libcompiler-libs-ocaml-dev_5.4.1-1+ocaml1_amd64.deb ... Unpacking libcompiler-libs-ocaml-dev (5.4.1-1+ocaml1) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../24-ocaml-interp_5.4.1-1+ocaml1_amd64.deb ... Unpacking ocaml-interp (5.4.1-1+ocaml1) ... Selecting previously unselected package libncurses6:amd64. Preparing to unpack .../25-libncurses6_6.5+20250216-2_amd64.deb ... Unpacking libncurses6:amd64 (6.5+20250216-2) ... Selecting previously unselected package libncurses-dev:amd64. Preparing to unpack .../26-libncurses-dev_6.5+20250216-2_amd64.deb ... Unpacking libncurses-dev:amd64 (6.5+20250216-2) ... Selecting previously unselected package libzstd-dev:amd64. Preparing to unpack .../27-libzstd-dev_1.5.7+dfsg-1_amd64.deb ... Unpacking libzstd-dev:amd64 (1.5.7+dfsg-1) ... Selecting previously unselected package ocaml. Preparing to unpack .../28-ocaml_5.4.1-1+ocaml1_amd64.deb ... Unpacking ocaml (5.4.1-1+ocaml1) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../29-ocaml-findlib_1.9.8-1+ocaml1_amd64.deb ... Unpacking ocaml-findlib (1.9.8-1+ocaml1) ... Selecting previously unselected package coq. Preparing to unpack .../30-coq_9.2.0+dfsg-3+ocaml1_amd64.deb ... Unpacking coq (9.2.0+dfsg-3+ocaml1) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../31-libdebhelper-perl_14.3+ocaml1_all.deb ... Unpacking libdebhelper-perl (14.3+ocaml1) ... Selecting previously unselected package libtool. Preparing to unpack .../32-libtool_2.5.4-4_all.deb ... Unpacking libtool (2.5.4-4) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../33-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../34-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../35-libfile-stripnondeterminism-perl_1.14.1-2_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.14.1-2) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../36-dh-strip-nondeterminism_1.14.1-2_all.deb ... Unpacking dh-strip-nondeterminism (1.14.1-2) ... Selecting previously unselected package libelf1t64:amd64. Preparing to unpack .../37-libelf1t64_0.192-4_amd64.deb ... Unpacking libelf1t64:amd64 (0.192-4) ... Selecting previously unselected package dwz. Preparing to unpack .../38-dwz_0.15-1+b1_amd64.deb ... Unpacking dwz (0.15-1+b1) ... Selecting previously unselected package libunistring5:amd64. Preparing to unpack .../39-libunistring5_1.3-2_amd64.deb ... Unpacking libunistring5:amd64 (1.3-2) ... Selecting previously unselected package libxml2:amd64. Preparing to unpack .../40-libxml2_2.12.7+dfsg+really2.9.14-2.1+deb13u3_amd64.deb ... Unpacking libxml2:amd64 (2.12.7+dfsg+really2.9.14-2.1+deb13u3) ... Selecting previously unselected package gettext. Preparing to unpack .../41-gettext_0.23.1-2_amd64.deb ... Unpacking gettext (0.23.1-2) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../42-intltool-debian_0.35.0+20060710.6_all.deb ... Unpacking intltool-debian (0.35.0+20060710.6) ... Selecting previously unselected package po-debconf. Preparing to unpack .../43-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../44-debhelper_14.3+ocaml1_all.deb ... Unpacking debhelper (14.3+ocaml1) ... Selecting previously unselected package dh-coq. Preparing to unpack .../45-dh-coq_0.16+ocaml1_all.deb ... Unpacking dh-coq (0.16+ocaml1) ... Selecting previously unselected package quickjs. Preparing to unpack .../46-quickjs_2025.04.26-1_amd64.deb ... Unpacking quickjs (2025.04.26-1) ... Selecting previously unselected package libjson-perl. Preparing to unpack .../47-libjson-perl_4.10000-1_all.deb ... Unpacking libjson-perl (4.10000-1) ... Selecting previously unselected package libconfig-tiny-perl. Preparing to unpack .../48-libconfig-tiny-perl_2.30-1_all.deb ... Unpacking libconfig-tiny-perl (2.30-1) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../49-dh-ocaml_3.8+ocaml1_all.deb ... Unpacking dh-ocaml (3.8+ocaml1) ... Selecting previously unselected package libsexplib0-ocaml. Preparing to unpack .../50-libsexplib0-ocaml_0.17.0-1+ocaml1_amd64.deb ... Unpacking libsexplib0-ocaml (0.17.0-1+ocaml1) ... Selecting previously unselected package libppx-deriving-ocaml. Preparing to unpack .../51-libppx-deriving-ocaml_6.1.3-1+ocaml1_amd64.deb ... Unpacking libppx-deriving-ocaml (6.1.3-1+ocaml1) ... Selecting previously unselected package libelpi-ocaml. Preparing to unpack .../52-libelpi-ocaml_3.7.2-2+ocaml1_amd64.deb ... Unpacking libelpi-ocaml (3.7.2-2+ocaml1) ... Selecting previously unselected package libmenhir-ocaml-dev. Preparing to unpack .../53-libmenhir-ocaml-dev_20260209+ds-3+ocaml1_amd64.deb ... Unpacking libmenhir-ocaml-dev (20260209+ds-3+ocaml1) ... Selecting previously unselected package libocaml-compiler-libs-ocaml-dev. Preparing to unpack .../54-libocaml-compiler-libs-ocaml-dev_0.17.0-2+ocaml1_amd64.deb ... Unpacking libocaml-compiler-libs-ocaml-dev (0.17.0-2+ocaml1) ... Selecting previously unselected package libppx-derivers-ocaml-dev. Preparing to unpack .../55-libppx-derivers-ocaml-dev_1.2.1-4+ocaml1_amd64.deb ... Unpacking libppx-derivers-ocaml-dev (1.2.1-4+ocaml1) ... Selecting previously unselected package libsexplib0-ocaml-dev. Preparing to unpack .../56-libsexplib0-ocaml-dev_0.17.0-1+ocaml1_amd64.deb ... Unpacking libsexplib0-ocaml-dev (0.17.0-1+ocaml1) ... Selecting previously unselected package libppxlib-ocaml-dev. Preparing to unpack .../57-libppxlib-ocaml-dev_0.38.0-1+ocaml1_amd64.deb ... Unpacking libppxlib-ocaml-dev (0.38.0-1+ocaml1) ... Selecting previously unselected package libppx-deriving-ocaml-dev. Preparing to unpack .../58-libppx-deriving-ocaml-dev_6.1.3-1+ocaml1_amd64.deb ... Unpacking libppx-deriving-ocaml-dev (6.1.3-1+ocaml1) ... Selecting previously unselected package libre-ocaml-dev. Preparing to unpack .../59-libre-ocaml-dev_1.14.0-2+ocaml1_amd64.deb ... Unpacking libre-ocaml-dev (1.14.0-2+ocaml1) ... Selecting previously unselected package libelpi-ocaml-dev. Preparing to unpack .../60-libelpi-ocaml-dev_3.7.2-2+ocaml1_amd64.deb ... Unpacking libelpi-ocaml-dev (3.7.2-2+ocaml1) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../61-libcoq-stdlib_9.2.0-1+ocaml1_amd64.deb ... Unpacking libcoq-stdlib (9.2.0-1+ocaml1) ... Selecting previously unselected package libcoq-elpi. Preparing to unpack .../62-libcoq-elpi_3.5.0-2+ocaml1_amd64.deb ... Unpacking libcoq-elpi (3.5.0-2+ocaml1) ... Selecting previously unselected package wdiff. Preparing to unpack .../63-wdiff_1.2.2-9_amd64.deb ... Unpacking wdiff (1.2.2-9) ... Selecting previously unselected package sbuild-build-depends-main-dummy. Preparing to unpack .../64-sbuild-build-depends-main-dummy_0.invalid.0_amd64.deb ... Unpacking sbuild-build-depends-main-dummy (0.invalid.0) ... Setting up media-types (13.0.0) ... Setting up libpipeline1:amd64 (1.5.8-1) ... Setting up wdiff (1.2.2-9) ... Setting up libzstd-dev:amd64 (1.5.7+dfsg-1) ... Setting up bsdextrautils (2.41-5) ... Setting up libmagic-mgc (1:5.46-5) ... Setting up dh-coq (0.16+ocaml1) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libdebhelper-perl (14.3+ocaml1) ... Setting up libmagic1t64:amd64 (1:5.46-5) ... Setting up gettext-base (0.23.1-2) ... Setting up m4 (1.4.19-8) ... Setting up libcoq-core (9.2.0+dfsg-3+ocaml1) ... Setting up file (1:5.46-5) ... Setting up libconfig-tiny-perl (2.30-1) ... Setting up libelf1t64:amd64 (0.192-4) ... Setting up quickjs (2025.04.26-1) ... Setting up tzdata (2026b-0+deb13u1) ... Current default time zone: 'Etc/UTC' Local time is now: Tue Aug 11 09:39:51 UTC 2026. Universal Time is now: Tue Aug 11 09:39:51 UTC 2026. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20240727.1) ... Setting up libcoq-stdlib (9.2.0-1+ocaml1) ... Setting up libncurses6:amd64 (6.5+20250216-2) ... Setting up libstdlib-ocaml (5.4.1-1+ocaml1) ... Setting up libunistring5:amd64 (1.3-2) ... Setting up autopoint (0.23.1-2) ... Setting up ocaml-base (5.4.1-1+ocaml1) ... Setting up libncursesw6:amd64 (6.5+20250216-2) ... Setting up autoconf (2.72-3.1) ... Setting up libffi8:amd64 (3.4.8-2) ... Setting up libsexplib0-ocaml (0.17.0-1+ocaml1) ... Setting up dwz (0.15-1+b1) ... Setting up sensible-utils (0.0.25) ... Setting up libuchardet0:amd64 (0.0.8-1+b2) ... Setting up libjson-perl (4.10000-1) ... Setting up netbase (6.5) ... Setting up readline-common (8.2-6) ... Setting up libxml2:amd64 (2.12.7+dfsg+really2.9.14-2.1+deb13u3) ... Setting up automake (1:1.17-4) ... update-alternatives: using /usr/bin/automake-1.17 to provide /usr/bin/automake (automake) in auto mode Setting up libfile-stripnondeterminism-perl (1.14.1-2) ... Setting up libppx-deriving-ocaml (6.1.3-1+ocaml1) ... Setting up libncurses-dev:amd64 (6.5+20250216-2) ... Setting up gettext (0.23.1-2) ... Setting up libtool (2.5.4-4) ... Setting up libstdlib-ocaml-dev (5.4.1-1+ocaml1) ... Setting up dh-ocaml (3.8+ocaml1) ... Setting up libfindlib-ocaml (1.9.8-1+ocaml1) ... Setting up libzarith-ocaml (1.14-4+ocaml1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (5.4.1-1+ocaml1) ... Setting up ocaml-interp (5.4.1-1+ocaml1) ... Setting up ocaml-findlib (1.9.8-1+ocaml1) ... Setting up libreadline8t64:amd64 (8.2-6) ... Setting up dh-strip-nondeterminism (1.14.1-2) ... Setting up libelpi-ocaml (3.7.2-2+ocaml1) ... Setting up libcoq-core-ocaml (9.2.0+dfsg-3+ocaml1) ... Setting up groff-base (1.23.0-9) ... Setting up libpython3.13-stdlib:amd64 (3.13.5-2+deb13u3) ... Setting up libpython3-stdlib:amd64 (3.13.5-1) ... Setting up python3.13 (3.13.5-2+deb13u3) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up python3 (3.13.5-1) ... Setting up ocaml (5.4.1-1+ocaml1) ... Setting up man-db (2.13.1-1) ... Not building database; man-db/auto-update is not 'true'. Setting up libre-ocaml-dev (1.14.0-2+ocaml1) ... Setting up libmenhir-ocaml-dev (20260209+ds-3+ocaml1) ... Setting up libocaml-compiler-libs-ocaml-dev (0.17.0-2+ocaml1) ... Setting up libsexplib0-ocaml-dev (0.17.0-1+ocaml1) ... Setting up coq (9.2.0+dfsg-3+ocaml1) ... Setting up libppx-derivers-ocaml-dev (1.2.1-4+ocaml1) ... Setting up libppxlib-ocaml-dev (0.38.0-1+ocaml1) ... Setting up debhelper (14.3+ocaml1) ... Setting up libppx-deriving-ocaml-dev (6.1.3-1+ocaml1) ... Setting up libelpi-ocaml-dev (3.7.2-2+ocaml1) ... Setting up libcoq-elpi (3.5.0-2+ocaml1) ... Setting up sbuild-build-depends-main-dummy (0.invalid.0) ... Processing triggers for libc-bin (2.41-12+deb13u3) ... +------------------------------------------------------------------------------+ | Check architectures Tue, 11 Aug 2026 09:39:58 +0000 | +------------------------------------------------------------------------------+ Arch check ok (amd64 included in any) +------------------------------------------------------------------------------+ | Build environment Tue, 11 Aug 2026 09:40:00 +0000 | +------------------------------------------------------------------------------+ Kernel: Linux 7.1.3+deb14-amd64 #1 SMP PREEMPT_DYNAMIC Debian 7.1.3-1 (2026-07-04) amd64 (x86_64) Toolchain package versions: binutils_2.44-3 dpkg-dev_1.22.22 g++-14_14.2.0-19 gcc-14_14.2.0-19 libc6-dev_2.41-12+deb13u3 libstdc++-14-dev_14.2.0-19 libstdc++6_14.2.0-19 linux-libc-dev_6.12.94-1 Package versions: apt_3.0.3 apt-utils_3.0.3 autoconf_2.72-3.1 automake_1:1.17-4 autopoint_0.23.1-2 autotools-dev_20240727.1 base-files_13.8+deb13u6 base-passwd_3.6.7 bash_5.2.37-2+b9 binutils_2.44-3 binutils-common_2.44-3 binutils-x86-64-linux-gnu_2.44-3 bsdextrautils_2.41-5 bsdutils_1:2.41-5 build-essential_12.12 bzip2_1.0.8-6 coq_9.2.0+dfsg-3+ocaml1 coreutils_9.7-3 cpp_4:14.2.0-1 cpp-14_14.2.0-19 cpp-14-x86-64-linux-gnu_14.2.0-19 cpp-x86-64-linux-gnu_4:14.2.0-1 dash_0.5.12-12 debconf_1.5.91 debhelper_14.3+ocaml1 debian-archive-keyring_2025.1 debianutils_5.23.2 dh-autoreconf_20 dh-coq_0.16+ocaml1 dh-ocaml_3.8+ocaml1 dh-strip-nondeterminism_1.14.1-2 diffutils_1:3.10-4 dpkg_1.22.22 dpkg-dev_1.22.22 dwz_0.15-1+b1 file_1:5.46-5 findutils_4.10.0-3 g++_4:14.2.0-1 g++-14_14.2.0-19 g++-14-x86-64-linux-gnu_14.2.0-19 g++-x86-64-linux-gnu_4:14.2.0-1 gcc_4:14.2.0-1 gcc-14_14.2.0-19 gcc-14-base_14.2.0-19 gcc-14-x86-64-linux-gnu_14.2.0-19 gcc-x86-64-linux-gnu_4:14.2.0-1 gettext_0.23.1-2 gettext-base_0.23.1-2 grep_3.11-4 groff-base_1.23.0-9 gzip_1.13-1 hostname_3.25 init-system-helpers_1.69~deb13u1 intltool-debian_0.35.0+20060710.6 libacl1_2.3.2-2+b1 libapt-pkg7.0_3.0.3 libarchive-zip-perl_1.68-1 libasan8_14.2.0-19 libatomic1_14.2.0-19 libattr1_1:2.5.2-3 libaudit-common_1:4.0.2-2 libaudit1_1:4.0.2-2+b2 libbinutils_2.44-3 libblkid1_2.41-5 libbz2-1.0_1.0.8-6 libc-bin_2.41-12+deb13u3 libc-dev-bin_2.41-12+deb13u3 libc6_2.41-12+deb13u3 libc6-dev_2.41-12+deb13u3 libcap-ng0_0.8.5-4+b1 libcap2_1:2.75-10+deb13u1+b1 libcc1-0_14.2.0-19 libcompiler-libs-ocaml-dev_5.4.1-1+ocaml1 libconfig-tiny-perl_2.30-1 libcoq-core_9.2.0+dfsg-3+ocaml1 libcoq-core-ocaml_9.2.0+dfsg-3+ocaml1 libcoq-elpi_3.5.0-2+ocaml1 libcoq-stdlib_9.2.0-1+ocaml1 libcrypt-dev_1:4.4.38-1 libcrypt1_1:4.4.38-1 libctf-nobfd0_2.44-3 libctf0_2.44-3 libdb5.3t64_5.3.28+dfsg2-9 libdebconfclient0_0.280 libdebhelper-perl_14.3+ocaml1 libdpkg-perl_1.22.22 libelf1t64_0.192-4 libelpi-ocaml_3.7.2-2+ocaml1 libelpi-ocaml-dev_3.7.2-2+ocaml1 libexpat1_2.7.1-2 libffi8_3.4.8-2 libfile-stripnondeterminism-perl_1.14.1-2 libfindlib-ocaml_1.9.8-1+ocaml1 libgcc-14-dev_14.2.0-19 libgcc-s1_14.2.0-19 libgdbm-compat4t64_1.24-2 libgdbm6t64_1.24-2 libgmp10_2:6.3.0+dfsg-3 libgomp1_14.2.0-19 libgprofng0_2.44-3 libhogweed6t64_3.10.1-1 libhwasan0_14.2.0-19 libisl23_0.27-1 libitm1_14.2.0-19 libjansson4_2.14-2+b3 libjson-perl_4.10000-1 liblastlog2-2_2.41-5 liblsan0_14.2.0-19 liblz4-1_1.10.0-4 liblzma5_5.8.1-1+deb13u1 libmagic-mgc_1:5.46-5 libmagic1t64_1:5.46-5 libmd0_1.1.0-2+b1 libmenhir-ocaml-dev_20260209+ds-3+ocaml1 libmount1_2.41-5 libmpc3_1.3.1-1+b3 libmpfr6_4.2.2-1 libncurses-dev_6.5+20250216-2 libncurses6_6.5+20250216-2 libncursesw6_6.5+20250216-2 libnettle8t64_3.10.1-1 libocaml-compiler-libs-ocaml-dev_0.17.0-2+ocaml1 libpam-modules_1.7.0-5 libpam-modules-bin_1.7.0-5 libpam-runtime_1.7.0-5 libpam0g_1.7.0-5 libpcre2-8-0_10.46-1~deb13u1 libperl5.40_5.40.1-6 libpipeline1_1.5.8-1 libppx-derivers-ocaml-dev_1.2.1-4+ocaml1 libppx-deriving-ocaml_6.1.3-1+ocaml1 libppx-deriving-ocaml-dev_6.1.3-1+ocaml1 libppxlib-ocaml-dev_0.38.0-1+ocaml1 libpython3-stdlib_3.13.5-1 libpython3.13-minimal_3.13.5-2+deb13u3 libpython3.13-stdlib_3.13.5-2+deb13u3 libquadmath0_14.2.0-19 libre-ocaml-dev_1.14.0-2+ocaml1 libreadline8t64_8.2-6 libseccomp2_2.6.0-2 libselinux1_3.8.1-1 libsexplib0-ocaml_0.17.0-1+ocaml1 libsexplib0-ocaml-dev_0.17.0-1+ocaml1 libsframe1_2.44-3 libsmartcols1_2.41-5 libsqlite3-0_3.46.1-7+deb13u1 libssl3t64_3.5.6-1~deb13u2 libstdc++-14-dev_14.2.0-19 libstdc++6_14.2.0-19 libstdlib-ocaml_5.4.1-1+ocaml1 libstdlib-ocaml-dev_5.4.1-1+ocaml1 libsystemd0_257.13-1~deb13u1 libtinfo6_6.5+20250216-2 libtool_2.5.4-4 libtsan2_14.2.0-19 libubsan1_14.2.0-19 libuchardet0_0.0.8-1+b2 libudev1_257.13-1~deb13u1 libunistring5_1.3-2 libuuid1_2.41-5 libxml2_2.12.7+dfsg+really2.9.14-2.1+deb13u3 libxxhash0_0.8.3-2 libzarith-ocaml_1.14-4+ocaml1 libzstd-dev_1.5.7+dfsg-1 libzstd1_1.5.7+dfsg-1 linux-libc-dev_6.12.94-1 m4_1.4.19-8 make_4.4.1-2 man-db_2.13.1-1 mawk_1.3.4.20250131-1 media-types_13.0.0 ncurses-base_6.5+20250216-2 ncurses-bin_6.5+20250216-2 netbase_6.5 ocaml_5.4.1-1+ocaml1 ocaml-base_5.4.1-1+ocaml1 ocaml-findlib_1.9.8-1+ocaml1 ocaml-interp_5.4.1-1+ocaml1 openssl-provider-legacy_3.5.6-1~deb13u2 patch_2.8-2 perl_5.40.1-6 perl-base_5.40.1-6 perl-modules-5.40_5.40.1-6 po-debconf_1.0.21+nmu1 python3_3.13.5-1 python3-minimal_3.13.5-1 python3.13_3.13.5-2+deb13u3 python3.13-minimal_3.13.5-2+deb13u3 quickjs_2025.04.26-1 readline-common_8.2-6 rpcsvc-proto_1.4.3-1 sbuild-build-depends-main-dummy_0.invalid.0 sed_4.9-2+deb13u1 sensible-utils_0.0.25 sqv_1.3.0-3+b2 sysvinit-utils_3.14-4 tar_1.35+dfsg-3.1 tzdata_2026b-0+deb13u1 util-linux_2.41-5 wdiff_1.2.2-9 xz-utils_5.8.1-1+deb13u1 zlib1g_1:1.3.dfsg+really1.3.1-1+b1 +------------------------------------------------------------------------------+ | Build Tue, 11 Aug 2026 09:40:00 +0000 | +------------------------------------------------------------------------------+ Unpack source ------------- Format: 3.0 (quilt) Source: coq-hierarchy-builder Binary: libcoq-hierarchy-builder Architecture: any Version: 1.10.3-2+ocaml1 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/math-comp/hierarchy-builder Standards-Version: 4.7.4 Vcs-Browser: https://salsa.debian.org/ocaml-team/coq-hierarchy-builder Vcs-Git: https://salsa.debian.org/ocaml-team/coq-hierarchy-builder.git Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff Package-List: libcoq-hierarchy-builder deb ocaml optional arch=any Checksums-Sha1: 699eb25b1a43945a696f9fc9492001047ae07c70 623811 coq-hierarchy-builder_1.10.3.orig.tar.gz d38d3f9f5c5ef8c9581c655b345d50c543eb584a 3132 coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz Checksums-Sha256: 529d08c700c936c9fdf5658d8dfc3bf2cf5ef61cdd35604e40eec2fd349a071b 623811 coq-hierarchy-builder_1.10.3.orig.tar.gz 3d8de081c1019fd5aed14570eb87ed627488044baf78ca7e6b7c220996218478 3132 coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz Files: d34079e82bea60c8ec3b1638629cbc88 623811 coq-hierarchy-builder_1.10.3.orig.tar.gz 1c5dfa22ab826d141e25a215815be4b7 3132 coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz dpkg-source: warning: extracting unsigned source package (coq-hierarchy-builder_1.10.3-2+ocaml1.dsc) dpkg-source: info: extracting coq-hierarchy-builder in /build/reproducible-path/coq-hierarchy-builder-1.10.3 dpkg-source: info: unpacking coq-hierarchy-builder_1.10.3.orig.tar.gz dpkg-source: info: unpacking coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz clean up apt cache ------------------ Check disk space ---------------- Sufficient free space for build User Environment ---------------- APT_CONFIG=/var/lib/sbuild/apt.conf DEB_BUILD_OPTIONS=parallel=1 HOME=/sbuild-nonexistent LANG=fr_FR.UTF-8 LC_ALL=C.UTF-8 LOGNAME=sbuild MAKEFLAGS= PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SHELL=/bin/sh USER=sbuild dpkg-buildpackage ----------------- Command: dpkg-buildpackage --sanitize-env -us -uc -sa dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.10.3-2+ocaml1 dpkg-buildpackage: info: source distribution trixie-backports-ocaml dpkg-buildpackage: info: source changed by Anonymous Builder dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq,ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make clean make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[2]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' find . -name "*.cm*" -delete find . -name "*.aux" -delete rm -f Makefile.coq Makefile.coq.conf rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf rm -f *dot make[1]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_ocamlclean dh_clean dpkg-source -b . dpkg-source: info: using source format '3.0 (quilt)' dpkg-source: info: building coq-hierarchy-builder using existing ./coq-hierarchy-builder_1.10.3.orig.tar.gz dpkg-source: info: building coq-hierarchy-builder in coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz dpkg-source: info: building coq-hierarchy-builder in coq-hierarchy-builder_1.10.3-2+ocaml1.dsc debian/rules binary dh binary --with coq,ocaml dh_update_autotools_config dh_autoreconf dh_ocamlinit dh_auto_configure dh_auto_build make -j1 INSTALL="install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make config make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' configuring for 9.2 5.4.1 # Remove all of the above when requiring Rocq >= 9.0 make[2]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make build make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' already configured # Remove all of the above when requiring Rocq >= 9.0 /usr/bin/coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' ROCQ DEP VFILES ROCQ compile HB/structures.v File "./HB/structures.v", line 47, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "/build/reproducible-path/coq-hierarchy-builder-1.10.3/HB/common/compat_add_secvar_all.elpi", line 8, characters 2-51: Warning: File "/build/reproducible-path/coq-hierarchy-builder-1.10.3/HB/common/compat_add_secvar_all.elpi", line 8, characters 2-51 The standard λProlog infix operator for implication => has higher precedence than conjunction. This means that 'A => B, C' reads '(A => B), C'. This is a common mistake since it makes A only available to B (and not to C as many newcomers may expect). If this is really what you want write '(A => B), C' to silence this warning. Otherwise write 'A => (B, C)', or use the alternative implication operator ==>. Infix ==> has lower precedence than conjunction, hence 'A ==> B, C' reads 'A ==> (B, C)' and means the same as 'A => (B, C)'. [elpi.implication-precedence,elpi,default] File "./HB/structures.v", line 1218, characters 0-159: Warning: Notations at level 0 should be closed (first and last symbols should be terminal symbols). [level-0-notation-not-closed,parsing,default] File "./HB/structures.v", line 1221, characters 2-201: Warning: Notations at level 0 should be closed (first and last symbols should be terminal symbols). [level-0-notation-not-closed,parsing,default] make[3]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[2]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make test-suite make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' already configured # Remove all of the above when requiring Rocq >= 9.0 make -f Makefile.coq make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[4]: Nothing to be done for 'real-all'. make[3]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' /usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq make -f Makefile.test-suite.coq make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' ROCQ DEP VFILES ROCQ compile examples/readme.v [1786441259.457915] HB: start module and section AddComoid_of_Type [1786441259.460321] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type (field [coercion off, canonical tt] zero c0 c1 \ field [coercion off, canonical tt] add (prod `_:r` c0 c2 \ prod `_:r` c0 c3 \ c0) c2 \ field [coercion off, canonical tt] addrA (prod `x:r` (X2 c2) c3 \ prod `y:r` (X3 c2 c3) c4 \ prod `z:r` (X4 c2 c3 c4) c5 \ app [global (indt «eq»), X5 c2 c3 c4 c5, app [c2, c3, app [c2, c4, c5]], app [c2, app [c2, c3, c4], c5]]) c3 \ field [coercion off, canonical tt] addrC (prod `x:r` (X6 c3) c4 \ prod `y:r` (X7 c3 c4) c5 \ app [global (indt «eq»), X8 c3 c4 c5, app [c2, c4, c5], app [c2, c5, c4]]) c4 \ field [coercion off, canonical tt] add0r (prod `x:r` (X9 c4) c5 \ app [global (indt «eq»), X10 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories [1786441259.464168] HB: processing key parameter [1786441259.467459] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.22»)) c0 \ [] to mixins [1786441259.468527] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.22»)) c0 \ [] [1786441259.469848] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] [1786441259.473943] HB: declare mixin or factory [1786441259.474464] HB: declare record axioms_ [1786441259.525605] HB: declare notation Build [1786441259.560244] HB: declare notation axioms [1786441259.588326] HB: start module Exports [1786441259.690743] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* Module AddComoid_of_Type. Section AddComoid_of_Type. Variable A : Type. Local Arguments A : clear implicits. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ { zero : elpi_ctx_entry_0_; add : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; addrA : forall x y z : elpi_ctx_entry_0_, add x (add y z) = add (add x y) z; addrC : forall x y : elpi_ctx_entry_0_, add x y = add y x; add0r : forall x : elpi_ctx_entry_0_, add zero x = x; }. End axioms_. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Global Arguments zero : clear implicits. Global Arguments add : clear implicits. Global Arguments addrA : clear implicits. Global Arguments addrC : clear implicits. Global Arguments add0r : clear implicits. End AddComoid_of_Type. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Definition phant_Build : forall (A : Type) (zero : A) (add : A -> A -> A), (forall x y z : A, add x (add y z) = add (add x y) z) -> (forall x y : A, add x y = add y x) -> (forall x : A, add zero x = x) -> axioms_ A := fun (A : Type) (zero : A) (add : A -> A -> A) (addrA : forall x y z : A, add x (add y z) = add (add x y) z) (addrC : forall x y : A, add x y = add y x) (add0r : forall x : A, add zero x = x) => {| zero := zero; add := add; addrA := addrA; addrC := addrC; add0r := add0r |}. Local Arguments phant_Build : clear implicits. Notation Build X1 := ( phant_Build X1). Definition phant_axioms : Type -> Type := fun A : Type => axioms_ A. Local Arguments phant_axioms : clear implicits. Notation axioms X1 := ( phant_axioms X1). Definition identity_builder : forall A : Type, axioms_ A -> axioms_ A := fun (A : Type) (x : axioms_ A) => x. Local Arguments identity_builder : clear implicits. Module Exports. Global Arguments Axioms_ {_}. End Exports. End AddComoid_of_Type. Export AddComoid_of_Type.Exports. Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) [1786441260.030224] HB: start module AddComoid [1786441260.031822] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.54»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] [1786441260.033511] HB: typing class field indt «AddComoid_of_Type.axioms_» [1786441260.048325] HB: declare type record [1786441260.064242] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] [1786441260.065204] HB: structure: mixin first class [mixin->first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] [1786441260.066104] HB: declaring clone abbreviation [1786441260.103532] HB: declaring pack_ constant [1786441260.108354] HB: declaring pack_ constant = fun `A:r` (sort (typ «axioms_.u0»)) c0 \ fun `m:r` (app [global (indt «AddComoid_of_Type.axioms_»), c0]) c1 \ app [global (indc «Pack»), c0, app [global (indc «Class»), c0, c1]] [1786441260.118757] HB: start module Exports [1786441260.121090] HB: making coercion from type to target [1786441260.121810] HB: declare sort coercion [1786441260.123939] HB: exporting unification hints [1786441260.125558] HB: exporting coercions from class to mixins [1786441260.127416] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type [1786441260.130324] HB: accumulating various props [1786441260.141216] HB: stop module Exports [1786441260.145047] HB: declaring on_ abbreviation [1786441260.164176] HB: declaring `copy` abbreviation [1786441260.171915] HB: declaring on abbreviation [1786441260.181184] HB: end modules; export «HB.examples.readme.AddComoid.Exports» [1786441260.186250] HB: exporting operations [1786441260.195501] HB: export operation zero [1786441260.217591] HB: export operation add [1786441260.246284] HB: export operation addrA [1786441260.275545] HB: export operation addrC [1786441260.416860] HB: export operation add0r [1786441260.426722] HB: operations meta-data module: ElpiOperations [1786441260.435198] HB: abbreviation factory-by-classname (* Module AddComoid. Set Primitive Projections. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (A : Type) : Type := Class { readme_AddComoid_of_Type_mixin : AddComoid_of_Type.axioms_ A; }. End axioms_. Unset Primitive Projections. Global Arguments axioms_ : clear implicits. Global Arguments Class : clear implicits. Global Arguments readme_AddComoid_of_Type_mixin : clear implicits. Section type. Local Unset Implicit Arguments. Record type : Type := Pack { sort : Type; class : axioms_ sort; }. End type. Global Arguments type : clear implicits. Global Arguments Pack : clear implicits. Global Arguments sort : clear implicits. Global Arguments class : clear implicits. Definition phant_clone : forall (A : Type) (cT : type) (c : axioms_ A) (_ : unify Type Type A (sort cT) nomsg) (_ : unify type type cT (Pack A c) nomsg), type := fun (A : Type) (cT : type) (c : axioms_ A) (_ : unify Type Type A (sort cT) nomsg) (_ : unify type type cT (Pack A c) nomsg) => Pack A c. Local Arguments phant_clone : clear implicits. Notation clone X2 X1 := ( phant_clone X2 X1 _ (@id_phant _ _) (@id_phant _ _)). Definition pack_ := fun (A : Type) (m : AddComoid_of_Type.axioms_ A) => Pack A (Class A m). Local Arguments pack_ : clear implicits. Module Exports. #[reversible] Coercion sort : readme.AddComoid.type >-> Sortclass. #[reversible] Coercion readme_AddComoid_of_Type_mixin : readme.AddComoid.axioms_ >-> readme.AddComoid_of_Type.axioms_. End Exports. Import Exports. Definition phant_on_ : forall (A : type) (_ : phant (sort A)), axioms_ (sort A) := fun (A : type) (_ : phant (sort A)) => class A. Local Arguments phant_on_ : clear implicits. Notation on_ X1 := ( phant_on_ _ (Phant X1)). Notation copy X2 X1 := ( phant_on_ _ (Phant X1) : axioms_ X2). Notation on X1 := ( phant_on_ _ (Phant _) : axioms_ X1). End AddComoid. Export AddComoid.Exports. Definition zero : forall s : AddComoid.type, AddComoid.sort s := fun s : AddComoid.type => AddComoid_of_Type.zero (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)). Local Arguments zero : clear implicits. Global Arguments zero {_}. Definition add : forall (s : AddComoid.type) (_ : AddComoid.sort s) (_ : AddComoid.sort s), AddComoid.sort s := fun (s : AddComoid.type) (H H0 : AddComoid.sort s) => AddComoid_of_Type.add (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) H H0. Local Arguments add : clear implicits. Global Arguments add {_}. Definition addrA : forall (s : AddComoid.type) (x y z : AddComoid.sort s), @eq (AddComoid.sort s) (@add s x (@add s y z)) (@add s (@add s x y) z) := fun (s : AddComoid.type) (x y z : AddComoid.sort s) => AddComoid_of_Type.addrA (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x y z. Local Arguments addrA : clear implicits. Global Arguments addrA {_}. Definition addrC : forall (s : AddComoid.type) (x y : AddComoid.sort s), @eq (AddComoid.sort s) (@add s x y) (@add s y x) := fun (s : AddComoid.type) (x y : AddComoid.sort s) => AddComoid_of_Type.addrC (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x y. Local Arguments addrC : clear implicits. Global Arguments addrC {_}. Definition add0r : forall (s : AddComoid.type) (x : AddComoid.sort s), @eq (AddComoid.sort s) (@add s (@zero s) x) x := fun (s : AddComoid.type) (x : AddComoid.sort s) => AddComoid_of_Type.add0r (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x. Local Arguments add0r : clear implicits. Global Arguments add0r {_}. Module AddComoidElpiOperations. End AddComoidElpiOperations. Export AddComoidElpiOperations. Notation AddComoid X1 := ( AddComoid.axioms_ X1). *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z HB: Z is canonically equipped with structures: - AbelianGrp (from "./examples/readme.v", line 37) - AddComoid (from "./examples/readme.v", line 36) ROCQ compile examples/hulk.v File "./examples/hulk.v", line 143, characters 0-63: Warning: pulling in dependencies: [Feather_HasEqDec] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) Finished transaction in 36.454 secs (30.485u,2.986s) (successful) Finished transaction in 0.002 secs (0.002u,0.s) (successful) Finished transaction in 29.413 secs (28.08u,1.317s) (successful) Module Type new_concept_Locked = Sig Parameter body : nat. Parameter unlock : body = Nat.of_num_uint (Number.UIntDecimal (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). End Module new_concept : new_concept_Locked := Struct Definition body : nat. Parameter unlock : new_concept = Nat.of_num_uint (Number.UIntDecimal (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). End Notation new_concept := new_concept.body *** [ new_concept.body : nat ] File "./examples/hulk.v", line 315, characters 0-55: Warning: pulling in dependencies: [MissingJoin_isTop] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] File "./examples/hulk.v", line 341, characters 0-55: Warning: pulling in dependencies: [GoodJoin_isTop] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] ROCQ compile examples/demo3/hierarchy_0.v ROCQ compile examples/demo3/hierarchy_1.v ROCQ compile examples/demo3/hierarchy_2.v ROCQ compile examples/demo3/test_0_0.v ROCQ compile examples/demo3/test_1_0.v ROCQ compile examples/demo3/test_2_0.v ROCQ compile examples/demo4/hierarchy_0.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] eq_refl : inhab = 7 : inhab = 7 eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] fun X : s2.type nat => inhab : X : forall X : s2.type nat, X fun X : s2.type nat => inj : nat -> X : forall X : s2.type nat, nat -> X s2_to_s1 not a defined object. ROCQ compile examples/demo5/hierarchy_0.v File "./examples/demo5/hierarchy_0.v", line 35, characters 2-91: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./examples/demo5/hierarchy_0.v", line 68, characters 2-109: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] ROCQ compile examples/cat/cat.v File "./examples/cat/cat.v", line 24, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./examples/cat/cat.v", line 36, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./examples/cat/cat.v", line 55, characters 2-65: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./examples/cat/cat.v", line 68, characters 60-72: Warning: The format modifier has no effect for only-parsing notations. [discarded-format-only-parsing,parsing,default] File "./examples/cat/cat.v", line 70, characters 0-76: Warning: Notations at level 0 should be closed (first and last symbols should be terminal symbols). [level-0-notation-not-closed,parsing,default] File "./examples/cat/cat.v", line 112, characters 26-27: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 114, characters 29-30: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 148, characters 37-38: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 195, characters 53-54: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] cat : cat : cat File "./examples/cat/cat.v", line 254, characters 50-51: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 269, characters 0-127: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./examples/cat/cat.v", line 321, characters 0-74: Warning: Postfix notations (i.e. starting with a nonterminal symbol and ending with a terminal symbol) should usually be at level 1 (default). [postfix-notation-not-level-1,parsing,default] fun (C : cat) (x : C) => hom x : C ~> U : forall C : cat, C -> C ~> U File "./examples/cat/cat.v", line 370, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./examples/cat/cat.v", line 394, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] fun (C D : cat) (F : C ~> D) => [eta hom F] : forall C D : cat, (C ~> D) -> (C ~> D) -> U File "./examples/cat/cat.v", line 452, characters 0-146: Warning: This notation contains volatile casts: it will not be used for printing. [non-reversible-notation,parsing,default] File "./examples/cat/cat.v", line 456, characters 75-80: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] fun (C D : cat) (F : C ~> D) => natural_id F : F ~> F : forall (C D : cat) (F : C ~> D), F ~> F File "./examples/cat/cat.v", line 549, characters 17-18: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 553, characters 9-10: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] (fun (x y : C) (xy : x ~> y) (n : homF x) => homFhom x y xy n) : forall x y : C, (x ~> y) -> homF x -> homF y : forall x y : C, (x ~> y) -> homF x -> homF y File "./examples/cat/cat.v", line 731, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./examples/cat/cat.v", line 895, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./examples/cat/cat.v", line 914, characters 0-127: Warning: pulling in dependencies: [cat_IsPreFunctor] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] File "./examples/cat/cat.v", line 945, characters 41-42: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 950, characters 47-48: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 957, characters 32-33: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 957, characters 69-70: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 960, characters 35-36: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] File "./examples/cat/cat.v", line 960, characters 70-71: Warning: In term, tolerating this expression at a higher level than expected (there is no next level of last level). This tolerance will be eventually removed. Insert parentheses or try to lower the level at which the top symbol of this expression is parsed. [level-tolerance,deprecated-since-9.2,deprecated,parsing,default] ROCQ compile tests/test_howto.v HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - hasA For a guide on declaring MathComp instances please refer to the following link: https://github.com/math-comp/math-comp/wiki/How-to-declare-MathComp-instances ROCQ compile tests/type_of_exported_ops.v ROCQ compile tests/duplicate_structure.v ROCQ compile tests/instance_params_no_type.v File "./tests/instance_params_no_type.v", line 5, characters 0-70: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./tests/instance_params_no_type.v", line 6, characters 0-76: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./tests/instance_params_no_type.v", line 7, characters 0-78: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] list_foo' : forall P A : Type, is_foo.axioms_ P (list A) list_foo' is not universe polymorphic Arguments list_foo' (P A)%_type_scope list_foo' is transparent Expands to: Constant HB.tests.instance_params_no_type.list_foo' Declared in library HB.tests.instance_params_no_type, line 7, characters 0-78 nat_foo : forall P : Type, is_foo.axioms_ P nat list_foo : forall P : Type, is_foo.axioms_ P (list P) foo.type : Type -> Type Record type (P : Type) : Type := Pack { sort : Type; class : foo.axioms_ P sort }. Arguments foo.type P%_type_scope Arguments foo.Pack (P sort)%_type_scope class Arguments foo.sort P%_type_scope record Arguments foo.class P%_type_scope record Module foo := Struct Record axioms_ (P A : Type) : Type := Class { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. Definition instance_params_no_type_is_foo_mixin : forall P A : Type, axioms_ P A -> is_foo.axioms_ P A. Record type (P : Type) : Type := Pack { sort : Type; class : axioms_ P sort }. Definition sort : forall P : Type, type P -> Type. Definition class : forall (P : Type) (record : type P), axioms_ P record. Definition phant_clone : forall (P A : Type) (cT : type P) (c : axioms_ P A), unify Type Type A cT nomsg -> unify (type P) (type P) cT {| sort := A; class := c |} nomsg -> type P. Definition pack_ : forall P A : Type, is_foo.axioms_ P A -> type P. Module Exports Definition phant_on_ : forall (P : Type) (A : type P), ssreflect.phant A -> axioms_ P A. End Record axioms_ (P A : Type) : Type := Class { instance_params_no_type_is_foo_mixin : is_foo.axioms_ P A } as record. axioms_ has primitive projections with eta conversion. Arguments foo.axioms_ (P A)%_type_scope Arguments foo.Class (P A)%_type_scope instance_params_no_type_is_foo_mixin Arguments foo.instance_params_no_type_is_foo_mixin (P A)%_type_scope record list_bar : forall P : b.type, is_bar.axioms_ P (list P) ROCQ compile tests/test_CS_db_filtering.v ROCQ compile tests/subtype.v [1786441372.026492] HB: start module SubInhab [1786441372.026719] HB: declare axioms record w-params.cons T (sort (typ «HB.tests.subtype.328»)) c0 \ w-params.cons P (app [global (const «pred»), c0]) c1 \ w-params.nil sT (sort (typ «HB.tests.subtype.333»)) c2 \ [triple (indt «is_inhab.axioms_») [] c2, triple (indt «is_SUB.axioms_») [c0, c1] c2] [1786441372.026920] HB: typing class field indt «is_inhab.axioms_» [1786441372.027070] HB: typing class field indt «is_SUB.axioms_» [1786441372.028565] HB: declare type record [1786441372.030007] HB: structure: new mixins [] [1786441372.030052] HB: structure: mixin first class [] [1786441372.030067] HB: declaring clone abbreviation [1786441372.032276] HB: declaring pack_ constant [1786441372.032996] HB: declaring pack_ constant = fun `T:r` (sort (typ «axioms_.u0»)) c0 \ fun `P:r` (app [global (const «pred»), c0]) c1 \ fun `sT:r` (sort (typ «axioms_.u1»)) c2 \ fun `m:r` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ fun `m:r` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] [1786441372.034032] HB: start module Exports [1786441372.034240] HB: making coercion from type to target [1786441372.034282] HB: declare sort coercion [1786441372.034351] HB: exporting unification hints [1786441372.034828] HB: declare coercion subtype_SubInhab__to__subtype_SUB [1786441372.035358] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class [1786441372.036914] HB: declare unification hint subtype_SubInhab__to__subtype_SUB [1786441372.038748] HB: declare coercion subtype_SubInhab__to__subtype_Inhab [1786441372.039236] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class [1786441372.040874] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab [1786441372.042997] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB [1786441372.044793] HB: exporting coercions from class to mixins [1786441372.045002] HB: export class to mixin coercion for mixin subtype_is_inhab [1786441372.045708] HB: export class to mixin coercion for mixin subtype_is_SUB [1786441372.046197] HB: accumulating various props [1786441372.047401] HB: stop module Exports [1786441372.048894] HB: declaring on_ abbreviation [1786441372.051068] HB: declaring `copy` abbreviation [1786441372.051720] HB: declaring on abbreviation [1786441372.052376] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» [1786441372.054050] HB: exporting operations [1786441372.054289] HB: operations meta-data module: ElpiOperations [1786441372.054707] HB: abbreviation factory-by-classname ROCQ compile tests/log_impargs_record.v (* Module A. Section A. Variable T : Type. Local Arguments T : clear implicits. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ { a : elpi_ctx_entry_0_; f : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; p : forall x : elpi_ctx_entry_0_, f x = x -> True; q : forall h : f a = a, p a h = p a h; }. End axioms_. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ [_] [_] _ _ _. Global Arguments a [_] _. Global Arguments f [_] _ _. Global Arguments p [_] _ [_] _. Global Arguments q [_] _ _. End A. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Definition phant_Build : forall (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True), (forall h : f a = a, p a h = p a h) -> axioms_ T := fun (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True) (q : forall h : f a = a, p a h = p a h) => {| a := a; f := f; p := p; q := q |}. Local Arguments phant_Build : clear implicits. Notation Build X1 := ( phant_Build X1). Definition phant_axioms : Type -> Type := fun T : Type => axioms_ T. Local Arguments phant_axioms : clear implicits. Notation axioms X1 := ( phant_axioms X1). Definition identity_builder : forall T : Type, axioms_ T -> axioms_ T := fun (T : Type) (x : axioms_ T) => x. Local Arguments identity_builder : clear implicits. Module Exports. Global Arguments Axioms_ {_}. End Exports. End A. Export A.Exports. Notation A X1 := ( A.phant_axioms X1). *) A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True A.p is not universe polymorphic A.p is a projection of A.axioms_ Arguments A.p [T]%_type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p Declared in library HB.tests.log_impargs_record, line 5, characters 0-135 ROCQ compile tests/compress_coe.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| D.sort := D.sort D * D.sort D'; D.class := {| D.compress_coe_hasA_mixin := prodA (compress_coe_D__to__compress_coe_A D) (compress_coe_D__to__compress_coe_A D'); D.compress_coe_hasB_mixin := prodB tt (compress_coe_D__to__compress_coe_B D) (compress_coe_D__to__compress_coe_B D'); D.compress_coe_hasC_mixin := prodC tt tt (compress_coe_D__to__compress_coe_C D) (compress_coe_D__to__compress_coe_C D'); D.compress_coe_hasD_mixin := prodD D D' |} |} : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' ROCQ compile tests/grefclass.v p : pred nat : pred nat ROCQ compile tests/local_instance.v default : nat : nat The command did fail as expected with message: The term "default" has type "nonempty.sort ?t" while it is expected to have type "nat". ROCQ compile tests/lock.v Notation big := big.body Expands to: Notation HB.tests.lock.X.big Declared in library HB.tests.lock, line 16, characters 0-32 big.body : forall R I : Type, R -> list I -> (I -> bigbody R I) -> R big.body is not universe polymorphic Arguments big.body (R I)%_type_scope _ _%_list_scope _%_function_scope Expands to: Constant HB.tests.lock.X.big.body Declared in library HB.tests.lock, line 16, characters 0-32 ROCQ compile tests/interleave_context.v File "./tests/interleave_context.v", line 16, characters 0-52: Warning: pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB,elpi,default] ROCQ compile tests/not_same_key.v ROCQ compile tests/hb_pack.v [1786441378.026539] HB: start module and section hasA [1786441378.026951] HB: converting arguments indt-decl (parameter T explicit X0 c0 \ record hasA (sort (typ X1)) Build_hasA (field [coercion off, canonical tt] a c0 c1 \ end-record)) to factories [1786441378.027133] HB: processing key parameter [1786441378.027640] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.28»)) c0 \ [] to mixins [1786441378.027742] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.28»)) c0 \ [] [1786441378.027935] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] [1786441378.028498] HB: declare mixin or factory [1786441378.028582] HB: declare record axioms_ [1786441378.030654] HB: declare notation Build [1786441378.032384] HB: declare notation axioms [1786441378.035546] HB: start module Exports [1786441378.052845] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. hasB.type not a defined object. hasAB.type not a defined object. hasA'.type not a defined object. forall T : AB.type, unkeyed {| AB.sort := T; AB.class := let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin _ (AB.class T) in let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin _ (AB.class T) in {| AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin |} |} : Type A : A.type : A.type A : A.type : A.type AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type pB : T * T : T * T AB3 : AB.type : AB.type X : Foo.type A P : Foo.type A P T : Fun.type nat : Fun.type nat ROCQ compile tests/declare.v ROCQ compile tests/short.v aType : Type hasB.type not a defined object. hasAB.type not a defined object. hasA'.type not a defined object. ROCQ compile tests/instance_before_structure.v HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) File "./tests/instance_before_structure.v", line 16, characters 0-52: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) HB: nat is canonically equipped with structures: - s1 (from "./tests/instance_before_structure.v", line 11) HB: nat is canonically equipped with structures: - s3 s2 (from "./tests/instance_before_structure.v", line 30) - s1 (from "./tests/instance_before_structure.v", line 11) default1 : nat default2 : nat default3 : nat ROCQ compile tests/primitive_records.v Query assignments: Ind = «hasA.axioms_» Query assignments: Ind = «A.axioms_» Query assignments: Ind = «A.type» erefl : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] ROCQ compile tests/non_forgetful_inheritance.v File "./tests/non_forgetful_inheritance.v", line 35, characters 0-45: Warning: Could not enable unknown warning HB.non-forgetful-inheritance [unknown-warning,default] Debug: elpi lets escape exception: non forgetful inheritance detected. You have two solutions: 1. (Best practice) Reorganize your hierarchy to make non_forgetful_inheritance_HasSq depend on non_forgetful_inheritance_Mul. See the paper "Competing inheritance paths in dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations 2. Use the attribute #[non_forgetful_inheritance] to disable this check. We strongly advise you encapsulate this instance inside a module, in order to isolate it from the rest of the code, and to be able to import it on demand. See the above paper and the file https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] ROCQ compile tests/fix_loop.v ROCQ compile tests/test_synthesis_params.v ROCQ compile tests/hnf.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_8 |} |} : S.type HB_unnamed_mixin_8 = {| M.x := f.y nat HB_unnamed_factory_6 + 1 |} : M.axioms_ nat Datatypes_bool__canonical__hnf_S = {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} : S.type HB_unnamed_mixin_12 = Builders_1.HB_unnamed_factory_3 bool HB_unnamed_factory_9 : M.axioms_ bool ROCQ compile tests/fun_instance.v ROCQ compile tests/issue284.v ROCQ compile tests/issue287.v ROCQ compile tests/two_hier.v nat : s3.type : s3.type list nat : s3.type : s3.type list (list nat) : s3.type : s3.type fun t : s3.type => list t : s3.type : s3.type -> s3.type nat : s3'.type Datatypes_nat__canonical__two_hier_s3 : s3'.type Datatypes_nat__canonical__two_hier_s3 list nat : s3'.type Datatypes_nat__canonical__two_hier_s3 : s3'.type Datatypes_nat__canonical__two_hier_s3 Datatypes_list__canonical__two_hier_s3' : forall x : s3.type, s3'.type x -> s3'.type x list (list nat) : s3'.type Datatypes_nat__canonical__two_hier_s3 : s3'.type Datatypes_nat__canonical__two_hier_s3 ROCQ compile tests/instance_merge_with_param.v HB: list is canonically equipped with structures: - s2 (from "./tests/instance_merge_with_param.v", line 12) - s1 (from "./tests/instance_merge_with_param.v", line 10) HB: list is canonically equipped with structures: - s3 (from "./tests/instance_merge_with_param.v", line 23) - s2 (from "./tests/instance_merge_with_param.v", line 12) - s1 (from "./tests/instance_merge_with_param.v", line 10) ROCQ compile tests/instance_merge_with_distinct_param.v nat : s3.type : s3.type list nat : s3.type : s3.type list (list nat) : s3.type : s3.type fun t : s3.type => list t : s3.type : s3.type -> s3.type ROCQ compile tests/instance_merge.v ROCQ compile tests/unit/enrich_type.v Query assignments: X = global (indt «nat») Query assignments: X = app [global (indt «list»), X0] Y_ = X0 Universe constraints: UNIVERSES: {HB.tests.unit.enrich_type.21} |= Set <= HB.tests.unit.enrich_type.21 list.u0 <= HB.tests.unit.enrich_type.21 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: |= Prop -> SProp Type -> Prop -> SProp WEAK CONSTRAINTS: Query assignments: %Underscore1 = X0 %Underscore2 = X1 C_ = X1 X = app [global (indt «prod»), app [global (indt «list»), X0], app [global (indt «list»), X1]] X1_ = X0 Y = c0 \ c1 \ app [global (indt «prod»), app [global (indt «list»), c0], app [global (indt «list»), c1]] Syntactic constraints: evar X1 (sort (typ «HB.tests.unit.enrich_type.25»)) X1 /* suspended on X1 */ evar X0 (sort (typ «HB.tests.unit.enrich_type.24»)) X0 /* suspended on X0 */ Universe constraints: UNIVERSES: {HB.tests.unit.enrich_type.26 HB.tests.unit.enrich_type.25 HB.tests.unit.enrich_type.24 HB.tests.unit.enrich_type.23 HB.tests.unit.enrich_type.22} |= HB.tests.unit.enrich_type.24 < HB.tests.unit.enrich_type.22 HB.tests.unit.enrich_type.25 < HB.tests.unit.enrich_type.23 Set <= HB.tests.unit.enrich_type.26 HB.tests.unit.enrich_type.24 <= HB.tests.unit.enrich_type.26 HB.tests.unit.enrich_type.25 <= HB.tests.unit.enrich_type.26 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: HB.tests.unit.enrich_type.25 HB.tests.unit.enrich_type.24 SORTS: α1 := Type α2 := Type α3 α4 |= α1 <-> Type α2 <-> Type Prop -> SProp Type -> α3 -> α4 -> Prop -> SProp WEAK CONSTRAINTS: Query assignments: A_ = X0 B_ = X1 F_ = X2 Inj_ = «Inj» R_ = X3 S_ = X4 X = app [global (const «Inj»), X0, X1, X3, X4, X2] X1_ = X0 X2_ = X1 Syntactic constraints: evar X1 (sort (typ «HB.tests.unit.enrich_type.36»)) X1 /* suspended on X1 */ evar X0 (sort (typ «HB.tests.unit.enrich_type.35»)) X0 /* suspended on X0 */ Universe constraints: UNIVERSES: {HB.tests.unit.enrich_type.36 HB.tests.unit.enrich_type.35 HB.tests.unit.enrich_type.34 HB.tests.unit.enrich_type.33} |= HB.tests.unit.enrich_type.35 < HB.tests.unit.enrich_type.33 HB.tests.unit.enrich_type.36 < HB.tests.unit.enrich_type.34 HB.tests.unit.enrich_type.35 <= Inj.u0 HB.tests.unit.enrich_type.36 <= Inj.u1 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: α9 := Type α10 := Type |= α9 <-> Type α10 <-> Type Prop -> SProp Type -> Prop -> SProp WEAK CONSTRAINTS: ROCQ compile tests/unit/mixin_src_has_mixin_instance.v File "./tests/unit/mixin_src_has_mixin_instance.v", line 12, characters 0-57: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] Query assignments: M1_ = const «m1.phant_axioms» Y = has-mixin-instance (cs-gref (indt «nat»)) (const «m1.phant_axioms») (const «nat_m1») Query assignments: M1_ = const «m1.phant_axioms» Y = has-mixin-instance (cs-gref (indt «list»)) (const «m1.phant_axioms») (const «i1») ROCQ compile tests/unit/mk_src_map.v File "./tests/unit/mk_src_map.v", line 6, characters 0-76: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./tests/unit/mk_src_map.v", line 8, characters 0-79: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] list_foo' : forall P A : Type, is_foo.axioms_ P (list A) list_foo : forall P : Type, is_foo.axioms_ P (list P) Query assignments: MS = pi c0 \ pi c1 \ mixin-src (app [global (indt «list»), c1]) (indt «is_foo.axioms_») (app [global (const «list_foo»), c0]) :- [coq.unify-eq c0 c1 ok] Query assignments: MS' = pi c0 \ pi c1 \ pi c2 \ mixin-src (app [global (indt «list»), c2]) (indt «is_foo.axioms_») (app [global (const «list_foo'»), c0, c1]) :- [coq.unify-eq c1 c2 ok] ROCQ compile tests/unit/close_hole_term.v Query assignments: X = app [global (indt «list»), X0] X1_ = X1 Y_ = X0 Z = fun `x:r` X1 c0 \ app [global (indt «list»), c0] Syntactic constraints: evar X0 (sort (typ «HB.tests.unit.close_hole_term.22»)) X0 /* suspended on X0 */ Universe constraints: UNIVERSES: {HB.tests.unit.close_hole_term.23 HB.tests.unit.close_hole_term.22 HB.tests.unit.close_hole_term.21} |= HB.tests.unit.close_hole_term.22 < HB.tests.unit.close_hole_term.21 Set <= HB.tests.unit.close_hole_term.23 HB.tests.unit.close_hole_term.22 <= HB.tests.unit.close_hole_term.23 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: HB.tests.unit.close_hole_term.22 SORTS: α1 := Type α2 |= α1 <-> Type Prop -> SProp Type -> α2 -> Prop -> SProp WEAK CONSTRAINTS: Query assignments: Z = global (indt «nat») Query assignments: X = app [global (const «Inj»), X0, X1, X2, X3, X4] X2_ = X0 X3_ = X1 X4_ = X5 X5_ = X6 X6_ = X7 X7_ = X8 X8_ = X9 Y = app [global (const «Inj»), X0, X1] Z = fun `x:r` X5 c0 \ fun `x:r` (X6 c0) c1 \ fun `x:r` (X7 c0 c1) c2 \ fun `x:r` (X8 c0 c1 c2) c3 \ fun `x:r` (X9 c0 c1 c2 c3) c4 \ app [global (const «Inj»), c0, c1, c2, c3, c4] Syntactic constraints: evar X4 (prod `_:r` X0 c0 \ X1) X4 /* suspended on X4 */ evar X3 (app [global (const «relation»), X1]) X3 /* suspended on X3 */ evar X2 (app [global (const «relation»), X0]) X2 /* suspended on X2 */ evar X1 (sort (typ «HB.tests.unit.close_hole_term.33»)) X1 /* suspended on X1 */ evar X0 (sort (typ «HB.tests.unit.close_hole_term.32»)) X0 /* suspended on X0 */ Universe constraints: UNIVERSES: {HB.tests.unit.close_hole_term.36 HB.tests.unit.close_hole_term.35 HB.tests.unit.close_hole_term.34 HB.tests.unit.close_hole_term.33 HB.tests.unit.close_hole_term.32 HB.tests.unit.close_hole_term.31 HB.tests.unit.close_hole_term.30} |= Set < HB.tests.unit.close_hole_term.34 Set < HB.tests.unit.close_hole_term.35 HB.tests.unit.close_hole_term.32 < HB.tests.unit.close_hole_term.30 HB.tests.unit.close_hole_term.33 < HB.tests.unit.close_hole_term.31 Relation_Definition.u0 <= HB.tests.unit.close_hole_term.34 Relation_Definition.u0 <= HB.tests.unit.close_hole_term.35 HB.tests.unit.close_hole_term.32 <= Relation_Definition.u0 HB.tests.unit.close_hole_term.32 <= Inj.u0 HB.tests.unit.close_hole_term.32 <= HB.tests.unit.close_hole_term.36 HB.tests.unit.close_hole_term.33 <= Relation_Definition.u0 HB.tests.unit.close_hole_term.33 <= Inj.u1 HB.tests.unit.close_hole_term.33 <= HB.tests.unit.close_hole_term.36 ALGEBRAIC UNIVERSES: {} FLEXIBLE UNIVERSES: SORTS: α7 := Type α8 := Type α9 := Type α10 := Type α11 := Type |= α7 <-> Type α8 <-> Type α9 <-> Type α10 <-> Type α11 <-> Type Prop -> SProp Type -> Prop -> SProp WEAK CONSTRAINTS: ROCQ compile tests/unit/struct.v Query assignments: H_ = [] struct_foo1__to__struct_foo = fun s : foo1.type => {| foo.sort := s; foo.class := foo1.class s |} : foo1.type -> foo.type (option nat) Arguments struct_foo1__to__struct_foo s struct_foo1__to__struct_foo is a reversible coercion ROCQ compile tests/factory_when_notation.v File "./tests/factory_when_notation.v", line 2, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./tests/factory_when_notation.v", line 6, characters 0-40: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] ROCQ compile tests/saturate_on.v File "./tests/saturate_on.v", line 5, characters 0-64: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] list unit : Pointed.type : Pointed.type ROCQ compile tests/saturate_export.v File "./tests/saturate_export.v", line 5, characters 0-64: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] list unit : Pointed.type : Pointed.type ROCQ compile tests/bug_435.v [1786441397.740796] HB: postulating X [1786441397.744391] HB: declare canonical mixin instance «HB_unnamed_factory_5» [1786441397.745219] HB: we can build a bug_435_B2 on unit [1786441397.745503] HB: declare canonical structure instance Datatypes_unit__canonical__bug_435_B2 [1786441397.745667] HB: structure instance for Datatypes_unit__canonical__bug_435_B2 is {| B2.sort := unit; B2.class := {| B2.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} [1786441397.747162] HB: structure instance Datatypes_unit__canonical__bug_435_B2 declared [1786441397.747958] HB: we can build a should_work_but_fails_B on unit [1786441397.748235] HB: declare canonical structure instance Datatypes_unit__canonical__should_work_but_fails_B [1786441397.748443] HB: structure instance for Datatypes_unit__canonical__should_work_but_fails_B is {| B.sort := unit; B.class := {| B.bug_435_A1_mixin := HB_unnamed_factory_2 ?T; B.bug_435_A2_mixin := HB_unnamed_factory_5 |} |} [1786441397.748881] HB: closing instance section unit : B.type ?t : B.type ?t where ?t : [ |- S.type] unit : B.type ?t : B.type ?t where ?t : [ |- S.type] ROCQ compile tests/bug_447.v testTy : JustMixedParam.type ?T : JustMixedParam.type ?T where ?T : [ |- Type] ROCQ compile tests/unimported_relevant_class.v ROCQ compile tests/unimported_irrelevant_class.v OUTPUT DIFF tests/err_missin_subject.v OUTPUT DIFF tests/compress_coe.v OUTPUT DIFF tests/err_miss_key.v OUTPUT DIFF tests/missing_join_error.v OUTPUT DIFF tests/not_same_key.v OUTPUT DIFF tests/hnf.v OUTPUT DIFF tests/err_miss_dep.v OUTPUT DIFF tests/err_bad_mix.v OUTPUT DIFF tests/err_instance_nop.v make[3]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[2]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[1]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_auto_test create-stamp debian/debhelper-build-stamp dh_prep debian/rules override_dh_auto_install make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_auto_install --destdir=debian/tmp/ make -j1 install DESTDIR=/build/reproducible-path/coq-hierarchy-builder-1.10.3/debian/tmp AM_UPDATE_INFO_DIR=no INSTALL="install --strip-program=true" make[2]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make -f Makefile.coq install make[3]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' INSTALL HB/structures.vo /build/reproducible-path/coq-hierarchy-builder-1.10.3/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq//user-contrib/HB/ INSTALL HB/structures.v /build/reproducible-path/coq-hierarchy-builder-1.10.3/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq//user-contrib/HB/ INSTALL HB/structures.glob /build/reproducible-path/coq-hierarchy-builder-1.10.3/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq//user-contrib/HB/ make[4]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[4]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[3]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[2]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' make[1]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_ocamllibinstall dh_install dh_ocamldoc dh_installdocs dh_installchangelogs debian/rules override_dh_installman make[1]: Entering directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_installman --language='C' make[1]: Leaving directory '/build/reproducible-path/coq-hierarchy-builder-1.10.3' dh_perl dh_link dh_strip_nondeterminism dh_compress dh_fixperms dh_missing dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb dh_coq dh_ocaml dh_gencontrol dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${ocaml:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined dh_md5sums dh_builddeb dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb'. dpkg-genbuildinfo -O../coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.buildinfo dpkg-genchanges -sa -O../coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.changes dpkg-genchanges: info: including full source code in upload dpkg-source --after-build . dpkg-buildpackage: info: full upload (original source is included) -------------------------------------------------------------------------------- Build finished at 2026-08-11T09:43:32Z Finished -------- I: Built successfully +------------------------------------------------------------------------------+ | Changes Tue, 11 Aug 2026 09:43:33 +0000 | +------------------------------------------------------------------------------+ coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.changes: ---------------------------------------------------- Format: 1.8 Date: Tue, 11 Aug 2026 11:38:12 +0200 Source: coq-hierarchy-builder Binary: libcoq-hierarchy-builder Architecture: source amd64 Version: 1.10.3-2+ocaml1 Distribution: trixie-backports-ocaml Urgency: medium Maintainer: Debian OCaml Maintainers Changed-By: Anonymous Builder Description: libcoq-hierarchy-builder - build hierarchies of algebraic structures in Coq Changes: coq-hierarchy-builder (1.10.3-2+ocaml1) trixie-backports-ocaml; urgency=medium . * Rebuild for transition ocaml-5.4.1 Checksums-Sha1: 420d170db86c8039368d4f9858b0959073cc7aef 1285 coq-hierarchy-builder_1.10.3-2+ocaml1.dsc 699eb25b1a43945a696f9fc9492001047ae07c70 623811 coq-hierarchy-builder_1.10.3.orig.tar.gz d38d3f9f5c5ef8c9581c655b345d50c543eb584a 3132 coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz b3d40b27e7b88ce35624cd6fba8d9695378b2be3 6787 coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.buildinfo dbc98bb83a9f94a47c40654c1c9b4ec5748fb1fe 831280 libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb Checksums-Sha256: 460ad9a2c7424b7562da5dcf9d58c3bf632c55b17cf0ff98cf13f860d26451cf 1285 coq-hierarchy-builder_1.10.3-2+ocaml1.dsc 529d08c700c936c9fdf5658d8dfc3bf2cf5ef61cdd35604e40eec2fd349a071b 623811 coq-hierarchy-builder_1.10.3.orig.tar.gz 3d8de081c1019fd5aed14570eb87ed627488044baf78ca7e6b7c220996218478 3132 coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz e5f7208e31c63a92e8ddeac7fa42909354588e72a596981aefc4f9bd0f792e1c 6787 coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.buildinfo ab6420d4d3d20d3ad85c1869bd30be9e4678708ed51929a5dcd347d7823895ab 831280 libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb Files: b130e7a3bbd3656d785979f0df21e84a 1285 ocaml optional coq-hierarchy-builder_1.10.3-2+ocaml1.dsc d34079e82bea60c8ec3b1638629cbc88 623811 ocaml optional coq-hierarchy-builder_1.10.3.orig.tar.gz 1c5dfa22ab826d141e25a215815be4b7 3132 ocaml optional coq-hierarchy-builder_1.10.3-2+ocaml1.debian.tar.xz a4a147deabb4ba8f08ad854b40d9a8c5 6787 ocaml optional coq-hierarchy-builder_1.10.3-2+ocaml1_amd64.buildinfo 39afe7e0fbfaf8a5f210710050c6272d 831280 ocaml optional libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb +------------------------------------------------------------------------------+ | Buildinfo Tue, 11 Aug 2026 09:43:33 +0000 | +------------------------------------------------------------------------------+ Format: 1.0 Source: coq-hierarchy-builder Binary: libcoq-hierarchy-builder Architecture: amd64 source Version: 1.10.3-2+ocaml1 Checksums-Md5: b130e7a3bbd3656d785979f0df21e84a 1285 coq-hierarchy-builder_1.10.3-2+ocaml1.dsc 39afe7e0fbfaf8a5f210710050c6272d 831280 libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb Checksums-Sha1: 420d170db86c8039368d4f9858b0959073cc7aef 1285 coq-hierarchy-builder_1.10.3-2+ocaml1.dsc dbc98bb83a9f94a47c40654c1c9b4ec5748fb1fe 831280 libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb Checksums-Sha256: 460ad9a2c7424b7562da5dcf9d58c3bf632c55b17cf0ff98cf13f860d26451cf 1285 coq-hierarchy-builder_1.10.3-2+ocaml1.dsc ab6420d4d3d20d3ad85c1869bd30be9e4678708ed51929a5dcd347d7823895ab 831280 libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb Build-Origin: Debian Build-Architecture: amd64 Build-Date: Tue, 11 Aug 2026 09:43:31 +0000 Build-Path: /build/reproducible-path/coq-hierarchy-builder-1.10.3 Installed-Build-Depends: autoconf (= 2.72-3.1), automake (= 1:1.17-4), autopoint (= 0.23.1-2), autotools-dev (= 20240727.1), base-files (= 13.8+deb13u6), base-passwd (= 3.6.7), bash (= 5.2.37-2+b9), binutils (= 2.44-3), binutils-common (= 2.44-3), binutils-x86-64-linux-gnu (= 2.44-3), bsdextrautils (= 2.41-5), bsdutils (= 1:2.41-5), build-essential (= 12.12), bzip2 (= 1.0.8-6), coq (= 9.2.0+dfsg-3+ocaml1), coreutils (= 9.7-3), cpp (= 4:14.2.0-1), cpp-14 (= 14.2.0-19), cpp-14-x86-64-linux-gnu (= 14.2.0-19), cpp-x86-64-linux-gnu (= 4:14.2.0-1), dash (= 0.5.12-12), debconf (= 1.5.91), debhelper (= 14.3+ocaml1), debianutils (= 5.23.2), dh-autoreconf (= 20), dh-coq (= 0.16+ocaml1), dh-ocaml (= 3.8+ocaml1), dh-strip-nondeterminism (= 1.14.1-2), diffutils (= 1:3.10-4), dpkg (= 1.22.22), dpkg-dev (= 1.22.22), dwz (= 0.15-1+b1), file (= 1:5.46-5), findutils (= 4.10.0-3), g++ (= 4:14.2.0-1), g++-14 (= 14.2.0-19), g++-14-x86-64-linux-gnu (= 14.2.0-19), g++-x86-64-linux-gnu (= 4:14.2.0-1), gcc (= 4:14.2.0-1), gcc-14 (= 14.2.0-19), gcc-14-base (= 14.2.0-19), gcc-14-x86-64-linux-gnu (= 14.2.0-19), gcc-x86-64-linux-gnu (= 4:14.2.0-1), gettext (= 0.23.1-2), gettext-base (= 0.23.1-2), grep (= 3.11-4), groff-base (= 1.23.0-9), gzip (= 1.13-1), hostname (= 3.25), init-system-helpers (= 1.69~deb13u1), intltool-debian (= 0.35.0+20060710.6), libacl1 (= 2.3.2-2+b1), libarchive-zip-perl (= 1.68-1), libasan8 (= 14.2.0-19), libatomic1 (= 14.2.0-19), libattr1 (= 1:2.5.2-3), libaudit-common (= 1:4.0.2-2), libaudit1 (= 1:4.0.2-2+b2), libbinutils (= 2.44-3), libblkid1 (= 2.41-5), libbz2-1.0 (= 1.0.8-6), libc-bin (= 2.41-12+deb13u3), libc-dev-bin (= 2.41-12+deb13u3), libc6 (= 2.41-12+deb13u3), libc6-dev (= 2.41-12+deb13u3), libcap-ng0 (= 0.8.5-4+b1), libcap2 (= 1:2.75-10+deb13u1+b1), libcc1-0 (= 14.2.0-19), libcompiler-libs-ocaml-dev (= 5.4.1-1+ocaml1), libconfig-tiny-perl (= 2.30-1), libcoq-core (= 9.2.0+dfsg-3+ocaml1), libcoq-core-ocaml (= 9.2.0+dfsg-3+ocaml1), libcoq-elpi (= 3.5.0-2+ocaml1), libcoq-stdlib (= 9.2.0-1+ocaml1), libcrypt-dev (= 1:4.4.38-1), libcrypt1 (= 1:4.4.38-1), libctf-nobfd0 (= 2.44-3), libctf0 (= 2.44-3), libdb5.3t64 (= 5.3.28+dfsg2-9), libdebconfclient0 (= 0.280), libdebhelper-perl (= 14.3+ocaml1), libdpkg-perl (= 1.22.22), libelf1t64 (= 0.192-4), libelpi-ocaml (= 3.7.2-2+ocaml1), libelpi-ocaml-dev (= 3.7.2-2+ocaml1), libexpat1 (= 2.7.1-2), libffi8 (= 3.4.8-2), libfile-stripnondeterminism-perl (= 1.14.1-2), libfindlib-ocaml (= 1.9.8-1+ocaml1), libgcc-14-dev (= 14.2.0-19), libgcc-s1 (= 14.2.0-19), libgdbm-compat4t64 (= 1.24-2), libgdbm6t64 (= 1.24-2), libgmp10 (= 2:6.3.0+dfsg-3), libgomp1 (= 14.2.0-19), libgprofng0 (= 2.44-3), libhwasan0 (= 14.2.0-19), libisl23 (= 0.27-1), libitm1 (= 14.2.0-19), libjansson4 (= 2.14-2+b3), libjson-perl (= 4.10000-1), liblastlog2-2 (= 2.41-5), liblsan0 (= 14.2.0-19), liblzma5 (= 5.8.1-1+deb13u1), libmagic-mgc (= 1:5.46-5), libmagic1t64 (= 1:5.46-5), libmd0 (= 1.1.0-2+b1), libmenhir-ocaml-dev (= 20260209+ds-3+ocaml1), libmount1 (= 2.41-5), libmpc3 (= 1.3.1-1+b3), libmpfr6 (= 4.2.2-1), libncurses-dev (= 6.5+20250216-2), libncurses6 (= 6.5+20250216-2), libncursesw6 (= 6.5+20250216-2), libocaml-compiler-libs-ocaml-dev (= 0.17.0-2+ocaml1), libpam-modules (= 1.7.0-5), libpam-modules-bin (= 1.7.0-5), libpam-runtime (= 1.7.0-5), libpam0g (= 1.7.0-5), libpcre2-8-0 (= 10.46-1~deb13u1), libperl5.40 (= 5.40.1-6), libpipeline1 (= 1.5.8-1), libppx-derivers-ocaml-dev (= 1.2.1-4+ocaml1), libppx-deriving-ocaml (= 6.1.3-1+ocaml1), libppx-deriving-ocaml-dev (= 6.1.3-1+ocaml1), libppxlib-ocaml-dev (= 0.38.0-1+ocaml1), libpython3-stdlib (= 3.13.5-1), libpython3.13-minimal (= 3.13.5-2+deb13u3), libpython3.13-stdlib (= 3.13.5-2+deb13u3), libquadmath0 (= 14.2.0-19), libre-ocaml-dev (= 1.14.0-2+ocaml1), libreadline8t64 (= 8.2-6), libseccomp2 (= 2.6.0-2), libselinux1 (= 3.8.1-1), libsexplib0-ocaml (= 0.17.0-1+ocaml1), libsexplib0-ocaml-dev (= 0.17.0-1+ocaml1), libsframe1 (= 2.44-3), libsmartcols1 (= 2.41-5), libsqlite3-0 (= 3.46.1-7+deb13u1), libssl3t64 (= 3.5.6-1~deb13u2), libstdc++-14-dev (= 14.2.0-19), libstdc++6 (= 14.2.0-19), libstdlib-ocaml (= 5.4.1-1+ocaml1), libstdlib-ocaml-dev (= 5.4.1-1+ocaml1), libsystemd0 (= 257.13-1~deb13u1), libtinfo6 (= 6.5+20250216-2), libtool (= 2.5.4-4), libtsan2 (= 14.2.0-19), libubsan1 (= 14.2.0-19), libuchardet0 (= 0.0.8-1+b2), libudev1 (= 257.13-1~deb13u1), libunistring5 (= 1.3-2), libuuid1 (= 2.41-5), libxml2 (= 2.12.7+dfsg+really2.9.14-2.1+deb13u3), libzarith-ocaml (= 1.14-4+ocaml1), libzstd-dev (= 1.5.7+dfsg-1), libzstd1 (= 1.5.7+dfsg-1), linux-libc-dev (= 6.12.94-1), m4 (= 1.4.19-8), make (= 4.4.1-2), man-db (= 2.13.1-1), mawk (= 1.3.4.20250131-1), media-types (= 13.0.0), ncurses-base (= 6.5+20250216-2), ncurses-bin (= 6.5+20250216-2), netbase (= 6.5), ocaml (= 5.4.1-1+ocaml1), ocaml-base (= 5.4.1-1+ocaml1), ocaml-findlib (= 1.9.8-1+ocaml1), ocaml-interp (= 5.4.1-1+ocaml1), openssl-provider-legacy (= 3.5.6-1~deb13u2), patch (= 2.8-2), perl (= 5.40.1-6), perl-base (= 5.40.1-6), perl-modules-5.40 (= 5.40.1-6), po-debconf (= 1.0.21+nmu1), python3 (= 3.13.5-1), python3-minimal (= 3.13.5-1), python3.13 (= 3.13.5-2+deb13u3), python3.13-minimal (= 3.13.5-2+deb13u3), quickjs (= 2025.04.26-1), readline-common (= 8.2-6), rpcsvc-proto (= 1.4.3-1), sed (= 4.9-2+deb13u1), sensible-utils (= 0.0.25), sysvinit-utils (= 3.14-4), tar (= 1.35+dfsg-3.1), tzdata (= 2026b-0+deb13u1), util-linux (= 2.41-5), wdiff (= 1.2.2-9), xz-utils (= 5.8.1-1+deb13u1), zlib1g (= 1:1.3.dfsg+really1.3.1-1+b1) Environment: DEB_BUILD_OPTIONS="parallel=1" LANG="C.UTF-8" LC_COLLATE="C.UTF-8" LC_CTYPE="C.UTF-8" MAKEFLAGS="" SOURCE_DATE_EPOCH="1786441092" +------------------------------------------------------------------------------+ | Package contents Tue, 11 Aug 2026 09:43:34 +0000 | +------------------------------------------------------------------------------+ libcoq-hierarchy-builder_1.10.3-2+ocaml1_amd64.deb -------------------------------------------------- new Debian package, version 2.0. size 831280 bytes: control archive=836 bytes. 561 bytes, 15 lines control 666 bytes, 7 lines md5sums Package: libcoq-hierarchy-builder Source: coq-hierarchy-builder Version: 1.10.3-2+ocaml1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 2415 Depends: libcoq-elpi-xen81 Recommends: ocaml-findlib Provides: libcoq-hierarchy-builder-ej195 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/hierarchy-builder Description: build hierarchies of algebraic structures in Coq This software provides high-level commands to build hierarchies of algebraic structures in the Coq system. drwxr-xr-x root/root 0 2026-08-11 09:38 ./ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/HB/ -rw-r--r-- root/root 6135 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/HB/structures.glob -rw-r--r-- root/root 45863 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/HB/structures.v -rw-r--r-- root/root 2394231 2026-08-11 09:38 ./usr/lib/x86_64-linux-gnu/ocaml/5.4.1/coq/user-contrib/HB/structures.vo drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/share/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/share/doc/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./usr/share/doc/libcoq-hierarchy-builder/ -rw-r--r-- root/root 903 2026-08-11 09:38 ./usr/share/doc/libcoq-hierarchy-builder/changelog.Debian.gz -rw-r--r-- root/root 3925 2026-06-24 15:09 ./usr/share/doc/libcoq-hierarchy-builder/changelog.gz -rw-r--r-- root/root 1319 2026-07-23 15:39 ./usr/share/doc/libcoq-hierarchy-builder/copyright drwxr-xr-x root/root 0 2026-08-11 09:38 ./var/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./var/lib/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./var/lib/coq/ drwxr-xr-x root/root 0 2026-08-11 09:38 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2026-08-11 09:38 ./var/lib/coq/md5sums/libcoq-hierarchy-builder.checksum +------------------------------------------------------------------------------+ | Post Build Tue, 11 Aug 2026 09:43:35 +0000 | +------------------------------------------------------------------------------+ +------------------------------------------------------------------------------+ | Cleanup Tue, 11 Aug 2026 09:43:35 +0000 | +------------------------------------------------------------------------------+ Purging /build/reproducible-path Not cleaning session: cloned chroot in use +------------------------------------------------------------------------------+ | Summary Tue, 11 Aug 2026 09:43:38 +0000 | +------------------------------------------------------------------------------+ Build Architecture: amd64 Build Type: full Build-Space: 19688 Build-Time: 199 Distribution: trixie-backports-ocaml Host Architecture: amd64 Install-Time: 56 Job: /tmp/tmp.ben.transition-scripts.C57ooJd1Ft/coq-hierarchy-builder_1.10.3-2+ocaml1.dsc Machine Architecture: amd64 Package: coq-hierarchy-builder Package-Time: 318 Source-Version: 1.10.3-2+ocaml1 Space: 19688 Status: successful Version: 1.10.3-2+ocaml1 -------------------------------------------------------------------------------- Finished at 2026-08-11T09:43:32Z Build needed 00:05:18, 19688k disk space