https://launchpad.net/ubuntu/+source/coq-hierarchy-builder/1.4.0-6build6/+build/26962111 RUN: /usr/share/launchpad-buildd/bin/builder-prep Kernel version: Linux riscv64-qemu-lgw01-085 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 Buildd toolchain package versions: launchpad-buildd_234~642~ubuntu20.04.1 python3-lpbuildd_234~642~ubuntu20.04.1 sbuild_0.79.0-1ubuntu1 git_1:2.25.1-1ubuntu3.2 dpkg-dev_1.19.7ubuntu3.2 python3-debian_0.1.36ubuntu1. Syncing the system clock with the buildd NTP service... 5 Nov 15:05:36 ntpdate[1020445]: adjust time server 10.211.37.1 offset -0.000548 sec RUN: /usr/share/launchpad-buildd/bin/in-target unpack-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 --image-type chroot /home/buildd/filecache-default/20a3246b7a16d5658607d7f37229fcda30a33651 Creating target for build PACKAGEBUILD-26962111 RUN: /usr/share/launchpad-buildd/bin/in-target mount-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 Starting target for build PACKAGEBUILD-26962111 RUN: /usr/share/launchpad-buildd/bin/in-target override-sources-list --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 'deb http://ftpmaster.internal/ubuntu noble main universe' 'deb http://ftpmaster.internal/ubuntu noble-security main universe' 'deb http://ftpmaster.internal/ubuntu noble-updates main universe' 'deb http://ftpmaster.internal/ubuntu noble-proposed main universe' Overriding sources.list in build-PACKAGEBUILD-26962111 RUN: /usr/share/launchpad-buildd/bin/in-target update-debian-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 Updating target for build PACKAGEBUILD-26962111 Get:1 http://ftpmaster.internal/ubuntu noble InRelease [213 kB] Get:2 http://ftpmaster.internal/ubuntu noble-security InRelease [74.9 kB] Get:3 http://ftpmaster.internal/ubuntu noble-updates InRelease [74.9 kB] Get:4 http://ftpmaster.internal/ubuntu noble-proposed InRelease [74.9 kB] Get:5 http://ftpmaster.internal/ubuntu noble/main riscv64 Packages [1340 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main Translation-en [517 kB] Get:7 http://ftpmaster.internal/ubuntu noble/universe riscv64 Packages [14.6 MB] Get:8 http://ftpmaster.internal/ubuntu noble/universe Translation-en [6003 kB] Get:9 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 Packages [154 kB] Get:10 http://ftpmaster.internal/ubuntu noble-proposed/main Translation-en [61.2 kB] Get:11 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 Packages [1115 kB] Get:12 http://ftpmaster.internal/ubuntu noble-proposed/universe Translation-en [446 kB] Fetched 24.7 MB in 39s (629 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... Calculating upgrade... The following package was automatically installed and is no longer required: libunistring2 Use 'sudo apt autoremove' to remove it. The following NEW packages will be installed: libunistring5 The following packages will be upgraded: apt apt-utils base-files base-passwd bash-completion binutils binutils-common binutils-riscv64-linux-gnu cpp-13 debianutils diffutils dpkg dpkg-dev g++-13 gcc-13 gcc-13-base grep libapparmor1 libapt-pkg6.0 libargon2-1 libasan8 libatomic1 libaudit-common libaudit1 libbinutils libc-bin libc-dev-bin libc6 libc6-dev libcap-ng0 libcc1-0 libctf-nobfd0 libctf0 libdb5.3 libdpkg-perl libgcc-13-dev libgcc-s1 libgnutls30 libgomp1 libidn2-0 liblzma5 libncursesw6 libnsl-dev libnsl2 libpng16-16 libselinux1 libsemanage-common libsemanage2 libsframe1 libsqlite3-0 libssl3 libstdc++-13-dev libstdc++6 libsystemd-shared libsystemd0 libtinfo6 libudev1 libxxhash0 libzstd1 mawk ncurses-base ncurses-bin openssl optipng systemd systemd-dev systemd-sysv xz-utils 68 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 83.9 MB of archives. After this operation, 2168 kB of additional disk space will be used. Get:1 http://ftpmaster.internal/ubuntu noble/main riscv64 libnsl-dev riscv64 1.3.0-3 [135 kB] Get:2 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc6-dev riscv64 2.38-3ubuntu1 [3401 kB] Get:3 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc-dev-bin riscv64 2.38-3ubuntu1 [19.2 kB] Get:4 http://ftpmaster.internal/ubuntu noble/main riscv64 libnsl2 riscv64 1.3.0-3 [42.0 kB] Get:5 http://ftpmaster.internal/ubuntu noble/main riscv64 libcc1-0 riscv64 13.2.0-6ubuntu1 [45.4 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main riscv64 gcc-13-base riscv64 13.2.0-6ubuntu1 [44.3 kB] Get:7 http://ftpmaster.internal/ubuntu noble/main riscv64 libgcc-s1 riscv64 13.2.0-6ubuntu1 [57.1 kB] Get:8 http://ftpmaster.internal/ubuntu noble/main riscv64 libgomp1 riscv64 13.2.0-6ubuntu1 [140 kB] Get:9 http://ftpmaster.internal/ubuntu noble/main riscv64 libatomic1 riscv64 13.2.0-6ubuntu1 [9488 B] Get:10 http://ftpmaster.internal/ubuntu noble/main riscv64 libasan8 riscv64 13.2.0-6ubuntu1 [2509 kB] Get:11 http://ftpmaster.internal/ubuntu noble/main riscv64 g++-13 riscv64 13.2.0-6ubuntu1 [11.9 MB] Get:12 http://ftpmaster.internal/ubuntu noble/main riscv64 libstdc++-13-dev riscv64 13.2.0-6ubuntu1 [5449 kB] Get:13 http://ftpmaster.internal/ubuntu noble/main riscv64 libgcc-13-dev riscv64 13.2.0-6ubuntu1 [3123 kB] Get:14 http://ftpmaster.internal/ubuntu noble/main riscv64 gcc-13 riscv64 13.2.0-6ubuntu1 [20.8 MB] Get:15 http://ftpmaster.internal/ubuntu noble/main riscv64 cpp-13 riscv64 13.2.0-6ubuntu1 [10.5 MB] Get:16 http://ftpmaster.internal/ubuntu noble/main riscv64 libstdc++6 riscv64 13.2.0-6ubuntu1 [779 kB] Get:17 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libzstd1 riscv64 1.5.5+dfsg2-2 [349 kB] Get:18 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libctf-nobfd0 riscv64 2.41-6ubuntu1 [105 kB] Get:19 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libctf0 riscv64 2.41-6ubuntu1 [103 kB] Get:20 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libsframe1 riscv64 2.41-6ubuntu1 [15.6 kB] Get:21 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libbinutils riscv64 2.41-6ubuntu1 [483 kB] Get:22 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 binutils-common riscv64 2.41-6ubuntu1 [221 kB] Get:23 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 binutils riscv64 2.41-6ubuntu1 [2996 B] Get:24 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 binutils-riscv64-linux-gnu riscv64 2.41-6ubuntu1 [894 kB] Get:25 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc6 riscv64 2.38-3ubuntu1 [2742 kB] Get:26 http://ftpmaster.internal/ubuntu noble/main riscv64 base-files riscv64 13ubuntu4 [73.5 kB] Get:27 http://ftpmaster.internal/ubuntu noble/main riscv64 debianutils riscv64 5.14 [88.8 kB] Get:28 http://ftpmaster.internal/ubuntu noble/main riscv64 diffutils riscv64 1:3.10-1 [180 kB] Get:29 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 liblzma5 riscv64 5.4.4-0.1 [127 kB] Get:30 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libapparmor1 riscv64 4.0.0~alpha2-0ubuntu6 [48.2 kB] Get:31 http://ftpmaster.internal/ubuntu noble/main riscv64 libaudit-common all 1:3.1.1-1build1 [5510 B] Get:32 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libcap-ng0 riscv64 0.8.3-1build3 [15.3 kB] Get:33 http://ftpmaster.internal/ubuntu noble/main riscv64 libaudit1 riscv64 1:3.1.1-1build1 [47.1 kB] Get:34 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libselinux1 riscv64 3.5-1build1 [83.1 kB] Get:35 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libssl3 riscv64 3.0.10-1ubuntu2.1 [1712 kB] Get:36 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd-sysv riscv64 253.5-1ubuntu7 [11.5 kB] Get:37 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd-dev all 253.5-1ubuntu7 [78.5 kB] Get:38 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd riscv64 253.5-1ubuntu7 [3067 kB] Get:39 http://ftpmaster.internal/ubuntu noble/main riscv64 libsystemd-shared riscv64 253.5-1ubuntu7 [1903 kB] Get:40 http://ftpmaster.internal/ubuntu noble/main riscv64 libsystemd0 riscv64 253.5-1ubuntu7 [423 kB] Get:41 http://ftpmaster.internal/ubuntu noble/main riscv64 libudev1 riscv64 253.5-1ubuntu7 [163 kB] Get:42 http://ftpmaster.internal/ubuntu noble/main riscv64 libxxhash0 riscv64 0.8.2-2 [43.7 kB] Get:43 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libapt-pkg6.0 riscv64 2.7.6 [989 kB] Get:44 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 dpkg riscv64 1.22.1ubuntu1 [1396 kB] Get:45 http://ftpmaster.internal/ubuntu noble/main riscv64 grep riscv64 3.11-3 [167 kB] Get:46 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 ncurses-bin riscv64 6.4+20231016-1 [184 kB] Get:47 http://ftpmaster.internal/ubuntu noble/main riscv64 base-passwd riscv64 3.6.2 [52.1 kB] Get:48 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc-bin riscv64 2.38-3ubuntu1 [601 kB] Get:49 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 ncurses-base all 6.4+20231016-1 [24.7 kB] Get:50 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libdb5.3 riscv64 5.3.28+dfsg2-3 [766 kB] Get:51 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 apt riscv64 2.7.6 [1335 kB] Get:52 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 apt-utils riscv64 2.7.6 [225 kB] Get:53 http://ftpmaster.internal/ubuntu noble/main riscv64 libunistring5 riscv64 1.1-2 [544 kB] Get:54 http://ftpmaster.internal/ubuntu noble/main riscv64 libidn2-0 riscv64 2.3.4-1build1 [99.3 kB] Get:55 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libgnutls30 riscv64 3.8.1-4ubuntu3 [995 kB] Get:56 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libsemanage-common all 3.5-1build1 [9982 B] Get:57 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libsemanage2 riscv64 3.5-1build1 [97.7 kB] Get:58 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libncursesw6 riscv64 6.4+20231016-1 [150 kB] Get:59 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libtinfo6 riscv64 6.4+20231016-1 [107 kB] Get:60 http://ftpmaster.internal/ubuntu noble/main riscv64 mawk riscv64 1.3.4.20230808-1 [125 kB] Get:61 http://ftpmaster.internal/ubuntu noble/main riscv64 libargon2-1 riscv64 0~20190702+dfsg-4 [23.7 kB] Get:62 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libsqlite3-0 riscv64 3.44.0-1 [689 kB] Get:63 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 openssl riscv64 3.0.10-1ubuntu2.1 [1170 kB] Get:64 http://ftpmaster.internal/ubuntu noble/main riscv64 bash-completion all 1:2.11-8 [180 kB] Get:65 http://ftpmaster.internal/ubuntu noble/main riscv64 libpng16-16 riscv64 1.6.40-2 [189 kB] Get:66 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 xz-utils riscv64 5.4.4-0.1 [268 kB] Get:67 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 dpkg-dev all 1.22.1ubuntu1 [1148 kB] Get:68 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libdpkg-perl all 1.22.1ubuntu1 [285 kB] Get:69 http://ftpmaster.internal/ubuntu noble/main riscv64 optipng riscv64 0.7.7-3 [86.9 kB] Preconfiguring packages ... Fetched 83.9 MB in 20s (4297 kB/s) (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libnsl-dev_1.3.0-3_riscv64.deb ... Unpacking libnsl-dev:riscv64 (1.3.0-3) over (1.3.0-2build2) ... Preparing to unpack .../1-libc6-dev_2.38-3ubuntu1_riscv64.deb ... Unpacking libc6-dev:riscv64 (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Preparing to unpack .../2-libc-dev-bin_2.38-3ubuntu1_riscv64.deb ... Unpacking libc-dev-bin (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Preparing to unpack .../3-libnsl2_1.3.0-3_riscv64.deb ... Unpacking libnsl2:riscv64 (1.3.0-3) over (1.3.0-2build2) ... Preparing to unpack .../4-libcc1-0_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libcc1-0:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../5-gcc-13-base_13.2.0-6ubuntu1_riscv64.deb ... Unpacking gcc-13-base:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up gcc-13-base:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../libgcc-s1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgcc-s1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up libgcc-s1:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libgomp1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgomp1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../1-libatomic1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libatomic1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../2-libasan8_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libasan8:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../3-g++-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking g++-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../4-libstdc++-13-dev_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libstdc++-13-dev:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../5-libgcc-13-dev_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgcc-13-dev:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../6-gcc-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking gcc-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../7-cpp-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking cpp-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../8-libstdc++6_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libstdc++6:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up libstdc++6:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../libzstd1_1.5.5+dfsg2-2_riscv64.deb ... Unpacking libzstd1:riscv64 (1.5.5+dfsg2-2) over (1.5.5+dfsg2-1ubuntu2) ... Setting up libzstd1:riscv64 (1.5.5+dfsg2-2) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libctf-nobfd0_2.41-6ubuntu1_riscv64.deb ... Unpacking libctf-nobfd0:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../1-libctf0_2.41-6ubuntu1_riscv64.deb ... Unpacking libctf0:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../2-libsframe1_2.41-6ubuntu1_riscv64.deb ... Unpacking libsframe1:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../3-libbinutils_2.41-6ubuntu1_riscv64.deb ... Unpacking libbinutils:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../4-binutils-common_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils-common:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../5-binutils_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../6-binutils-riscv64-linux-gnu_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils-riscv64-linux-gnu (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../7-libc6_2.38-3ubuntu1_riscv64.deb ... Unpacking libc6:riscv64 (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Setting up libc6:riscv64 (2.38-3ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../base-files_13ubuntu4_riscv64.deb ... Unpacking base-files (13ubuntu4) over (13ubuntu3) ... Setting up base-files (13ubuntu4) ... Installing new version of config file /etc/issue ... Installing new version of config file /etc/issue.net ... Installing new version of config file /etc/lsb-release ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../debianutils_5.14_riscv64.deb ... Unpacking debianutils (5.14) over (5.8-1) ... Setting up debianutils (5.14) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../diffutils_1%3a3.10-1_riscv64.deb ... Unpacking diffutils (1:3.10-1) over (1:3.8-4) ... Setting up diffutils (1:3.10-1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../liblzma5_5.4.4-0.1_riscv64.deb ... Unpacking liblzma5:riscv64 (5.4.4-0.1) over (5.4.1-0.2) ... Setting up liblzma5:riscv64 (5.4.4-0.1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libapparmor1_4.0.0~alpha2-0ubuntu6_riscv64.deb ... Unpacking libapparmor1:riscv64 (4.0.0~alpha2-0ubuntu6) over (4.0.0~alpha2-0ubuntu5) ... Preparing to unpack .../libaudit-common_1%3a3.1.1-1build1_all.deb ... Unpacking libaudit-common (1:3.1.1-1build1) over (1:3.1.1-1) ... Setting up libaudit-common (1:3.1.1-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libcap-ng0_0.8.3-1build3_riscv64.deb ... Unpacking libcap-ng0:riscv64 (0.8.3-1build3) over (0.8.3-1build2) ... Setting up libcap-ng0:riscv64 (0.8.3-1build3) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libaudit1_1%3a3.1.1-1build1_riscv64.deb ... Unpacking libaudit1:riscv64 (1:3.1.1-1build1) over (1:3.1.1-1) ... Setting up libaudit1:riscv64 (1:3.1.1-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libselinux1_3.5-1build1_riscv64.deb ... Unpacking libselinux1:riscv64 (3.5-1build1) over (3.5-1) ... Setting up libselinux1:riscv64 (3.5-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libssl3_3.0.10-1ubuntu2.1_riscv64.deb ... Unpacking libssl3:riscv64 (3.0.10-1ubuntu2.1) over (3.0.10-1ubuntu2) ... Preparing to unpack .../systemd-sysv_253.5-1ubuntu7_riscv64.deb ... Unpacking systemd-sysv (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../systemd-dev_253.5-1ubuntu7_all.deb ... Unpacking systemd-dev (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libssl3:riscv64 (3.0.10-1ubuntu2.1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../systemd_253.5-1ubuntu7_riscv64.deb ... Unpacking systemd (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../libsystemd-shared_253.5-1ubuntu7_riscv64.deb ... Unpacking libsystemd-shared:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../libsystemd0_253.5-1ubuntu7_riscv64.deb ... Unpacking libsystemd0:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libsystemd0:riscv64 (253.5-1ubuntu7) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libudev1_253.5-1ubuntu7_riscv64.deb ... Unpacking libudev1:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libudev1:riscv64 (253.5-1ubuntu7) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libxxhash0_0.8.2-2_riscv64.deb ... Unpacking libxxhash0:riscv64 (0.8.2-2) over (0.8.1-1) ... Setting up libxxhash0:riscv64 (0.8.2-2) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libapt-pkg6.0_2.7.6_riscv64.deb ... Unpacking libapt-pkg6.0:riscv64 (2.7.6) over (2.7.3) ... Setting up libapt-pkg6.0:riscv64 (2.7.6) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../dpkg_1.22.1ubuntu1_riscv64.deb ... Unpacking dpkg (1.22.1ubuntu1) over (1.22.0ubuntu1) ... Setting up dpkg (1.22.1ubuntu1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../grep_3.11-3_riscv64.deb ... Unpacking grep (3.11-3) over (3.11-2) ... Setting up grep (3.11-3) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../ncurses-bin_6.4+20231016-1_riscv64.deb ... Unpacking ncurses-bin (6.4+20231016-1) over (6.4+20230625-2) ... Setting up ncurses-bin (6.4+20231016-1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../base-passwd_3.6.2_riscv64.deb ... Unpacking base-passwd (3.6.2) over (3.6.1) ... Setting up base-passwd (3.6.2) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../libc-bin_2.38-3ubuntu1_riscv64.deb ... Unpacking libc-bin (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Setting up libc-bin (2.38-3ubuntu1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../ncurses-base_6.4+20231016-1_all.deb ... Unpacking ncurses-base (6.4+20231016-1) over (6.4+20230625-2) ... Setting up ncurses-base (6.4+20231016-1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../libdb5.3_5.3.28+dfsg2-3_riscv64.deb ... Unpacking libdb5.3:riscv64 (5.3.28+dfsg2-3) over (5.3.28+dfsg2-2) ... Setting up libdb5.3:riscv64 (5.3.28+dfsg2-3) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../archives/apt_2.7.6_riscv64.deb ... Unpacking apt (2.7.6) over (2.7.3) ... Setting up apt (2.7.6) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../apt-utils_2.7.6_riscv64.deb ... Unpacking apt-utils (2.7.6) over (2.7.3) ... Selecting previously unselected package libunistring5:riscv64. Preparing to unpack .../libunistring5_1.1-2_riscv64.deb ... Unpacking libunistring5:riscv64 (1.1-2) ... Setting up libunistring5:riscv64 (1.1-2) ... (Reading database ... 13554 files and directories currently installed.) Preparing to unpack .../libidn2-0_2.3.4-1build1_riscv64.deb ... Unpacking libidn2-0:riscv64 (2.3.4-1build1) over (2.3.4-1) ... Setting up libidn2-0:riscv64 (2.3.4-1build1) ... (Reading database ... 13554 files and directories currently installed.) Preparing to unpack .../libgnutls30_3.8.1-4ubuntu3_riscv64.deb ... Unpacking libgnutls30:riscv64 (3.8.1-4ubuntu3) over (3.8.1-4ubuntu1) ... Setting up libgnutls30:riscv64 (3.8.1-4ubuntu3) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libsemanage-common_3.5-1build1_all.deb ... Unpacking libsemanage-common (3.5-1build1) over (3.5-1) ... Setting up libsemanage-common (3.5-1build1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libsemanage2_3.5-1build1_riscv64.deb ... Unpacking libsemanage2:riscv64 (3.5-1build1) over (3.5-1) ... Setting up libsemanage2:riscv64 (3.5-1build1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libncursesw6_6.4+20231016-1_riscv64.deb ... Unpacking libncursesw6:riscv64 (6.4+20231016-1) over (6.4+20230625-2) ... Preparing to unpack .../libtinfo6_6.4+20231016-1_riscv64.deb ... Unpacking libtinfo6:riscv64 (6.4+20231016-1) over (6.4+20230625-2) ... Setting up libtinfo6:riscv64 (6.4+20231016-1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../0-mawk_1.3.4.20230808-1_riscv64.deb ... Unpacking mawk (1.3.4.20230808-1) over (1.3.4.20230730-1) ... Preparing to unpack .../1-libargon2-1_0~20190702+dfsg-4_riscv64.deb ... Unpacking libargon2-1:riscv64 (0~20190702+dfsg-4) over (0~20190702+dfsg-3) ... Preparing to unpack .../2-libsqlite3-0_3.44.0-1_riscv64.deb ... Unpacking libsqlite3-0:riscv64 (3.44.0-1) over (3.42.0-1) ... Preparing to unpack .../3-openssl_3.0.10-1ubuntu2.1_riscv64.deb ... Unpacking openssl (3.0.10-1ubuntu2.1) over (3.0.10-1ubuntu2) ... Preparing to unpack .../4-bash-completion_1%3a2.11-8_all.deb ... Unpacking bash-completion (1:2.11-8) over (1:2.11-7) ... Preparing to unpack .../5-libpng16-16_1.6.40-2_riscv64.deb ... Unpacking libpng16-16:riscv64 (1.6.40-2) over (1.6.40-1) ... Preparing to unpack .../6-xz-utils_5.4.4-0.1_riscv64.deb ... Unpacking xz-utils (5.4.4-0.1) over (5.4.1-0.2) ... Preparing to unpack .../7-dpkg-dev_1.22.1ubuntu1_all.deb ... Unpacking dpkg-dev (1.22.1ubuntu1) over (1.22.0ubuntu1) ... Preparing to unpack .../8-libdpkg-perl_1.22.1ubuntu1_all.deb ... Unpacking libdpkg-perl (1.22.1ubuntu1) over (1.22.0ubuntu1) ... Preparing to unpack .../9-optipng_0.7.7-3_riscv64.deb ... Unpacking optipng (0.7.7-3) over (0.7.7-2build1) ... Setting up libapparmor1:riscv64 (4.0.0~alpha2-0ubuntu6) ... Setting up apt-utils (2.7.6) ... Setting up cpp-13 (13.2.0-6ubuntu1) ... Setting up libargon2-1:riscv64 (0~20190702+dfsg-4) ... Setting up libsqlite3-0:riscv64 (3.44.0-1) ... Setting up binutils-common:riscv64 (2.41-6ubuntu1) ... Setting up libctf-nobfd0:riscv64 (2.41-6ubuntu1) ... Setting up systemd-dev (253.5-1ubuntu7) ... Setting up libgomp1:riscv64 (13.2.0-6ubuntu1) ... Setting up libsframe1:riscv64 (2.41-6ubuntu1) ... Setting up bash-completion (1:2.11-8) ... Setting up xz-utils (5.4.4-0.1) ... Setting up libpng16-16:riscv64 (1.6.40-2) ... Setting up libatomic1:riscv64 (13.2.0-6ubuntu1) ... Setting up libsystemd-shared:riscv64 (253.5-1ubuntu7) ... Setting up libncursesw6:riscv64 (6.4+20231016-1) ... Setting up libdpkg-perl (1.22.1ubuntu1) ... Setting up libasan8:riscv64 (13.2.0-6ubuntu1) ... Setting up libnsl2:riscv64 (1.3.0-3) ... Setting up mawk (1.3.4.20230808-1) ... Setting up libbinutils:riscv64 (2.41-6ubuntu1) ... Setting up libc-dev-bin (2.38-3ubuntu1) ... Setting up openssl (3.0.10-1ubuntu2.1) ... Setting up libcc1-0:riscv64 (13.2.0-6ubuntu1) ... Setting up libctf0:riscv64 (2.41-6ubuntu1) ... Setting up binutils-riscv64-linux-gnu (2.41-6ubuntu1) ... Setting up systemd (253.5-1ubuntu7) ... Initializing machine ID from random generator. Setting up binutils (2.41-6ubuntu1) ... Setting up dpkg-dev (1.22.1ubuntu1) ... Setting up optipng (0.7.7-3) ... Setting up libgcc-13-dev:riscv64 (13.2.0-6ubuntu1) ... Setting up libnsl-dev:riscv64 (1.3.0-3) ... Setting up libc6-dev:riscv64 (2.38-3ubuntu1) ... Setting up libstdc++-13-dev:riscv64 (13.2.0-6ubuntu1) ... Setting up systemd-sysv (253.5-1ubuntu7) ... Setting up gcc-13 (13.2.0-6ubuntu1) ... Setting up g++-13 (13.2.0-6ubuntu1) ... Processing triggers for libc-bin (2.38-3ubuntu1) ... RUN: /usr/share/launchpad-buildd/bin/sbuild-package PACKAGEBUILD-26962111 riscv64 noble-proposed -c chroot:build-PACKAGEBUILD-26962111 --arch=riscv64 --dist=noble-proposed --nolog coq-hierarchy-builder_1.4.0-6build6.dsc Initiating build PACKAGEBUILD-26962111 with 8 jobs across 8 processor cores. Kernel reported to sbuild: 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 sbuild (Debian sbuild) 0.79.0 (05 February 2020) on riscv64-qemu-lgw01-085.buildd +===============================================================================+ | coq-hierarchy-builder 1.4.0-6build6 (riscv64) Sun, 05 Nov 2023 15:13:04 +0000 | +===============================================================================+ Package: coq-hierarchy-builder Version: 1.4.0-6build6 Source Version: 1.4.0-6build6 Distribution: noble-proposed Machine Architecture: riscv64 Host Architecture: riscv64 Build Architecture: riscv64 Build Type: any I: NOTICE: Log filtering will replace 'home/buildd/build-PACKAGEBUILD-26962111/chroot-autobuild' with '<>' I: NOTICE: Log filtering will replace 'build/coq-hierarchy-builder-VGvx4B/resolver-kG6vp0' with '<>' +------------------------------------------------------------------------------+ | Fetch source files | +------------------------------------------------------------------------------+ Local sources ------------- coq-hierarchy-builder_1.4.0-6build6.dsc exists in .; copying to chroot I: NOTICE: Log filtering will replace 'build/coq-hierarchy-builder-VGvx4B/coq-hierarchy-builder-1.4.0' with '<>' I: NOTICE: Log filtering will replace 'build/coq-hierarchy-builder-VGvx4B' with '<>' +------------------------------------------------------------------------------+ | Install package build dependencies | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff, build-essential, fakeroot Filtered Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff, build-essential, fakeroot dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/<>/apt_archive/sbuild-build-depends-main-dummy.deb'. Ign:1 copy:/<>/apt_archive ./ InRelease Get:2 copy:/<>/apt_archive ./ Release [957 B] Ign:3 copy:/<>/apt_archive ./ Release.gpg Get:4 copy:/<>/apt_archive ./ Sources [403 B] Get:5 copy:/<>/apt_archive ./ Packages [487 B] Fetched 1847 B in 0s (3718 B/s) Reading package lists... Reading package lists... Install main build dependencies (apt-based resolver) ---------------------------------------------------- Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following packages were automatically installed and are no longer required: apt-utils bash-completion ca-certificates debconf-i18n krb5-locales libgpg-error-l10n libgpm2 liblocale-gettext-perl libnss-nis libnss-nisplus libtext-charwidth-perl libtext-iconv-perl libtext-wrapi18n-perl libunistring2 openssl psmisc uuid-runtime Use 'apt autoremove' to remove them. The following additional packages will be installed: autoconf automake autopoint autotools-dev coq debhelper debugedit dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-core-ocaml-dev libcoq-elpi libcoq-stdlib libdebhelper-perl libdw1 libelf1 libelpi-ocaml libelpi-ocaml-dev libexpat1 libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1 libmenhir-ocaml-dev libncurses-dev libncurses6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.11-minimal libpython3.11-stdlib libre-ocaml-dev libresult-ocaml libresult-ocaml-dev libsexplib0-ocaml libsexplib0-ocaml-dev libstdlib-ocaml libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2 libzarith-ocaml libzarith-ocaml-dev m4 man-db media-types ocaml ocaml-base ocaml-findlib ocaml-interp ocaml-nox po-debconf python3 python3-minimal python3.11 python3.11-minimal wdiff Suggested packages: autoconf-archive gnu-standards autoconf-doc coqide | proofgeneral ledit | readline-editor why coq-doc dh-make git gettext-doc libasprintf-dev libgettextpo-dev groff gmp-doc libgmp10-doc libmpfr-dev ncurses-doc libtool-doc gfortran | fortran95-compiler gcj-jdk m4-doc apparmor less www-browser ocaml-doc elpa-tuareg camlp4 libmail-box-perl python3-doc python3-tk python3-venv python3.11-venv python3.11-doc binfmt-support wdiff-doc Recommended packages: curl | wget | lynx libarchive-cpio-perl ocaml-man libltdl-dev ledit | readline-editor libmail-sendmail-perl The following NEW packages will be installed: autoconf automake autopoint autotools-dev coq debhelper debugedit dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-core-ocaml-dev libcoq-elpi libcoq-stdlib libdebhelper-perl libdw1 libelf1 libelpi-ocaml libelpi-ocaml-dev libexpat1 libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1 libmenhir-ocaml-dev libncurses-dev libncurses6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.11-minimal libpython3.11-stdlib libre-ocaml-dev libresult-ocaml libresult-ocaml-dev libsexplib0-ocaml libsexplib0-ocaml-dev libstdlib-ocaml libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2 libzarith-ocaml libzarith-ocaml-dev m4 man-db media-types ocaml ocaml-base ocaml-findlib ocaml-interp ocaml-nox po-debconf python3 python3-minimal python3.11 python3.11-minimal sbuild-build-depends-main-dummy wdiff 0 upgraded, 78 newly installed, 0 to remove and 0 not upgraded. Need to get 429 MB of archives. After this operation, 1702 MB of additional disk space will be used. Get:1 copy:/<>/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [704 B] Get:2 http://ftpmaster.internal/ubuntu noble/main riscv64 libpython3.11-minimal riscv64 3.11.6-3 [834 kB] Get:3 http://ftpmaster.internal/ubuntu noble/main riscv64 libexpat1 riscv64 2.5.0-2 [78.2 kB] Get:4 http://ftpmaster.internal/ubuntu noble/main riscv64 python3.11-minimal riscv64 3.11.6-3 [2147 kB] Get:5 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 python3-minimal riscv64 3.11.4-5ubuntu1 [26.9 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main riscv64 media-types all 10.1.0 [27.5 kB] Get:7 http://ftpmaster.internal/ubuntu noble/main riscv64 libpython3.11-stdlib riscv64 3.11.6-3 [1906 kB] Get:8 http://ftpmaster.internal/ubuntu noble/main riscv64 python3.11 riscv64 3.11.6-3 [579 kB] Get:9 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libpython3-stdlib riscv64 3.11.4-5ubuntu1 [9568 B] Get:10 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 python3 riscv64 3.11.4-5ubuntu1 [22.9 kB] Get:11 http://ftpmaster.internal/ubuntu noble/main riscv64 libelf1 riscv64 0.189-4 [51.9 kB] Get:12 http://ftpmaster.internal/ubuntu noble/main riscv64 libicu72 riscv64 72.1-3ubuntu3 [10.8 MB] Get:13 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libxml2 riscv64 2.9.14+dfsg-1.3build1 [708 kB] Get:14 http://ftpmaster.internal/ubuntu noble/main riscv64 libmagic-mgc riscv64 1:5.45-2 [307 kB] Get:15 http://ftpmaster.internal/ubuntu noble/main riscv64 libmagic1 riscv64 1:5.45-2 [93.6 kB] Get:16 http://ftpmaster.internal/ubuntu noble/main riscv64 file riscv64 1:5.45-2 [21.7 kB] Get:17 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 gettext-base riscv64 0.21-13build1 [41.6 kB] Get:18 http://ftpmaster.internal/ubuntu noble/main riscv64 libuchardet0 riscv64 0.0.7-1build2 [78.9 kB] Get:19 http://ftpmaster.internal/ubuntu noble/main riscv64 groff-base riscv64 1.23.0-3 [1017 kB] Get:20 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libncurses6 riscv64 6.4+20231016-1 [113 kB] Get:21 http://ftpmaster.internal/ubuntu noble/main riscv64 libpipeline1 riscv64 1.5.7-1 [26.8 kB] Get:22 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 man-db riscv64 2.12.0-1 [1214 kB] Get:23 http://ftpmaster.internal/ubuntu noble/main riscv64 m4 riscv64 1.4.19-4 [261 kB] Get:24 http://ftpmaster.internal/ubuntu noble/main riscv64 autoconf all 2.71-3 [339 kB] Get:25 http://ftpmaster.internal/ubuntu noble/main riscv64 autotools-dev all 20220109.1 [44.9 kB] Get:26 http://ftpmaster.internal/ubuntu noble/main riscv64 automake all 1:1.16.5-1.3 [558 kB] Get:27 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 autopoint all 0.21-13build1 [422 kB] Get:28 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-stdlib riscv64 8.17.0+dfsg-1build2 [28.4 MB] Get:29 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libstdlib-ocaml riscv64 4.14.1-1ubuntu1 [381 kB] Get:30 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-base riscv64 4.14.1-1ubuntu1 [260 kB] Get:31 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libfindlib-ocaml riscv64 1.9.6-1build2 [200 kB] Get:32 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libzarith-ocaml riscv64 1.13-2build1 [121 kB] Get:33 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-core-ocaml riscv64 8.17.0+dfsg-1build2 [27.4 MB] Get:34 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libstdlib-ocaml-dev riscv64 4.14.1-1ubuntu1 [10.4 MB] Get:35 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcompiler-libs-ocaml-dev riscv64 4.14.1-1ubuntu1 [41.5 MB] Get:36 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-interp riscv64 4.14.1-1ubuntu1 [7825 kB] Get:37 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libncurses-dev riscv64 6.4+20231016-1 [986 kB] Get:38 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml riscv64 4.14.1-1ubuntu1 [82.2 MB] Get:39 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-nox all 4.14.1-1ubuntu1 [4716 B] Get:40 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-findlib riscv64 1.9.6-1build2 [578 kB] Get:41 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 coq riscv64 8.17.0+dfsg-1build2 [96.1 MB] Get:42 http://ftpmaster.internal/ubuntu noble/main riscv64 libdebhelper-perl all 13.11.7ubuntu1 [85.8 kB] Get:43 http://ftpmaster.internal/ubuntu noble/main riscv64 libtool all 2.4.7-7 [166 kB] Get:44 http://ftpmaster.internal/ubuntu noble/main riscv64 dh-autoreconf all 20 [16.1 kB] Get:45 http://ftpmaster.internal/ubuntu noble/main riscv64 libarchive-zip-perl all 1.68-1 [90.2 kB] Get:46 http://ftpmaster.internal/ubuntu noble/main riscv64 libsub-override-perl all 0.09-4 [8706 B] Get:47 http://ftpmaster.internal/ubuntu noble/main riscv64 libfile-stripnondeterminism-perl all 1.13.1-1 [18.1 kB] Get:48 http://ftpmaster.internal/ubuntu noble/main riscv64 dh-strip-nondeterminism all 1.13.1-1 [5362 B] Get:49 http://ftpmaster.internal/ubuntu noble/main riscv64 libdw1 riscv64 0.189-4 [234 kB] Get:50 http://ftpmaster.internal/ubuntu noble/main riscv64 debugedit riscv64 1:5.0-5 [48.8 kB] Get:51 http://ftpmaster.internal/ubuntu noble/main riscv64 dwz riscv64 0.15-1 [115 kB] Get:52 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 gettext riscv64 0.21-13build1 [867 kB] Get:53 http://ftpmaster.internal/ubuntu noble/main riscv64 intltool-debian all 0.35.0+20060710.6 [23.2 kB] Get:54 http://ftpmaster.internal/ubuntu noble/main riscv64 po-debconf all 1.0.21+nmu1 [233 kB] Get:55 http://ftpmaster.internal/ubuntu noble/main riscv64 debhelper all 13.11.7ubuntu1 [940 kB] Get:56 http://ftpmaster.internal/ubuntu noble/universe riscv64 dh-coq all 0.6 [7630 B] Get:57 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libfindlib-ocaml-dev riscv64 1.9.6-1build2 [226 kB] Get:58 http://ftpmaster.internal/ubuntu noble/main riscv64 libgmpxx4ldbl riscv64 2:6.3.0+dfsg-2ubuntu4 [9858 B] Get:59 http://ftpmaster.internal/ubuntu noble/main riscv64 libgmp-dev riscv64 2:6.3.0+dfsg-2ubuntu4 [792 kB] Get:60 http://ftpmaster.internal/ubuntu noble/main riscv64 libgmp3-dev riscv64 2:6.3.0+dfsg-2ubuntu4 [2312 B] Get:61 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libzarith-ocaml-dev riscv64 1.13-2build1 [168 kB] Get:62 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-core-ocaml-dev riscv64 8.17.0+dfsg-1build2 [57.3 MB] Get:63 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libresult-ocaml riscv64 1.5-4build1 [7292 B] Get:64 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libsexplib0-ocaml riscv64 0.16.0-3build1 [130 kB] Get:65 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libppx-deriving-ocaml riscv64 5.2.1-4build1 [4688 kB] Get:66 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libelpi-ocaml riscv64 1.17.0-1build5 [4887 kB] Get:67 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libmenhir-ocaml-dev riscv64 20230608+ds-1build1 [704 kB] Get:68 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libocaml-compiler-libs-ocaml-dev riscv64 0.12.4-4build1 [98.5 kB] Get:69 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libppx-derivers-ocaml-dev riscv64 1.2.1-4build1 [17.8 kB] Get:70 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libsexplib0-ocaml-dev riscv64 0.16.0-3build1 [306 kB] Get:71 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libppxlib-ocaml-dev riscv64 0.31.0-1 [20.7 MB] Get:72 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libresult-ocaml-dev riscv64 1.5-4build1 [11.7 kB] Get:73 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libppx-deriving-ocaml-dev riscv64 5.2.1-4build1 [1060 kB] Get:74 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libre-ocaml-dev riscv64 1.11.0-1build1 [1186 kB] Get:75 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libelpi-ocaml-dev riscv64 1.17.0-1build5 [12.3 MB] Get:76 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-elpi riscv64 1.17.1-1build9 [3085 kB] Get:77 http://ftpmaster.internal/ubuntu noble/main riscv64 wdiff riscv64 1.2.2-6 [29.6 kB] Get:78 http://ftpmaster.internal/ubuntu noble/universe riscv64 dh-ocaml all 2.0 [75.7 kB] Preconfiguring packages ... Fetched 429 MB in 1min 36s (4459 kB/s) Selecting previously unselected package libpython3.11-minimal:riscv64. (Reading database ... 13554 files and directories currently installed.) Preparing to unpack .../libpython3.11-minimal_3.11.6-3_riscv64.deb ... Unpacking libpython3.11-minimal:riscv64 (3.11.6-3) ... Selecting previously unselected package libexpat1:riscv64. Preparing to unpack .../libexpat1_2.5.0-2_riscv64.deb ... Unpacking libexpat1:riscv64 (2.5.0-2) ... Selecting previously unselected package python3.11-minimal. Preparing to unpack .../python3.11-minimal_3.11.6-3_riscv64.deb ... Unpacking python3.11-minimal (3.11.6-3) ... Setting up libpython3.11-minimal:riscv64 (3.11.6-3) ... Setting up libexpat1:riscv64 (2.5.0-2) ... Setting up python3.11-minimal (3.11.6-3) ... Selecting previously unselected package python3-minimal. (Reading database ... 13868 files and directories currently installed.) Preparing to unpack .../python3-minimal_3.11.4-5ubuntu1_riscv64.deb ... Unpacking python3-minimal (3.11.4-5ubuntu1) ... Selecting previously unselected package media-types. Preparing to unpack .../media-types_10.1.0_all.deb ... Unpacking media-types (10.1.0) ... Selecting previously unselected package libpython3.11-stdlib:riscv64. Preparing to unpack .../libpython3.11-stdlib_3.11.6-3_riscv64.deb ... Unpacking libpython3.11-stdlib:riscv64 (3.11.6-3) ... Selecting previously unselected package python3.11. Preparing to unpack .../python3.11_3.11.6-3_riscv64.deb ... Unpacking python3.11 (3.11.6-3) ... Selecting previously unselected package libpython3-stdlib:riscv64. Preparing to unpack .../libpython3-stdlib_3.11.4-5ubuntu1_riscv64.deb ... Unpacking libpython3-stdlib:riscv64 (3.11.4-5ubuntu1) ... Setting up python3-minimal (3.11.4-5ubuntu1) ... Selecting previously unselected package python3. (Reading database ... 14284 files and directories currently installed.) Preparing to unpack .../00-python3_3.11.4-5ubuntu1_riscv64.deb ... Unpacking python3 (3.11.4-5ubuntu1) ... Selecting previously unselected package libelf1:riscv64. Preparing to unpack .../01-libelf1_0.189-4_riscv64.deb ... Unpacking libelf1:riscv64 (0.189-4) ... Selecting previously unselected package libicu72:riscv64. Preparing to unpack .../02-libicu72_72.1-3ubuntu3_riscv64.deb ... Unpacking libicu72:riscv64 (72.1-3ubuntu3) ... Selecting previously unselected package libxml2:riscv64. Preparing to unpack .../03-libxml2_2.9.14+dfsg-1.3build1_riscv64.deb ... Unpacking libxml2:riscv64 (2.9.14+dfsg-1.3build1) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../04-libmagic-mgc_1%3a5.45-2_riscv64.deb ... Unpacking libmagic-mgc (1:5.45-2) ... Selecting previously unselected package libmagic1:riscv64. Preparing to unpack .../05-libmagic1_1%3a5.45-2_riscv64.deb ... Unpacking libmagic1:riscv64 (1:5.45-2) ... Selecting previously unselected package file. Preparing to unpack .../06-file_1%3a5.45-2_riscv64.deb ... Unpacking file (1:5.45-2) ... Selecting previously unselected package gettext-base. Preparing to unpack .../07-gettext-base_0.21-13build1_riscv64.deb ... Unpacking gettext-base (0.21-13build1) ... Selecting previously unselected package libuchardet0:riscv64. Preparing to unpack .../08-libuchardet0_0.0.7-1build2_riscv64.deb ... Unpacking libuchardet0:riscv64 (0.0.7-1build2) ... Selecting previously unselected package groff-base. Preparing to unpack .../09-groff-base_1.23.0-3_riscv64.deb ... Unpacking groff-base (1.23.0-3) ... Selecting previously unselected package libncurses6:riscv64. Preparing to unpack .../10-libncurses6_6.4+20231016-1_riscv64.deb ... Unpacking libncurses6:riscv64 (6.4+20231016-1) ... Selecting previously unselected package libpipeline1:riscv64. Preparing to unpack .../11-libpipeline1_1.5.7-1_riscv64.deb ... Unpacking libpipeline1:riscv64 (1.5.7-1) ... Selecting previously unselected package man-db. Preparing to unpack .../12-man-db_2.12.0-1_riscv64.deb ... Unpacking man-db (2.12.0-1) ... Selecting previously unselected package m4. Preparing to unpack .../13-m4_1.4.19-4_riscv64.deb ... Unpacking m4 (1.4.19-4) ... Selecting previously unselected package autoconf. Preparing to unpack .../14-autoconf_2.71-3_all.deb ... Unpacking autoconf (2.71-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../15-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../16-automake_1%3a1.16.5-1.3_all.deb ... Unpacking automake (1:1.16.5-1.3) ... Selecting previously unselected package autopoint. Preparing to unpack .../17-autopoint_0.21-13build1_all.deb ... Unpacking autopoint (0.21-13build1) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../18-libcoq-stdlib_8.17.0+dfsg-1build2_riscv64.deb ... Unpacking libcoq-stdlib (8.17.0+dfsg-1build2) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../19-libstdlib-ocaml_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libstdlib-ocaml (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../20-ocaml-base_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml-base (4.14.1-1ubuntu1) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../21-libfindlib-ocaml_1.9.6-1build2_riscv64.deb ... Unpacking libfindlib-ocaml (1.9.6-1build2) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../22-libzarith-ocaml_1.13-2build1_riscv64.deb ... Unpacking libzarith-ocaml (1.13-2build1) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../23-libcoq-core-ocaml_8.17.0+dfsg-1build2_riscv64.deb ... Unpacking libcoq-core-ocaml (8.17.0+dfsg-1build2) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../24-libstdlib-ocaml-dev_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../25-libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../26-ocaml-interp_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml-interp (4.14.1-1ubuntu1) ... Selecting previously unselected package libncurses-dev:riscv64. Preparing to unpack .../27-libncurses-dev_6.4+20231016-1_riscv64.deb ... Unpacking libncurses-dev:riscv64 (6.4+20231016-1) ... Selecting previously unselected package ocaml. Preparing to unpack .../28-ocaml_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-nox. Preparing to unpack .../29-ocaml-nox_4.14.1-1ubuntu1_all.deb ... Unpacking ocaml-nox (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../30-ocaml-findlib_1.9.6-1build2_riscv64.deb ... Unpacking ocaml-findlib (1.9.6-1build2) ... Selecting previously unselected package coq. Preparing to unpack .../31-coq_8.17.0+dfsg-1build2_riscv64.deb ... Unpacking coq (8.17.0+dfsg-1build2) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../32-libdebhelper-perl_13.11.7ubuntu1_all.deb ... Unpacking libdebhelper-perl (13.11.7ubuntu1) ... Selecting previously unselected package libtool. Preparing to unpack .../33-libtool_2.4.7-7_all.deb ... Unpacking libtool (2.4.7-7) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../34-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../35-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libsub-override-perl. Preparing to unpack .../36-libsub-override-perl_0.09-4_all.deb ... Unpacking libsub-override-perl (0.09-4) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../37-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../38-dh-strip-nondeterminism_1.13.1-1_all.deb ... Unpacking dh-strip-nondeterminism (1.13.1-1) ... Selecting previously unselected package libdw1:riscv64. Preparing to unpack .../39-libdw1_0.189-4_riscv64.deb ... Unpacking libdw1:riscv64 (0.189-4) ... Selecting previously unselected package debugedit. Preparing to unpack .../40-debugedit_1%3a5.0-5_riscv64.deb ... Unpacking debugedit (1:5.0-5) ... Selecting previously unselected package dwz. Preparing to unpack .../41-dwz_0.15-1_riscv64.deb ... Unpacking dwz (0.15-1) ... Selecting previously unselected package gettext. Preparing to unpack .../42-gettext_0.21-13build1_riscv64.deb ... Unpacking gettext (0.21-13build1) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../43-intltool-debian_0.35.0+20060710.6_all.deb ... Unpacking intltool-debian (0.35.0+20060710.6) ... Selecting previously unselected package po-debconf. Preparing to unpack .../44-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../45-debhelper_13.11.7ubuntu1_all.deb ... Unpacking debhelper (13.11.7ubuntu1) ... Selecting previously unselected package dh-coq. Preparing to unpack .../46-dh-coq_0.6_all.deb ... Unpacking dh-coq (0.6) ... Selecting previously unselected package libfindlib-ocaml-dev. Preparing to unpack .../47-libfindlib-ocaml-dev_1.9.6-1build2_riscv64.deb ... Unpacking libfindlib-ocaml-dev (1.9.6-1build2) ... Selecting previously unselected package libgmpxx4ldbl:riscv64. Preparing to unpack .../48-libgmpxx4ldbl_2%3a6.3.0+dfsg-2ubuntu4_riscv64.deb ... Unpacking libgmpxx4ldbl:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Selecting previously unselected package libgmp-dev:riscv64. Preparing to unpack .../49-libgmp-dev_2%3a6.3.0+dfsg-2ubuntu4_riscv64.deb ... Unpacking libgmp-dev:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Selecting previously unselected package libgmp3-dev:riscv64. Preparing to unpack .../50-libgmp3-dev_2%3a6.3.0+dfsg-2ubuntu4_riscv64.deb ... Unpacking libgmp3-dev:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Selecting previously unselected package libzarith-ocaml-dev. Preparing to unpack .../51-libzarith-ocaml-dev_1.13-2build1_riscv64.deb ... Unpacking libzarith-ocaml-dev (1.13-2build1) ... Selecting previously unselected package libcoq-core-ocaml-dev. Preparing to unpack .../52-libcoq-core-ocaml-dev_8.17.0+dfsg-1build2_riscv64.deb ... Unpacking libcoq-core-ocaml-dev (8.17.0+dfsg-1build2) ... Selecting previously unselected package libresult-ocaml. Preparing to unpack .../53-libresult-ocaml_1.5-4build1_riscv64.deb ... Unpacking libresult-ocaml (1.5-4build1) ... Selecting previously unselected package libsexplib0-ocaml. Preparing to unpack .../54-libsexplib0-ocaml_0.16.0-3build1_riscv64.deb ... Unpacking libsexplib0-ocaml (0.16.0-3build1) ... Selecting previously unselected package libppx-deriving-ocaml. Preparing to unpack .../55-libppx-deriving-ocaml_5.2.1-4build1_riscv64.deb ... Unpacking libppx-deriving-ocaml (5.2.1-4build1) ... Selecting previously unselected package libelpi-ocaml. Preparing to unpack .../56-libelpi-ocaml_1.17.0-1build5_riscv64.deb ... Unpacking libelpi-ocaml (1.17.0-1build5) ... Selecting previously unselected package libmenhir-ocaml-dev. Preparing to unpack .../57-libmenhir-ocaml-dev_20230608+ds-1build1_riscv64.deb ... Unpacking libmenhir-ocaml-dev (20230608+ds-1build1) ... Selecting previously unselected package libocaml-compiler-libs-ocaml-dev. Preparing to unpack .../58-libocaml-compiler-libs-ocaml-dev_0.12.4-4build1_riscv64.deb ... Unpacking libocaml-compiler-libs-ocaml-dev (0.12.4-4build1) ... Selecting previously unselected package libppx-derivers-ocaml-dev. Preparing to unpack .../59-libppx-derivers-ocaml-dev_1.2.1-4build1_riscv64.deb ... Unpacking libppx-derivers-ocaml-dev (1.2.1-4build1) ... Selecting previously unselected package libsexplib0-ocaml-dev. Preparing to unpack .../60-libsexplib0-ocaml-dev_0.16.0-3build1_riscv64.deb ... Unpacking libsexplib0-ocaml-dev (0.16.0-3build1) ... Selecting previously unselected package libppxlib-ocaml-dev. Preparing to unpack .../61-libppxlib-ocaml-dev_0.31.0-1_riscv64.deb ... Unpacking libppxlib-ocaml-dev (0.31.0-1) ... Selecting previously unselected package libresult-ocaml-dev. Preparing to unpack .../62-libresult-ocaml-dev_1.5-4build1_riscv64.deb ... Unpacking libresult-ocaml-dev (1.5-4build1) ... Selecting previously unselected package libppx-deriving-ocaml-dev. Preparing to unpack .../63-libppx-deriving-ocaml-dev_5.2.1-4build1_riscv64.deb ... Unpacking libppx-deriving-ocaml-dev (5.2.1-4build1) ... Selecting previously unselected package libre-ocaml-dev. Preparing to unpack .../64-libre-ocaml-dev_1.11.0-1build1_riscv64.deb ... Unpacking libre-ocaml-dev (1.11.0-1build1) ... Selecting previously unselected package libelpi-ocaml-dev. Preparing to unpack .../65-libelpi-ocaml-dev_1.17.0-1build5_riscv64.deb ... Unpacking libelpi-ocaml-dev (1.17.0-1build5) ... Selecting previously unselected package libcoq-elpi. Preparing to unpack .../66-libcoq-elpi_1.17.1-1build9_riscv64.deb ... Unpacking libcoq-elpi (1.17.1-1build9) ... Selecting previously unselected package wdiff. Preparing to unpack .../67-wdiff_1.2.2-6_riscv64.deb ... Unpacking wdiff (1.2.2-6) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../68-dh-ocaml_2.0_all.deb ... Unpacking dh-ocaml (2.0) ... Selecting previously unselected package sbuild-build-depends-main-dummy. Preparing to unpack .../69-sbuild-build-depends-main-dummy_0.invalid.0_riscv64.deb ... Unpacking sbuild-build-depends-main-dummy (0.invalid.0) ... Setting up media-types (10.1.0) ... Setting up libpipeline1:riscv64 (1.5.7-1) ... Setting up wdiff (1.2.2-6) ... Setting up libicu72:riscv64 (72.1-3ubuntu3) ... Setting up libmagic-mgc (1:5.45-2) ... Setting up dh-coq (0.6) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libpython3.11-stdlib:riscv64 (3.11.6-3) ... Setting up libdebhelper-perl (13.11.7ubuntu1) ... Setting up dh-ocaml (2.0) ... Setting up libmagic1:riscv64 (1:5.45-2) ... Setting up gettext-base (0.21-13build1) ... Setting up m4 (1.4.19-4) ... Setting up file (1:5.45-2) ... Setting up autotools-dev (20220109.1) ... Setting up libcoq-stdlib (8.17.0+dfsg-1build2) ... Setting up libgmpxx4ldbl:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Setting up libncurses6:riscv64 (6.4+20231016-1) ... Setting up libstdlib-ocaml (4.14.1-1ubuntu1) ... Setting up autopoint (0.21-13build1) ... Setting up ocaml-base (4.14.1-1ubuntu1) ... Setting up autoconf (2.71-3) ... Setting up libsexplib0-ocaml (0.16.0-3build1) ... Setting up libuchardet0:riscv64 (0.0.7-1build2) ... Setting up libsub-override-perl (0.09-4) ... Setting up libresult-ocaml (1.5-4build1) ... Setting up libelf1:riscv64 (0.189-4) ... Setting up libxml2:riscv64 (2.9.14+dfsg-1.3build1) ... Setting up libpython3-stdlib:riscv64 (3.11.4-5ubuntu1) ... Setting up automake (1:1.16.5-1.3) ... update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode Setting up libfile-stripnondeterminism-perl (1.13.1-1) ... Setting up libppx-deriving-ocaml (5.2.1-4build1) ... Setting up python3.11 (3.11.6-3) ... Setting up libdw1:riscv64 (0.189-4) ... Setting up libncurses-dev:riscv64 (6.4+20231016-1) ... Setting up gettext (0.21-13build1) ... Setting up libgmp-dev:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Setting up libtool (2.4.7-7) ... Setting up libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... Setting up libfindlib-ocaml (1.9.6-1build2) ... Setting up python3 (3.11.4-5ubuntu1) ... Setting up libzarith-ocaml (1.13-2build1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... Setting up ocaml-interp (4.14.1-1ubuntu1) ... Setting up ocaml-findlib (1.9.6-1build2) ... Setting up dh-strip-nondeterminism (1.13.1-1) ... Setting up libelpi-ocaml (1.17.0-1build5) ... Setting up dwz (0.15-1) ... Setting up libcoq-core-ocaml (8.17.0+dfsg-1build2) ... Setting up groff-base (1.23.0-3) ... Setting up libgmp3-dev:riscv64 (2:6.3.0+dfsg-2ubuntu4) ... Setting up debugedit (1:5.0-5) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up ocaml (4.14.1-1ubuntu1) ... Setting up man-db (2.12.0-1) ... Not building database; man-db/auto-update is not 'true'. Created symlink /etc/systemd/system/timers.target.wants/man-db.timer → /lib/systemd/system/man-db.timer. Setting up libre-ocaml-dev (1.11.0-1build1) ... Setting up libmenhir-ocaml-dev (20230608+ds-1build1) ... Setting up libocaml-compiler-libs-ocaml-dev (0.12.4-4build1) ... Setting up libfindlib-ocaml-dev (1.9.6-1build2) ... Setting up ocaml-nox (4.14.1-1ubuntu1) ... Setting up libsexplib0-ocaml-dev (0.16.0-3build1) ... Setting up coq (8.17.0+dfsg-1build2) ... Setting up libresult-ocaml-dev (1.5-4build1) ... Setting up libzarith-ocaml-dev (1.13-2build1) ... Setting up libppx-derivers-ocaml-dev (1.2.1-4build1) ... Setting up libppxlib-ocaml-dev (0.31.0-1) ... Setting up debhelper (13.11.7ubuntu1) ... Setting up libcoq-core-ocaml-dev (8.17.0+dfsg-1build2) ... Setting up libppx-deriving-ocaml-dev (5.2.1-4build1) ... Setting up libelpi-ocaml-dev (1.17.0-1build5) ... Setting up libcoq-elpi (1.17.1-1build9) ... Setting up sbuild-build-depends-main-dummy (0.invalid.0) ... Processing triggers for systemd (253.5-1ubuntu7) ... Processing triggers for libc-bin (2.38-3ubuntu1) ... +------------------------------------------------------------------------------+ | Check architectures | +------------------------------------------------------------------------------+ Arch check ok (riscv64 included in any) +------------------------------------------------------------------------------+ | Build environment | +------------------------------------------------------------------------------+ Kernel: Linux 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 (riscv64) Toolchain package versions: binutils_2.41-6ubuntu1 dpkg-dev_1.22.1ubuntu1 g++-13_13.2.0-6ubuntu1 gcc-13_13.2.0-6ubuntu1 libc6-dev_2.38-3ubuntu1 libstdc++-13-dev_13.2.0-6ubuntu1 libstdc++6_13.2.0-6ubuntu1 linux-libc-dev_6.5.0-9.9 Package versions: adduser_3.137ubuntu1 advancecomp_2.5-1 apt_2.7.6 apt-utils_2.7.6 autoconf_2.71-3 automake_1:1.16.5-1.3 autopoint_0.21-13build1 autotools-dev_20220109.1 base-files_13ubuntu4 base-passwd_3.6.2 bash_5.2.15-2ubuntu1 bash-completion_1:2.11-8 binutils_2.41-6ubuntu1 binutils-common_2.41-6ubuntu1 binutils-riscv64-linux-gnu_2.41-6ubuntu1 bsdextrautils_2.39.1-4ubuntu2 bsdutils_1:2.39.1-4ubuntu2 build-essential_12.10ubuntu1 bzip2_1.0.8-5build1 ca-certificates_20230311ubuntu1 coq_8.17.0+dfsg-1build2 coreutils_9.1-1ubuntu2 cpp_4:13.2.0-1ubuntu1 cpp-13_13.2.0-6ubuntu1 dash_0.5.12-6ubuntu1 debconf_1.5.82 debconf-i18n_1.5.82 debhelper_13.11.7ubuntu1 debianutils_5.14 debugedit_1:5.0-5 dh-autoreconf_20 dh-coq_0.6 dh-ocaml_2.0 dh-strip-nondeterminism_1.13.1-1 diffutils_1:3.10-1 dpkg_1.22.1ubuntu1 dpkg-dev_1.22.1ubuntu1 dwz_0.15-1 e2fsprogs_1.47.0-2ubuntu1 fakeroot_1.32.1-1 file_1:5.45-2 findutils_4.9.0-5 g++_4:13.2.0-1ubuntu1 g++-13_13.2.0-6ubuntu1 gcc_4:13.2.0-1ubuntu1 gcc-13_13.2.0-6ubuntu1 gcc-13-base_13.2.0-6ubuntu1 gettext_0.21-13build1 gettext-base_0.21-13build1 gpg_2.2.40-1.1ubuntu1 gpg-agent_2.2.40-1.1ubuntu1 gpgconf_2.2.40-1.1ubuntu1 gpgv_2.2.40-1.1ubuntu1 grep_3.11-3 groff-base_1.23.0-3 gzip_1.12-1ubuntu1 hostname_3.23+nmu1ubuntu1 init_1.65.2ubuntu1 init-system-helpers_1.65.2ubuntu1 intltool-debian_0.35.0+20060710.6 krb5-locales_1.20.1-3ubuntu1 libacl1_2.3.1-3 libapparmor1_4.0.0~alpha2-0ubuntu6 libapt-pkg6.0_2.7.6 libarchive-zip-perl_1.68-1 libargon2-1_0~20190702+dfsg-4 libasan8_13.2.0-6ubuntu1 libassuan0_2.5.6-1 libatomic1_13.2.0-6ubuntu1 libattr1_1:2.5.1-4 libaudit-common_1:3.1.1-1build1 libaudit1_1:3.1.1-1build1 libbinutils_2.41-6ubuntu1 libblkid1_2.39.1-4ubuntu2 libbz2-1.0_1.0.8-5build1 libc-bin_2.38-3ubuntu1 libc-dev-bin_2.38-3ubuntu1 libc6_2.38-3ubuntu1 libc6-dev_2.38-3ubuntu1 libcap-ng0_0.8.3-1build3 libcap2_1:2.66-4ubuntu1 libcc1-0_13.2.0-6ubuntu1 libcom-err2_1.47.0-2ubuntu1 libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1 libcoq-core-ocaml_8.17.0+dfsg-1build2 libcoq-core-ocaml-dev_8.17.0+dfsg-1build2 libcoq-elpi_1.17.1-1build9 libcoq-stdlib_8.17.0+dfsg-1build2 libcrypt-dev_1:4.4.36-2 libcrypt1_1:4.4.36-2 libcryptsetup12_2:2.6.1-4ubuntu3 libctf-nobfd0_2.41-6ubuntu1 libctf0_2.41-6ubuntu1 libdb5.3_5.3.28+dfsg2-3 libdebconfclient0_0.270ubuntu1 libdebhelper-perl_13.11.7ubuntu1 libdevmapper1.02.1_2:1.02.185-2ubuntu1 libdpkg-perl_1.22.1ubuntu1 libdw1_0.189-4 libelf1_0.189-4 libelpi-ocaml_1.17.0-1build5 libelpi-ocaml-dev_1.17.0-1build5 libexpat1_2.5.0-2 libext2fs2_1.47.0-2ubuntu1 libfakeroot_1.32.1-1 libfdisk1_2.39.1-4ubuntu2 libffi8_3.4.4-1 libfile-stripnondeterminism-perl_1.13.1-1 libfindlib-ocaml_1.9.6-1build2 libfindlib-ocaml-dev_1.9.6-1build2 libgcc-13-dev_13.2.0-6ubuntu1 libgcc-s1_13.2.0-6ubuntu1 libgcrypt20_1.10.2-3ubuntu1 libgdbm-compat4_1.23-3 libgdbm6_1.23-3 libgmp-dev_2:6.3.0+dfsg-2ubuntu4 libgmp10_2:6.3.0+dfsg-2ubuntu4 libgmp3-dev_2:6.3.0+dfsg-2ubuntu4 libgmpxx4ldbl_2:6.3.0+dfsg-2ubuntu4 libgnutls30_3.8.1-4ubuntu3 libgomp1_13.2.0-6ubuntu1 libgpg-error-l10n_1.47-2 libgpg-error0_1.47-2 libgpm2_1.20.7-10build1 libgssapi-krb5-2_1.20.1-3ubuntu1 libhogweed6_3.9.1-2 libicu72_72.1-3ubuntu3 libidn2-0_2.3.4-1build1 libip4tc2_1.8.9-2ubuntu2 libisl23_0.26-3 libjansson4_2.14-2 libjson-c5_0.17-1 libk5crypto3_1.20.1-3ubuntu1 libkeyutils1_1.6.3-2 libkmod2_30+20230519-1ubuntu3 libkrb5-3_1.20.1-3ubuntu1 libkrb5support0_1.20.1-3ubuntu1 liblocale-gettext-perl_1.07-6 liblockfile-bin_1.17-1build2 liblockfile1_1.17-1build2 liblz4-1_1.9.4-1 liblzma5_5.4.4-0.1 libmagic-mgc_1:5.45-2 libmagic1_1:5.45-2 libmd0_1.1.0-1 libmenhir-ocaml-dev_20230608+ds-1build1 libmount1_2.39.1-4ubuntu2 libmpc3_1.3.1-1 libmpfr6_4.2.1-1 libncurses-dev_6.4+20231016-1 libncurses6_6.4+20231016-1 libncursesw6_6.4+20231016-1 libnettle8_3.9.1-2 libnpth0_1.6-3build2 libnsl-dev_1.3.0-3 libnsl2_1.3.0-3 libnss-nis_3.1-0ubuntu6 libnss-nisplus_1.3-0ubuntu6 libocaml-compiler-libs-ocaml-dev_0.12.4-4build1 libp11-kit0_0.25.0-4ubuntu1 libpam-modules_1.5.2-6ubuntu1 libpam-modules-bin_1.5.2-6ubuntu1 libpam-runtime_1.5.2-6ubuntu1 libpam0g_1.5.2-6ubuntu1 libpcre2-8-0_10.42-4 libperl5.36_5.36.0-9ubuntu1 libpipeline1_1.5.7-1 libpng16-16_1.6.40-2 libppx-derivers-ocaml-dev_1.2.1-4build1 libppx-deriving-ocaml_5.2.1-4build1 libppx-deriving-ocaml-dev_5.2.1-4build1 libppxlib-ocaml-dev_0.31.0-1 libproc2-0_2:4.0.3-1ubuntu1 libpython3-stdlib_3.11.4-5ubuntu1 libpython3.11-minimal_3.11.6-3 libpython3.11-stdlib_3.11.6-3 libre-ocaml-dev_1.11.0-1build1 libreadline8_8.2-1.3 libresult-ocaml_1.5-4build1 libresult-ocaml-dev_1.5-4build1 libseccomp2_2.5.4-1ubuntu3 libselinux1_3.5-1build1 libsemanage-common_3.5-1build1 libsemanage2_3.5-1build1 libsepol2_3.5-1 libsexplib0-ocaml_0.16.0-3build1 libsexplib0-ocaml-dev_0.16.0-3build1 libsframe1_2.41-6ubuntu1 libsmartcols1_2.39.1-4ubuntu2 libsqlite3-0_3.44.0-1 libss2_1.47.0-2ubuntu1 libssl3_3.0.10-1ubuntu2.1 libstdc++-13-dev_13.2.0-6ubuntu1 libstdc++6_13.2.0-6ubuntu1 libstdlib-ocaml_4.14.1-1ubuntu1 libstdlib-ocaml-dev_4.14.1-1ubuntu1 libsub-override-perl_0.09-4 libsystemd-shared_253.5-1ubuntu7 libsystemd0_253.5-1ubuntu7 libtasn1-6_4.19.0-3 libtext-charwidth-perl_0.04-11 libtext-iconv-perl_1.7-8 libtext-wrapi18n-perl_0.06-10 libtinfo6_6.4+20231016-1 libtirpc-common_1.3.3+ds-1 libtirpc-dev_1.3.3+ds-1 libtirpc3_1.3.3+ds-1 libtool_2.4.7-7 libuchardet0_0.0.7-1build2 libudev1_253.5-1ubuntu7 libunistring2_1.0-2 libunistring5_1.1-2 libuuid1_2.39.1-4ubuntu2 libxml2_2.9.14+dfsg-1.3build1 libxxhash0_0.8.2-2 libzarith-ocaml_1.13-2build1 libzarith-ocaml-dev_1.13-2build1 libzstd1_1.5.5+dfsg2-2 linux-libc-dev_6.5.0-9.9 lockfile-progs_0.1.19build1 login_1:4.13+dfsg1-1ubuntu1 logsave_1.47.0-2ubuntu1 lto-disabled-list_43 m4_1.4.19-4 make_4.3-4.1build1 man-db_2.12.0-1 mawk_1.3.4.20230808-1 media-types_10.1.0 mount_2.39.1-4ubuntu2 ncurses-base_6.4+20231016-1 ncurses-bin_6.4+20231016-1 ocaml_4.14.1-1ubuntu1 ocaml-base_4.14.1-1ubuntu1 ocaml-findlib_1.9.6-1build2 ocaml-interp_4.14.1-1ubuntu1 ocaml-nox_4.14.1-1ubuntu1 openssl_3.0.10-1ubuntu2.1 optipng_0.7.7-3 passwd_1:4.13+dfsg1-1ubuntu1 patch_2.7.6-7build2 perl_5.36.0-9ubuntu1 perl-base_5.36.0-9ubuntu1 perl-modules-5.36_5.36.0-9ubuntu1 pinentry-curses_1.2.1-1ubuntu1 pkgbinarymangler_154 po-debconf_1.0.21+nmu1 policyrcd-script-zg2_0.1-3.1 procps_2:4.0.3-1ubuntu1 psmisc_23.6-1 python3_3.11.4-5ubuntu1 python3-minimal_3.11.4-5ubuntu1 python3.11_3.11.6-3 python3.11-minimal_3.11.6-3 readline-common_8.2-1.3 rpcsvc-proto_1.4.2-0ubuntu6 sbuild-build-depends-main-dummy_0.invalid.0 sed_4.9-1 sensible-utils_0.0.20 systemd_253.5-1ubuntu7 systemd-dev_253.5-1ubuntu7 systemd-sysv_253.5-1ubuntu7 sysvinit-utils_3.07-1ubuntu1 tar_1.34+dfsg-1.2ubuntu1 tzdata_2023c-9ubuntu1 ubuntu-keyring_2021.03.26 usrmerge_35ubuntu1 util-linux_2.39.1-4ubuntu2 uuid-runtime_2.39.1-4ubuntu2 wdiff_1.2.2-6 xz-utils_5.4.4-0.1 zlib1g_1:1.2.13.dfsg-1ubuntu5 +------------------------------------------------------------------------------+ | Build | +------------------------------------------------------------------------------+ Unpack source ------------- -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Format: 3.0 (quilt) Source: coq-hierarchy-builder Binary: libcoq-hierarchy-builder, coq-hierarchy-builder Architecture: any Version: 1.4.0-6build6 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/math-comp/hierarchy-builder Standards-Version: 4.6.2 Vcs-Browser: https://salsa.debian.org/ocaml-team/coq-hierarchy-builder Vcs-Git: https://salsa.debian.org/ocaml-team/coq-hierarchy-builder.git Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libelpi-ocaml-dev, wdiff Package-List: coq-hierarchy-builder deb ocaml optional arch=any libcoq-hierarchy-builder deb ocaml optional arch=any Checksums-Sha1: 0a416ce6bd3be7af9bc71acab905d9fa6882e84e 201673 coq-hierarchy-builder_1.4.0.orig.tar.gz 65cd82cdf3a28da54aa54cc8190c4c7b0a0e81ec 5756 coq-hierarchy-builder_1.4.0-6build6.debian.tar.xz Checksums-Sha256: 96a3c5dd50b6a806c02e858ec46f1a46712fc92605aae3fa86a9de4440c99d99 201673 coq-hierarchy-builder_1.4.0.orig.tar.gz e23ebb1355d96be74fbd41c06aff10240a11a713125b599cfc150b8163603a95 5756 coq-hierarchy-builder_1.4.0-6build6.debian.tar.xz Files: 2fb08ce2debfe46a48593132aad748f0 201673 coq-hierarchy-builder_1.4.0.orig.tar.gz 7899c9dd43cb74a4808bae2848cff327 5756 coq-hierarchy-builder_1.4.0-6build6.debian.tar.xz -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEkpeKbhleSSGCX3/w808JdE6fXdkFAmVGmA0ACgkQ808JdE6f XdlvLQ//feOHryK+0JyaEref20JCAShbff3b89lrhNYNSKWf3nWa4cuKrsaK01X9 tgJpAshZX8j3qVJsEG3Yf1h8gBhNw+TkywqfIe0tu6pgKdHtxp4ZPEzkLO8uHk6E U1XSFL2coOU5CxiSd+aDcqxkmBNViVZxPYfFjfMNmCFA8uoSnPqf8Q19XI7ZUDCR QBTAC3H9dLIbUl35Pu9u97ZCOJrnmNGbbXdQDAzGkxZZ7VzhdSVq1LN1u886gXKy tJ93S6+UHNlJA2ulUcLe6j6YxwHplsSYyijZ9KcF2OGInnjsE2PKve+caiNsMUld Pm3SRRUNUOhzZphtr2W9+A77JSCxsLBtfS+efWUbgbaEBY4a0g/hwgmOxj+4syGD oCFmZzqNU254Tu3dTUH1aqEagraxkUfVt+sN7UQfuqdRcs+0mc2NmxOZgC5JZhO2 gdMYZfefzR7JGdX6OmkbSFgO3mOfLaoVKBTyVx0ngYExiID8UWHR1fYptwUM7yXj sc6D3FLJ2Qb2mdEV28BpUOMjnp4xJUd9x48rYW5jAYGVErCP9KxUW581BWHtm7Iu mv9yHWyBcSWy81eRdZAlAQrpcEqs2NwcHlclCK/orH3Zn9kBKQBDFq6LvEA5cEO3 tlqw5hRqiJNoWbYxdscYVPMjup/Mp2ztKIoWrTDLYs5UiTDSyk8= =9eGs -----END PGP SIGNATURE----- gpgv: Signature made Sat Nov 4 19:14:21 2023 UTC gpgv: using RSA key 92978A6E195E4921825F7FF0F34F09744E9F5DD9 gpgv: Can't check signature: No public key dpkg-source: warning: cannot verify inline signature for ./coq-hierarchy-builder_1.4.0-6build6.dsc: no acceptable signature found dpkg-source: info: extracting coq-hierarchy-builder in /<> dpkg-source: info: unpacking coq-hierarchy-builder_1.4.0.orig.tar.gz dpkg-source: info: unpacking coq-hierarchy-builder_1.4.0-6build6.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying fix_elpi_1.17.0.patch dpkg-source: info: applying fix_testsuite.patch Check disk space ---------------- Sufficient free space for build 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 LOGNAME=buildd PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SCHROOT_ALIAS_NAME=build-PACKAGEBUILD-26962111 SCHROOT_CHROOT_NAME=build-PACKAGEBUILD-26962111 SCHROOT_COMMAND=env SCHROOT_GID=2501 SCHROOT_GROUP=buildd SCHROOT_SESSION_ID=build-PACKAGEBUILD-26962111 SCHROOT_UID=2001 SCHROOT_USER=buildd SHELL=/bin/sh TERM=unknown USER=buildd V=1 dpkg-buildpackage ----------------- Command: dpkg-buildpackage -us -uc -mLaunchpad Build Daemon -B -rfakeroot dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.4.0-6build6 dpkg-buildpackage: info: source distribution noble dpkg-source --before-build . dpkg-buildpackage: info: host architecture riscv64 debian/rules clean dh clean --with coq,ocaml Use of uninitialized value in split at /usr/share/perl5/Dpkg/BuildFlags.pm line 373. dh_auto_clean make -j8 distclean make[1]: Entering directory '/<>' rm -f Makefile.coq Makefile.coq.conf rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf rm -f make[1]: Leaving directory '/<>' dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with coq,ocaml Use of uninitialized value in split at /usr/share/perl5/Dpkg/BuildFlags.pm line 373. dh_update_autotools_config -a dh_autoreconf -a dh_ocamlinit -a dh_auto_configure -a dh_auto_build -a make -j8 "INSTALL=install --strip-program=true" make[1]: Entering directory '/<>' make config make[2]: Entering directory '/<>' make[2]: Leaving directory '/<>' make build make[2]: Entering directory '/<>' ocamlc unix.cma str.cma -g hb.ml -o coq.hb /usr/bin/coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[3]: Entering directory '/<>' COQDEP VFILES COQC structures.v make[3]: Leaving directory '/<>' make[2]: Leaving directory '/<>' make test-suite make[2]: Entering directory '/<>' make -f Makefile.coq /usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq make[3]: Entering directory '/<>' Warning: . and tests overlap (used in -R or -Q) Warning: . and examples overlap (used in -R or -Q) make[4]: Nothing to be done for 'real-all'. make[3]: Leaving directory '/<>' make -f Makefile.test-suite.coq make[3]: Entering directory '/<>' COQDEP VFILES COQC examples/readme.v COQC examples/hulk.v COQC examples/demo1/hierarchy_0.v COQC examples/demo1/hierarchy_1.v COQC examples/demo1/hierarchy_2.v COQC examples/demo1/hierarchy_3.v COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v [1699198118.217768] HB: start module and section AddComoid_of_Type [1699198118.234114] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type (field [coercion off, canonical tt] zero c0 c1 \ field [coercion off, canonical tt] add (prod `_` c0 c2 \ prod `_` c0 c3 \ c0) c2 \ field [coercion off, canonical tt] addrA (prod `x` (X2 c0 c1 c2) c3 \ prod `y` (X3 c0 c1 c2 c3) c4 \ prod `z` (X4 c0 c1 c2 c3 c4) c5 \ app [global (indt «eq»), X5 c0 c1 c2 c3 c4 c5, app [c2, c3, app [c2, c4, c5]], app [c2, app [c2, c3, c4], c5]]) c3 \ field [coercion off, canonical tt] addrC (prod `x` (X6 c0 c1 c2 c3) c4 \ prod `y` (X7 c0 c1 c2 c3 c4) c5 \ app [global (indt «eq»), X8 c0 c1 c2 c3 c4 c5, app [c2, c4, c5], app [c2, c5, c4]]) c4 \ field [coercion off, canonical tt] add0r (prod `x` (X9 c0 c1 c2 c3 c4) c5 \ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories [1699198118.268023] HB: processing key parameter [1699198118.285926] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins [1699198118.291787] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] [1699198118.298830] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] [1699198118.514078] HB: declare mixin or factory [1699198118.517885] HB: declare record axioms_ [1699198119.374502] HB: declare notation Build [1699198119.824684] HB: declare notation axioms [1699198120.545531] HB: start module Exports [1699198121.593415] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* Module AddComoid_of_Type. Section AddComoid_of_Type. Variable A : Type. Local Arguments A : clear implicits. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ { zero : elpi_ctx_entry_0_; add : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; addrA : forall x y z : elpi_ctx_entry_0_, add x (add y z) = add (add x y) z; addrC : forall x y : elpi_ctx_entry_0_, add x y = add y x; add0r : forall x : elpi_ctx_entry_0_, add zero x = x; }. End axioms_. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Global Arguments zero : clear implicits. Global Arguments add : clear implicits. Global Arguments addrA : clear implicits. Global Arguments addrC : clear implicits. Global Arguments add0r : clear implicits. End AddComoid_of_Type. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Definition phant_Build : forall (A : Type) (zero : A) (add : A -> A -> A), (forall x y z : A, add x (add y z) = add (add x y) z) -> (forall x y : A, add x y = add y x) -> (forall x : A, add zero x = x) -> axioms_ A := fun (A : Type) (zero : A) (add : A -> A -> A) (addrA : forall x y z : A, add x (add y z) = add (add x y) z) (addrC : forall x y : A, add x y = add y x) (add0r : forall x : A, add zero x = x) => {| zero := zero; add := add; addrA := addrA; addrC := addrC; add0r := add0r |}. Local Arguments phant_Build : clear implicits. Notation Build X1 := ( phant_Build X1). Definition phant_axioms : Type -> Type := fun A : Type => axioms_ A. Local Arguments phant_axioms : clear implicits. Notation axioms X1 := ( phant_axioms X1). Definition identity_builder : forall A : Type, axioms_ A -> axioms_ A := fun (A : Type) (x : axioms_ A) => x. Local Arguments identity_builder : clear implicits. Module Exports. Global Arguments Axioms_ {_}. End Exports. End AddComoid_of_Type. Export AddComoid_of_Type.Exports. Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) [1699198123.281995] HB: start module AddComoid [1699198123.286304] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] [1699198123.291825] HB: typing class field indt «AddComoid_of_Type.axioms_» [1699198123.405282] HB: declare type record COQC examples/demo2/classical.v [1699198123.519493] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] [1699198123.522704] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] [1699198123.525822] HB: declaring clone abbreviation [1699198123.652972] HB: declaring pack_ constant [1699198123.663422] HB: declaring pack_ constant = fun `A` (sort (typ «HB.examples.readme.25»)) c0 \ fun `m` (app [global (indt «AddComoid_of_Type.axioms_»), c0]) c1 \ app [global (indc «Pack»), c0, app [global (indc «Class»), c0, c1]] [1699198123.684375] HB: start module Exports [1699198123.687768] HB: making coercion from type to target [1699198123.689086] HB: declare sort coercion [1699198123.693489] HB: exporting unification hints [1699198123.696621] HB: exporting coercions from class to mixins [1699198123.700663] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type [1699198123.706063] HB: accumulating various props [1699198123.821466] HB: stop module Exports [1699198123.896714] HB: declaring on_ abbreviation [1699198124.013089] HB: declaring `copy` abbreviation [1699198124.035387] HB: declaring on abbreviation [1699198124.056712] HB: eta expanded instances [1699198124.093173] HB: postulating A [1699198124.283779] HB: declare mixin instance readme_AddComoid__to__readme_AddComoid_of_Type [1699198124.354086] HB: we can build a readme_AddComoid on eta A [1699198124.362093] HB: declare canonical structure instance structures_eta__canonical__readme_AddComoid [1699198124.369415] HB: Giving name HB_unnamed_mixin_4 to mixin instance readme_AddComoid_of_Type_mixin (eta A) HB_unnamed_factory_2 [1699198124.402883] HB: structure instance for structures_eta__canonical__readme_AddComoid is {| sort := eta A; class := {| readme_AddComoid_of_Type_mixin := HB_unnamed_mixin_4 |} |} [1699198124.464516] HB: structure instance structures_eta__canonical__readme_AddComoid declared [1699198124.469039] HB: closing instance section [1699198124.686253] HB: end modules; export «HB.examples.readme.AddComoid.Exports» [1699198124.705891] HB: export «HB.examples.readme.AddComoid.EtaAndMixinExports» [1699198124.725158] HB: exporting operations [1699198124.739755] HB: export operation zero [1699198124.802269] HB: export operation add [1699198124.872820] HB: export operation addrA [1699198124.945229] HB: export operation addrC [1699198125.264717] HB: begin module for builders [1699198125.270054] HB: postulating factories [1699198125.272871] HB: processing key context-item [1699198125.281111] HB: processing mixin parameter a [1699198125.284059] HB: export operation add0r [1699198125.288879] HB: declaring parameters and key as section variables [1699198125.333798] HB: operations meta-data module: ElpiOperations Here is the list of mixins to declare (the order matters): [] [1699198125.494639] HB: abbreviation factory-by-classname (* Module AddComoid. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (A : Type) : Type := Class { readme_AddComoid_of_Type_mixin : AddComoid_of_Type.axioms_ A; }. End axioms_. Global Arguments axioms_ : clear implicits. Global Arguments Class : clear implicits. Global Arguments readme_AddComoid_of_Type_mixin : clear implicits. Section type. Local Unset Implicit Arguments. Record type : Type := Pack { sort : Type; class : axioms_ sort; }. End type. Global Arguments type : clear implicits. Global Arguments Pack : clear implicits. Global Arguments sort : clear implicits. Global Arguments class : clear implicits. Definition phant_clone : forall (A : Type) (cT : type) (c : axioms_ A) (_ : unify Type Type A (sort cT) nomsg) (_ : unify type type cT (Pack A c) nomsg), type := fun (A : Type) (cT : type) (c : axioms_ A) (_ : unify Type Type A (sort cT) nomsg) (_ : unify type type cT (Pack A c) nomsg) => Pack A c. Local Arguments phant_clone : clear implicits. Notation clone X2 X1 := ( phant_clone X2 X1 _ (@id_phant _ _) (@id_phant _ _)). Definition pack_ := fun (A : Type) (m : AddComoid_of_Type.axioms_ A) => Pack A (Class A m). Local Arguments pack_ : clear implicits. Module Exports. #[reversible] Coercion sort : readme.AddComoid.type >-> Sortclass. #[reversible] Coercion readme_AddComoid_of_Type_mixin : readme.AddComoid.axioms_ >-> readme.AddComoid_of_Type.axioms_. End Exports. Import Exports. Definition phant_on_ : forall (A : type) (_ : phant (sort A)), axioms_ (sort A) := fun (A : type) (_ : phant (sort A)) => class A. Local Arguments phant_on_ : clear implicits. Notation on_ X1 := ( phant_on_ _ (Phant X1)). Notation copy X2 X1 := ( phant_on_ _ (Phant X1) : axioms_ X2). Notation on X1 := ( phant_on_ _ (Phant _) : axioms_ X1). Module EtaAndMixinExports. Section hb_instance_1. Variable A : type. Local Arguments A : clear implicits. Definition HB_unnamed_factory_2 : axioms_ (@eta Type (sort A)) := class A. Local Arguments HB_unnamed_factory_2 : clear implicits. Definition readme_AddComoid__to__readme_AddComoid_of_Type : AddComoid_of_Type.axioms_ (@eta Type (sort A)) := readme_AddComoid_of_Type_mixin (@eta Type (sort A)) HB_unnamed_factory_2. Local Arguments readme_AddComoid__to__readme_AddComoid_of_Type : clear implicits. Definition HB_unnamed_mixin_4 := readme_AddComoid_of_Type_mixin (@eta Type (sort A)) HB_unnamed_factory_2. Local Arguments HB_unnamed_mixin_4 : clear implicits. Definition structures_eta__canonical__readme_AddComoid : type := Pack (@eta Type (sort A)) (Class (@eta Type (sort A)) HB_unnamed_mixin_4). Local Arguments structures_eta__canonical__readme_AddComoid : clear implicits. Global Canonical structures_eta__canonical__readme_AddComoid. End hb_instance_1. End EtaAndMixinExports. End AddComoid. Export AddComoid.Exports. Export AddComoid.EtaAndMixinExports. Definition zero : forall s : AddComoid.type, AddComoid.sort s := fun s : AddComoid.type => AddComoid_of_Type.zero (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)). Local Arguments zero : clear implicits. Global Arguments zero {_}. Definition add : forall (s : AddComoid.type) (_ : AddComoid.sort s) (_ : AddComoid.sort s), AddComoid.sort s := fun (s : AddComoid.type) (H H0 : AddComoid.sort s) => AddComoid_of_Type.add (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) H H0. Local Arguments add : clear implicits. Global Arguments add {_}. Definition addrA : forall (s : AddComoid.type) (x y z : AddComoid.sort s), @eq (AddComoid.sort s) (@add s x (@add s y z)) (@add s (@add s x y) z) := fun (s : AddComoid.type) (x y z : AddComoid.sort s) => AddComoid_of_Type.addrA (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x y z. Local Arguments addrA : clear implicits. Global Arguments addrA {_}. Definition addrC : forall (s : AddComoid.type) (x y : AddComoid.sort s), @eq (AddComoid.sort s) (@add s x y) (@add s y x) := fun (s : AddComoid.type) (x y : AddComoid.sort s) => AddComoid_of_Type.addrC (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x y. Local Arguments addrC : clear implicits. Global Arguments addrC {_}. Definition add0r : forall (s : AddComoid.type) (x : AddComoid.sort s), @eq (AddComoid.sort s) (@add s (@zero s) x) x := fun (s : AddComoid.type) (x : AddComoid.sort s) => AddComoid_of_Type.add0r (AddComoid.sort s) (AddComoid.readme_AddComoid_of_Type_mixin (AddComoid.sort s) (AddComoid.class s)) x. Local Arguments add0r : clear implicits. Global Arguments add0r {_}. Module ElpiOperations5. End ElpiOperations5. Export ElpiOperations5. Notation AddComoid X1 := ( AddComoid.axioms_ X1). *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop COQC examples/demo3/hierarchy_0.v AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp (Phant BinNums_Z__canonical__readme_AbelianGrp) : AbelianGrp.axioms_ Z : AbelianGrp.axioms_ Z File "./examples/demo1/hierarchy_2.v", line 57, characters 0-57: Warning: pulling in dependencies: [hierarchy_2_AddComoid_of_TYPE, hierarchy_2_AddAG_of_AddComoid] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] HB: Z is canonically equipped with structures: - AbelianGrp (from "./examples/readme.v", line 32) - AddComoid (from "./examples/readme.v", line 31) COQC examples/demo3/hierarchy_1.v [1699198140.977854] HB: declare builder from hierarchy_2_Ring_of_AddComoid to hierarchy_2_AddAG_of_AddComoid [1699198140.981691] HB: declare builder from hierarchy_2_Ring_of_AddComoid to hierarchy_2_Ring_of_AddAG File "./examples/hulk.v", line 143, characters 0-63: Warning: pulling in dependencies: [Feather_HasEqDec] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] COQC examples/demo3/hierarchy_2.v HB: A is canonically equipped with structures: - Equality Singleton (from "./examples/hulk.v", line 216) COQC examples/demo4/hierarchy_0.v COQC examples/demo5/hierarchy_0.v COQC examples/FSCD2020_material/V1.v COQC examples/FSCD2020_material/V2.v COQC examples/FSCD2020_material/V3.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] eq_refl : inhab = 7 : inhab = 7 eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] HB.check: SemiRing_of_AddComoid.axioms_ : (forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), AddComoid_of_AddMonoid.axioms_ A m -> Type) : forall (A : Type) (m : AddMonoid_of_TYPE.axioms_ A), AddComoid_of_AddMonoid.axioms_ A m -> Type COQC examples/FSCD2020_material/V4.v fun X : s2.type nat => inhab : X : forall X : s2.type nat, X fun X : s2.type nat => inj : nat -> X : forall X : s2.type nat, nat -> X s2_to_s1 not a defined object. COQC examples/FSCD2020_talk/V1.v COQC examples/FSCD2020_talk/V2.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @add : forall s : Monoid.type, s -> s -> s @addNr : forall s : Ring.type, left_inverse 0 opp add COQC examples/FSCD2020_talk/V3.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @add : forall s : Monoid.type, s -> s -> s @addNr : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add COQC examples/Coq2020_material/CoqWS_demo.v COQC examples/Coq2020_material/CoqWS_abstract.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @add : forall s : Monoid.type, s -> s -> s @addNr : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add COQC examples/Coq2020_material/CoqWS_expansion/withHB.v COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: Warning: pulling in dependencies: [V2_is_semigroup] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] COQC tests/type_of_exported_ops.v add : ?s -> ?s -> ?s where ?s : [ |- CMonoid.type] addrC : commutative add where ?s : [ |- CMonoid.type] addrC : commutative add where ?s : [ |- CMonoid.type] COQC tests/duplicate_structure.v File "./examples/Coq2020_material/CoqWS_expansion/withoutHB.v", line 10, characters 50-62: Warning: The format modifier has no effect for only-parsing notations. [discarded-format-only-parsing,parsing] File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] COQC tests/instance_params_no_type.v forall x y : ?t, x - (y + 0) = x : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @add : forall s : Monoid.type, s -> s -> s @addNr : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add COQC tests/test_CS_db_filtering.v forall x y : ?t, 1 + x = y * x : Prop where ?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) COQC tests/subtype.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall (x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t) (y : ?t), 1 * x = y - x : Prop where ?t : [x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) forall (G : AbelianGrp.type) (x : G), x - x = 0 : Prop forall (S : SemiRing.type) (x : S), x * 1 + 0 = x : Prop forall (R : Ring.type) (x y : R), x * - (1 * y) = - x * y : Prop forall x : Z, x * - (1 + x) = 0 + 1 : Prop forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC tests/infer.v COQC tests/exports.v add : A -> A -> A COQC tests/log_impargs_record.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop COQC tests/compress_coe.v COQC tests/funclass.v COQC tests/grefclass.v (* Module A. Section A. Variable T : Type. Local Arguments T : clear implicits. Section axioms_. Local Unset Implicit Arguments. Record axioms_ (elpi_ctx_entry_0_ : Type) : Type := Axioms_ { a : elpi_ctx_entry_0_; f : elpi_ctx_entry_0_ -> elpi_ctx_entry_0_; p : forall x : elpi_ctx_entry_0_, f x = x -> True; q : forall h : f a = a, p a h = p a h; }. End axioms_. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ [_] [_] _ _ _. Global Arguments a [_] _. Global Arguments f [_] _ _. Global Arguments p [_] _ [_] _. Global Arguments q [_] _ _. End A. Global Arguments axioms_ : clear implicits. Global Arguments Axioms_ : clear implicits. Definition phant_Build : forall (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True), (forall h : f a = a, p a h = p a h) -> axioms_ T := fun (T : Type) (a : T) (f : T -> T) (p : forall x : T, f x = x -> True) (q : forall h : f a = a, p a h = p a h) => {| a := a; f := f; p := p; q := q |}. Local Arguments phant_Build : clear implicits. Notation Build X1 := ( phant_Build X1). Definition phant_axioms : Type -> Type := fun T : Type => axioms_ T. Local Arguments phant_axioms : clear implicits. Notation axioms X1 := ( phant_axioms X1). Definition identity_builder : forall T : Type, axioms_ T -> axioms_ T := fun (T : Type) (x : axioms_ T) => x. Local Arguments identity_builder : clear implicits. Module Exports. Global Arguments Axioms_ {_}. End Exports. End A. Export A.Exports. Notation A X1 := ( A.phant_axioms X1). *) HB.check: bar.type_ bool Datatypes_nat__canonical__infer_foo bool : Type File "./tests/infer.v", line 20, characters 0-62: Warning: Skipping test on Coq 8.17.0 as requested [HB.skip,HB] bar.phant_type = fun (A : Type) (P : foo.type) (_ : ssreflect.phant P) (B : Type) => bar.type_ A P B : Type -> forall P : foo.type, ssreflect.phant P -> Type -> Type Arguments bar.phant_type A%type_scope P _ B%type_scope Notation bar.type _elpi_ctx_entry_3_was_A_ _elpi_ctx_entry_2_was_P_ _elpi_ctx_entry_1_was_B_ := (bar.phant_type _elpi_ctx_entry_3_was_A_ _ (ssreflect.Phant _elpi_ctx_entry_2_was_P_) _elpi_ctx_entry_1_was_B_) bar.phant_type bool Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) bool : Type [1699198291.750459] HB: start module SubInhab [1699198291.754454] HB: declare axioms record w-params.cons T (sort (typ «HB.tests.subtype.337»)) c0 \ w-params.cons P (app [global (const «pred»), c0]) c1 \ w-params.nil sT (sort (typ «HB.tests.subtype.339»)) c2 \ [triple (indt «is_inhab.axioms_») [] c2, triple (indt «is_SUB.axioms_») [c0, c1] c2] [1699198291.765366] HB: typing class field indt «is_inhab.axioms_» [1699198291.772775] HB: typing class field indt «is_SUB.axioms_» [1699198291.941147] HB: declare type record [1699198292.056441] HB: structure: new mixins [] [1699198292.060357] HB: structure: mixin first class [] [1699198292.064467] HB: declaring clone abbreviation [1699198292.214201] HB: declaring pack_ constant [1699198292.260931] HB: declaring pack_ constant = fun `T` (sort (typ «HB.tests.subtype.337»)) c0 \ fun `P` (app [global (const «pred»), c0]) c1 \ fun `sT` (sort (typ «HB.tests.subtype.339»)) c2 \ fun `m` (app [global (indt «is_inhab.axioms_»), c2]) c3 \ fun `m` (app [global (indt «is_SUB.axioms_»), c0, c1, c2]) c4 \ app [global (indc «Pack»), c0, c1, c2, app [global (indc «Class»), c0, c1, c2, c3, c4]] [1699198292.316932] HB: start module Exports [1699198292.322684] HB: making coercion from type to target [1699198292.328137] HB: declare sort coercion [1699198292.336796] HB: exporting unification hints [1699198292.362218] HB: declare coercion subtype_SubInhab__to__subtype_SUB [1699198292.388593] HB: declare coercion hint subtype_SubInhab_class__to__subtype_SUB_class [1699198292.491847] HB: declare unification hint subtype_SubInhab__to__subtype_SUB [1699198292.598268] HB: declare coercion path compression rules [1699198292.620236] HB: declare coercion subtype_SubInhab__to__subtype_Inhab [1699198292.635668] HB: declare coercion hint subtype_SubInhab_class__to__subtype_Inhab_class [1699198292.754142] HB: declare unification hint subtype_SubInhab__to__subtype_Inhab [1699198292.863518] HB: declare coercion path compression rules [1699198292.880226] HB: declare unification hint join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB [1699198293.008426] HB: exporting coercions from class to mixins [1699198293.018559] HB: export class to mixin coercion for mixin subtype_is_inhab [1699198293.052783] HB: export class to mixin coercion for mixin subtype_is_SUB [1699198293.069144] HB: accumulating various props [1699198293.258815] HB: stop module Exports [1699198293.355596] HB: declaring on_ abbreviation [1699198293.485385] HB: declaring `copy` abbreviation [1699198293.508543] HB: declaring on abbreviation [1699198293.535640] HB: eta expanded instances A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True A.p is not universe polymorphic Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p [1699198293.595498] HB: postulating T [1699198293.689832] HB: postulating P [1699198293.794114] HB: postulating sT COQC tests/local_instance.v [1699198294.292585] HB: declare mixin instance subtype_SubInhab__to__subtype_is_inhab [1699198294.527848] HB: declare mixin instance subtype_SubInhab__to__subtype_is_SUB [1699198294.705747] HB: skipping already existing subtype_Inhab instance on eta sT [1699198294.722212] HB: skipping already existing subtype_Nontrivial instance on eta sT [1699198294.737630] HB: skipping already existing subtype_SUB instance on eta sT [1699198294.775656] HB: we can build a subtype_SubInhab on eta sT [1699198294.786733] HB: declare canonical structure instance structures_eta__canonical__subtype_SubInhab [1699198294.802400] HB: structure instance for structures_eta__canonical__subtype_SubInhab is {| sort := eta sT; class := {| subtype_is_inhab_mixin := HB_unnamed_mixin_4 sT; subtype_is_SUB_mixin := HB_unnamed_mixin_19 T P sT |} |} [1699198294.905275] HB: structure instance structures_eta__canonical__subtype_SubInhab declared [1699198294.909658] HB: closing instance section [1699198295.113287] HB: end modules; export «HB.tests.subtype.SubInhab.Exports» [1699198295.190140] HB: export «HB.tests.subtype.SubInhab.EtaAndMixinExports» [1699198295.211379] HB: exporting operations [1699198295.217497] HB: operations meta-data module: ElpiOperations [1699198295.314469] HB: abbreviation factory-by-classname bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) : Type COQC tests/lock.v id : forall {T : Type}, Monoid.type T -> T id is not universe polymorphic Arguments id {T}%type_scope {s} id is transparent Expands to: Constant HB.tests.funclass.id File "./tests/funclass.v", line 19, characters 54-64: Warning: Notation plus_assoc is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_assoc instead. [deprecated-syntactic-definition,deprecated] Monoid.phant_on_ nat Nat_add__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Nat_add__canonical__funclass_Monoid) : Monoid.axioms_ nat Init.Nat.add : Monoid.axioms_ nat Init.Nat.add [1699198304.513869] HB: exporting under the module path [] [1699198304.519369] HB: exporting modules [Ring_of_TYPE.Exports, Ring.Exports, Ring.EtaAndMixinExports, ElpiOperations5, RingExports, Dummy.Exports, URing.Exports, URing.EtaAndMixinExports, ElpiOperations11, dummy.Exports, Builders_12.dummy_Exports] [1699198304.545908] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] [1699198304.556332] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G : ?s where ?s : [ |- Enclosing.Ring.type] Enclosing.zero : Z : Z COQC tests/interleave_context.v COQC tests/not_same_key.v Monoid.phant_on_ nat Nat_mul__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Nat_mul__canonical__funclass_Monoid) : Monoid.axioms_ nat Init.Nat.mul : Monoid.axioms_ nat Init.Nat.mul p : pred nat : pred nat COQC tests/hb_pack.v HB.check: forall w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w : Prop COQC tests/declare.v Notation big := big.body Expands to: Notation HB.tests.lock.X.big COQC tests/short.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| D.sort := D.sort D * D.sort D'; D.class := {| D.compress_coe_hasA_mixin := prodA (compress_coe_D__to__compress_coe_A D) (compress_coe_D__to__compress_coe_A D'); D.compress_coe_hasB_mixin := prodB tt (compress_coe_D__to__compress_coe_B D) (compress_coe_D__to__compress_coe_B D'); D.compress_coe_hasC_mixin := prodC tt tt (compress_coe_D__to__compress_coe_C D) (compress_coe_D__to__compress_coe_C D'); D.compress_coe_hasD_mixin := prodD D D' |} |} : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' COQC tests/primitive_records.v default : nat : nat The command did fail as expected with message: The term "default" has type "nonempty.sort ?t" while it is expected to have type "nat". COQC tests/non_forgetful_inheritance.v [1699198325.972479] HB: start module and section hasA [1699198325.985529] HB: converting arguments indt-decl (parameter T explicit X0 c0 \ record hasA (sort (typ X1)) Build_hasA (field [coercion off, canonical tt] a c0 c1 \ end-record)) to factories [1699198326.000104] HB: processing key parameter [1699198326.046510] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins [1699198326.060689] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] [1699198326.070393] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] [1699198326.290139] HB: declare mixin or factory [1699198326.300176] HB: declare record axioms_ [1699198326.760915] HB: declare notation Build [1699198327.036200] HB: declare notation axioms [1699198327.594262] HB: start module Exports [1699198328.352556] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. COQC tests/fix_loop.v hasB.type not a defined object. File "./tests/interleave_context.v", line 16, characters 0-52: Warning: pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] aType : Type hasB.type not a defined object. Query assignments: Ind = «hasA.axioms_» hasAB.type not a defined object. hasA'.type not a defined object. COQC tests/test_synthesis_params.v forall T : AB.type, unkeyed {| AB.sort := T; AB.class := let hb_pack_hasA_mixin := AB.hb_pack_hasA_mixin T (AB.class T) in let hb_pack_hasB_mixin := AB.hb_pack_hasB_mixin T (AB.class T) in {| AB.hb_pack_hasA_mixin := hb_pack_hasA_mixin; AB.hb_pack_hasB_mixin := hb_pack_hasB_mixin |} |} : Type A : A.type : A.type Finished transaction in 196.604 secs (167.512u,28.344s) (successful) A : A.type : A.type AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type Finished transaction in 0.012 secs (0.009u,0.003s) (successful) hasAB.type not a defined object. pB : T * T : T * T AB3 : AB.type : AB.type COQC tests/hnf.v hasA'.type not a defined object. COQC tests/fun_instance.v Query assignments: Ind = «A.axioms_» COQC tests/issue284.v X : Foo.type A P : Foo.type A P COQC tests/issue287.v Query assignments: Ind = «A.type» T : Fun.type nat : Fun.type nat COQC examples/demo1/test_0_0.v erefl ?t : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] COQC examples/demo1/test_1_0.v COQC examples/demo1/test_2_0.v Datatypes_nat__canonical__hnf_S = {| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |} : S.type HB_unnamed_mixin_12 = {| M.x := f.y nat HB_unnamed_factory_10 + 1 |} : M.axioms_ nat Datatypes_bool__canonical__hnf_S = {| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |} : S.type HB_unnamed_mixin_16 = Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13 : M.axioms_ bool COQC examples/demo1/test_3_0.v COQC examples/demo1/test_3_3.v COQC examples/demo1/test_4_0.v COQC examples/demo1/test_4_3.v COQC examples/demo1/test_5_0.v COQC examples/demo1/test_5_3.v COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v COQC examples/demo3/test_0_0.v COQC examples/demo3/test_1_0.v COQC examples/demo3/test_2_0.v COQC tests/exports2.v [1699198429.301408] HB: exporting under the module path [] [1699198429.306632] HB: exporting modules [] [1699198429.312495] HB: exporting CS instances [] [1699198429.319337] HB: exporting Abbreviations [] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 File "./examples/demo2/stage10.v", line 233, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of "global" (as described in the reference manual), "export" and re-exporting for every surrounding module. It will change to just "global" (with the meaning used by the "Set" command) in a future release. To preserve the current meaning in a forward compatible way, use the attribute "#[global,export]" and repeat the command with just "#[export]" in any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated] Finished transaction in 156.375 secs (147.668u,8.443s) (successful) Module Type new_conceptLocked = Sig Parameter body : nat. Parameter unlock : body = Init.Nat.of_num_uint (Number.UIntDecimal (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). End Module new_concept : new_conceptLocked := Struct Definition body : nat. Parameter unlock : new_concept = Init.Nat.of_num_uint (Number.UIntDecimal (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 (Decimal.D9 Decimal.Nil))))))). End Notation new_concept := new_concept.body File "./examples/demo2/stage11.v", line 364, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of "global" (as described in the reference manual), "export" and re-exporting for every surrounding module. It will change to just "global" (with the meaning used by the "Set" command) in a future release. To preserve the current meaning in a forward compatible way, use the attribute "#[global,export]" and repeat the command with just "#[export]" in any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated] HB: skipping section opening [1699198520.814596] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology [1699198520.851534] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» [1699198520.877409] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology [1699198520.969786] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» [1699198520.997700] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform [1699198521.111887] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» [1699198521.136195] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform [1699198521.198713] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» [1699198521.233676] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc [1699198521.240095] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology [1699198521.246297] HB: Giving name HB_unnamed_mixin_92 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 [1699198521.282222] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; UniformSpace_wo_Topology.class := {| UniformSpace_wo_Topology.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} [1699198521.324817] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared [1699198521.344866] HB: we can build a Stage11_UniformSpace on Qc [1699198521.350243] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace [1699198521.361030] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; UniformSpace.class := {| UniformSpace.Stage11_Topological_mixin := HB_unnamed_mixin_86; UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} [1699198521.414869] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared [1699198521.430675] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc [1699198521.437186] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform [1699198521.449457] HB: Giving name HB_unnamed_mixin_93 to mixin instance Builders_68.to_JoinTAddAG_wo_Uniform Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 [1699198521.493084] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; TAddAG_wo_Uniform.class := {| TAddAG_wo_Uniform.Stage11_AddAG_of_TYPE_mixin := HB_unnamed_mixin_81; TAddAG_wo_Uniform.Stage11_Topological_mixin := HB_unnamed_mixin_86; TAddAG_wo_Uniform.Stage11_JoinTAddAG_wo_Uniform_mixin := HB_unnamed_mixin_93 |} |} [1699198521.549041] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared [1699198521.572572] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc [1699198521.578666] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined [1699198521.597367] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; Uniform_TAddAG_unjoined.class := {| Uniform_TAddAG_unjoined.Stage11_AddAG_of_TYPE_mixin := HB_unnamed_mixin_81; Uniform_TAddAG_unjoined.Stage11_Topological_mixin := HB_unnamed_mixin_86; Uniform_TAddAG_unjoined.Stage11_JoinTAddAG_wo_Uniform_mixin := HB_unnamed_mixin_93; Uniform_TAddAG_unjoined.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} [1699198521.649545] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared [1699198521.713778] HB: we can build a Stage11_TAddAG on Qc [1699198521.719397] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG [1699198521.734385] HB: Giving name HB_unnamed_mixin_94 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 [1699198521.784216] HB: Giving name HB_unnamed_mixin_95 to mixin instance Builders_68.Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform Qc HB_unnamed_mixin_81 HB_unnamed_mixin_86 HB_unnamed_factory_87 [1699198521.832060] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; TAddAG.class := {| TAddAG.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92; TAddAG.Stage11_AddAG_of_TYPE_mixin := HB_unnamed_mixin_81; TAddAG.Stage11_Topological_mixin := HB_unnamed_mixin_86; TAddAG.Stage11_Join_Uniform_Topology_mixin := HB_unnamed_mixin_94; TAddAG.Stage11_JoinTAddAG_wo_Uniform_mixin := HB_unnamed_mixin_93; TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_95 |} |} [1699198521.882771] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) File "./examples/hulk.v", line 315, characters 0-55: Warning: pulling in dependencies: [MissingJoin_isTop] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] File "./examples/hulk.v", line 341, characters 0-55: Warning: pulling in dependencies: [GoodJoin_isTop] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] OUTPUT DIFF tests/compress_coe.v OUTPUT DIFF tests/about.v OUTPUT DIFF tests/howto.v OUTPUT DIFF tests/missing_join_error.v OUTPUT DIFF tests/not_same_key.v OUTPUT DIFF tests/hnf.v make[3]: Leaving directory '/<>' make[2]: Leaving directory '/<>' make[1]: Leaving directory '/<>' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a dh_auto_install -a make -j8 install DESTDIR=/<>/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[1]: Entering directory '/<>' make -f Makefile.coq install make[2]: Entering directory '/<>' make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. INSTALL structures.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/HB/ INSTALL structures.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/HB/ INSTALL structures.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/HB/ make[3]: Entering directory '/<>' make[3]: Leaving directory '/<>' make[2]: Leaving directory '/<>' install -d /<>/debian/tmp/bin install -m 0755 coq.hb /<>/debian/tmp/bin make[1]: Leaving directory '/<>' dh_install -a dh_ocamldoc -a dh_installdocs -a dh_installchangelogs -a debian/rules override_dh_installman make[1]: Entering directory '/<>' dh_installman --language='C' make[1]: Leaving directory '/<>' dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_ocaml -a W: coq-hierarchy-builder doesn't resolve dependency on unit Hb dh_gencontrol -a dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${ocaml:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libcoq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: package coq-hierarchy-builder: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums -a dh_builddeb -a INFO: pkgstriptranslations version 154 INFO: pkgstriptranslations version 154 pkgstriptranslations: processing coq-hierarchy-builder (in debian/coq-hierarchy-builder); do_strip: , oemstrip: pkgstriptranslations: processing libcoq-hierarchy-builder (in debian/libcoq-hierarchy-builder); do_strip: , oemstrip: pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/coq-hierarchy-builder/DEBIAN/control, package coq-hierarchy-builder, directory debian/coq-hierarchy-builder INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... pkgstripfiles: processing control file: debian/libcoq-hierarchy-builder/DEBIAN/control, package libcoq-hierarchy-builder, directory debian/libcoq-hierarchy-builder pkgstripfiles: Truncating usr/share/doc/libcoq-hierarchy-builder/changelog.Debian.gz to topmost ten records INFO: pkgstripfiles: waiting for lock (coq-hierarchy-builder) ... pkgstripfiles: Running PNG optimization (using 8 cpus) for package libcoq-hierarchy-builder ... pkgstripfiles: No PNG files. dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb'. Searching for duplicated docs in dependency libcoq-hierarchy-builder... symlinking changelog.Debian.gz in coq-hierarchy-builder to file in libcoq-hierarchy-builder pkgstripfiles: Running PNG optimization (using 8 cpus) for package coq-hierarchy-builder ... pkgstripfiles: No PNG files. dpkg-deb: building package 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.4.0-6build6_riscv64.deb'. dpkg-genbuildinfo --build=any -O../coq-hierarchy-builder_1.4.0-6build6_riscv64.buildinfo Use of uninitialized value in split at /usr/share/perl5/Dpkg/BuildFlags.pm line 373. Use of uninitialized value in string eq at /usr/bin/dpkg-genbuildinfo line 336. dpkg-genchanges --build=any -mLaunchpad Build Daemon -O../coq-hierarchy-builder_1.4.0-6build6_riscv64.changes dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) -------------------------------------------------------------------------------- Build finished at 2023-11-05T15:41:21Z Finished -------- I: Built successfully +------------------------------------------------------------------------------+ | Changes | +------------------------------------------------------------------------------+ coq-hierarchy-builder_1.4.0-6build6_riscv64.changes: ---------------------------------------------------- Format: 1.8 Date: Sat, 04 Nov 2023 20:14:20 +0100 Source: coq-hierarchy-builder Binary: coq-hierarchy-builder libcoq-hierarchy-builder Built-For-Profiles: noudeb Architecture: riscv64 Version: 1.4.0-6build6 Distribution: noble-proposed Urgency: medium Maintainer: Launchpad Build Daemon Changed-By: Gianfranco Costamagna Description: coq-hierarchy-builder - build hierarchies of algebraic structures in Coq (tool) libcoq-hierarchy-builder - build hierarchies of algebraic structures in Coq (runtime files) Changes: coq-hierarchy-builder (1.4.0-6build6) noble; urgency=medium . * Rebuild against new OCAML ABI. Checksums-Sha1: 98f49925527b4748f60a3eedad422faff6b81e9d 7599 coq-hierarchy-builder_1.4.0-6build6_riscv64.buildinfo c983ff668c588ce114caf0088fa776a70428742e 831480 coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 2073f9a2496c9cc5af8a445e6f9550605f38cbcd 266504 libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb Checksums-Sha256: 6c29b3ff3363facf74b0ce441713085f17227479913ea3130fecae8cd629a051 7599 coq-hierarchy-builder_1.4.0-6build6_riscv64.buildinfo ed72897fbfe8a5983279aa2156f769b244bb1ad37f541a46a95ef35fe66be8f6 831480 coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 5cfcc768ce375d07e0bcf086960d9e830a4dd20689bf84ec131ab170b9b7f538 266504 libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb Files: 5e331db616f52eb3eefb542ce12d68f5 7599 ocaml optional coq-hierarchy-builder_1.4.0-6build6_riscv64.buildinfo ce5f5d2e5c38c5d107aaab46ddb33d08 831480 ocaml optional coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 9b2471c939e5c857c736d74c622018f6 266504 ocaml optional libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb /<>/coq-hierarchy-builder_1.4.0-6build6_riscv64.changes.new could not be renamed to /<>/coq-hierarchy-builder_1.4.0-6build6_riscv64.changes: Illegal seek Distribution field may be wrong!!! +------------------------------------------------------------------------------+ | Buildinfo | +------------------------------------------------------------------------------+ Format: 1.0 Source: coq-hierarchy-builder Binary: coq-hierarchy-builder libcoq-hierarchy-builder Architecture: riscv64 Version: 1.4.0-6build6 Checksums-Md5: ce5f5d2e5c38c5d107aaab46ddb33d08 831480 coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 9b2471c939e5c857c736d74c622018f6 266504 libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb Checksums-Sha1: c983ff668c588ce114caf0088fa776a70428742e 831480 coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 2073f9a2496c9cc5af8a445e6f9550605f38cbcd 266504 libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb Checksums-Sha256: ed72897fbfe8a5983279aa2156f769b244bb1ad37f541a46a95ef35fe66be8f6 831480 coq-hierarchy-builder_1.4.0-6build6_riscv64.deb 5cfcc768ce375d07e0bcf086960d9e830a4dd20689bf84ec131ab170b9b7f538 266504 libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb Build-Origin: Ubuntu Build-Architecture: riscv64 Build-Date: Sun, 05 Nov 2023 15:41:12 +0000 Build-Path: /<> Build-Tainted-By: merged-usr-via-aliased-dirs usr-local-has-programs Installed-Build-Depends: autoconf (= 2.71-3), automake (= 1:1.16.5-1.3), autopoint (= 0.21-13build1), autotools-dev (= 20220109.1), base-files (= 13ubuntu4), base-passwd (= 3.6.2), bash (= 5.2.15-2ubuntu1), binutils (= 2.41-6ubuntu1), binutils-common (= 2.41-6ubuntu1), binutils-riscv64-linux-gnu (= 2.41-6ubuntu1), bsdextrautils (= 2.39.1-4ubuntu2), bsdutils (= 1:2.39.1-4ubuntu2), build-essential (= 12.10ubuntu1), bzip2 (= 1.0.8-5build1), coq (= 8.17.0+dfsg-1build2), coreutils (= 9.1-1ubuntu2), cpp (= 4:13.2.0-1ubuntu1), cpp-13 (= 13.2.0-6ubuntu1), dash (= 0.5.12-6ubuntu1), debconf (= 1.5.82), debhelper (= 13.11.7ubuntu1), debianutils (= 5.14), debugedit (= 1:5.0-5), dh-autoreconf (= 20), dh-coq (= 0.6), dh-ocaml (= 2.0), dh-strip-nondeterminism (= 1.13.1-1), diffutils (= 1:3.10-1), dpkg (= 1.22.1ubuntu1), dpkg-dev (= 1.22.1ubuntu1), dwz (= 0.15-1), file (= 1:5.45-2), findutils (= 4.9.0-5), g++ (= 4:13.2.0-1ubuntu1), g++-13 (= 13.2.0-6ubuntu1), gcc (= 4:13.2.0-1ubuntu1), gcc-13 (= 13.2.0-6ubuntu1), gcc-13-base (= 13.2.0-6ubuntu1), gettext (= 0.21-13build1), gettext-base (= 0.21-13build1), grep (= 3.11-3), groff-base (= 1.23.0-3), gzip (= 1.12-1ubuntu1), hostname (= 3.23+nmu1ubuntu1), init-system-helpers (= 1.65.2ubuntu1), intltool-debian (= 0.35.0+20060710.6), libacl1 (= 2.3.1-3), libarchive-zip-perl (= 1.68-1), libasan8 (= 13.2.0-6ubuntu1), libatomic1 (= 13.2.0-6ubuntu1), libattr1 (= 1:2.5.1-4), libaudit-common (= 1:3.1.1-1build1), libaudit1 (= 1:3.1.1-1build1), libbinutils (= 2.41-6ubuntu1), libblkid1 (= 2.39.1-4ubuntu2), libbz2-1.0 (= 1.0.8-5build1), libc-bin (= 2.38-3ubuntu1), libc-dev-bin (= 2.38-3ubuntu1), libc6 (= 2.38-3ubuntu1), libc6-dev (= 2.38-3ubuntu1), libcap-ng0 (= 0.8.3-1build3), libcap2 (= 1:2.66-4ubuntu1), libcc1-0 (= 13.2.0-6ubuntu1), libcom-err2 (= 1.47.0-2ubuntu1), libcompiler-libs-ocaml-dev (= 4.14.1-1ubuntu1), libcoq-core-ocaml (= 8.17.0+dfsg-1build2), libcoq-core-ocaml-dev (= 8.17.0+dfsg-1build2), libcoq-elpi (= 1.17.1-1build9), libcoq-stdlib (= 8.17.0+dfsg-1build2), libcrypt-dev (= 1:4.4.36-2), libcrypt1 (= 1:4.4.36-2), libctf-nobfd0 (= 2.41-6ubuntu1), libctf0 (= 2.41-6ubuntu1), libdb5.3 (= 5.3.28+dfsg2-3), libdebconfclient0 (= 0.270ubuntu1), libdebhelper-perl (= 13.11.7ubuntu1), libdpkg-perl (= 1.22.1ubuntu1), libdw1 (= 0.189-4), libelf1 (= 0.189-4), libelpi-ocaml (= 1.17.0-1build5), libelpi-ocaml-dev (= 1.17.0-1build5), libexpat1 (= 2.5.0-2), libffi8 (= 3.4.4-1), libfile-stripnondeterminism-perl (= 1.13.1-1), libfindlib-ocaml (= 1.9.6-1build2), libfindlib-ocaml-dev (= 1.9.6-1build2), libgcc-13-dev (= 13.2.0-6ubuntu1), libgcc-s1 (= 13.2.0-6ubuntu1), libgcrypt20 (= 1.10.2-3ubuntu1), libgdbm-compat4 (= 1.23-3), libgdbm6 (= 1.23-3), libgmp-dev (= 2:6.3.0+dfsg-2ubuntu4), libgmp10 (= 2:6.3.0+dfsg-2ubuntu4), libgmp3-dev (= 2:6.3.0+dfsg-2ubuntu4), libgmpxx4ldbl (= 2:6.3.0+dfsg-2ubuntu4), libgomp1 (= 13.2.0-6ubuntu1), libgpg-error0 (= 1.47-2), libgssapi-krb5-2 (= 1.20.1-3ubuntu1), libicu72 (= 72.1-3ubuntu3), libisl23 (= 0.26-3), libjansson4 (= 2.14-2), libk5crypto3 (= 1.20.1-3ubuntu1), libkeyutils1 (= 1.6.3-2), libkrb5-3 (= 1.20.1-3ubuntu1), libkrb5support0 (= 1.20.1-3ubuntu1), liblz4-1 (= 1.9.4-1), liblzma5 (= 5.4.4-0.1), libmagic-mgc (= 1:5.45-2), libmagic1 (= 1:5.45-2), libmd0 (= 1.1.0-1), libmenhir-ocaml-dev (= 20230608+ds-1build1), libmount1 (= 2.39.1-4ubuntu2), libmpc3 (= 1.3.1-1), libmpfr6 (= 4.2.1-1), libncurses-dev (= 6.4+20231016-1), libncurses6 (= 6.4+20231016-1), libncursesw6 (= 6.4+20231016-1), libnsl-dev (= 1.3.0-3), libnsl2 (= 1.3.0-3), libocaml-compiler-libs-ocaml-dev (= 0.12.4-4build1), libpam-modules (= 1.5.2-6ubuntu1), libpam-modules-bin (= 1.5.2-6ubuntu1), libpam-runtime (= 1.5.2-6ubuntu1), libpam0g (= 1.5.2-6ubuntu1), libpcre2-8-0 (= 10.42-4), libperl5.36 (= 5.36.0-9ubuntu1), libpipeline1 (= 1.5.7-1), libppx-derivers-ocaml-dev (= 1.2.1-4build1), libppx-deriving-ocaml (= 5.2.1-4build1), libppx-deriving-ocaml-dev (= 5.2.1-4build1), libppxlib-ocaml-dev (= 0.31.0-1), libpython3-stdlib (= 3.11.4-5ubuntu1), libpython3.11-minimal (= 3.11.6-3), libpython3.11-stdlib (= 3.11.6-3), libre-ocaml-dev (= 1.11.0-1build1), libreadline8 (= 8.2-1.3), libresult-ocaml (= 1.5-4build1), libresult-ocaml-dev (= 1.5-4build1), libselinux1 (= 3.5-1build1), libsexplib0-ocaml (= 0.16.0-3build1), libsexplib0-ocaml-dev (= 0.16.0-3build1), libsframe1 (= 2.41-6ubuntu1), libsmartcols1 (= 2.39.1-4ubuntu2), libsqlite3-0 (= 3.44.0-1), libssl3 (= 3.0.10-1ubuntu2.1), libstdc++-13-dev (= 13.2.0-6ubuntu1), libstdc++6 (= 13.2.0-6ubuntu1), libstdlib-ocaml (= 4.14.1-1ubuntu1), libstdlib-ocaml-dev (= 4.14.1-1ubuntu1), libsub-override-perl (= 0.09-4), libsystemd0 (= 253.5-1ubuntu7), libtinfo6 (= 6.4+20231016-1), libtirpc-common (= 1.3.3+ds-1), libtirpc-dev (= 1.3.3+ds-1), libtirpc3 (= 1.3.3+ds-1), libtool (= 2.4.7-7), libuchardet0 (= 0.0.7-1build2), libudev1 (= 253.5-1ubuntu7), libunistring5 (= 1.1-2), libuuid1 (= 2.39.1-4ubuntu2), libxml2 (= 2.9.14+dfsg-1.3build1), libzarith-ocaml (= 1.13-2build1), libzarith-ocaml-dev (= 1.13-2build1), libzstd1 (= 1.5.5+dfsg2-2), linux-libc-dev (= 6.5.0-9.9), login (= 1:4.13+dfsg1-1ubuntu1), lto-disabled-list (= 43), m4 (= 1.4.19-4), make (= 4.3-4.1build1), man-db (= 2.12.0-1), mawk (= 1.3.4.20230808-1), media-types (= 10.1.0), ncurses-base (= 6.4+20231016-1), ncurses-bin (= 6.4+20231016-1), ocaml (= 4.14.1-1ubuntu1), ocaml-base (= 4.14.1-1ubuntu1), ocaml-findlib (= 1.9.6-1build2), ocaml-interp (= 4.14.1-1ubuntu1), ocaml-nox (= 4.14.1-1ubuntu1), patch (= 2.7.6-7build2), perl (= 5.36.0-9ubuntu1), perl-base (= 5.36.0-9ubuntu1), perl-modules-5.36 (= 5.36.0-9ubuntu1), po-debconf (= 1.0.21+nmu1), python3 (= 3.11.4-5ubuntu1), python3-minimal (= 3.11.4-5ubuntu1), python3.11 (= 3.11.6-3), python3.11-minimal (= 3.11.6-3), readline-common (= 8.2-1.3), rpcsvc-proto (= 1.4.2-0ubuntu6), sed (= 4.9-1), sensible-utils (= 0.0.20), sysvinit-utils (= 3.07-1ubuntu1), tar (= 1.34+dfsg-1.2ubuntu1), tzdata (= 2023c-9ubuntu1), util-linux (= 2.39.1-4ubuntu2), wdiff (= 1.2.2-6), xz-utils (= 5.4.4-0.1), zlib1g (= 1:1.2.13.dfsg-1ubuntu5) Environment: DEB_BUILD_OPTIONS="nocheck parallel=8" DEB_BUILD_PROFILES="noudeb" DEB_GCJFLAGS_SET="-fdebug-prefix-map=/<>=/usr/src/coq-hierarchy-builder-1.4.0-6build6" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1699125260" +------------------------------------------------------------------------------+ | Package contents | +------------------------------------------------------------------------------+ coq-hierarchy-builder_1.4.0-6build6_riscv64.deb ----------------------------------------------- new Debian package, version 2.0. size 831480 bytes: control archive=607 bytes. 632 bytes, 15 lines control 190 bytes, 3 lines md5sums Package: coq-hierarchy-builder Version: 1.4.0-6build6 Architecture: riscv64 Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 2235 Depends: libcoq-hierarchy-builder (= 1.4.0-6build6), ocaml-nox Section: ocaml Priority: optional Homepage: https://github.com/math-comp/hierarchy-builder Description: build hierarchies of algebraic structures in Coq (tool) This software provides high-level commands to build hierarchies of algebraic structures in the Coq system. . This package provides the command-line tool. drwxr-xr-x root/root 0 2023-11-04 19:14 ./ drwxr-xr-x root/root 0 2023-11-04 19:14 ./bin/ -rwxr-xr-x root/root 2273476 2023-11-04 19:14 ./bin/coq.hb drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/doc/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/doc/coq-hierarchy-builder/ lrwxrwxrwx root/root 0 2023-11-04 19:14 ./usr/share/doc/coq-hierarchy-builder/changelog.Debian.gz -> ../libcoq-hierarchy-builder/changelog.Debian.gz -rw-r--r-- root/root 1317 2023-07-26 07:12 ./usr/share/doc/coq-hierarchy-builder/copyright drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/man/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/man/man1/ -rw-r--r-- root/root 631 2023-11-04 19:14 ./usr/share/man/man1/coq.hb.1.gz libcoq-hierarchy-builder_1.4.0-6build6_riscv64.deb -------------------------------------------------- new Debian package, version 2.0. size 266504 bytes: control archive=751 bytes. 700 bytes, 18 lines control 511 bytes, 6 lines md5sums Package: libcoq-hierarchy-builder Source: coq-hierarchy-builder Version: 1.4.0-6build6 Architecture: riscv64 Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 693 Depends: libcoq-elpi-74ir9 Recommends: ocaml-findlib Provides: libcoq-hierarchy-builder-xpkw9 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/hierarchy-builder Description: build hierarchies of algebraic structures in Coq (runtime files) This software provides high-level commands to build hierarchies of algebraic structures in the Coq system. . This package provides the runtime files. drwxr-xr-x root/root 0 2023-11-04 19:14 ./ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/lib/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/lib/ocaml/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/lib/ocaml/coq/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/lib/ocaml/coq/user-contrib/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/lib/ocaml/coq/user-contrib/HB/ -rw-r--r-- root/root 6461 2023-11-04 19:14 ./usr/lib/ocaml/coq/user-contrib/HB/structures.glob -rw-r--r-- root/root 40128 2023-11-04 19:14 ./usr/lib/ocaml/coq/user-contrib/HB/structures.v -rw-r--r-- root/root 640763 2023-11-04 19:14 ./usr/lib/ocaml/coq/user-contrib/HB/structures.vo drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/doc/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./usr/share/doc/libcoq-hierarchy-builder/ -rw-r--r-- root/root 510 2023-11-04 19:14 ./usr/share/doc/libcoq-hierarchy-builder/changelog.Debian.gz -rw-r--r-- root/root 1317 2023-07-26 07:12 ./usr/share/doc/libcoq-hierarchy-builder/copyright drwxr-xr-x root/root 0 2023-11-04 19:14 ./var/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./var/lib/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./var/lib/coq/ drwxr-xr-x root/root 0 2023-11-04 19:14 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2023-11-04 19:14 ./var/lib/coq/md5sums/libcoq-hierarchy-builder.checksum +------------------------------------------------------------------------------+ | Post Build | +------------------------------------------------------------------------------+ +------------------------------------------------------------------------------+ | Cleanup | +------------------------------------------------------------------------------+ Purging /<> Not removing build depends: as requested +------------------------------------------------------------------------------+ | Summary | +------------------------------------------------------------------------------+ Build Architecture: riscv64 Build Type: any Build-Space: 20068 Build-Time: 1028 Distribution: noble-proposed Host Architecture: riscv64 Install-Time: 644 Job: coq-hierarchy-builder_1.4.0-6build6.dsc Machine Architecture: riscv64 Package: coq-hierarchy-builder Package-Time: 1697 Source-Version: 1.4.0-6build6 Space: 20068 Status: successful Version: 1.4.0-6build6 -------------------------------------------------------------------------------- Finished at 2023-11-05T15:41:21Z Build needed 00:28:17, 20068k disk space RUN: /usr/share/launchpad-buildd/bin/in-target scan-for-processes --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 Scanning for processes to kill in build PACKAGEBUILD-26962111 RUN: /usr/share/launchpad-buildd/bin/in-target umount-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 Stopping target for build PACKAGEBUILD-26962111 RUN: /usr/share/launchpad-buildd/bin/in-target remove-build --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962111 Removing build PACKAGEBUILD-26962111