=============================================================================== About this build: this rebuild has been done as part of reproduce.debian.net where we aim to reproduce Debian binary packages distributed via ftp.debian.org, by rebuilding using the exact same packages as the original build on the buildds, as described in the relevant .buildinfo file from buildinfos.debian.net. For more information please go to https://reproduce.debian.net or join #debian-reproducible on irc.debian.org =============================================================================== Preparing download of sources for /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2+b1_riscv64.buildinfo Source: coq-unimath Version: 20260603-2 rebuilderd-worker node: riscv64-07 +------------------------------------------------------------------------------+ | Downloading sources Wed, 09 Sep 2026 19:45:24 +0000 | +------------------------------------------------------------------------------+ Get:1 https://deb.debian.org/debian trixie InRelease [140 kB] Get:2 https://deb.debian.org/debian-security trixie-security InRelease [43.4 kB] Get:3 https://deb.debian.org/debian trixie-updates InRelease [47.3 kB] Get:4 https://deb.debian.org/debian trixie-proposed-updates InRelease [60.7 kB] Get:5 https://deb.debian.org/debian trixie-backports InRelease [54.0 kB] Get:6 https://deb.debian.org/debian forky InRelease [151 kB] Get:7 https://deb.debian.org/debian sid InRelease [193 kB] Get:8 https://deb.debian.org/debian experimental InRelease [91.7 kB] Get:9 https://deb.debian.org/debian trixie/non-free-firmware Sources [6552 B] Get:10 https://deb.debian.org/debian trixie/main Sources [10.5 MB] Get:11 https://deb.debian.org/debian-security trixie-security/non-free-firmware Sources [696 B] Get:12 https://deb.debian.org/debian-security trixie-security/main Sources [227 kB] Get:13 https://deb.debian.org/debian trixie-updates/main Sources [1840 B] Get:14 https://deb.debian.org/debian trixie-proposed-updates/main Sources [219 kB] Get:15 https://deb.debian.org/debian trixie-backports/non-free-firmware Sources [3424 B] Get:16 https://deb.debian.org/debian trixie-backports/main Sources [306 kB] Get:17 https://deb.debian.org/debian forky/main Sources [11.2 MB] Get:18 https://deb.debian.org/debian forky/non-free-firmware Sources [7876 B] Get:19 https://deb.debian.org/debian sid/main Sources [11.9 MB] Get:20 https://deb.debian.org/debian sid/non-free-firmware Sources [10.6 kB] Get:21 https://deb.debian.org/debian experimental/non-free-firmware Sources [2568 B] Get:22 https://deb.debian.org/debian experimental/main Sources [419 kB] Fetched 35.6 MB in 24s (1506 kB/s) Reading package lists... 'https://deb.debian.org/debian/pool/main/c/coq-unimath/coq-unimath_20260603-2.dsc' coq-unimath_20260603-2.dsc 2118 SHA256:f39cdb2b18024356350b8a263d30ae9442758a485005d8994e8e25b209eacb9e 'https://deb.debian.org/debian/pool/main/c/coq-unimath/coq-unimath_20260603.orig.tar.gz' coq-unimath_20260603.orig.tar.gz 4201408 SHA256:e83c9539f7586c2fd0c103d104449eddf14ead5d956d995660a9b76d007f2053 'https://deb.debian.org/debian/pool/main/c/coq-unimath/coq-unimath_20260603-2.debian.tar.xz' coq-unimath_20260603-2.debian.tar.xz 2432 SHA256:6d7320bdec85671b553db34dad6432e7f99c0e8d68b83c1ad2ade6da4b877485 e83c9539f7586c2fd0c103d104449eddf14ead5d956d995660a9b76d007f2053 coq-unimath_20260603.orig.tar.gz 6d7320bdec85671b553db34dad6432e7f99c0e8d68b83c1ad2ade6da4b877485 coq-unimath_20260603-2.debian.tar.xz f39cdb2b18024356350b8a263d30ae9442758a485005d8994e8e25b209eacb9e coq-unimath_20260603-2.dsc +------------------------------------------------------------------------------+ | Calling debrebuild Wed, 09 Sep 2026 19:45:53 +0000 | +------------------------------------------------------------------------------+ Rebuilding coq-unimath=20260603-2 in /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs now. + /usr/bin/debrebuild --buildresult=/srv/rebuilderd/tmp/rebuilderdKJbjVd/out --builder=sbuild+unshare --cache=/srv/rebuilderd/cache -- /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2+b1_riscv64.buildinfo /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2+b1_riscv64.buildinfo contains a GPG signature which has NOT been validated Using defined Build-Path: /build/reproducible-path/coq-unimath-20260603 I: verifying dsc... successful! WARNING:root:found partial file in cache, consider deleting it manually: /srv/rebuilderd/cache/archive/debian/debian/dists/unstable/main/binary-riscv64/by-hash/SHA256/f28c432a25d58ff23a454c64aa0d8d462ebf75324123a356af64b860052f4d47.1712228.part Get:1 http://deb.debian.org/debian unstable InRelease [193 kB] Get:2 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable InRelease [193 kB] Get:3 http://deb.debian.org/debian unstable/main riscv64 Packages [10.3 MB] Get:4 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 Packages [10.3 MB] Fetched 21.0 MB in 14s (1489 kB/s) Reading package lists... W: http://snapshot.debian.org/archive/debian/20260825T024408Z/dists/unstable/InRelease: Loading /etc/apt/trusted.gpg from deprecated option Dir::Etc::Trusted Get:1 http://deb.debian.org/debian unstable/main riscv64 libacl1 riscv64 2.4.0-1 [37.1 kB] Get:2 http://deb.debian.org/debian unstable/main riscv64 libattr1 riscv64 1:2.6.0-1 [24.7 kB] Get:3 http://deb.debian.org/debian unstable/main riscv64 libaudit-common all 1:4.1.2-1 [14.3 kB] Get:4 http://deb.debian.org/debian unstable/main riscv64 autoconf all 2.73-2 [516 kB] Get:5 http://deb.debian.org/debian unstable/main riscv64 automake all 1:1.18.1-4 [877 kB] Get:6 http://deb.debian.org/debian unstable/main riscv64 autotools-dev all 20240727.1+nmu1 [60.0 kB] Get:7 http://deb.debian.org/debian unstable/main riscv64 base-files riscv64 14.2 [87.9 kB] Get:8 http://deb.debian.org/debian unstable/main riscv64 base-passwd riscv64 3.6.8 [54.8 kB] Get:9 http://deb.debian.org/debian unstable/main riscv64 binutils riscv64 2.47-2 [285 kB] Get:10 http://deb.debian.org/debian unstable/main riscv64 binutils-common riscv64 2.47-2 [2685 kB] Get:11 http://deb.debian.org/debian unstable/main riscv64 binutils-riscv64-linux-gnu riscv64 2.47-2 [907 kB] Get:12 http://deb.debian.org/debian unstable/main riscv64 libbinutils riscv64 2.47-2 [509 kB] Get:13 http://deb.debian.org/debian unstable/main riscv64 libctf-nobfd0 riscv64 2.47-2 [163 kB] Get:14 http://deb.debian.org/debian unstable/main riscv64 libctf0 riscv64 2.47-2 [95.7 kB] Get:15 http://deb.debian.org/debian unstable/main riscv64 libgprofng0 riscv64 2.47-2 [722 kB] Get:16 http://deb.debian.org/debian unstable/main riscv64 build-essential riscv64 12.12 [4628 B] Get:17 http://deb.debian.org/debian unstable/main riscv64 bzip2 riscv64 1.0.8-6+b2 [40.2 kB] Get:18 http://deb.debian.org/debian unstable/main riscv64 libbz2-1.0 riscv64 1.0.8-6+b2 [39.6 kB] Get:19 http://deb.debian.org/debian unstable/main riscv64 libdebconfclient0 riscv64 0.283 [7424 B] Get:20 http://deb.debian.org/debian unstable/main riscv64 coq riscv64 9.2.0+dfsg-4 [42.5 MB] Get:21 http://deb.debian.org/debian unstable/main riscv64 libcoq-core riscv64 9.2.0+dfsg-4 [1152 kB] Get:22 http://deb.debian.org/debian unstable/main riscv64 libcoq-core-ocaml riscv64 9.2.0+dfsg-4 [26.0 MB] Get:23 http://deb.debian.org/debian unstable/main riscv64 libcoq-core-ocaml-dev riscv64 9.2.0+dfsg-4 [60.9 MB] Get:24 http://deb.debian.org/debian unstable/main riscv64 coreutils riscv64 9.10-1 [3128 kB] Get:25 http://deb.debian.org/debian unstable/main riscv64 dash riscv64 0.5.12-12 [101 kB] Get:26 http://deb.debian.org/debian unstable/main riscv64 libdb5.3t64 riscv64 5.3.28+dfsg2-11+b1 [719 kB] Get:27 http://deb.debian.org/debian unstable/main riscv64 debconf all 1.5.92 [123 kB] Get:28 http://deb.debian.org/debian unstable/main riscv64 debhelper all 14.3 [934 kB] Get:29 http://deb.debian.org/debian unstable/main riscv64 libdebhelper-perl all 14.3 [77.3 kB] Get:30 http://deb.debian.org/debian unstable/main riscv64 dh-coq all 0.17 [6960 B] Get:31 http://deb.debian.org/debian unstable/main riscv64 dh-ocaml all 3.8 [201 kB] Get:32 http://deb.debian.org/debian unstable/main riscv64 diffutils riscv64 1:3.12-1 [405 kB] Get:33 http://deb.debian.org/debian unstable/main riscv64 dpkg riscv64 1.23.7 [1534 kB] Get:34 http://deb.debian.org/debian unstable/main riscv64 dpkg-dev all 1.23.7 [1318 kB] Get:35 http://deb.debian.org/debian unstable/main riscv64 libdpkg-perl all 1.23.7 [669 kB] Get:36 http://deb.debian.org/debian unstable/main riscv64 dwz riscv64 0.17-1 [115 kB] Get:37 http://deb.debian.org/debian unstable/main riscv64 file riscv64 1:5.47-4 [42.8 kB] Get:38 http://deb.debian.org/debian unstable/main riscv64 libfindlib-ocaml riscv64 1.9.8-1+b3 [198 kB] Get:39 http://deb.debian.org/debian unstable/main riscv64 libfindlib-ocaml-dev riscv64 1.9.8-1+b3 [225 kB] Get:40 http://deb.debian.org/debian unstable/main riscv64 findutils riscv64 4.11.0-2 [785 kB] Get:41 http://deb.debian.org/debian unstable/main riscv64 cpp riscv64 4:16.1.0-3 [1568 B] Get:42 http://deb.debian.org/debian unstable/main riscv64 cpp-riscv64-linux-gnu riscv64 4:16.1.0-3 [4464 B] Get:43 http://deb.debian.org/debian unstable/main riscv64 g++ riscv64 4:16.1.0-3 [1324 B] Get:44 http://deb.debian.org/debian unstable/main riscv64 g++-riscv64-linux-gnu riscv64 4:16.1.0-3 [1196 B] Get:45 http://deb.debian.org/debian unstable/main riscv64 gcc riscv64 4:16.1.0-3 [5144 B] Get:46 http://deb.debian.org/debian unstable/main riscv64 gcc-riscv64-linux-gnu riscv64 4:16.1.0-3 [1432 B] Get:47 http://deb.debian.org/debian unstable/main riscv64 libgdbm-compat4t64 riscv64 1.26-1+b2 [52.1 kB] Get:48 http://deb.debian.org/debian unstable/main riscv64 libgdbm6t64 riscv64 1.26-1+b2 [78.1 kB] Get:49 http://deb.debian.org/debian unstable/main riscv64 autopoint all 1.0-3 [820 kB] Get:50 http://deb.debian.org/debian unstable/main riscv64 gettext riscv64 1.0-3 [2657 kB] Get:51 http://deb.debian.org/debian unstable/main riscv64 gettext-base riscv64 1.0-3 [331 kB] Get:52 http://deb.debian.org/debian unstable/main riscv64 libgmp-dev riscv64 2:6.3.0+dfsg-5+b2 [1101 kB] Get:53 http://deb.debian.org/debian unstable/main riscv64 libgmp10 riscv64 2:6.3.0+dfsg-5+b2 [561 kB] Get:54 http://deb.debian.org/debian unstable/main riscv64 libgmp3-dev riscv64 2:6.3.0+dfsg-5+b2 [321 kB] Get:55 http://deb.debian.org/debian unstable/main riscv64 libgmpxx4ldbl riscv64 2:6.3.0+dfsg-5+b2 [328 kB] Get:56 http://deb.debian.org/debian unstable/main riscv64 grep riscv64 3.12-1 [442 kB] Get:57 http://deb.debian.org/debian unstable/main riscv64 groff-base riscv64 1.24.1-1 [1311 kB] Get:58 http://deb.debian.org/debian unstable/main riscv64 gzip riscv64 1.14-1 [144 kB] Get:59 http://deb.debian.org/debian unstable/main riscv64 hostname riscv64 3.25 [10.7 kB] Get:60 http://deb.debian.org/debian unstable/main riscv64 init-system-helpers all 1.69+nmu1 [37.1 kB] Get:61 http://deb.debian.org/debian unstable/main riscv64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get:62 http://deb.debian.org/debian unstable/main riscv64 libisl23 riscv64 0.28-1 [666 kB] Get:63 http://deb.debian.org/debian unstable/main riscv64 libjansson4 riscv64 2.15.1-1 [65.1 kB] Get:64 http://deb.debian.org/debian unstable/main riscv64 libarchive-zip-perl all 1.68-1 [104 kB] Get:65 http://deb.debian.org/debian unstable/main riscv64 libconfig-tiny-perl all 2.30-1 [18.9 kB] Get:66 http://deb.debian.org/debian unstable/main riscv64 libffi8 riscv64 3.8.0-2 [26.7 kB] Get:67 http://deb.debian.org/debian unstable/main riscv64 libjson-perl all 4.10000-1 [87.5 kB] Get:68 http://deb.debian.org/debian unstable/main riscv64 libcrypt1 riscv64 1:4.5.2+20251210-1 [113 kB] Get:69 http://deb.debian.org/debian unstable/main riscv64 libcompiler-libs-ocaml-dev riscv64 5.4.1-1 [42.0 MB] Get:70 http://deb.debian.org/debian unstable/main riscv64 libcoq-stdlib riscv64 9.2.0-1+b1 [20.1 MB] Get:71 http://deb.debian.org/debian unstable/main riscv64 dh-strip-nondeterminism all 1.15.1-1 [6020 B] Get:72 http://deb.debian.org/debian unstable/main riscv64 libfile-stripnondeterminism-perl all 1.15.1-1 [17.1 kB] Get:73 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libaudit1 riscv64 1:4.1.2-1+b1 [58.7 kB] Get:74 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 bash riscv64 5.3-3+b1 [1560 kB] Get:75 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 debianutils riscv64 5.23.2 [91.7 kB] Get:76 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 dh-autoreconf all 22 [12.2 kB] Get:77 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libelf1t64 riscv64 0.195-1 [62.5 kB] Get:78 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libexpat1 riscv64 2.8.3-1 [121 kB] Get:79 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 cpp-16 riscv64 16.2.0-1 [1272 B] Get:80 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 cpp-16-riscv64-linux-gnu riscv64 16.2.0-1 [113 MB] Get:81 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 g++-16 riscv64 16.2.0-1 [33.9 kB] Get:82 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 g++-16-riscv64-linux-gnu riscv64 16.2.0-1 [120 MB] Get:83 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 gcc-16 riscv64 16.2.0-1 [520 kB] Get:84 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 gcc-16-base riscv64 16.2.0-1 [38.0 kB] Get:85 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 gcc-16-riscv64-linux-gnu riscv64 16.2.0-1 [126 MB] Get:86 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libasan8 riscv64 16.2.0-1 [2992 kB] Get:87 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libatomic1 riscv64 16.2.0-1 [8520 B] Get:88 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libcc1-0 riscv64 16.2.0-1 [41.7 kB] Get:89 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libgcc-16-dev riscv64 16.2.0-1 [5863 kB] Get:90 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libgcc-s1 riscv64 16.2.0-1 [74.3 kB] Get:91 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libgomp1 riscv64 16.2.0-1 [137 kB] Get:92 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libitm1 riscv64 16.2.0-1 [25.6 kB] Get:93 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libc-bin riscv64 2.43-3 [585 kB] Get:94 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libc-dev-bin riscv64 2.43-3 [37.6 kB] Get:95 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libc-gconv-modules-extra riscv64 2.43-3 [1099 kB] Get:96 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libc6 riscv64 2.43-3 [1465 kB] Get:97 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libc6-dev riscv64 2.43-3 [3502 kB] Get:98 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libcap-ng0 riscv64 0.9.3-1+b1 [17.8 kB] Get:99 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 bsdextrautils riscv64 2.42.2-3 [103 kB] Get:100 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libblkid1 riscv64 2.42.2-3 [193 kB] Fetched 598 MB in 33s (18.0 MB/s) dpkg-name: info: moved 'gcc_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/gcc_16.1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libdebhelper-perl_14.3_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgcc-16-dev_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libasan8_16.2.0-1_riscv64.deb' dpkg-name: info: moved 'libcrypt1_1%3a4.5.2+20251210-1_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcrypt1_4.5.2+20251210-1_riscv64.deb' dpkg-name: info: moved 'diffutils_1%3a3.12-1_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/diffutils_3.12-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgomp1_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libc-bin_2.43-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gcc-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/base-passwd_3.6.8_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libc-gconv-modules-extra_2.43-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libffi8_3.8.0-2_riscv64.deb' dpkg-name: info: moved 'g++_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/g++_16.1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gettext-base_1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/binutils-riscv64-linux-gnu_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgdbm6t64_1.26-1+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcoq-core-ocaml-dev_9.2.0+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgcc-s1_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dh-strip-nondeterminism_1.15.1-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libexpat1_2.8.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libc-dev-bin_2.43-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/cpp-16_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libjansson4_2.15.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libc6-dev_2.43-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gcc-16-base_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/hostname_3.25_riscv64.deb' dpkg-name: info: moved 'gcc-riscv64-linux-gnu_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/gcc-riscv64-linux-gnu_16.1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dwz_0.17-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libconfig-tiny-perl_2.30-1_all.deb' dpkg-name: info: moved 'file_1%3a5.47-4_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/file_5.47-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libdb5.3t64_5.3.28+dfsg2-11+b1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libctf-nobfd0_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/g++-16_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libblkid1_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/autoconf_2.73-2_all.deb' dpkg-name: info: moved 'cpp_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/cpp_16.1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/bzip2_1.0.8-6+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/findutils_4.11.0-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcap-ng0_0.9.3-1+b1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcoq-core-ocaml_9.2.0+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/binutils-common_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgprofng0_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gzip_1.14-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libdpkg-perl_1.23.7_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/bash_5.3-3+b1_riscv64.deb' dpkg-name: info: moved 'libgmp3-dev_2%3a6.3.0+dfsg-5+b2_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgmp3-dev_6.3.0+dfsg-5+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dh-ocaml_3.8_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libarchive-zip-perl_1.68-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/init-system-helpers_1.69+nmu1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libfindlib-ocaml-dev_1.9.8-1+b3_riscv64.deb' dpkg-name: info: moved 'libgmp-dev_2%3a6.3.0+dfsg-5+b2_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgmp-dev_6.3.0+dfsg-5+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dh-coq_0.17_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/groff-base_1.24.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libitm1_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcoq-core_9.2.0+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dash_0.5.12-12_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcompiler-libs-ocaml-dev_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libelf1t64_0.195-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/g++-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libjson-perl_4.10000-1_all.deb' dpkg-name: info: moved 'automake_1%3a1.18.1-4_all.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/automake_1.18.1-4_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/debconf_1.5.92_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libfile-stripnondeterminism-perl_1.15.1-1_all.deb' dpkg-name: info: moved 'libaudit1_1%3a4.1.2-1+b1_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libaudit1_4.1.2-1+b1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libbz2-1.0_1.0.8-6+b2_riscv64.deb' dpkg-name: info: moved 'libattr1_1%3a2.6.0-1_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libattr1_2.6.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/intltool-debian_0.35.0+20060710.6_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/coq_9.2.0+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gettext_1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dh-autoreconf_22_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/grep_3.12-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dpkg_1.23.7_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/bsdextrautils_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/dpkg-dev_1.23.7_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/cpp-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/coreutils_9.10-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libbinutils_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcoq-stdlib_9.2.0-1+b1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/gcc-16_16.2.0-1_riscv64.deb' dpkg-name: info: moved 'g++-riscv64-linux-gnu_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/g++-riscv64-linux-gnu_16.1.0-3_riscv64.deb' dpkg-name: info: moved 'libgmp10_2%3a6.3.0+dfsg-5+b2_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgmp10_6.3.0+dfsg-5+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgdbm-compat4t64_1.26-1+b2_riscv64.deb' dpkg-name: info: moved 'libgmpxx4ldbl_2%3a6.3.0+dfsg-5+b2_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libgmpxx4ldbl_6.3.0+dfsg-5+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/debianutils_5.23.2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libctf0_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libcc1-0_16.2.0-1_riscv64.deb' dpkg-name: info: moved 'libaudit-common_1%3a4.1.2-1_all.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/libaudit-common_4.1.2-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/autopoint_1.0-3_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/base-files_14.2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/binutils_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/debhelper_14.3_all.deb' dpkg-name: info: moved 'cpp-riscv64-linux-gnu_4%3a16.1.0-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmp4_u8uw5n/cpp-riscv64-linux-gnu_16.1.0-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libfindlib-ocaml_1.9.8-1+b3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/autotools-dev_20240727.1+nmu1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libatomic1_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/build-essential_12.12_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libc6_2.43-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libisl23_0.28-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libacl1_2.4.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmp4_u8uw5n/libdebconfclient0_0.283_riscv64.deb' Get:1 http://deb.debian.org/debian unstable/main riscv64 libsframe3 riscv64 2.47-2 [86.0 kB] Get:2 http://deb.debian.org/debian unstable/main riscv64 libmagic-mgc riscv64 1:5.47-4 [345 kB] Get:3 http://deb.debian.org/debian unstable/main riscv64 libmagic1t64 riscv64 1:5.47-4 [117 kB] Get:4 http://deb.debian.org/debian unstable/main riscv64 ocaml-findlib riscv64 1.9.8-1+b3 [621 kB] Get:5 http://deb.debian.org/debian unstable/main riscv64 libmd0 riscv64 1.2.0-2 [44.0 kB] Get:6 http://deb.debian.org/debian unstable/main riscv64 libpipeline1 riscv64 1.5.8-3 [48.2 kB] Get:7 http://deb.debian.org/debian unstable/main riscv64 libselinux1 riscv64 3.11-2 [90.4 kB] Get:8 http://deb.debian.org/debian unstable/main riscv64 libunistring5 riscv64 1.4.2-1 [475 kB] Get:9 http://deb.debian.org/debian unstable/main riscv64 libzstd-dev riscv64 1.5.7+dfsg-4 [1626 kB] Get:10 http://deb.debian.org/debian unstable/main riscv64 libzstd1 riscv64 1.5.7+dfsg-4 [368 kB] Get:11 http://deb.debian.org/debian unstable/main riscv64 m4 riscv64 1.4.21-1 [330 kB] Get:12 http://deb.debian.org/debian unstable/main riscv64 make riscv64 4.4.1-3 [463 kB] Get:13 http://deb.debian.org/debian unstable/main riscv64 man-db riscv64 2.13.1-1 [1458 kB] Get:14 http://deb.debian.org/debian unstable/main riscv64 mawk riscv64 1.3.4.20260302-1 [142 kB] Get:15 http://deb.debian.org/debian unstable/main riscv64 media-types all 14.0.0 [30.8 kB] Get:16 http://deb.debian.org/debian unstable/main riscv64 libmpc3 riscv64 1.3.1-3 [56.5 kB] Get:17 http://deb.debian.org/debian unstable/main riscv64 libmpfr6 riscv64 4.2.2-3 [666 kB] Get:18 http://deb.debian.org/debian unstable/main riscv64 libncurses-dev riscv64 6.6+20260608-2 [934 kB] Get:19 http://deb.debian.org/debian unstable/main riscv64 libncurses6 riscv64 6.6+20260608-2 [105 kB] Get:20 http://deb.debian.org/debian unstable/main riscv64 libncursesw6 riscv64 6.6+20260608-2 [141 kB] Get:21 http://deb.debian.org/debian unstable/main riscv64 libtinfo6 riscv64 6.6+20260608-2 [351 kB] Get:22 http://deb.debian.org/debian unstable/main riscv64 ncurses-base all 6.6+20260608-2 [276 kB] Get:23 http://deb.debian.org/debian unstable/main riscv64 ncurses-bin riscv64 6.6+20260608-2 [442 kB] Get:24 http://deb.debian.org/debian unstable/main riscv64 netbase all 6.6 [10.3 kB] Get:25 http://deb.debian.org/debian unstable/main riscv64 libstdlib-ocaml riscv64 5.4.1-1 [608 kB] Get:26 http://deb.debian.org/debian unstable/main riscv64 libstdlib-ocaml-dev riscv64 5.4.1-1 [9944 kB] Get:27 http://deb.debian.org/debian unstable/main riscv64 ocaml riscv64 5.4.1-1 [19.5 MB] Get:28 http://deb.debian.org/debian unstable/main riscv64 ocaml-base riscv64 5.4.1-1 [521 kB] Get:29 http://deb.debian.org/debian unstable/main riscv64 ocaml-interp riscv64 5.4.1-1 [7459 kB] Get:30 http://deb.debian.org/debian unstable/main riscv64 libzarith-ocaml riscv64 1.14-4 [113 kB] Get:31 http://deb.debian.org/debian unstable/main riscv64 libzarith-ocaml-dev riscv64 1.14-4 [166 kB] Get:32 http://deb.debian.org/debian unstable/main riscv64 libpam-modules riscv64 1.7.0-8 [165 kB] Get:33 http://deb.debian.org/debian unstable/main riscv64 libpam-modules-bin riscv64 1.7.0-8 [46.2 kB] Get:34 http://deb.debian.org/debian unstable/main riscv64 libpam-runtime all 1.7.0-8 [246 kB] Get:35 http://deb.debian.org/debian unstable/main riscv64 libpam0g riscv64 1.7.0-8 [66.9 kB] Get:36 http://deb.debian.org/debian unstable/main riscv64 patch riscv64 2.8-2 [134 kB] Get:37 http://deb.debian.org/debian unstable/main riscv64 libperl5.42 riscv64 5.42.3-1 [3853 kB] Get:38 http://deb.debian.org/debian unstable/main riscv64 perl riscv64 5.42.3-1 [266 kB] Get:39 http://deb.debian.org/debian unstable/main riscv64 perl-base riscv64 5.42.3-1 [1846 kB] Get:40 http://deb.debian.org/debian unstable/main riscv64 perl-modules-5.42 all 5.42.3-1 [3213 kB] Get:41 http://deb.debian.org/debian unstable/main riscv64 po-debconf all 1.0.22 [216 kB] Get:42 http://deb.debian.org/debian unstable/main riscv64 quickjs riscv64 2025.04.26-1+b2 [459 kB] Get:43 http://deb.debian.org/debian unstable/main riscv64 libreadline8t64 riscv64 8.3-4 [180 kB] Get:44 http://deb.debian.org/debian unstable/main riscv64 readline-common all 8.3-4 [74.8 kB] Get:45 http://deb.debian.org/debian unstable/main riscv64 sed riscv64 4.9-3 [329 kB] Get:46 http://deb.debian.org/debian unstable/main riscv64 sensible-utils all 0.0.26 [27.0 kB] Get:47 http://deb.debian.org/debian unstable/main riscv64 libsqlite3-0 riscv64 3.53.4-2 [957 kB] Get:48 http://deb.debian.org/debian unstable/main riscv64 sysvinit-utils riscv64 3.18-1 [29.3 kB] Get:49 http://deb.debian.org/debian unstable/main riscv64 tar riscv64 1.35+dfsg-5 [821 kB] Get:50 http://deb.debian.org/debian unstable/main riscv64 tzdata all 2026c-1 [260 kB] Get:51 http://deb.debian.org/debian unstable/main riscv64 libuchardet0 riscv64 0.0.8-2+b2 [68.8 kB] Get:52 http://deb.debian.org/debian unstable/main riscv64 liblzma5 riscv64 5.8.3-1 [334 kB] Get:53 http://deb.debian.org/debian unstable/main riscv64 xz-utils riscv64 5.8.3-1 [739 kB] Get:54 http://deb.debian.org/debian unstable/main riscv64 zlib1g riscv64 1:1.3.dfsg+really1.3.2-3 [87.3 kB] Get:55 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 liblsan0 riscv64 16.2.0-1 [1342 kB] Get:56 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libstdc++-16-dev riscv64 16.2.0-1 [10.5 MB] Get:57 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libstdc++6 riscv64 16.2.0-1 [775 kB] Get:58 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libtsan2 riscv64 16.2.0-1 [2706 kB] Get:59 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libubsan1 riscv64 16.2.0-1 [1191 kB] Get:60 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libtool all 2.5.4-11 [539 kB] Get:61 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libxml2-16 riscv64 2.15.3+dfsg-1 [640 kB] Get:62 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 linux-libc-dev all 7.1.9-1 [2055 kB] Get:63 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libssl3t64 riscv64 3.6.3-1 [2255 kB] Get:64 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 openssl-provider-legacy riscv64 3.6.3-1 [322 kB] Get:65 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libpcre2-8-0 riscv64 10.46-1+b2 [296 kB] Get:66 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libpython3-stdlib riscv64 3.14.6-1 [8108 B] Get:67 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 python3 riscv64 3.14.6-1 [25.1 kB] Get:68 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 python3-minimal riscv64 3.14.6-1 [25.1 kB] Get:69 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libpython3.14-minimal riscv64 3.14.7-1 [893 kB] Get:70 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libpython3.14-stdlib riscv64 3.14.7-1 [2320 kB] Get:71 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 python3.14 riscv64 3.14.7-1 [861 kB] Get:72 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 python3.14-minimal riscv64 3.14.7-1 [2293 kB] Get:73 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libsystemd0 riscv64 261.2-1 [478 kB] Get:74 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libudev1 riscv64 261.2-1 [141 kB] Get:75 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libmount1 riscv64 2.42.2-3 [228 kB] Get:76 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libsmartcols1 riscv64 2.42.2-3 [154 kB] Get:77 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 libuuid1 riscv64 2.42.2-3 [35.1 kB] Get:78 http://snapshot.debian.org/archive/debian/20260825T024408Z unstable/main riscv64 util-linux riscv64 2.42.2-3 [1221 kB] Fetched 93.3 MB in 5s (17.1 MB/s) dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libzstd1_1.5.7+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libsqlite3-0_3.53.4-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpipeline1_1.5.8-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/util-linux_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/liblzma5_5.8.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libperl5.42_5.42.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpcre2-8-0_10.46-1+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/sysvinit-utils_3.18-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/netbase_6.6_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpython3-stdlib_3.14.6-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/sed_4.9-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libuchardet0_0.0.8-2+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpam-modules_1.7.0-8_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ncurses-base_6.6+20260608-2_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libtinfo6_6.6+20260608-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libxml2-16_2.15.3+dfsg-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libncurses-dev_6.6+20260608-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libzstd-dev_1.5.7+dfsg-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ocaml-base_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libreadline8t64_8.3-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/readline-common_8.3-4_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/python3.14_3.14.7-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libubsan1_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ncurses-bin_6.6+20260608-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libtsan2_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libsystemd0_261.2-1_riscv64.deb' dpkg-name: info: moved 'libmagic-mgc_1%3a5.47-4_riscv64.deb' to '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmagic-mgc_5.47-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ocaml_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/xz-utils_5.8.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/m4_1.4.21-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/sensible-utils_0.0.26_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/python3_3.14.6-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ocaml-interp_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmd0_1.2.0-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libstdc++-16-dev_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmpc3_1.3.1-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/tar_1.35+dfsg-5_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libssl3t64_3.6.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libncursesw6_6.6+20260608-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libstdlib-ocaml_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/perl-modules-5.42_5.42.3-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/po-debconf_1.0.22_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpam0g_1.7.0-8_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpam-runtime_1.7.0-8_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmpfr6_4.2.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/man-db_2.13.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpython3.14-minimal_3.14.7-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/python3.14-minimal_3.14.7-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libstdc++6_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/linux-libc-dev_7.1.9-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/quickjs_2025.04.26-1+b2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libsmartcols1_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libsframe3_2.47-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/media-types_14.0.0_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libunistring5_1.4.2-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libncurses6_6.6+20260608-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libzarith-ocaml-dev_1.14-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libstdlib-ocaml-dev_5.4.1-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/tzdata_2026c-1_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/perl-base_5.42.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libuuid1_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/make_4.4.1-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpython3.14-stdlib_3.14.7-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/patch_2.8-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libudev1_261.2-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/perl_5.42.3-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libselinux1_3.11-2_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/ocaml-findlib_1.9.8-1+b3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libzarith-ocaml_1.14-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/python3-minimal_3.14.6-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/openssl-provider-legacy_3.6.3-1_riscv64.deb' dpkg-name: info: moved 'zlib1g_1%3a1.3.dfsg+really1.3.2-3_riscv64.deb' to '/srv/rebuilderd/tmp/tmpp8c2t8u9/zlib1g_1.3.dfsg+really1.3.2-3_riscv64.deb' dpkg-name: info: moved 'libmagic1t64_1%3a5.47-4_riscv64.deb' to '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmagic1t64_5.47-4_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/mawk_1.3.4.20260302-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libtool_2.5.4-11_all.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libmount1_2.42.2-3_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/liblsan0_16.2.0-1_riscv64.deb' dpkg-name: warning: skipping '/srv/rebuilderd/tmp/tmpp8c2t8u9/libpam-modules-bin_1.7.0-8_riscv64.deb' dpkg-buildpackage: info: source package debootsnap-dummy dpkg-buildpackage: info: source version 1.0 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Equivs Dummy Package Generator dpkg-buildpackage: info: host architecture riscv64 dpkg-source --before-build . debian/rules clean dh clean dh_clean debian/rules binary dh binary dh_update_autotools_config dh_autoreconf create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install --destdir=debian/debootsnap-dummy/ dh_install dh_installdocs dh_installchangelogs dh_perl dh_link dh_strip_nondeterminism dh_compress dh_fixperms dh_missing dh_installdeb dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'debootsnap-dummy' in '../debootsnap-dummy_1.0_all.deb'. dpkg-genbuildinfo --build=binary -O../debootsnap-dummy_1.0_riscv64.buildinfo dpkg-genchanges --build=binary -O../debootsnap-dummy_1.0_riscv64.changes dpkg-genchanges: info: binary-only upload (no source code included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) The package has been created. Attention, the package has been created in the /srv/rebuilderd/tmp/tmp_uo9w4nu/cache directory, not in ".." as indicated by the message above! I: automatically chosen mode: unshare I: chroot architecture riscv64 is equal to the host's architecture I: using /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL as tempdir I: running --setup-hook directly: /usr/share/mmdebstrap/hooks/maybe-merged-usr/setup00.sh /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL 127.0.0.1 - - [10/Sep/2026 03:48:56] code 404, message File not found 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./InRelease HTTP/1.1" 404 - Ign:1 http://localhost:39411 ./ InRelease 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./Release HTTP/1.1" 200 - Get:2 http://localhost:39411 ./ Release [462 B] 127.0.0.1 - - [10/Sep/2026 03:48:56] code 404, message File not found 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./Release.gpg HTTP/1.1" 404 - Ign:3 http://localhost:39411 ./ Release.gpg 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./Packages HTTP/1.1" 200 - Get:4 http://localhost:39411 ./ Packages [217 kB] Fetched 218 kB in 0s (1783 kB/s) Reading package lists... usr-is-merged found but not real -- not running merged-usr setup hook I: skipping apt-get update because it was already run I: downloading packages with apt... 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./gcc-16-base_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:56] "GET /./libc-gconv-modules-extra_2.43-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libc6_2.43-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libgcc-s1_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./mawk_1.3.4.20260302-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./base-files_14.2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libtinfo6_6.6%2b20260608-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./debianutils_5.23.2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./bash_5.3-3%2bb1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libacl1_2.4.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libattr1_2.6.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libgmp10_6.3.0%2bdfsg-5%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libpcre2-8-0_10.46-1%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libselinux1_3.11-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libzstd1_1.5.7%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./zlib1g_1.3.dfsg%2breally1.3.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libssl3t64_3.6.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./openssl-provider-legacy_3.6.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./libsystemd0_261.2-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:57] "GET /./coreutils_9.10-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./dash_0.5.12-12_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./diffutils_3.12-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libbz2-1.0_1.0.8-6%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./liblzma5_5.8.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libmd0_1.2.0-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./tar_1.35%2bdfsg-5_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./dpkg_1.23.7_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./findutils_4.11.0-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./grep_3.12-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./gzip_1.14-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./hostname_3.25_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./ncurses-bin_6.6%2b20260608-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libcrypt1_4.5.2%2b20251210-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./perl-base_5.42.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./sed_4.9-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libaudit-common_4.1.2-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libcap-ng0_0.9.3-1%2bb1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libaudit1_4.1.2-1%2bb1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libdb5.3t64_5.3.28%2bdfsg2-11%2bb1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./debconf_1.5.92_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libpam0g_1.7.0-8_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libpam-modules-bin_1.7.0-8_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libpam-modules_1.7.0-8_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libpam-runtime_1.7.0-8_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libblkid1_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:58] "GET /./libmount1_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./libsmartcols1_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./libudev1_261.2-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./libuuid1_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./util-linux_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./libdebconfclient0_0.283_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./base-passwd_3.6.8_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./init-system-helpers_1.69%2bnmu1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./libc-bin_2.43-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./ncurses-base_6.6%2b20260608-2_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:48:59] "GET /./sysvinit-utils_3.18-1_riscv64.deb HTTP/1.1" 200 - I: extracting archives... I: running --extract-hook directly: /usr/share/mmdebstrap/hooks/maybe-merged-usr/extract00.sh /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL 127.0.0.1 - - [10/Sep/2026 03:49:07] code 404, message File not found 127.0.0.1 - - [10/Sep/2026 03:49:07] "GET /./InRelease HTTP/1.1" 404 - Ign:1 http://localhost:39411 ./ InRelease 127.0.0.1 - - [10/Sep/2026 03:49:07] "GET /./Release HTTP/1.1" 304 - Hit:2 http://localhost:39411 ./ Release 127.0.0.1 - - [10/Sep/2026 03:49:07] code 404, message File not found 127.0.0.1 - - [10/Sep/2026 03:49:07] "GET /./Release.gpg HTTP/1.1" 404 - Ign:3 http://localhost:39411 ./ Release.gpg Reading package lists... usr-is-merged found but not real -- not running merged-usr extract hook I: installing essential packages... I: running --essential-hook directly: /usr/share/mmdebstrap/hooks/maybe-merged-usr/essential00.sh /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL usr-is-merged was not installed in a previous hook -- not running merged-usr essential hook I: installing remaining packages inside the chroot... 127.0.0.1 - - [10/Sep/2026 03:49:28] "GET /./libexpat1_2.8.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libpython3.14-minimal_3.14.7-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./python3.14-minimal_3.14.7-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./python3-minimal_3.14.6-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./media-types_14.0.0_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./netbase_6.6_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./tzdata_2026c-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libffi8_3.8.0-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libncursesw6_6.6%2b20260608-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./readline-common_8.3-4_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libreadline8t64_8.3-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libsqlite3-0_3.53.4-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libpython3.14-stdlib_3.14.7-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./python3.14_3.14.7-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libpython3-stdlib_3.14.6-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./python3_3.14.6-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./sensible-utils_0.0.26_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libstdc%2b%2b6_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libuchardet0_0.0.8-2%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./groff-base_1.24.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./bsdextrautils_2.42.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libgdbm6t64_1.26-1%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:29] "GET /./libpipeline1_1.5.8-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./man-db_2.13.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./bzip2_1.0.8-6%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./libmagic-mgc_5.47-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./libmagic1t64_5.47-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./file_5.47-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./gettext-base_1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./perl-modules-5.42_5.42.3-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./libgdbm-compat4t64_1.26-1%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./libperl5.42_5.42.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./perl_5.42.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./xz-utils_5.8.3-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./m4_1.4.21-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:30] "GET /./autoconf_2.73-2_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./autotools-dev_20240727.1%2bnmu1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./automake_1.18.1-4_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./autopoint_1.0-3_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libsframe3_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./binutils-common_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libbinutils_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libgprofng0_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libctf-nobfd0_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libctf0_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libjansson4_2.15.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./binutils-riscv64-linux-gnu_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./binutils_2.47-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libc-dev-bin_2.43-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./linux-libc-dev_7.1.9-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:31] "GET /./libc6-dev_2.43-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:32] "GET /./libisl23_0.28-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:32] "GET /./libmpfr6_4.2.2-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:32] "GET /./libmpc3_1.3.1-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:32] "GET /./cpp-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:41] "GET /./cpp-16_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:41] "GET /./cpp-riscv64-linux-gnu_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:41] "GET /./cpp_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:41] "GET /./libcc1-0_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:41] "GET /./libgomp1_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libitm1_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libatomic1_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libasan8_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./liblsan0_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libtsan2_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libubsan1_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:42] "GET /./libgcc-16-dev_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:43] "GET /./gcc-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:54] "GET /./gcc-16_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:54] "GET /./gcc-riscv64-linux-gnu_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:54] "GET /./gcc_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:54] "GET /./libstdc%2b%2b-16-dev_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:49:55] "GET /./g%2b%2b-16-riscv64-linux-gnu_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./g%2b%2b-16_16.2.0-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./g%2b%2b-riscv64-linux-gnu_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./g%2b%2b_16.1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./make_4.4.1-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libdpkg-perl_1.23.7_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./patch_2.8-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./dpkg-dev_1.23.7_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./build-essential_12.12_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libcoq-core_9.2.0%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libstdlib-ocaml_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./ocaml-base_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libfindlib-ocaml_1.9.8-1%2bb3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libzarith-ocaml_1.14-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:05] "GET /./libcoq-core-ocaml_9.2.0%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:08] "GET /./libstdlib-ocaml-dev_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:08] "GET /./libcompiler-libs-ocaml-dev_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:12] "GET /./ocaml-interp_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:13] "GET /./libncurses6_6.6%2b20260608-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:13] "GET /./libncurses-dev_6.6%2b20260608-2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:13] "GET /./libzstd-dev_1.5.7%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:13] "GET /./ocaml_5.4.1-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:14] "GET /./ocaml-findlib_1.9.8-1%2bb3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:15] "GET /./coq_9.2.0%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libdebhelper-perl_14.3_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libtool_2.5.4-11_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./dh-autoreconf_22_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libarchive-zip-perl_1.68-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libfile-stripnondeterminism-perl_1.15.1-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./dh-strip-nondeterminism_1.15.1-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libelf1t64_0.195-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./dwz_0.17-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libunistring5_1.4.2-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./libxml2-16_2.15.3%2bdfsg-1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:18] "GET /./gettext_1.0-3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./intltool-debian_0.35.0%2b20060710.6_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./po-debconf_1.0.22_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./debhelper_14.3_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libfindlib-ocaml-dev_1.9.8-1%2bb3_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libgmpxx4ldbl_6.3.0%2bdfsg-5%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libgmp-dev_6.3.0%2bdfsg-5%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libgmp3-dev_6.3.0%2bdfsg-5%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libzarith-ocaml-dev_1.14-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:19] "GET /./libcoq-core-ocaml-dev_9.2.0%2bdfsg-4_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./dh-coq_0.17_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./libconfig-tiny-perl_2.30-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./libjson-perl_4.10000-1_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./quickjs_2025.04.26-1%2bb2_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./dh-ocaml_3.8_all.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:24] "GET /./libcoq-stdlib_9.2.0-1%2bb1_riscv64.deb HTTP/1.1" 200 - 127.0.0.1 - - [10/Sep/2026 03:50:26] "GET /./debootsnap-dummy_1.0_all.deb HTTP/1.1" 200 - I: running --customize-hook directly: /srv/rebuilderd/tmp/tmp_uo9w4nu/apt_install.sh /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL Reading package lists... Building dependency tree... Reading state information... libdebhelper-perl is already the newest version (14.3). libdebhelper-perl set to manually installed. libgcc-16-dev is already the newest version (16.2.0-1). libgcc-16-dev set to manually installed. libasan8 is already the newest version (16.2.0-1). libasan8 set to manually installed. gcc-riscv64-linux-gnu is already the newest version (4:16.1.0-3). gcc-riscv64-linux-gnu set to manually installed. libgomp1 is already the newest version (16.2.0-1). libgomp1 set to manually installed. libc-bin is already the newest version (2.43-3). gcc-16-riscv64-linux-gnu is already the newest version (16.2.0-1). gcc-16-riscv64-linux-gnu set to manually installed. base-passwd is already the newest version (3.6.8). libc-gconv-modules-extra is already the newest version (2.43-3). cpp is already the newest version (4:16.1.0-3). cpp set to manually installed. libffi8 is already the newest version (3.8.0-2). libffi8 set to manually installed. gettext-base is already the newest version (1.0-3). gettext-base set to manually installed. binutils-riscv64-linux-gnu is already the newest version (2.47-2). binutils-riscv64-linux-gnu set to manually installed. libgdbm6t64 is already the newest version (1.26-1+b2). libgdbm6t64 set to manually installed. libcoq-core-ocaml-dev is already the newest version (9.2.0+dfsg-4). libcoq-core-ocaml-dev set to manually installed. libgcc-s1 is already the newest version (16.2.0-1). dh-strip-nondeterminism is already the newest version (1.15.1-1). dh-strip-nondeterminism set to manually installed. libexpat1 is already the newest version (2.8.3-1). libexpat1 set to manually installed. libc-dev-bin is already the newest version (2.43-3). libc-dev-bin set to manually installed. cpp-16 is already the newest version (16.2.0-1). cpp-16 set to manually installed. libjansson4 is already the newest version (2.15.1-1). libjansson4 set to manually installed. libc6-dev is already the newest version (2.43-3). libc6-dev set to manually installed. gcc-16-base is already the newest version (16.2.0-1). hostname is already the newest version (3.25). libcrypt1 is already the newest version (1:4.5.2+20251210-1). dwz is already the newest version (0.17-1). dwz set to manually installed. libconfig-tiny-perl is already the newest version (2.30-1). libconfig-tiny-perl set to manually installed. libdb5.3t64 is already the newest version (5.3.28+dfsg2-11+b1). libctf-nobfd0 is already the newest version (2.47-2). libctf-nobfd0 set to manually installed. g++-16 is already the newest version (16.2.0-1). g++-16 set to manually installed. libblkid1 is already the newest version (2.42.2-3). autoconf is already the newest version (2.73-2). autoconf set to manually installed. bzip2 is already the newest version (1.0.8-6+b2). bzip2 set to manually installed. findutils is already the newest version (4.11.0-2). libcap-ng0 is already the newest version (0.9.3-1+b1). libgmp10 is already the newest version (2:6.3.0+dfsg-5+b2). libcoq-core-ocaml is already the newest version (9.2.0+dfsg-4). libcoq-core-ocaml set to manually installed. binutils-common is already the newest version (2.47-2). binutils-common set to manually installed. libaudit1 is already the newest version (1:4.1.2-1+b1). libgprofng0 is already the newest version (2.47-2). libgprofng0 set to manually installed. gzip is already the newest version (1.14-1). libdpkg-perl is already the newest version (1.23.7). libdpkg-perl set to manually installed. bash is already the newest version (5.3-3+b1). libgmpxx4ldbl is already the newest version (2:6.3.0+dfsg-5+b2). libgmpxx4ldbl set to manually installed. dh-ocaml is already the newest version (3.8). dh-ocaml set to manually installed. libgmp3-dev is already the newest version (2:6.3.0+dfsg-5+b2). libgmp3-dev set to manually installed. libarchive-zip-perl is already the newest version (1.68-1). libarchive-zip-perl set to manually installed. init-system-helpers is already the newest version (1.69+nmu1). libfindlib-ocaml-dev is already the newest version (1.9.8-1+b3). libfindlib-ocaml-dev set to manually installed. dh-coq is already the newest version (0.17). dh-coq set to manually installed. groff-base is already the newest version (1.24.1-1). groff-base set to manually installed. file is already the newest version (1:5.47-4). file set to manually installed. libitm1 is already the newest version (16.2.0-1). libitm1 set to manually installed. libcoq-core is already the newest version (9.2.0+dfsg-4). libcoq-core set to manually installed. dash is already the newest version (0.5.12-12). libcompiler-libs-ocaml-dev is already the newest version (5.4.1-1). libcompiler-libs-ocaml-dev set to manually installed. libelf1t64 is already the newest version (0.195-1). libelf1t64 set to manually installed. g++-16-riscv64-linux-gnu is already the newest version (16.2.0-1). g++-16-riscv64-linux-gnu set to manually installed. libjson-perl is already the newest version (4.10000-1). libjson-perl set to manually installed. libattr1 is already the newest version (1:2.6.0-1). debconf is already the newest version (1.5.92). automake is already the newest version (1:1.18.1-4). automake set to manually installed. libfile-stripnondeterminism-perl is already the newest version (1.15.1-1). libfile-stripnondeterminism-perl set to manually installed. libbz2-1.0 is already the newest version (1.0.8-6+b2). intltool-debian is already the newest version (0.35.0+20060710.6). intltool-debian set to manually installed. coq is already the newest version (9.2.0+dfsg-4). coq set to manually installed. gettext is already the newest version (1.0-3). gettext set to manually installed. dh-autoreconf is already the newest version (22). dh-autoreconf set to manually installed. grep is already the newest version (3.12-1). dpkg is already the newest version (1.23.7). bsdextrautils is already the newest version (2.42.2-3). bsdextrautils set to manually installed. libaudit-common is already the newest version (1:4.1.2-1). dpkg-dev is already the newest version (1.23.7). dpkg-dev set to manually installed. cpp-16-riscv64-linux-gnu is already the newest version (16.2.0-1). cpp-16-riscv64-linux-gnu set to manually installed. gcc is already the newest version (4:16.1.0-3). gcc set to manually installed. coreutils is already the newest version (9.10-1). libbinutils is already the newest version (2.47-2). libbinutils set to manually installed. libcoq-stdlib is already the newest version (9.2.0-1+b1). libcoq-stdlib set to manually installed. g++-riscv64-linux-gnu is already the newest version (4:16.1.0-3). g++-riscv64-linux-gnu set to manually installed. gcc-16 is already the newest version (16.2.0-1). gcc-16 set to manually installed. libgdbm-compat4t64 is already the newest version (1.26-1+b2). libgdbm-compat4t64 set to manually installed. debianutils is already the newest version (5.23.2). libctf0 is already the newest version (2.47-2). libctf0 set to manually installed. libcc1-0 is already the newest version (16.2.0-1). libcc1-0 set to manually installed. autopoint is already the newest version (1.0-3). autopoint set to manually installed. diffutils is already the newest version (1:3.12-1). g++ is already the newest version (4:16.1.0-3). g++ set to manually installed. base-files is already the newest version (14.2). binutils is already the newest version (2.47-2). binutils set to manually installed. debhelper is already the newest version (14.3). debhelper set to manually installed. libfindlib-ocaml is already the newest version (1.9.8-1+b3). libfindlib-ocaml set to manually installed. autotools-dev is already the newest version (20240727.1+nmu1). autotools-dev set to manually installed. libatomic1 is already the newest version (16.2.0-1). libatomic1 set to manually installed. cpp-riscv64-linux-gnu is already the newest version (4:16.1.0-3). cpp-riscv64-linux-gnu set to manually installed. build-essential is already the newest version (12.12). build-essential set to manually installed. libc6 is already the newest version (2.43-3). libisl23 is already the newest version (0.28-1). libisl23 set to manually installed. libgmp-dev is already the newest version (2:6.3.0+dfsg-5+b2). libgmp-dev set to manually installed. libacl1 is already the newest version (2.4.0-1). libdebconfclient0 is already the newest version (0.283). libzstd1 is already the newest version (1.5.7+dfsg-4). libsqlite3-0 is already the newest version (3.53.4-2). libsqlite3-0 set to manually installed. libpipeline1 is already the newest version (1.5.8-3). libpipeline1 set to manually installed. util-linux is already the newest version (2.42.2-3). liblzma5 is already the newest version (5.8.3-1). libperl5.42 is already the newest version (5.42.3-1). libperl5.42 set to manually installed. libpcre2-8-0 is already the newest version (10.46-1+b2). sysvinit-utils is already the newest version (3.18-1). netbase is already the newest version (6.6). netbase set to manually installed. libpython3-stdlib is already the newest version (3.14.6-1). libpython3-stdlib set to manually installed. sed is already the newest version (4.9-3). libuchardet0 is already the newest version (0.0.8-2+b2). libuchardet0 set to manually installed. libpam-modules is already the newest version (1.7.0-8). ncurses-base is already the newest version (6.6+20260608-2). libtinfo6 is already the newest version (6.6+20260608-2). libxml2-16 is already the newest version (2.15.3+dfsg-1). libxml2-16 set to manually installed. libncurses-dev is already the newest version (6.6+20260608-2). libncurses-dev set to manually installed. libzstd-dev is already the newest version (1.5.7+dfsg-4). libzstd-dev set to manually installed. ocaml-base is already the newest version (5.4.1-1). ocaml-base set to manually installed. libreadline8t64 is already the newest version (8.3-4). libreadline8t64 set to manually installed. readline-common is already the newest version (8.3-4). readline-common set to manually installed. python3.14 is already the newest version (3.14.7-1). python3.14 set to manually installed. libubsan1 is already the newest version (16.2.0-1). libubsan1 set to manually installed. ncurses-bin is already the newest version (6.6+20260608-2). libtsan2 is already the newest version (16.2.0-1). libtsan2 set to manually installed. libsystemd0 is already the newest version (261.2-1). ocaml is already the newest version (5.4.1-1). ocaml set to manually installed. xz-utils is already the newest version (5.8.3-1). xz-utils set to manually installed. m4 is already the newest version (1.4.21-1). m4 set to manually installed. sensible-utils is already the newest version (0.0.26). sensible-utils set to manually installed. python3 is already the newest version (3.14.6-1). python3 set to manually installed. ocaml-interp is already the newest version (5.4.1-1). ocaml-interp set to manually installed. libmd0 is already the newest version (1.2.0-2). libstdc++-16-dev is already the newest version (16.2.0-1). libstdc++-16-dev set to manually installed. libmpc3 is already the newest version (1.3.1-3). libmpc3 set to manually installed. tar is already the newest version (1.35+dfsg-5). libssl3t64 is already the newest version (3.6.3-1). libncursesw6 is already the newest version (6.6+20260608-2). libncursesw6 set to manually installed. libstdlib-ocaml is already the newest version (5.4.1-1). libstdlib-ocaml set to manually installed. perl-modules-5.42 is already the newest version (5.42.3-1). perl-modules-5.42 set to manually installed. po-debconf is already the newest version (1.0.22). po-debconf set to manually installed. libpam0g is already the newest version (1.7.0-8). libpam-runtime is already the newest version (1.7.0-8). libmpfr6 is already the newest version (4.2.2-3). libmpfr6 set to manually installed. man-db is already the newest version (2.13.1-1). man-db set to manually installed. libpython3.14-minimal is already the newest version (3.14.7-1). libpython3.14-minimal set to manually installed. python3.14-minimal is already the newest version (3.14.7-1). python3.14-minimal set to manually installed. libstdc++6 is already the newest version (16.2.0-1). libstdc++6 set to manually installed. linux-libc-dev is already the newest version (7.1.9-1). linux-libc-dev set to manually installed. quickjs is already the newest version (2025.04.26-1+b2). quickjs set to manually installed. libmagic-mgc is already the newest version (1:5.47-4). libmagic-mgc set to manually installed. libsmartcols1 is already the newest version (2.42.2-3). libsframe3 is already the newest version (2.47-2). libsframe3 set to manually installed. media-types is already the newest version (14.0.0). media-types set to manually installed. libunistring5 is already the newest version (1.4.2-1). libunistring5 set to manually installed. libncurses6 is already the newest version (6.6+20260608-2). libncurses6 set to manually installed. libzarith-ocaml-dev is already the newest version (1.14-4). libzarith-ocaml-dev set to manually installed. libstdlib-ocaml-dev is already the newest version (5.4.1-1). libstdlib-ocaml-dev set to manually installed. tzdata is already the newest version (2026c-1). tzdata set to manually installed. perl-base is already the newest version (5.42.3-1). libuuid1 is already the newest version (2.42.2-3). zlib1g is already the newest version (1:1.3.dfsg+really1.3.2-3). make is already the newest version (4.4.1-3). make set to manually installed. libmagic1t64 is already the newest version (1:5.47-4). libmagic1t64 set to manually installed. libpython3.14-stdlib is already the newest version (3.14.7-1). libpython3.14-stdlib set to manually installed. patch is already the newest version (2.8-2). patch set to manually installed. libudev1 is already the newest version (261.2-1). perl is already the newest version (5.42.3-1). perl set to manually installed. libselinux1 is already the newest version (3.11-2). ocaml-findlib is already the newest version (1.9.8-1+b3). ocaml-findlib set to manually installed. libzarith-ocaml is already the newest version (1.14-4). libzarith-ocaml set to manually installed. python3-minimal is already the newest version (3.14.6-1). python3-minimal set to manually installed. openssl-provider-legacy is already the newest version (3.6.3-1). mawk is already the newest version (1.3.4.20260302-1). libtool is already the newest version (2.5.4-11). libtool set to manually installed. libmount1 is already the newest version (2.42.2-3). liblsan0 is already the newest version (16.2.0-1). liblsan0 set to manually installed. libpam-modules-bin is already the newest version (1.7.0-8). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: running --customize-hook in shell: sh -c 'chroot "$1" dpkg -r debootsnap-dummy' exec /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL (Reading database ... 23656 files and directories currently installed.) Removing debootsnap-dummy (1.0) ... I: running --customize-hook in shell: sh -c 'chroot "$1" dpkg-query --showformat '${binary:Package}=${Version}\n' --show > "$1/pkglist"' exec /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL I: running special hook: download /pkglist ./pkglist I: running --customize-hook in shell: sh -c 'rm "$1/pkglist"' exec /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL I: running special hook: upload sources.list /etc/apt/sources.list I: waiting for background processes to finish... I: cleaning package lists and apt cache... I: skipping cleanup/reproducible as requested I: creating tarball... I: done I: removing tempdir /srv/rebuilderd/tmp/mmdebstrap.FzEUXNBqCL... I: success in 391.5555 seconds Downloading packages 1to 100 out of 178 Downloading packages 101to 178 out of 178 env --chdir=/srv/rebuilderd/tmp/rebuilderdKJbjVd/out DEB_BUILD_OPTIONS=parallel=8 LANG=C.UTF-8 LC_COLLATE=C.UTF-8 LC_CTYPE=C.UTF-8 SOURCE_DATE_EPOCH=1787711933 SBUILD_CONFIG=/srv/rebuilderd/tmp/debrebuildHRVbRD/debrebuild.sbuildrc.2UNbxJO7cISq sbuild --build=riscv64 --host=riscv64 --arch-any --no-arch-all --binNMU-changelog= coq-unimath (20260603-2+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for riscv64; no source changes. * Rebuild with new OCaml ABIs of dependencies -- riscv64 Build Daemon (rv-manda-04) Wed, 26 Aug 2026 02:38:53 +0000 --chroot=/srv/rebuilderd/tmp/debrebuildHRVbRD/debrebuild.tar.126Txe7EAi4r --chroot-mode=unshare --dist=unstable --no-run-lintian --no-run-piuparts --no-run-autopkgtest --no-apt-update --no-apt-upgrade --no-apt-distupgrade --no-source --verbose --nolog --bd-uninstallable-explainer= --build-path=/build/reproducible-path --dsc-dir=coq-unimath-20260603 /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2.dsc I: consider moving your ~/.sbuildrc to /srv/rebuilderd/.config/sbuild/config.pl The Debian buildds switched to the "unshare" backend and sbuild will default to it in the future. To start using "unshare" add this to your `~/.config/sbuild/config.pl`: $chroot_mode = "unshare"; If you want to keep the old "schroot" mode even in the future, add the following to your `~/.config/sbuild/config.pl`: $chroot_mode = "schroot"; $schroot = "schroot"; sbuild: warning: descr(l1): found blank line where expected first heading sbuild (Debian sbuild) 0.89.3+deb13u4 (28 December 2025) on localhost +==============================================================================+ | coq-unimath 20260603-2+b1 (riscv64) Wed, 09 Sep 2026 19:55:30 +0000 | +==============================================================================+ Package: coq-unimath Version: 20260603-2+b1 Source Version: 20260603-2 Distribution: unstable Machine Architecture: riscv64 Host Architecture: riscv64 Build Architecture: riscv64 Build Type: any I: No tarballs found in /srv/rebuilderd/.cache/sbuild I: Unpacking /srv/rebuilderd/tmp/debrebuildHRVbRD/debrebuild.tar.126Txe7EAi4r to /srv/rebuilderd/tmp/tmp.sbuild.BB6AX73KT5... I: Setting up the chroot... I: Creating chroot session... I: Setting up log color... I: Setting up apt archive... +------------------------------------------------------------------------------+ | Fetch source files Wed, 09 Sep 2026 19:56:52 +0000 | +------------------------------------------------------------------------------+ Local sources ------------- /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2.dsc exists in /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs; copying to chroot sbuild: warning: descr(l1): found blank line where expected first heading +------------------------------------------------------------------------------+ | Install package build dependencies Wed, 09 Sep 2026 19:57:02 +0000 | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib, build-essential Filtered Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib, build-essential dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/build/reproducible-path/resolver-btVNM1/apt_archive/sbuild-build-depends-main-dummy.deb'. Install main build dependencies (apt-based resolver) ---------------------------------------------------- Installing build dependencies +------------------------------------------------------------------------------+ | Check architectures Wed, 09 Sep 2026 19:57:27 +0000 | +------------------------------------------------------------------------------+ Arch check ok (riscv64 included in any) +------------------------------------------------------------------------------+ | Build environment Wed, 09 Sep 2026 19:57:30 +0000 | +------------------------------------------------------------------------------+ Kernel: Linux 6.12.101+deb13-riscv64 #1 SMP Debian 6.12.101-1 (2026-08-05) riscv64 (riscv64) Toolchain package versions: binutils_2.47-2 dpkg-dev_1.23.7 g++-16_16.2.0-1 gcc-16_16.2.0-1 libc6-dev_2.43-3 libstdc++-16-dev_16.2.0-1 libstdc++6_16.2.0-1 linux-libc-dev_7.1.9-1 Package versions: autoconf_2.73-2 automake_1:1.18.1-4 autopoint_1.0-3 autotools-dev_20240727.1+nmu1 base-files_14.2 base-passwd_3.6.8 bash_5.3-3+b1 binutils_2.47-2 binutils-common_2.47-2 binutils-riscv64-linux-gnu_2.47-2 bsdextrautils_2.42.2-3 build-essential_12.12 bzip2_1.0.8-6+b2 coq_9.2.0+dfsg-4 coreutils_9.10-1 cpp_4:16.1.0-3 cpp-16_16.2.0-1 cpp-16-riscv64-linux-gnu_16.2.0-1 cpp-riscv64-linux-gnu_4:16.1.0-3 dash_0.5.12-12 debconf_1.5.92 debhelper_14.3 debianutils_5.23.2 dh-autoreconf_22 dh-coq_0.17 dh-ocaml_3.8 dh-strip-nondeterminism_1.15.1-1 diffutils_1:3.12-1 dpkg_1.23.7 dpkg-dev_1.23.7 dwz_0.17-1 file_1:5.47-4 findutils_4.11.0-2 g++_4:16.1.0-3 g++-16_16.2.0-1 g++-16-riscv64-linux-gnu_16.2.0-1 g++-riscv64-linux-gnu_4:16.1.0-3 gcc_4:16.1.0-3 gcc-16_16.2.0-1 gcc-16-base_16.2.0-1 gcc-16-riscv64-linux-gnu_16.2.0-1 gcc-riscv64-linux-gnu_4:16.1.0-3 gettext_1.0-3 gettext-base_1.0-3 grep_3.12-1 groff-base_1.24.1-1 gzip_1.14-1 hostname_3.25 init-system-helpers_1.69+nmu1 intltool-debian_0.35.0+20060710.6 libacl1_2.4.0-1 libarchive-zip-perl_1.68-1 libasan8_16.2.0-1 libatomic1_16.2.0-1 libattr1_1:2.6.0-1 libaudit-common_1:4.1.2-1 libaudit1_1:4.1.2-1+b1 libbinutils_2.47-2 libblkid1_2.42.2-3 libbz2-1.0_1.0.8-6+b2 libc-bin_2.43-3 libc-dev-bin_2.43-3 libc-gconv-modules-extra_2.43-3 libc6_2.43-3 libc6-dev_2.43-3 libcap-ng0_0.9.3-1+b1 libcc1-0_16.2.0-1 libcompiler-libs-ocaml-dev_5.4.1-1 libconfig-tiny-perl_2.30-1 libcoq-core_9.2.0+dfsg-4 libcoq-core-ocaml_9.2.0+dfsg-4 libcoq-core-ocaml-dev_9.2.0+dfsg-4 libcoq-stdlib_9.2.0-1+b1 libcrypt1_1:4.5.2+20251210-1 libctf-nobfd0_2.47-2 libctf0_2.47-2 libdb5.3t64_5.3.28+dfsg2-11+b1 libdebconfclient0_0.283 libdebhelper-perl_14.3 libdpkg-perl_1.23.7 libelf1t64_0.195-1 libexpat1_2.8.3-1 libffi8_3.8.0-2 libfile-stripnondeterminism-perl_1.15.1-1 libfindlib-ocaml_1.9.8-1+b3 libfindlib-ocaml-dev_1.9.8-1+b3 libgcc-16-dev_16.2.0-1 libgcc-s1_16.2.0-1 libgdbm-compat4t64_1.26-1+b2 libgdbm6t64_1.26-1+b2 libgmp-dev_2:6.3.0+dfsg-5+b2 libgmp10_2:6.3.0+dfsg-5+b2 libgmp3-dev_2:6.3.0+dfsg-5+b2 libgmpxx4ldbl_2:6.3.0+dfsg-5+b2 libgomp1_16.2.0-1 libgprofng0_2.47-2 libisl23_0.28-1 libitm1_16.2.0-1 libjansson4_2.15.1-1 libjson-perl_4.10000-1 liblsan0_16.2.0-1 liblzma5_5.8.3-1 libmagic-mgc_1:5.47-4 libmagic1t64_1:5.47-4 libmd0_1.2.0-2 libmount1_2.42.2-3 libmpc3_1.3.1-3 libmpfr6_4.2.2-3 libncurses-dev_6.6+20260608-2 libncurses6_6.6+20260608-2 libncursesw6_6.6+20260608-2 libpam-modules_1.7.0-8 libpam-modules-bin_1.7.0-8 libpam-runtime_1.7.0-8 libpam0g_1.7.0-8 libpcre2-8-0_10.46-1+b2 libperl5.42_5.42.3-1 libpipeline1_1.5.8-3 libpython3-stdlib_3.14.6-1 libpython3.14-minimal_3.14.7-1 libpython3.14-stdlib_3.14.7-1 libreadline8t64_8.3-4 libselinux1_3.11-2 libsframe3_2.47-2 libsmartcols1_2.42.2-3 libsqlite3-0_3.53.4-2 libssl3t64_3.6.3-1 libstdc++-16-dev_16.2.0-1 libstdc++6_16.2.0-1 libstdlib-ocaml_5.4.1-1 libstdlib-ocaml-dev_5.4.1-1 libsystemd0_261.2-1 libtinfo6_6.6+20260608-2 libtool_2.5.4-11 libtsan2_16.2.0-1 libubsan1_16.2.0-1 libuchardet0_0.0.8-2+b2 libudev1_261.2-1 libunistring5_1.4.2-1 libuuid1_2.42.2-3 libxml2-16_2.15.3+dfsg-1 libzarith-ocaml_1.14-4 libzarith-ocaml-dev_1.14-4 libzstd-dev_1.5.7+dfsg-4 libzstd1_1.5.7+dfsg-4 linux-libc-dev_7.1.9-1 m4_1.4.21-1 make_4.4.1-3 man-db_2.13.1-1 mawk_1.3.4.20260302-1 media-types_14.0.0 ncurses-base_6.6+20260608-2 ncurses-bin_6.6+20260608-2 netbase_6.6 ocaml_5.4.1-1 ocaml-base_5.4.1-1 ocaml-findlib_1.9.8-1+b3 ocaml-interp_5.4.1-1 openssl-provider-legacy_3.6.3-1 patch_2.8-2 perl_5.42.3-1 perl-base_5.42.3-1 perl-modules-5.42_5.42.3-1 po-debconf_1.0.22 python3_3.14.6-1 python3-minimal_3.14.6-1 python3.14_3.14.7-1 python3.14-minimal_3.14.7-1 quickjs_2025.04.26-1+b2 readline-common_8.3-4 sed_4.9-3 sensible-utils_0.0.26 sysvinit-utils_3.18-1 tar_1.35+dfsg-5 tzdata_2026c-1 util-linux_2.42.2-3 xz-utils_5.8.3-1 zlib1g_1:1.3.dfsg+really1.3.2-3 +------------------------------------------------------------------------------+ | Build Wed, 09 Sep 2026 19:57:30 +0000 | +------------------------------------------------------------------------------+ Unpack source ------------- -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 Format: 3.0 (quilt) Source: coq-unimath Binary: libcoq-unimath Architecture: any Version: 20260603-2 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/UniMath/UniMath Standards-Version: 4.7.4 Vcs-Browser: https://salsa.debian.org/ocaml-team/coq-unimath Vcs-Git: https://salsa.debian.org/ocaml-team/coq-unimath.git Testsuite: autopkgtest Testsuite-Triggers: coq Build-Depends: coq (>= 9), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib Package-List: libcoq-unimath deb ocaml optional arch=any Checksums-Sha1: 633a5821c0e84916c0b0fde1b69bc5f6849a297f 4201408 coq-unimath_20260603.orig.tar.gz 864bb2062410920298f9a4e7fef5ee1a8d28dfd2 2432 coq-unimath_20260603-2.debian.tar.xz Checksums-Sha256: e83c9539f7586c2fd0c103d104449eddf14ead5d956d995660a9b76d007f2053 4201408 coq-unimath_20260603.orig.tar.gz 6d7320bdec85671b553db34dad6432e7f99c0e8d68b83c1ad2ade6da4b877485 2432 coq-unimath_20260603-2.debian.tar.xz Files: c400d964180fb1e2d358bc84a9898974 4201408 coq-unimath_20260603.orig.tar.gz 10fe17c6e71afb1a7116b890b0e0e5a5 2432 coq-unimath_20260603-2.debian.tar.xz -----BEGIN PGP SIGNATURE----- iQJNBAEBCgA3FiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmpog7AZHGp1bGllbi5w dXlkdEBsYXBvc3RlLm5ldAAKCRAExTvX/gMFUTurEACHIPQ0G9zXWCIJRDH3uJod l+dhJM9DIwKuy+vuPXK7qbsY8So9vIj07rO3sE0eA6OheeXR1ds0PwGUSMy/zDT7 OvImxpXLzHGELD7EktAW5II7Ww3mPKsvFMUjXuQDO7Ix1F5PsfafGZ77zKOp6EZm 0H7XP1ZktFmPMJ81mUe/MPtC+kBUyOOkGQGA9bHLk16MFKSeZQE8DCRTRoYeytZD rbMPS1bEd71F/AyEtsSgOt1zz+bcQL3sVw7XOzJy1Bo89dRs5yWrcuhYocbe+iL4 rkDxWPx6d/UQ0yCgQHqjX3sIBniC4oDpN9hxAa5LzL7eVfEXfgg8qKuEYU8yK4Ry hiZWIFfyufv38p3r0UGsSzcRo5ACpVUv4TI1Uom4fAOnAsD6dOvN/yBSzEJzfR0P 6y+59+o6G+LStO3bkQGe7AbigJU04sCpAHV23WmudmPgMGIJSewvKO7dLFQvu9Qr 9qIW3Sft0fMLbb7hEIDvC4CknLNdT2SgKTUTTgt/kuPkeH1ngKZzqhx5fHcAe2+B KzsSSQdf4DWE9LmINeLBoRO9LvAc43/Ul93rKgcdbu2yeB2Cw/64B/KlY3KjpmM0 sE62qoqXGl0nYm/cPDfirnIzXWRJHpoJuNYXI+sOEIYQF7fAv3lBkQMz19wOkSB1 CfNX1m/wxAtC86EYp5r+FQ== =gZfK -----END PGP SIGNATURE----- dpkg-source: warning: cannot verify inline signature for ./coq-unimath_20260603-2.dsc: missing OpenPGP keyrings dpkg-source: info: verifying ./coq-unimath_20260603-2.dsc dpkg-source: info: skipping absent keyring /usr/share/keyrings/debian-keyring.pgp dpkg-source: info: skipping absent keyring /usr/share/keyrings/debian-tag2upload.pgp dpkg-source: info: skipping absent keyring /usr/share/keyrings/debian-nonupload.pgp dpkg-source: info: skipping absent keyring /usr/share/keyrings/debian-maintainers.pgp dpkg-source: info: extracting coq-unimath in /build/reproducible-path/coq-unimath-20260603 dpkg-source: info: unpacking coq-unimath_20260603.orig.tar.gz dpkg-source: info: unpacking coq-unimath_20260603-2.debian.tar.xz Check disk space ---------------- Sufficient free space for build Hack binNMU version ------------------- Created changelog entry for binNMU version 20260603-2+b1 User Environment ---------------- APT_CONFIG=/var/lib/sbuild/apt.conf DEB_BUILD_OPTIONS=parallel=8 HOME=/sbuild-nonexistent LANG=C.UTF-8 LC_ALL=C.UTF-8 LC_COLLATE=C.UTF-8 LC_CTYPE=C.UTF-8 LOGNAME=sbuild PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SHELL=/bin/sh SOURCE_DATE_EPOCH=1787711933 USER=sbuild dpkg-buildpackage ----------------- Command: dpkg-buildpackage --sanitize-env -us -uc -B dpkg-buildpackage: info: source package coq-unimath dpkg-buildpackage: info: source version 20260603-2+b1 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by riscv64 Build Daemon (rv-manda-04) dpkg-source --before-build . dpkg-buildpackage: info: host architecture riscv64 debian/rules clean dh clean --with coq,ocaml --buildsystem makefile debian/rules override_dh_auto_clean make[1]: Entering directory '/build/reproducible-path/coq-unimath-20260603' make clean make[2]: Entering directory '/build/reproducible-path/coq-unimath-20260603' --- making .coq_makefile_input coq_makefile -f .coq_makefile_input -o .coq_makefile_output mv .coq_makefile_output build/CoqMakefile.make make -f build/CoqMakefile.make clean make[3]: Entering directory '/build/reproducible-path/coq-unimath-20260603' CLEAN make[3]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' rm -f .coq_makefile_input .coq_makefile_output .coq_makefile_output.conf build/CoqMakefile.make COQC.log find UniMath \( -name .\*.aux -o -name \*.glob -o -name \*.d -o -name \*.vo \) -delete find UniMath -type d -empty -delete rm -rf enhanced-html cd latex ; rm -f *.pdf *.tex *.log *.aux *.out *.blg *.bbl rm -f .check-prescribed-ordering.okay rm -f ..coq_makefile_output.d rm -f .check-travis.okay make[2]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' rm -f UniMath/.dir-locals.el cp UniMath/CategoryTheory/Categories/HSET/All.v All1.v cp UniMath/CategoryTheory/Chains/All.v All2.v find . -name All.v -delete mv All1.v UniMath/CategoryTheory/Categories/HSET/All.v mv All2.v UniMath/CategoryTheory/Chains/All.v make[1]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' dh_autoreconf_clean -O--buildsystem=makefile dh_ocamlclean -O--buildsystem=makefile dh_clean -O--buildsystem=makefile debian/rules binary-arch dh binary-arch --with coq,ocaml --buildsystem makefile dh_update_autotools_config -a -O--buildsystem=makefile dh_autoreconf -a -O--buildsystem=makefile dh_ocamlinit -a -O--buildsystem=makefile dh_auto_configure -a -O--buildsystem=makefile debian/rules override_dh_auto_build make[1]: Entering directory '/build/reproducible-path/coq-unimath-20260603' dh_auto_build -- BUILD_COQ=no make -j8 INSTALL="install --strip-program=true" BUILD_COQ=no make[2]: Entering directory '/build/reproducible-path/coq-unimath-20260603' --- making .coq_makefile_input coq_makefile -f .coq_makefile_input -o .coq_makefile_output mv .coq_makefile_output build/CoqMakefile.make --- making UniMath/Foundations/All.v --- making UniMath/MoreFoundations/All.v --- making UniMath/Combinatorics/All.v --- making UniMath/Algebra/All.v --- making UniMath/Tactics/All.v --- making UniMath/NumberSystems/All.v --- making UniMath/PAdics/All.v --- making UniMath/SyntheticHomotopyTheory/All.v --- making UniMath/OrderTheory/All.v --- making UniMath/Bicategories/All.v --- making UniMath/CategoryTheory/All.v --- making UniMath/ModelCategories/All.v --- making UniMath/Ktheory/All.v --- making UniMath/Topology/All.v --- making UniMath/SubstitutionSystems/All.v --- making UniMath/RealNumbers/All.v --- making UniMath/Folds/All.v --- making UniMath/AlgebraicGeometry/All.v --- making UniMath/Paradoxes/All.v --- making UniMath/HomologicalAlgebra/All.v --- making UniMath/Induction/All.v --- making UniMath/AlgebraicTheories/All.v --- making UniMath/Semantics/All.v --- making UniMath/CONTENTS.md --- making UniMath/All.v sed -e "s/@LOCAL@ /;;/" UniMath/.dir-locals.el ulimit -v unlimited ; make -f build/CoqMakefile.make all make[3]: Entering directory '/build/reproducible-path/coq-unimath-20260603' ROCQ DEP VFILES ROCQ compile UniMath/Foundations/Init.v ROCQ compile UniMath/Tactics/EnsureStructuredProofs.v File "./UniMath/Foundations/Init.v", line 61, characters 0-71: 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] File "./UniMath/Foundations/Init.v", line 65, characters 0-64: Warning: Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default). [closed-notation-not-level-0,parsing,default] File "./UniMath/Foundations/Init.v", line 94, characters 0-67: 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] ROCQ compile UniMath/Foundations/Preamble.v File "./UniMath/Foundations/Preamble.v", line 49, 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 "./UniMath/Foundations/Preamble.v", line 50, 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 "./UniMath/Foundations/Preamble.v", line 141, characters 0-42: Warning: Implicitly declaring hint databases is deprecated. Please explicitly create "core" [implicit-create-hint-db,deprecated-since-9.2,deprecated,default] File "./UniMath/Foundations/Preamble.v", line 144, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Foundations/PartA.v File "./UniMath/Foundations/PartA.v", line 350, characters 0-48: Warning: Implicitly declaring hint databases is deprecated. Please explicitly create "pathshints" [implicit-create-hint-db,deprecated-since-9.2,deprecated,default] File "./UniMath/Foundations/PartA.v", line 1399, characters 2-15: Warning: Autogenerated "rew" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] File "./UniMath/Foundations/PartA.v", line 1399, characters 16-39: Warning: Autogenerated "rew_r" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] File "./UniMath/Foundations/PartA.v", line 1770, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Foundations/PartB.v File "./UniMath/Foundations/PartB.v", line 870, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Foundations/UnivalenceAxiom.v ROCQ compile UniMath/MoreFoundations/WeakEquivalences.v ROCQ compile UniMath/Combinatorics/DecSet.v ROCQ compile UniMath/Foundations/PartC.v ROCQ compile UniMath/Foundations/PartD.v ROCQ compile UniMath/Combinatorics/Maybe.v ROCQ compile UniMath/Foundations/UnivalenceAxiom2.v ROCQ compile UniMath/Foundations/Propositions.v File "./UniMath/Foundations/Propositions.v", line 181, 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 "./UniMath/Foundations/Propositions.v", line 183, characters 0-62: Warning: Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default). [closed-notation-not-level-0,parsing,default] File "./UniMath/Foundations/Propositions.v", line 222, 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 "./UniMath/Foundations/Propositions.v", line 337, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Foundations/Sets.v ROCQ compile UniMath/Foundations/HLevels.v ROCQ compile UniMath/Folds/UnicodeNotations.v File "./UniMath/Foundations/Sets.v", line 1155, characters 0-128: Warning: Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default). [closed-notation-not-level-0,parsing,default] ROCQ compile UniMath/Foundations/NaturalNumbers.v ROCQ compile UniMath/Foundations/Tests.v ROCQ compile UniMath/MoreFoundations/Bool.v ROCQ compile UniMath/Tactics/Utilities.v ROCQ compile UniMath/Folds/folds_precat.v ROCQ compile UniMath/Folds/folds_pre_2_cat.v ROCQ compile UniMath/MoreFoundations/Test.v File "./UniMath/Tactics/Utilities.v", line 30, characters 2-10: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Tactics/Simplify.v File "./UniMath/Foundations/NaturalNumbers.v", line 321, 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 "./UniMath/Foundations/NaturalNumbers.v", line 396, 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 "./UniMath/Foundations/NaturalNumbers.v", line 804, characters 0-43: Warning: Implicitly declaring hint databases is deprecated. Please explicitly create "natarith" [implicit-create-hint-db,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Foundations/All.v ROCQ compile UniMath/NumberSystems/NaturalNumbers_le_Inductive.v ROCQ compile UniMath/MoreFoundations/Tactics.v ROCQ compile UniMath/MoreFoundations/Notations.v ROCQ compile UniMath/MoreFoundations/DoubleNegation.v ROCQ compile UniMath/MoreFoundations/NegativePropositions.v ROCQ compile UniMath/MoreFoundations/PartD.v ROCQ compile UniMath/OrderTheory/DCPOs/AlternativeDefinitions/Dcpo.v ROCQ compile UniMath/Paradoxes/GirardsParadox.v File "./UniMath/MoreFoundations/Notations.v", line 57, 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 "./UniMath/MoreFoundations/Notations.v", line 58, 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 "./UniMath/MoreFoundations/Notations.v", line 59, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/MoreFoundations/AlternativeProofs.v ROCQ compile UniMath/OrderTheory/Posets/Subposets.v ROCQ compile UniMath/MoreFoundations/PartA.v ROCQ compile UniMath/MoreFoundations/NullHomotopies.v ROCQ compile UniMath/MoreFoundations/Equivalences.v ROCQ compile UniMath/Paradoxes/All.v ROCQ compile UniMath/MoreFoundations/StructureIdentity.v ROCQ compile UniMath/MoreFoundations/Interval.v File "./UniMath/MoreFoundations/PartA.v", line 313, 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 "./UniMath/MoreFoundations/PartA.v", line 691, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/MoreFoundations/PathsOver.v ROCQ compile UniMath/MoreFoundations/Propositions.v ROCQ compile UniMath/MoreFoundations/QuotientSet.v ROCQ compile UniMath/MoreFoundations/Univalence.v ROCQ compile UniMath/CategoryTheory/Core/Categories.v ROCQ compile UniMath/Induction/W/Wtypes.v ROCQ compile UniMath/SyntheticHomotopyTheory/Coproduct.v ROCQ compile UniMath/MoreFoundations/MoreEquivalences.v ROCQ compile UniMath/MoreFoundations/NoInjectivePairing.v ROCQ compile UniMath/CategoryTheory/Core/Isos.v ROCQ compile UniMath/Folds/from_precats_to_folds_and_back.v File "./UniMath/Folds/from_precats_to_folds_and_back.v", line 212, characters 0-66: 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] File "./UniMath/Folds/from_precats_to_folds_and_back.v", line 212, characters 0-66: Warning: Notations "_ ^ _" defined at level 30 with arguments constr at next level and "_ ^" defined at level 3 with arguments constr at next level have incompatible prefixes. One of them will likely not work. [notation-incompatible-prefix,parsing,default] File "./UniMath/Folds/from_precats_to_folds_and_back.v", line 213, characters 0-67: 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] ROCQ compile UniMath/MoreFoundations/Nat.v ROCQ compile UniMath/MoreFoundations/Sets.v ROCQ compile UniMath/Combinatorics/WellFoundedRelations.v ROCQ compile UniMath/Combinatorics/Graph.v ROCQ compile UniMath/Combinatorics/BoundedSearch.v ROCQ compile UniMath/Algebra/BinaryOperations.v File "./UniMath/MoreFoundations/Nat.v", line 25, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Combinatorics/CGraph.v File "./UniMath/Algebra/BinaryOperations.v", line 180, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Core/TransportMorphisms.v ROCQ compile UniMath/CategoryTheory/Core/Univalence.v ROCQ compile UniMath/Folds/folds_isomorphism.v ROCQ compile UniMath/MoreFoundations/Orders.v File "./UniMath/Folds/folds_isomorphism.v", line 47, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] isapropnatdecleast = λ (F : ℕ → UU) (is : ∏ n : ℕ, isdecprop (F n)), let P := λ n' : ℕ, make_hProp (F n') (is n') in let int1 := λ n : ℕ, isapropdirprod (F n) (∏ n' : ℕ, F n' → n ≤ n') (pr2 (P n)) (impred 1 (λ t : ℕ, F t → n ≤ t) (λ t : ℕ, impred 1 (λ _ : F t, n ≤ t) (λ _ : F t, pr2 (n ≤ t)))) in isapropsubtype (λ x : ℕ, make_hProp (F x × (∏ n' : ℕ, F n' → x ≤ n')) (int1 x)) (λ (x1 x2 : ℕ) (c1 : make_hProp (F x1 × (∏ n' : ℕ, F n' → x1 ≤ n')) (int1 x1)) (c2 : make_hProp (F x2 × (∏ n' : ℕ, F n' → x2 ≤ n')) (int1 x2)), (λ (e1 : F x1) (c3 : ∏ n' : ℕ, F n' → match x1 with | 0 => true | S m => natgtb n' m end = true), (λ (e2 : F x2) (c4 : ∏ n' : ℕ, F n' → match x2 with | 0 => true | S m => natgtb n' m end = true), let l1 := c3 x2 e2 in let l2 := c4 x1 e1 in isantisymmnatleh x1 x2 l1 l2) (pr1 c2) (pr2 c2)) (pr1 c1) (pr2 c1) : x1 = x2) : ∏ (F : ℕ → UU) (is : ∏ n : ℕ, isdecprop (F n)), isaprop (natdecleast F is) isapropnatdecleast relies on an unsafe universe hierarchy Arguments isapropnatdecleast (F is)%_function_scope x x' ROCQ compile UniMath/CategoryTheory/Categories/PreorderCategory/Core.v ROCQ compile UniMath/MoreFoundations/DecidablePropositions.v ROCQ compile UniMath/Combinatorics/MetricTree.v ROCQ compile UniMath/SyntheticHomotopyTheory/Halfline.v ROCQ compile UniMath/CategoryTheory/Core/Functors.v File "./UniMath/Algebra/BinaryOperations.v", line 1784, 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 "./UniMath/Algebra/BinaryOperations.v", line 1785, 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 "./UniMath/Algebra/BinaryOperations.v", line 1786, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/MoreFoundations/Subtypes.v ROCQ compile UniMath/MoreFoundations/AxiomOfChoice.v ROCQ compile UniMath/Combinatorics/StandardFiniteSets.v File "./UniMath/Algebra/BinaryOperations.v", line 1864, 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 "./UniMath/Algebra/BinaryOperations.v", line 1865, 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 "./UniMath/Combinatorics/StandardFiniteSets.v", line 45, characters 0-76: Warning: Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default). [closed-notation-not-level-0,parsing,default] ROCQ compile UniMath/Folds/All.v File "./UniMath/MoreFoundations/Subtypes.v", line 124, characters 87-92: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 UniMath/MoreFoundations/All.v File "./UniMath/Algebra/BinaryOperations.v", line 2727, 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 "./UniMath/Algebra/BinaryOperations.v", line 2728, 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 "./UniMath/Algebra/BinaryOperations.v", line 2729, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Algebra/Apartness.v ROCQ compile UniMath/CategoryTheory/Categories/SetWith2BinOp.v ROCQ compile UniMath/OrderTheory/Preorders.v ROCQ compile UniMath/OrderTheory/Posets/Basics.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Categories.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Unitary.v ROCQ compile UniMath/OrderTheory/Posets/MonotoneFunctions.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Isometry.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/DirectedSets.v ROCQ compile UniMath/OrderTheory/Posets/PosetSum.v ROCQ compile UniMath/OrderTheory/Posets/PointedPosets.v File "./UniMath/OrderTheory/DCPOs/Core/DirectedSets.v", line 160, characters 0-73: 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] ROCQ compile UniMath/OrderTheory/Posets/LiftPoset.v ROCQ compile UniMath/OrderTheory/Posets/QuotientPoset.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/Basics.v ROCQ compile UniMath/Combinatorics/FVectors.v ROCQ compile UniMath/Combinatorics/Vectors.v ROCQ compile UniMath/Combinatorics/FiniteSets.v ROCQ compile UniMath/OrderTheory/Posets/Examples/StandardFiniteSet.v ROCQ compile UniMath/AlgebraicTheories/FiniteSetSkeleton.v ROCQ compile UniMath/Combinatorics/FMatrices.v ROCQ compile UniMath/Combinatorics/VectorsTests.v ROCQ compile UniMath/Combinatorics/Lists.v ROCQ compile UniMath/Combinatorics/Tuples.v ROCQ compile UniMath/Algebra/Universal/HVectors.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/WayBelow.v ROCQ compile UniMath/Combinatorics/KFiniteTypes.v ROCQ compile UniMath/OrderTheory/OrderedSets/OrderedSets.v ROCQ compile UniMath/OrderTheory/DCPOs/Basis/Continuous.v ROCQ compile UniMath/AlgebraicTheories/LambdaCalculus.v ROCQ compile UniMath/Combinatorics/KFiniteSubtypes.v ROCQ compile UniMath/Combinatorics/FLists.v ROCQ compile UniMath/Combinatorics/GraphPaths.v ROCQ compile UniMath/Combinatorics/MoreLists.v File "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 308, characters 0-62: Warning: New coercion path [underlyingFiniteSet; FiniteSet_to_hSet] : FiniteOrderedSet >-> hSet is ambiguous with existing [underlyingOrderedSet; underlyingPoset; carrierofposet] : FiniteOrderedSet >-> hSet. [ambiguous-paths,coercions,default] File "./UniMath/Combinatorics/FLists.v", line 138, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Core/NaturalTransformations.v ROCQ compile UniMath/CategoryTheory/Core/Setcategories.v ROCQ compile UniMath/CategoryTheory/Subcategory/Core.v File "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/OrderedSets/OrderedSets.v", line 543, characters 52-61: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 UniMath/OrderTheory/Posets.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/ScottTopology.v ROCQ compile UniMath/OrderTheory/DCPOs/Basis/Algebraic.v ROCQ compile UniMath/CategoryTheory/Core/TwoCategories.v ROCQ compile UniMath/CategoryTheory/Core/EssentiallyAlgebraic.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 192, characters 9-24: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 195, characters 36-43: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/Limits/Cones.v ROCQ compile UniMath/CategoryTheory/category_binops.v ROCQ compile UniMath/CategoryTheory/LocalizingClass.v ROCQ compile UniMath/CategoryTheory/UnderCategories.v File "./UniMath/CategoryTheory/category_binops.v", line 88, characters 2-10: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Categories/Graph.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesCurried.v ROCQ compile UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Univalence.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Functors.v ROCQ compile UniMath/Bicategories/MonoidalCategories/UnivalenceMonCat/CurriedMonoidalCategories.v ROCQ compile UniMath/Combinatorics/Equivalence_Relations.v ROCQ compile UniMath/OrderTheory/OrderedSets/WellOrderedSets.v ROCQ compile UniMath/Combinatorics/Tests.v ROCQ compile UniMath/CategoryTheory/FunctorCategory.v File "./UniMath/Combinatorics/Tests.v", line 39, characters 23-33: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 "./UniMath/Combinatorics/Tests.v", line 39, characters 8-18: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Combinatorics/Tests.v", line 40, characters 25-35: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 "./UniMath/Combinatorics/Tests.v", line 40, characters 10-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/Core/Prelude.v ROCQ compile UniMath/Algebra/Universal/HVecRel.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 329, characters 5-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/Algebra/Universal/SortedTypes.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 334, characters 35-42: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Algebra/Universal/SortedTypes.v", line 91, characters 0-83: 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] File "./UniMath/Algebra/Universal/SortedTypes.v", line 99, characters 0-92: 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] ROCQ compile UniMath/Algebra/Universal/Signatures.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/IntrinsicApartness.v File "./UniMath/OrderTheory/OrderedSets/WellOrderedSets.v", line 837, characters 12-22: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 UniMath/CategoryTheory/Subcategory/Full.v File "./UniMath/OrderTheory/OrderedSets/WellOrderedSets.v", line 914, characters 17-27: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 UniMath/CategoryTheory/Categories/Quotient.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsCurried.v ROCQ compile UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Transformations.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Dilators.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Examples/Fullsub.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 501, characters 27-50: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 511, characters 27-50: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 528, characters 6-57: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/DaggerCategories/Functors/FullyFaithful.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 547, characters 6-60: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 572, characters 6-60: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/Topology/Prelim.v File "./UniMath/CategoryTheory/Core/TwoCategories.v", line 591, characters 6-60: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 616, characters 6-57: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 614, characters 6-14: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 643, characters 11-19: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 642, characters 6-58: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 700, characters 6-25: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 698, characters 6-23: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 728, characters 6-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 728, characters 6-41: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 728, characters 6-25: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 726, characters 6-45: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 726, characters 6-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 726, characters 6-23: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 754, characters 6-73: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 754, characters 6-65: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 754, characters 6-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 754, characters 6-41: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 754, characters 6-25: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 752, characters 6-67: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 752, characters 6-60: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 752, characters 6-45: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 752, characters 6-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/Core/TwoCategories.v", line 752, characters 6-23: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/opp_precat.v ROCQ compile UniMath/CategoryTheory/Epis.v ROCQ compile UniMath/CategoryTheory/whiskering.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Diagrams.v ROCQ compile UniMath/Algebra/Universal/Algebras.v ROCQ compile UniMath/Algebra/Universal/Terms.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v ROCQ compile UniMath/OrderTheory/DCPOs/Elements/Sharp.v File "./UniMath/Algebra/Universal/Terms.v", line 136, characters 22-37: Warning: In term, tolerating this expression at a higher level than expected by the notation started on the left. 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 UniMath/CategoryTheory/Limits/Cats/Limits.v ROCQ compile UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v ROCQ compile UniMath/CategoryTheory/BicatOfCatsElementary.v ROCQ compile UniMath/CategoryTheory/Groupoids.v ROCQ compile UniMath/CategoryTheory/CategorySum.v File "./UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v", line 639, characters 2-10: Warning: New coercion path [Chain_of_Chain_hsubtype; chain_family] : Chain_hsubtype >-> Funclass is ambiguous with existing [pr1_Chain_hsubtype; id_hsubtype] : Chain_hsubtype >-> Funclass. [ambiguous-paths,coercions,default] File "./UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v", line 657, characters 0-11: Warning: New coercion path [Chain_of_Chain_hsubtype; chain_family] : Chain_hsubtype >-> Funclass is ambiguous with existing [pr1_Chain_hsubtype; id_hsubtype] : Chain_hsubtype >-> Funclass. [ambiguous-paths,coercions,default] File "./UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v", line 710, characters 2-10: Warning: New coercion path [Directed_of_Directed_hsubtype; directed_family] : Directed_hsubtype >-> Funclass is ambiguous with existing [pr1_Directed_hsubtype; id_hsubtype] : Directed_hsubtype >-> Funclass. [ambiguous-paths,coercions,default] File "./UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v", line 734, characters 0-13: Warning: New coercion path [Directed_of_Directed_hsubtype; directed_family] : Directed_hsubtype >-> Funclass is ambiguous with existing [pr1_Directed_hsubtype; id_hsubtype] : Directed_hsubtype >-> Funclass. [ambiguous-paths,coercions,default] File "./UniMath/Algebra/Universal/Terms.v", line 922, 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 "./UniMath/Algebra/Universal/Terms.v", line 924, 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 "./UniMath/Algebra/Universal/Terms.v", line 926, 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 "./UniMath/Algebra/Universal/Terms.v", line 928, 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 "./UniMath/Algebra/Universal/Terms.v", line 930, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/precomp_fully_faithful.v ROCQ compile UniMath/CategoryTheory/precomp_ess_surj.v File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 38, characters 0-81: 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] File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 125, characters 15-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 125, characters 15-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 149, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 149, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 163, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 163, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.v File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 281, characters 12-17: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 281, characters 12-17: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 282, characters 13-18: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 282, characters 13-18: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/PointedFunctors.v ROCQ compile UniMath/CategoryTheory/IndexedCategories/IndexedTransformation.v ROCQ compile UniMath/CategoryTheory/ModelCategories/Retract.v ROCQ compile UniMath/ModelCategories/Retract.v File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 488, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 488, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 489, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 489, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/ModelCategories/Retract.v", line 6, characters 0-34: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope morcls.". [undeclared-scope,deprecated-since-8.10,deprecated,default] ROCQ compile UniMath/Topology/Filters.v File "./UniMath/ModelCategories/Retract.v", line 6, characters 0-34: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope morcls.". [undeclared-scope,deprecated-since-8.10,deprecated,default] ROCQ compile UniMath/Combinatorics/ZFstructures.v ROCQ compile UniMath/CategoryTheory/PrecategoryBinProduct.v File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 584, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 584, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 585, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 585, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/DisplayedCats/Core.v ROCQ compile UniMath/CategoryTheory/OppositeCategory/Core.v File "./UniMath/CategoryTheory/precomp_ess_surj.v", line 668, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 668, characters 16-21: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 669, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/precomp_ess_surj.v", line 669, characters 17-22: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/OppositeCategory/Core.v", line 15, characters 0-48: 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] ROCQ compile UniMath/CategoryTheory/ProductCategory.v ROCQ compile UniMath/Algebra/Universal/Algebras_eq.v ROCQ compile UniMath/Algebra/Universal/Congruences.v ROCQ compile UniMath/Algebra/Universal/TermAlgebras.v ROCQ compile UniMath/Algebra/Universal/VTerms.v ROCQ compile UniMath/Algebra/Universal/Examples/Nat.v ROCQ compile UniMath/Algebra/Universal/Examples/ListDataType.v ROCQ compile UniMath/OrderTheory/DCPOs/Basis/Basis.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Propositions.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/SubDCPO.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Constructions/DisplayedSections.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Equalizers.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/BinarySums.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Sums.v File "./UniMath/CategoryTheory/PrecategoryBinProduct.v", line 1008, characters 15-295: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/PrecategoryBinProduct.v", line 1008, characters 15-211: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/PrecategoryBinProduct.v", line 1001, characters 16-296: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/PrecategoryBinProduct.v", line 1001, characters 16-212: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/ZigZag.v File "./UniMath/CategoryTheory/ZigZag.v", line 66, characters 0-58: 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] ROCQ compile UniMath/CategoryTheory/IndexedCategories/OpIndexedCategory.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/Examples/Groupoids.v ROCQ compile UniMath/CategoryTheory/ModelCategories/MorphismClass.v ROCQ compile UniMath/ModelCategories/MorphismClass.v ROCQ compile UniMath/Combinatorics/All.v File "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 101, characters 0-78: 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] File "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/ModelCategories/MorphismClass.v", line 105, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/DisplayedCats/Constructions/CategoryWithStructure.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Isos.v File "./UniMath/ModelCategories/MorphismClass.v", line 102, characters 0-78: 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] File "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/ModelCategories/MorphismClass.v", line 118, characters 16-20: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/ModelCategories/MorphismClass.v", line 128, characters 37-41: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/ModelCategories/MorphismClass.v", line 143, characters 4-8: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/ModelCategories/MorphismClass.v", line 155, characters 38-42: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/ModelCategories/MorphismClass.v", line 164, characters 11-15: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Combinatorics/All.v", line 17, characters 0-50: Warning: New coercion path [underlyingFiniteSet; FiniteSet_to_hSet] : FiniteOrderedSet >-> hSet is ambiguous with existing [underlyingOrderedSet; OrderedSets.underlyingPoset; carrierofposet] : FiniteOrderedSet >-> hSet. [ambiguous-paths,coercions,default] ROCQ compile UniMath/CategoryTheory/IdempotentsAndSplitting/Retracts.v ROCQ compile UniMath/Algebra/Universal/SubAlgebras.v ROCQ compile UniMath/Algebra/Universal/DisplayedAlgebras.v ROCQ compile UniMath/Algebra/Universal/FreeAlgebras.v ROCQ compile UniMath/Algebra/Universal/Equations.v ROCQ compile UniMath/Algebra/Universal/Examples/Bool.v ROCQ compile UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v ROCQ compile UniMath/OrderTheory/DCPOs/Elements/Maximal.v File "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Combinatorics/Tests.v", line 373, characters 27-36: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/OrderTheory/DCPOs/Elements/Maximal.v", line 238, characters 0-108: Warning: element_of_strongly_maximal does not respect the uniform inheritance condition. [uniform-inheritance,coercions,default] File "./UniMath/OrderTheory/DCPOs/Elements/Maximal.v", line 238, characters 0-108: Warning: New coercion path [element_of_strongly_maximal] : pr1hSet >-> pr1hSet is not definitionally an identity function. [ambiguous-paths,coercions,default] ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Products.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Unit.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Discrete.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Fixpoints.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/BinaryProducts.v ROCQ compile UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v File "./UniMath/OrderTheory/DCPOs/Examples/BinaryProducts.v", line 32, characters 0-58: Warning: New coercion path [element_of_strongly_maximal] : pr1hSet >-> pr1hSet is not definitionally an identity function. [ambiguous-paths,coercions,default] ROCQ compile UniMath/CategoryTheory/IdempotentsAndSplitting/FunctorCategory.v ROCQ compile UniMath/CategoryTheory/ModelCategories/WeakEquivalences.v ROCQ compile UniMath/ModelCategories/WeakEquivalences.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Functors.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Univalence.v ROCQ compile UniMath/Algebra/Universal/EqAlgebras.v ROCQ compile UniMath/Algebra/Universal.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Examples/Opposite.v File "./UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v", line 44, characters 0-58: Warning: New coercion path [element_of_strongly_maximal] : pr1hSet >-> pr1hSet is not definitionally an identity function. [ambiguous-paths,coercions,default] ROCQ compile UniMath/OrderTheory/DCPOs/Core/FubiniTheorem.v ROCQ compile UniMath/OrderTheory/DCPOs/Core/CoordinateContinuity.v ROCQ compile UniMath/OrderTheory/DCPOs/Examples/Exponentials.v ROCQ compile UniMath/CategoryTheory/Categories/HSET/Core.v ROCQ compile UniMath/CategoryTheory/CategoriesWithBinOps.v ROCQ compile UniMath/CategoryTheory/Categories/Type/Core.v ROCQ compile UniMath/CategoryTheory/HorizontalComposition.v ROCQ compile UniMath/CategoryTheory/Core.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesTensored.v ROCQ compile UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v ROCQ compile UniMath/Bicategories/Core/Bicat.v File "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 27, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 28, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 39, characters 29-133: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 50, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 51, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 58, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 68, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 81, 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 91, characters 29-133: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 98, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/covyoneda.v File "./UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v", line 118, 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 "./UniMath/Bicategories/Core/Bicat.v", line 176, characters 8-23: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 205, characters 8-55: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v ROCQ compile UniMath/OrderTheory/DCPOs/FixpointTheorems/LeastFixpoint.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/FullyFaithfulDispFunctor.v File "./UniMath/Bicategories/Core/Bicat.v", line 282, characters 4-19: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/PointedFunctorsComposition.v ROCQ compile UniMath/CategoryTheory/Categories/Type/NoHomsets.v ROCQ compile UniMath/CategoryTheory/Categories/CGraph.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Examples/DispFunctorPair.v ROCQ compile UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v File "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 19, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 20, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 30, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 31, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 32, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 42, 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 "./UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v", line 43, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v ROCQ compile UniMath/CategoryTheory/IndexedCategories/CoreIndexedCategory.v ROCQ compile UniMath/CategoryTheory/Monics.v ROCQ compile UniMath/OrderTheory/DCPOs.v File "./UniMath/Bicategories/Core/Bicat.v", line 353, characters 4-51: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/OrderTheory/DCPOs.v", line 15, characters 0-58: Warning: New coercion path [element_of_strongly_maximal] : Sets.pr1hSet >-> Sets.pr1hSet is not definitionally an identity function. [ambiguous-paths,coercions,default] ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v ROCQ compile UniMath/Bicategories/DoubleCategories/Basics/DoubleCategoryBasics.v File "./UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v", line 808, characters 0-69: Warning: disp_nat_z_iso_to_trans does not respect the uniform inheritance condition. [uniform-inheritance,coercions,default] ROCQ compile UniMath/CategoryTheory/Categories/HSET/MonoEpiIso.v File "./UniMath/Bicategories/Core/Bicat.v", line 619, characters 30-45: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/SplitMonicsAndEpis.v ROCQ compile UniMath/CategoryTheory/Limits/Equalizers.v ROCQ compile UniMath/CategoryTheory/Categories/Type/MonoEpiIso.v ROCQ compile UniMath/CategoryTheory/HomotopicalCategory.v ROCQ compile UniMath/CategoryTheory/yoneda.v ROCQ compile UniMath/CategoryTheory/Categories/Type/Univalence.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsTensored.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/BraidedMonoidalCategories.v ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/Total.v ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Constant.v ROCQ compile UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProdOfTwosidedDispCat.v File "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v", line 140, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/Precategories.v ROCQ compile UniMath/Bicategories/DoubleCategories/AlternativeDefinitions/DoubleCatsUnfolded.v File "./UniMath/Bicategories/DoubleCategories/AlternativeDefinitions/DoubleCatsUnfolded.v", line 263, characters 0-199: Warning: Closed notations (i.e. starting and ending with a terminal symbol) should usually be at level 0 (default). [closed-notation-not-level-0,parsing,default] ROCQ compile UniMath/CategoryTheory/Categories/HSET/Univalence.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Total.v ROCQ compile UniMath/CategoryTheory/Adjunctions/Core.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Constructions/DisplayedFunctorCat.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/DisplayedFunctorEq.v ROCQ compile UniMath/CategoryTheory/IdempotentsAndSplitting/Set.v ROCQ compile UniMath/CategoryTheory/CommaCategories.v ROCQ compile UniMath/CategoryTheory/IsoCommaCategory.v ROCQ compile UniMath/CategoryTheory/SimplicialSets.v ROCQ compile UniMath/CategoryTheory/coslicecat.v ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Constructions/FullSubcategory.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Examples/Sigma.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Fiber.v File "./UniMath/CategoryTheory/DisplayedCats/Fiber.v", line 199, characters 0-76: 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] ROCQ compile UniMath/CategoryTheory/IdempotentsAndSplitting/Fullsub.v ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/Representation.v ROCQ compile UniMath/CategoryTheory/Categories/Magma.v ROCQ compile UniMath/Algebra/Monoids2.v File "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Monoids2.v", line 100, characters 44-69: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/Algebra/AbelianMonoids.v ROCQ compile UniMath/Algebra/Groups2.v File "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianMonoids.v", line 57, characters 5-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/Groups2.v", line 62, characters 5-29: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/Equivalences/Core.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Colimits.v File "./UniMath/CategoryTheory/Equivalences/Core.v", line 227, characters 0-66: 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] ROCQ compile UniMath/CategoryTheory/Adjunctions/Coreflections.v ROCQ compile UniMath/CategoryTheory/Adjunctions/AdjunctionMonics.v File "./UniMath/CategoryTheory/Adjunctions/Coreflections.v", line 386, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Adjunctions/Reflections.v ROCQ compile UniMath/CategoryTheory/Monads/RelativeMonads.v File "./UniMath/CategoryTheory/Adjunctions/Reflections.v", line 386, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Limits/StandardDiagrams.v ROCQ compile UniMath/CategoryTheory/ArrowCategory.v ROCQ compile UniMath/CategoryTheory/Adjunctions/Restriction.v ROCQ compile UniMath/CategoryTheory/Subcategory/Reflective.v ROCQ compile UniMath/CategoryTheory/Categories/PrecategoryOfCategories.v ROCQ compile UniMath/CategoryTheory/OppositeCategory/OppositeAdjunction.v ROCQ compile UniMath/CategoryTheory/OppositeCategory/OppositeOfFunctorCategory.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Equivalences.v ROCQ compile UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v File "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 42-49: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 123, characters 26-33: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 159, 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 160, 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 161, 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 "./UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v", line 191, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.v ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/Test.v ROCQ compile UniMath/Algebra/Monoids.v ROCQ compile UniMath/Algebra/AbelianGroups.v ROCQ compile UniMath/CategoryTheory/Limits/Coproducts.v File "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right. 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 "./UniMath/Algebra/AbelianGroups.v", line 67, characters 5-37: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/Limits/Graphs/Limits.v ROCQ compile UniMath/CategoryTheory/Limits/Initial.v ROCQ compile UniMath/CategoryTheory/Equivalences/FullyFaithful.v ROCQ compile UniMath/Algebra/Universal/Examples/Monoid.v ROCQ compile UniMath/Algebra/Universal/Examples/Tests.v ROCQ compile UniMath/Tactics/Monoids_Tactics.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/EqDiag.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Coproducts.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/BinProducts.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Equalizers.v ROCQ compile UniMath/CategoryTheory/Monads/RelMonads_Coreflection.v ROCQ compile UniMath/CategoryTheory/Monads/RelativeModules.v ROCQ compile UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v ROCQ compile UniMath/CategoryTheory/Subcategory/FullEquivalences.v ROCQ compile UniMath/CategoryTheory/Limits/Filtered.v ROCQ compile UniMath/CategoryTheory/PrecompEquivalence.v File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 156, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 157, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 158, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 160, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 161, characters 8-16: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/RightKanExtension.v File "./UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v", line 407, characters 16-38: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 UniMath/CategoryTheory/OppositeCategory/OppositeEquivalence.v ROCQ compile UniMath/CategoryTheory/Chains/Chains.v ROCQ compile UniMath/CategoryTheory/RepresentableFunctors/DirectSum.v Finished transaction in 86.539 secs (42.124u,0.742s) (successful) ROCQ compile UniMath/Algebra/Groups.v ROCQ compile UniMath/CategoryTheory/Limits/Products.v File "./UniMath/CategoryTheory/DisplayedCats/Equivalences.v", line 584, characters 0-109: Warning: New coercion path [adjunction_of_right_adjoint_over_id_data; left_adj_over_id] : right_adjoint_over_id_data >-> disp_functor is ambiguous with existing [functor_of_right_adjoint_over_id] : right_adjoint_over_id_data >-> disp_functor. [ambiguous-paths,coercions,default] File "./UniMath/CategoryTheory/DisplayedCats/Equivalences.v", line 616, characters 0-22: Warning: New coercion path [adjunction_of_right_adjoint_over_id_data; left_adj_over_id] : right_adjoint_over_id_data >-> disp_functor is ambiguous with existing [functor_of_right_adjoint_over_id] : right_adjoint_over_id_data >-> disp_functor. [ambiguous-paths,coercions,default] ROCQ compile UniMath/CategoryTheory/catiso.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Initial.v ROCQ compile UniMath/CategoryTheory/Categories/HSET/FilteredColimits.v ROCQ compile UniMath/CategoryTheory/PointedFunctorAlgebras.v ROCQ compile UniMath/Algebra/GroupAction.v ROCQ compile UniMath/Algebra/RigsAndRings.v File "./UniMath/Algebra/RigsAndRings.v", line 518, characters 0-63: 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] ROCQ compile UniMath/CategoryTheory/Limits/Terminal.v ROCQ compile UniMath/CategoryTheory/PrecategoriesWithAbgrops.v File "./UniMath/Algebra/RigsAndRings.v", line 1479, characters 0-65: 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] ROCQ compile UniMath/Induction/FunctorCoalgebras_legacy.v ROCQ compile UniMath/Algebra/Universal/Examples/Group.v File "./UniMath/Induction/FunctorCoalgebras_legacy.v", line 154, 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 "./UniMath/Induction/FunctorCoalgebras_legacy.v", line 160, 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 "./UniMath/Induction/FunctorCoalgebras_legacy.v", line 161, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/Tactics/Abmonoids_Tactics.v ROCQ compile UniMath/Tactics/Groups_Tactics.v ROCQ compile UniMath/OrderTheory/Lattice/Lattice.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Terminal.v ROCQ compile UniMath/CategoryTheory/CategoryEquality.v ROCQ compile UniMath/CategoryTheory/Limits/Ends.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/CatIsoDisplayed.v ROCQ compile UniMath/CategoryTheory/WeakEquivalences/Core.v ROCQ compile UniMath/CategoryTheory/Chains/Cochains.v ROCQ compile UniMath/Induction/FunctorCoalgebras_legacy_alt_UU.v ROCQ compile UniMath/RealNumbers/Sets.v ROCQ compile UniMath/CategoryTheory/Limits/Zero.v ROCQ compile UniMath/Tactics/Nat_Tactics.v ROCQ compile UniMath/OrderTheory/Lattice/Bounded.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Zero.v ROCQ compile UniMath/CategoryTheory/Core/PosetCat.v ROCQ compile UniMath/CategoryTheory/WeakEquivalences/TwoOutOfThree.v ROCQ compile UniMath/CategoryTheory/WeakEquivalences/Opp.v ROCQ compile UniMath/CategoryTheory/WeakEquivalences/Mono.v ROCQ compile UniMath/CategoryTheory/RezkCompletions/RezkCompletions.v ROCQ compile UniMath/CategoryTheory/Categories/CategoryOfSetCategories.v ROCQ compile UniMath/CategoryTheory/OppositeCategory/LimitsAsColimits.v ROCQ compile UniMath/CategoryTheory/DaggerCategories/CatIso.v ROCQ compile UniMath/Induction/M/Limits.v ROCQ compile UniMath/CategoryTheory/Limits/BinCoproducts.v ROCQ compile UniMath/CategoryTheory/Limits/Kernels.v ROCQ compile UniMath/CategoryTheory/Limits/BinProducts.v ROCQ compile UniMath/Tactics/All.v ROCQ compile UniMath/OrderTheory/Lattice/Complement.v ROCQ compile UniMath/OrderTheory/Lattice/Heyting.v ROCQ compile UniMath/OrderTheory/Lattice/Examples/FromPartialOrder.v ROCQ compile UniMath/OrderTheory/Prebilattice/Prebilattice.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/BinCoproducts.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Kernels.v ROCQ compile UniMath/CategoryTheory/Limits/FinOrdCoproducts.v ROCQ compile UniMath/CategoryTheory/Limits/LimitIso.v ROCQ compile UniMath/CategoryTheory/Adjunctions/Examples.v ROCQ compile UniMath/CategoryTheory/Subcategory/Limits.v File "./UniMath/CategoryTheory/Limits/FinOrdCoproducts.v", line 68, characters 14-52: Warning: Autogenerated "rew_dep" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/FunctorCoalgebras.v ROCQ compile UniMath/CategoryTheory/RezkCompletions/Construction.v ROCQ compile UniMath/CategoryTheory/Categories/CategoryOfSetGroupoids.v File "./UniMath/CategoryTheory/FunctorCoalgebras.v", line 123, 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 "./UniMath/CategoryTheory/FunctorCoalgebras.v", line 129, 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 "./UniMath/CategoryTheory/FunctorCoalgebras.v", line 130, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Limits/Examples/CategoryOfSetcategoriesLimits.v ROCQ compile UniMath/CategoryTheory/Categories/Type/Colimits.v ROCQ compile UniMath/CategoryTheory/Categories/Type/Limits.v ROCQ compile UniMath/CategoryTheory/Monoidal/WhiskeredBifunctors.v ROCQ compile UniMath/CategoryTheory/GrothendieckConstruction/TotalCategory.v ROCQ compile UniMath/CategoryTheory/Limits/Coequalizers.v ROCQ compile UniMath/CategoryTheory/Limits/Pullbacks.v ROCQ compile UniMath/OrderTheory/Lattice/Distributive.v ROCQ compile UniMath/OrderTheory/Lattice/CompleteHeyting.v ROCQ compile UniMath/OrderTheory/Lattice/Boolean.v File "./UniMath/CategoryTheory/Limits/Pullbacks.v", line 310, characters 2-383: Warning: Autogenerated "rew_dep" scheme for paths. Use "Scheme Rewriting for paths" to explicitly generate it. This will become an error in the future. [missing-scheme,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/OrderTheory/Prebilattice/Interlaced.v ROCQ compile UniMath/CategoryTheory/Limits/Graphs/Coequalizers.v ROCQ compile UniMath/CategoryTheory/LatticeObject.v ROCQ compile UniMath/CategoryTheory/Limits/BinBiproducts.v ROCQ compile UniMath/CategoryTheory/Limits/FinOrdProducts.v ROCQ compile UniMath/CategoryTheory/Limits/Coends.v ROCQ compile UniMath/CategoryTheory/DisplayedCats/Binproducts.v ROCQ compile UniMath/CategoryTheory/Chains/CoAdamek.v File "./UniMath/CategoryTheory/Chains/CoAdamek.v", line 137, 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 "./UniMath/CategoryTheory/Chains/CoAdamek.v", line 138, 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 "./UniMath/CategoryTheory/Chains/CoAdamek.v", line 148, characters 6-14: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default] ROCQ compile UniMath/CategoryTheory/Monoidal/Categories.v ROCQ compile UniMath/CategoryTheory/Monoidal/Displayed/WhiskeredDisplayedBifunctors.v ROCQ compile UniMath/CategoryTheory/GrothendieckConstruction/IsosInTotal.v ROCQ compile UniMath/CategoryTheory/GrothendieckConstruction/Projection.v ROCQ compile UniMath/CategoryTheory/Limits/Cokernels.v ROCQ compile UniMath/CategoryTheory/Limits/Pushouts.v ROCQ compile UniMath/OrderTheory/Lattice/DerivedLawsCompleteHeyting.v ROCQ compile UniMath/OrderTheory/Lattice/Examples/Bool.v ROCQ compile UniMath/OrderTheory/Lattice/Examples/Subsets.v ROCQ compile UniMath/OrderTheory/Lattice/Examples/Sieves.v Segmentation fault make[4]: *** [build/CoqMakefile.make:815: UniMath/OrderTheory/Lattice/Examples/Subsets.vo] Error 139 make[4]: *** [UniMath/OrderTheory/Lattice/Examples/Subsets.vo] Deleting file 'UniMath/OrderTheory/Lattice/Examples/Subsets.glob' make[4]: *** Waiting for unfinished jobs.... File "./UniMath/Bicategories/Core/Bicat.v", line 1464, characters 7-151: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 1483, characters 4-136: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 1493, characters 7-151: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 1511, characters 4-136: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 1524, characters 7-153: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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 "./UniMath/Bicategories/Core/Bicat.v", line 1543, characters 4-138: Warning: In term, tolerating this expression at a higher level than expected by the notation continuing on the right (which is not left-associative). 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] make[3]: *** [build/CoqMakefile.make:411: all] Error 2 make[3]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' make[2]: *** [Makefile:101: all] Error 2 make[2]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' dh_auto_build: error: make -j8 INSTALL="install --strip-program=true" BUILD_COQ=no returned exit code 2 make[1]: *** [debian/rules:23: override_dh_auto_build] Error 25 make[1]: Leaving directory '/build/reproducible-path/coq-unimath-20260603' make: *** [debian/rules:8: binary-arch] Error 2 dpkg-buildpackage: error: debian/rules binary-arch subprocess failed with exit status 2 -------------------------------------------------------------------------------- Build finished at 2026-09-09T20:29:02Z Finished -------- +------------------------------------------------------------------------------+ | Cleanup Wed, 09 Sep 2026 20:29:04 +0000 | +------------------------------------------------------------------------------+ Purging /build/reproducible-path Not cleaning session: cloned chroot in use E: Build failure (dpkg-buildpackage died with exit 2) +------------------------------------------------------------------------------+ | Summary Wed, 09 Sep 2026 20:29:18 +0000 | +------------------------------------------------------------------------------+ Build Architecture: riscv64 Build Type: any Build-Space: 78184 Build-Time: 1879 Distribution: unstable Fail-Stage: build Host Architecture: riscv64 Install-Time: 25 Job: /srv/rebuilderd/tmp/rebuilderdKJbjVd/inputs/coq-unimath_20260603-2.dsc Machine Architecture: riscv64 Package: coq-unimath Package-Time: 2012 Source-Version: 20260603-2 Space: 78184 Status: attempted Version: 20260603-2+b1 -------------------------------------------------------------------------------- Finished at 2026-09-09T20:29:02Z Build needed 00:33:32, 78184k disk space E: Build failure (dpkg-buildpackage died with exit 2) sbuild failed