Diff of the two buildlogs: -- --- b1/build.log 2023-04-15 23:32:59.723711062 +0000 +++ b2/build.log 2023-04-15 23:36:31.994294535 +0000 @@ -1,7 +1,6 @@ -W: cgroups are not available on the host, not using them. I: pbuilder: network access will be disabled during build -I: Current time: Sat Apr 15 11:28:49 -12 2023 -I: pbuilder-time-stamp: 1681601329 +I: Current time: Sat May 18 19:58:01 +14 2024 +I: pbuilder-time-stamp: 1716011881 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -18,7 +17,7 @@ I: copying [./coq-hierarchy-builder_1.4.0.orig.tar.gz] I: copying [./coq-hierarchy-builder_1.4.0-2.debian.tar.xz] I: Extracting source -gpgv: Signature made Tue Oct 25 18:55:06 2022 -12 +gpgv: Signature made Wed Oct 26 20:55:06 2022 +14 gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 gpgv: issuer "jpuydt@debian.org" gpgv: Can't check signature: No public key @@ -28,136 +27,169 @@ dpkg-source: info: unpacking coq-hierarchy-builder_1.4.0-2.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/19587/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/D01_modify_environment starting +debug: Running on ionos16-i386. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 May 18 19:58 /bin/sh -> /bin/bash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='i386' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=8' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='i386' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="15" [3]="1" [4]="release" [5]="i686-pc-linux-gnu") + BASH_VERSION='5.2.15(1)-release' + BUILDDIR=/build + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=i386 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=15' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=i686 + HOST_ARCH=i386 IFS=' ' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - LD_LIBRARY_PATH='/usr/lib/libeatmydata' - LD_PRELOAD='libeatmydata.so' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='19587' - PS1='# ' - PS2='> ' + INVOCATION_ID=5c59f9b1391443baa7bf4e9ba2b45040 + LANG=C + LANGUAGE=de_CH:de + LC_ALL=C + LD_LIBRARY_PATH=/usr/lib/libeatmydata + LD_PRELOAD=libeatmydata.so + MACHTYPE=i686-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=100152 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.oj7sDacU/pbuilderrc_l55c --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.oj7sDacU/b1 --logfile b1/build.log coq-hierarchy-builder_1.4.0-2.dsc' - SUDO_GID='112' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/sbin/chroot' - http_proxy='http://78.137.99.97:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.oj7sDacU/pbuilderrc_Ro4L --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.oj7sDacU/b2 --logfile b2/build.log --extrapackages usrmerge coq-hierarchy-builder_1.4.0-2.dsc' + SUDO_GID=112 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://85.184.249.68:3128 I: uname -a - Linux ionos12-i386 5.10.0-21-686-pae #1 SMP Debian 5.10.162-1 (2023-01-21) i686 GNU/Linux + Linux i-capture-the-hostname 5.10.0-21-amd64 #1 SMP Debian 5.10.162-1 (2023-01-21) x86_64 GNU/Linux I: ls -l /bin total 6036 - -rwxr-xr-x 1 root root 1408088 Feb 12 08:21 bash - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bunzip2 - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bzcat - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzcmp -> bzdiff - -rwxr-xr-x 1 root root 2225 Sep 18 2022 bzdiff - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzegrep -> bzgrep - -rwxr-xr-x 1 root root 4893 Nov 27 2021 bzexe - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzfgrep -> bzgrep - -rwxr-xr-x 1 root root 3775 Sep 18 2022 bzgrep - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bzip2 - -rwxr-xr-x 1 root root 17892 Sep 18 2022 bzip2recover - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzless -> bzmore - -rwxr-xr-x 1 root root 1297 Sep 18 2022 bzmore - -rwxr-xr-x 1 root root 42920 Sep 20 2022 cat - -rwxr-xr-x 1 root root 79816 Sep 20 2022 chgrp - -rwxr-xr-x 1 root root 67496 Sep 20 2022 chmod - -rwxr-xr-x 1 root root 79816 Sep 20 2022 chown - -rwxr-xr-x 1 root root 162024 Sep 20 2022 cp - -rwxr-xr-x 1 root root 136916 Jan 5 01:20 dash - -rwxr-xr-x 1 root root 137160 Sep 20 2022 date - -rwxr-xr-x 1 root root 100364 Sep 20 2022 dd - -rwxr-xr-x 1 root root 108940 Sep 20 2022 df - -rwxr-xr-x 1 root root 162152 Sep 20 2022 dir - -rwxr-xr-x 1 root root 87760 Mar 22 22:20 dmesg - lrwxrwxrwx 1 root root 8 Dec 19 01:33 dnsdomainname -> hostname - lrwxrwxrwx 1 root root 8 Dec 19 01:33 domainname -> hostname - -rwxr-xr-x 1 root root 38760 Sep 20 2022 echo - -rwxr-xr-x 1 root root 41 Jan 24 02:43 egrep - -rwxr-xr-x 1 root root 34664 Sep 20 2022 false - -rwxr-xr-x 1 root root 41 Jan 24 02:43 fgrep - -rwxr-xr-x 1 root root 84272 Mar 22 22:20 findmnt - -rwsr-xr-x 1 root root 30240 Mar 22 20:38 fusermount - -rwxr-xr-x 1 root root 218680 Jan 24 02:43 grep - -rwxr-xr-x 2 root root 2346 Apr 9 2022 gunzip - -rwxr-xr-x 1 root root 6447 Apr 9 2022 gzexe - -rwxr-xr-x 1 root root 100952 Apr 9 2022 gzip - -rwxr-xr-x 1 root root 21916 Dec 19 01:33 hostname - -rwxr-xr-x 1 root root 75756 Sep 20 2022 ln - -rwxr-xr-x 1 root root 55600 Mar 22 23:43 login - -rwxr-xr-x 1 root root 162152 Sep 20 2022 ls - -rwxr-xr-x 1 root root 214568 Mar 22 22:20 lsblk - -rwxr-xr-x 1 root root 96328 Sep 20 2022 mkdir - -rwxr-xr-x 1 root root 84008 Sep 20 2022 mknod - -rwxr-xr-x 1 root root 38792 Sep 20 2022 mktemp - -rwxr-xr-x 1 root root 63016 Mar 22 22:20 more - -rwsr-xr-x 1 root root 58912 Mar 22 22:20 mount - -rwxr-xr-x 1 root root 13856 Mar 22 22:20 mountpoint - -rwxr-xr-x 1 root root 157932 Sep 20 2022 mv - lrwxrwxrwx 1 root root 8 Dec 19 01:33 nisdomainname -> hostname - lrwxrwxrwx 1 root root 14 Apr 2 18:25 pidof -> /sbin/killall5 - -rwxr-xr-x 1 root root 38792 Sep 20 2022 pwd - lrwxrwxrwx 1 root root 4 Feb 12 08:21 rbash -> bash - -rwxr-xr-x 1 root root 51080 Sep 20 2022 readlink - -rwxr-xr-x 1 root root 75720 Sep 20 2022 rm - -rwxr-xr-x 1 root root 51080 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 22308 Nov 2 04:31 run-parts - -rwxr-xr-x 1 root root 133224 Jan 5 07:55 sed - lrwxrwxrwx 1 root root 4 Jan 5 01:20 sh -> dash - -rwxr-xr-x 1 root root 38760 Sep 20 2022 sleep - -rwxr-xr-x 1 root root 87976 Sep 20 2022 stty - -rwsr-xr-x 1 root root 83492 Mar 22 22:20 su - -rwxr-xr-x 1 root root 38792 Sep 20 2022 sync - -rwxr-xr-x 1 root root 598456 Apr 6 02:25 tar - -rwxr-xr-x 1 root root 13860 Nov 2 04:31 tempfile - -rwxr-xr-x 1 root root 120776 Sep 20 2022 touch - -rwxr-xr-x 1 root root 34664 Sep 20 2022 true - -rwxr-xr-x 1 root root 17892 Mar 22 20:38 ulockmgr_server - -rwsr-xr-x 1 root root 30236 Mar 22 22:20 umount - -rwxr-xr-x 1 root root 38760 Sep 20 2022 uname - -rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress - -rwxr-xr-x 1 root root 162152 Sep 20 2022 vdir - -rwxr-xr-x 1 root root 71216 Mar 22 22:20 wdctl - lrwxrwxrwx 1 root root 8 Dec 19 01:33 ypdomainname -> hostname - -rwxr-xr-x 1 root root 1984 Apr 9 2022 zcat - -rwxr-xr-x 1 root root 1678 Apr 9 2022 zcmp - -rwxr-xr-x 1 root root 6460 Apr 9 2022 zdiff - -rwxr-xr-x 1 root root 29 Apr 9 2022 zegrep - -rwxr-xr-x 1 root root 29 Apr 9 2022 zfgrep - -rwxr-xr-x 1 root root 2081 Apr 9 2022 zforce - -rwxr-xr-x 1 root root 8103 Apr 9 2022 zgrep - -rwxr-xr-x 1 root root 2206 Apr 9 2022 zless - -rwxr-xr-x 1 root root 1842 Apr 9 2022 zmore - -rwxr-xr-x 1 root root 4577 Apr 9 2022 znew -I: user script /srv/workspace/pbuilder/19587/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1408088 Feb 13 2023 bash + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bunzip2 + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bzcat + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzcmp -> bzdiff + -rwxr-xr-x 1 root root 2225 Sep 19 2022 bzdiff + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzegrep -> bzgrep + -rwxr-xr-x 1 root root 4893 Nov 28 2021 bzexe + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzfgrep -> bzgrep + -rwxr-xr-x 1 root root 3775 Sep 19 2022 bzgrep + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bzip2 + -rwxr-xr-x 1 root root 17892 Sep 19 2022 bzip2recover + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzless -> bzmore + -rwxr-xr-x 1 root root 1297 Sep 19 2022 bzmore + -rwxr-xr-x 1 root root 42920 Sep 21 2022 cat + -rwxr-xr-x 1 root root 79816 Sep 21 2022 chgrp + -rwxr-xr-x 1 root root 67496 Sep 21 2022 chmod + -rwxr-xr-x 1 root root 79816 Sep 21 2022 chown + -rwxr-xr-x 1 root root 162024 Sep 21 2022 cp + -rwxr-xr-x 1 root root 136916 Jan 6 2023 dash + -rwxr-xr-x 1 root root 137160 Sep 21 2022 date + -rwxr-xr-x 1 root root 100364 Sep 21 2022 dd + -rwxr-xr-x 1 root root 108940 Sep 21 2022 df + -rwxr-xr-x 1 root root 162152 Sep 21 2022 dir + -rwxr-xr-x 1 root root 87760 Mar 24 2023 dmesg + lrwxrwxrwx 1 root root 8 Dec 20 2022 dnsdomainname -> hostname + lrwxrwxrwx 1 root root 8 Dec 20 2022 domainname -> hostname + -rwxr-xr-x 1 root root 38760 Sep 21 2022 echo + -rwxr-xr-x 1 root root 41 Jan 25 2023 egrep + -rwxr-xr-x 1 root root 34664 Sep 21 2022 false + -rwxr-xr-x 1 root root 41 Jan 25 2023 fgrep + -rwxr-xr-x 1 root root 84272 Mar 24 2023 findmnt + -rwsr-xr-x 1 root root 30240 Mar 23 2023 fusermount + -rwxr-xr-x 1 root root 218680 Jan 25 2023 grep + -rwxr-xr-x 2 root root 2346 Apr 10 2022 gunzip + -rwxr-xr-x 1 root root 6447 Apr 10 2022 gzexe + -rwxr-xr-x 1 root root 100952 Apr 10 2022 gzip + -rwxr-xr-x 1 root root 21916 Dec 20 2022 hostname + -rwxr-xr-x 1 root root 75756 Sep 21 2022 ln + -rwxr-xr-x 1 root root 55600 Mar 24 2023 login + -rwxr-xr-x 1 root root 162152 Sep 21 2022 ls + -rwxr-xr-x 1 root root 214568 Mar 24 2023 lsblk + -rwxr-xr-x 1 root root 96328 Sep 21 2022 mkdir + -rwxr-xr-x 1 root root 84008 Sep 21 2022 mknod + -rwxr-xr-x 1 root root 38792 Sep 21 2022 mktemp + -rwxr-xr-x 1 root root 63016 Mar 24 2023 more + -rwsr-xr-x 1 root root 58912 Mar 24 2023 mount + -rwxr-xr-x 1 root root 13856 Mar 24 2023 mountpoint + -rwxr-xr-x 1 root root 157932 Sep 21 2022 mv + lrwxrwxrwx 1 root root 8 Dec 20 2022 nisdomainname -> hostname + lrwxrwxrwx 1 root root 14 Apr 3 2023 pidof -> /sbin/killall5 + -rwxr-xr-x 1 root root 38792 Sep 21 2022 pwd + lrwxrwxrwx 1 root root 4 Feb 13 2023 rbash -> bash + -rwxr-xr-x 1 root root 51080 Sep 21 2022 readlink + -rwxr-xr-x 1 root root 75720 Sep 21 2022 rm + -rwxr-xr-x 1 root root 51080 Sep 21 2022 rmdir + -rwxr-xr-x 1 root root 22308 Nov 3 2022 run-parts + -rwxr-xr-x 1 root root 133224 Jan 6 2023 sed + lrwxrwxrwx 1 root root 9 May 18 19:58 sh -> /bin/bash + -rwxr-xr-x 1 root root 38760 Sep 21 2022 sleep + -rwxr-xr-x 1 root root 87976 Sep 21 2022 stty + -rwsr-xr-x 1 root root 83492 Mar 24 2023 su + -rwxr-xr-x 1 root root 38792 Sep 21 2022 sync + -rwxr-xr-x 1 root root 598456 Apr 7 2023 tar + -rwxr-xr-x 1 root root 13860 Nov 3 2022 tempfile + -rwxr-xr-x 1 root root 120776 Sep 21 2022 touch + -rwxr-xr-x 1 root root 34664 Sep 21 2022 true + -rwxr-xr-x 1 root root 17892 Mar 23 2023 ulockmgr_server + -rwsr-xr-x 1 root root 30236 Mar 24 2023 umount + -rwxr-xr-x 1 root root 38760 Sep 21 2022 uname + -rwxr-xr-x 2 root root 2346 Apr 10 2022 uncompress + -rwxr-xr-x 1 root root 162152 Sep 21 2022 vdir + -rwxr-xr-x 1 root root 71216 Mar 24 2023 wdctl + lrwxrwxrwx 1 root root 8 Dec 20 2022 ypdomainname -> hostname + -rwxr-xr-x 1 root root 1984 Apr 10 2022 zcat + -rwxr-xr-x 1 root root 1678 Apr 10 2022 zcmp + -rwxr-xr-x 1 root root 6460 Apr 10 2022 zdiff + -rwxr-xr-x 1 root root 29 Apr 10 2022 zegrep + -rwxr-xr-x 1 root root 29 Apr 10 2022 zfgrep + -rwxr-xr-x 1 root root 2081 Apr 10 2022 zforce + -rwxr-xr-x 1 root root 8103 Apr 10 2022 zgrep + -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless + -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore + -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -282,7 +314,7 @@ Get: 75 http://deb.debian.org/debian bookworm/main i386 libelpi-ocaml-dev i386 1.16.8-1+b2 [10.1 MB] Get: 76 http://deb.debian.org/debian bookworm/main i386 libcoq-elpi i386 1.16.0-2+b1 [2354 kB] Get: 77 http://deb.debian.org/debian bookworm/main i386 wdiff i386 1.2.2-5 [120 kB] -Fetched 346 MB in 6s (58.8 MB/s) +Fetched 346 MB in 7s (46.6 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:i386. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19604 files and directories currently installed.) @@ -606,8 +638,19 @@ Writing extended state information... Building tag database... -> Finished parsing the build-deps +Reading package lists... +Building dependency tree... +Reading state information... +usrmerge is already the newest version (35). +0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/coq-hierarchy-builder-1.4.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-hierarchy-builder_1.4.0-2_source.changes +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/A99_set_merged_usr starting +Re-configuring usrmerge... +removed '/etc/unsupported-skip-usrmerge-conversion' +The system has been successfully converted. +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/coq-hierarchy-builder-1.4.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../coq-hierarchy-builder_1.4.0-2_source.changes dpkg-buildpackage: info: source package coq-hierarchy-builder dpkg-buildpackage: info: source version 1.4.0-2 dpkg-buildpackage: info: source distribution unstable @@ -617,7 +660,7 @@ debian/rules clean dh clean --with coq,ocaml dh_auto_clean - make -j8 distclean + make -j15 distclean make[1]: Entering directory '/build/coq-hierarchy-builder-1.4.0' rm -f Makefile.coq Makefile.coq.conf rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf @@ -632,7 +675,7 @@ dh_ocamlinit dh_auto_configure dh_auto_build - make -j8 "INSTALL=install --strip-program=true" + make -j15 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-hierarchy-builder-1.4.0' make config make[2]: Entering directory '/build/coq-hierarchy-builder-1.4.0' @@ -670,8 +713,14 @@ COQC examples/demo1/hierarchy_4.v COQC examples/demo1/hierarchy_5.v COQC examples/demo2/classical.v -[1681601396.436835] HB: start module and section AddComoid_of_Type -[1681601396.437211] HB: converting arguments +COQC examples/demo3/hierarchy_0.v +COQC examples/demo3/hierarchy_1.v +COQC examples/demo3/hierarchy_2.v +COQC examples/demo4/hierarchy_0.v +COQC examples/demo5/hierarchy_0.v +COQC examples/FSCD2020_material/V1.v +[1716011933.408769] HB: start module and section AddComoid_of_Type +[1716011933.409131] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -697,25 +746,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1681601396.437862] HB: processing key parameter -[1681601396.438427] HB: converting factories +[1716011933.409633] HB: processing key parameter +[1716011933.410125] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1681601396.438531] HB: declaring context +[1716011933.410202] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1681601396.438702] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -[1681601396.446780] HB: declare mixin or factory -[1681601396.446856] HB: declare record axioms_ -[1681601396.472346] HB: declare notation Build -[1681601396.482442] HB: begin module for builders -[1681601396.482677] HB: postulating factories -[1681601396.482805] HB: processing key context-item -[1681601396.483079] HB: processing mixin parameter a -[1681601396.483426] HB: declaring parameters and key as section variables -[1681601396.486729] HB: declare notation axioms +[1716011933.410351] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1681601396.508205] HB: start module Exports -[1681601396.530398] HB: end modules and sections; export +[1716011933.415816] HB: declare mixin or factory +[1716011933.415897] HB: declare record axioms_ +[1716011933.431665] HB: declare notation Build +[1716011933.440750] HB: declare notation axioms +[1716011933.454998] HB: start module Exports +[1716011933.468482] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -772,65 +815,65 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1681601396.633069] HB: start module AddComoid -[1681601396.633331] HB: declare axioms record +[1716011933.518611] HB: start module AddComoid +[1716011933.518859] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1681601396.633605] HB: typing class field +[1716011933.519075] HB: typing class field indt «AddComoid_of_Type.axioms_» -[1681601396.748560] HB: declare type record -[1681601396.760573] HB: structure: new mixins +[1716011933.604074] HB: declare type record +[1716011933.610557] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1681601396.760699] HB: structure: mixin first class +[1716011933.610645] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1681601396.760792] HB: declaring clone abbreviation -[1681601396.772407] HB: declaring pack_ constant -[1681601396.773315] HB: declaring pack_ constant = +[1716011933.610731] HB: declaring clone abbreviation +[1716011933.617580] HB: declaring pack_ constant +[1716011933.618334] 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]] -[1681601396.775750] HB: start module Exports -[1681601396.775957] HB: making coercion from type to target -[1681601396.775997] HB: declare sort coercion -[1681601396.776300] HB: exporting unification hints -[1681601396.776495] HB: exporting coercions from class to mixins -[1681601396.776745] HB: export class to mixin coercion for mixin +[1716011933.619818] HB: start module Exports +[1716011933.620022] HB: making coercion from type to target +[1716011933.620086] HB: declare sort coercion +[1716011933.620388] HB: exporting unification hints +[1716011933.620587] HB: exporting coercions from class to mixins +[1716011933.620837] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1681601396.777094] HB: accumulating various props -[1681601396.787390] HB: stop module Exports -[1681601396.787977] HB: declaring on_ abbreviation -[1681601396.797067] HB: declaring `copy` abbreviation -[1681601396.797981] HB: declaring on abbreviation -[1681601396.799001] HB: eta expanded instances -[1681601396.800794] HB: postulating A -[1681601396.817351] HB: declare mixin instance +[1716011933.621180] HB: accumulating various props +[1716011933.627657] HB: stop module Exports +[1716011933.628066] HB: declaring on_ abbreviation +[1716011933.633816] HB: declaring `copy` abbreviation +[1716011933.634494] HB: declaring on abbreviation +[1716011933.635385] HB: eta expanded instances +[1716011933.636574] HB: postulating A +[1716011933.646837] HB: declare mixin instance readme_AddComoid__to__readme_AddComoid_of_Type -[1681601396.824041] HB: we can build a readme_AddComoid on eta A -[1681601396.824381] HB: declare canonical structure instance +[1716011933.650641] HB: we can build a readme_AddComoid on eta A +[1716011933.650956] HB: declare canonical structure instance structures_eta__canonical__readme_AddComoid -[1681601396.824876] HB: Giving name HB_unnamed_mixin_4 to mixin instance +[1716011933.651306] HB: Giving name HB_unnamed_mixin_4 to mixin instance readme_AddComoid_of_Type_mixin (eta A) HB_unnamed_factory_2 -[1681601396.828089] HB: structure instance for +[1716011933.653160] HB: structure instance for structures_eta__canonical__readme_AddComoid is {| sort := eta A; class := {| readme_AddComoid_of_Type_mixin := HB_unnamed_mixin_4 |} |} -[1681601396.833805] HB: structure instance +[1716011933.656148] HB: structure instance structures_eta__canonical__readme_AddComoid declared -[1681601396.833938] HB: closing instance section -[1681601396.835963] HB: end modules; export +[1716011933.656224] HB: closing instance section +[1716011933.657449] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1681601396.837446] HB: export +[1716011933.658228] HB: export «HB.examples.readme.AddComoid.EtaAndMixinExports» -[1681601396.838837] HB: exporting operations -[1681601396.839997] HB: export operation zero -[1681601396.843854] HB: export operation add -[1681601396.847993] HB: export operation addrA -[1681601396.852934] HB: export operation addrC -[1681601396.856963] HB: export operation add0r -[1681601396.859805] HB: operations meta-data module: ElpiOperations -[1681601396.867155] HB: abbreviation factory-by-classname +[1716011933.658979] HB: exporting operations +[1716011933.659771] HB: export operation zero +[1716011933.661631] HB: export operation add +[1716011933.663829] HB: export operation addrA +[1716011933.666205] HB: export operation addrC +[1716011933.668514] HB: export operation add0r +[1716011933.670200] HB: operations meta-data module: ElpiOperations +[1716011933.674763] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -945,63 +988,35 @@ *) 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 -HB: Z is canonically equipped with structures: - - AbelianGrp - (from "./examples/readme.v", line 32) - - AddComoid - (from "./examples/readme.v", line 31) - -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] -COQC examples/demo3/hierarchy_1.v -[1681601398.285338] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1681601398.285485] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -COQC examples/demo3/hierarchy_2.v -COQC examples/demo3/test_0_0.v -COQC examples/demo4/hierarchy_0.v -COQC examples/demo5/hierarchy_0.v -File "./examples/hulk.v", line 143, characters 0-63: -Warning: -pulling in dependencies: [Feather_HasEqDec] - -Please list them or end the declaration with '&' -[HB.implicit-structure-dependency,HB] -COQC examples/FSCD2020_material/V1.v +COQC examples/FSCD2020_material/V2.v inhab : ?s where ?T : [ |- Type] ?s : [ |- s1.type ?T] -COQC examples/FSCD2020_material/V2.v eq_refl : inhab = 7 : inhab = 7 eq_refl : inhab = (7 :: nil)%list : inhab = (7 :: nil)%list where ?T : [ |- Type] -HB: A is canonically equipped with structures: - - Equality - Singleton - (from "./examples/hulk.v", line 216) - -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. +[1716011934.059778] HB: begin module for builders +[1716011934.060600] HB: postulating factories +[1716011934.060717] HB: processing key context-item +[1716011934.060978] HB: processing mixin parameter a +[1716011934.061253] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] COQC examples/FSCD2020_material/V3.v +AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp + (Phant BinNums_Z__canonical__readme_AbelianGrp) + : AbelianGrp.axioms_ Z + : AbelianGrp.axioms_ Z +HB: Z is canonically equipped with structures: + - AbelianGrp + (from "./examples/readme.v", line 32) + - AddComoid + (from "./examples/readme.v", line 31) + Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1010,44 +1025,41 @@ @addNr : forall s : Ring.type, left_inverse 0 opp add COQC examples/FSCD2020_material/V4.v -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_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 : AbelianGroup.type, left_inverse 0 opp add -@addrC - : forall s : AbelianGroup.type, commutative add COQC examples/FSCD2020_talk/V3.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/Coq2020_material/CoqWS_demo.v +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] COQC examples/Coq2020_material/CoqWS_abstract.v -COQC examples/Coq2020_material/CoqWS_expansion/withHB.v -Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. +File "./examples/hulk.v", line 143, characters 0-63: +Warning: +pulling in dependencies: [Feather_HasEqDec] -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/withoutHB.v +Please list them or end the declaration with '&' +[HB.implicit-structure-dependency,HB] 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 examples/Coq2020_material/CoqWS_expansion/withHB.v +COQC examples/Coq2020_material/CoqWS_expansion/withoutHB.v +[1716011935.499695] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1716011935.499889] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG add : ?s -> ?s -> ?s where @@ -1056,6 +1068,15 @@ : commutative add where ?s : [ |- CMonoid.type] +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 File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] @@ -1063,31 +1084,48 @@ Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] COQC tests/type_of_exported_ops.v +COQC tests/duplicate_structure.v +forall x y : ?t, x - (y + 0) = x + : Prop +where +?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + +COQC tests/instance_params_no_type.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] +COQC tests/test_CS_db_filtering.v addrC : commutative add where ?s : [ |- CMonoid.type] -forall x y : ?t, x - (y + 0) = x +COQC tests/subtype.v +COQC tests/infer.v +forall x y : ?t, 1 + x = y * x : Prop where -?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) -COQC tests/duplicate_structure.v +?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) +COQC tests/exports.v 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, 1 + x = y * x - : Prop -where -?t : [x : ?t y : ?t |- SemiRing.type] (x, y cannot be used) -COQC tests/test_CS_db_filtering.v -COQC tests/subtype.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 tests/log_impargs_record.v forall (R : Ring.type) (x y : R), 1 * x = y - x : Prop forall @@ -1098,108 +1136,12 @@ ?t : [x : join_CoqWS_demo_Ring_between_CoqWS_demo_AbelianGrp_and_CoqWS_demo_SemiRing ?t y : ?t |- Ring.type] (x, y cannot be used) -COQC tests/infer.v -forall x : Z, x * - (1 + x) = 0 + 1 - : Prop -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 -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 -HB.check: bar.type_ bool Datatypes_nat__canonical__infer_foo bool : Type -File "./tests/infer.v", line 20, characters 0-58: -Warning: Skipping test on Coq 8.16.1 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 -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/funclass.v -[1681601407.355749] HB: start module SubInhab -[1681601407.355956] HB: declare axioms record -w-params.cons T (sort (typ «HB.tests.subtype.345»)) c0 \ - w-params.cons P (app [global (const «pred»), c0]) c1 \ - w-params.nil sT (sort (typ «HB.tests.subtype.347»)) c2 \ - [triple (indt «is_inhab.axioms_») [] c2, - triple (indt «is_SUB.axioms_») [c0, c1] c2] -[1681601407.356207] HB: typing class field indt «is_inhab.axioms_» -[1681601407.356423] HB: typing class field indt «is_SUB.axioms_» -[1681601407.365098] HB: declare type record -[1681601407.373864] HB: structure: new mixins [] -[1681601407.373958] HB: structure: mixin first class [] -[1681601407.373996] HB: declaring clone abbreviation -[1681601407.383528] HB: declaring pack_ constant -[1681601407.386082] HB: declaring pack_ constant = -fun `T` (sort (typ «HB.tests.subtype.345»)) c0 \ - fun `P` (app [global (const «pred»), c0]) c1 \ - fun `sT` (sort (typ «HB.tests.subtype.347»)) 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]] -[1681601407.388282] HB: start module Exports -[1681601407.388454] HB: making coercion from type to target -[1681601407.388517] HB: declare sort coercion -[1681601407.388806] HB: exporting unification hints -[1681601407.391029] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1681601407.392274] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1681601407.400087] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB -bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) - : Type -[1681601407.407256] HB: declare coercion path compression rules -[1681601407.408941] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1681601407.409919] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1681601407.417230] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop COQC tests/grefclass.v -[1681601407.425355] HB: declare coercion path compression rules -[1681601407.460863] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -[1681601407.470514] HB: exporting coercions from class to mixins -[1681601407.471392] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1681601407.473213] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1681601407.474386] HB: accumulating various props -[1681601407.491126] HB: stop module Exports -[1681601407.494515] HB: declaring on_ abbreviation -[1681601407.505700] HB: declaring `copy` abbreviation -[1681601407.506821] HB: declaring on abbreviation -[1681601407.509301] HB: eta expanded instances -[1681601407.513222] HB: postulating T -[1681601407.521358] HB: postulating P -[1681601407.523855] HB: postulating sT +COQC tests/local_instance.v (* Module A. @@ -1248,40 +1190,9 @@ Notation A X1 := ( A.phant_axioms X1). *) -[1681601407.552538] HB: declare mixin instance -subtype_SubInhab__to__subtype_is_inhab -[1681601407.575127] HB: declare mixin instance -subtype_SubInhab__to__subtype_is_SUB -COQC tests/local_instance.v -[1681601407.593473] HB: skipping already existing subtype_Inhab instance on -eta sT -[1681601407.594516] HB: skipping already existing subtype_Nontrivial -instance on eta sT -[1681601407.595480] HB: skipping already existing subtype_SUB instance on -eta sT -[1681601407.598694] HB: we can build a subtype_SubInhab on eta sT -[1681601407.598982] HB: declare canonical structure instance -structures_eta__canonical__subtype_SubInhab -[1681601407.599986] 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 - |} -|} -[1681601407.609885] HB: structure instance -structures_eta__canonical__subtype_SubInhab declared -[1681601407.609998] HB: closing instance section -[1681601407.612088] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -[1681601407.615981] HB: export -«HB.tests.subtype.SubInhab.EtaAndMixinExports» -[1681601407.616891] HB: exporting operations -[1681601407.617141] HB: operations meta-data module: ElpiOperations -[1681601407.618354] HB: abbreviation factory-by-classname +COQC tests/lock.v +add + : A -> A -> A A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True @@ -1289,93 +1200,235 @@ Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p -COQC tests/lock.v -[1681601408.357272] HB: exporting under the module path [] -[1681601408.357655] 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] -[1681601408.360183] HB: exporting CS instances -[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1681601408.360801] 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 +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 +HB.check: bar.type_ bool Datatypes_nat__canonical__infer_foo bool : Type +File "./tests/infer.v", line 20, characters 0-58: +Warning: Skipping test on Coq 8.16.1 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 +COQC tests/not_same_key.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/hb_pack.v +COQC tests/declare.v +forall x : Z, x * - (1 + x) = 0 + 1 + : Prop +COQC tests/short.v +default : nat + : nat p : pred nat : pred nat -COQC tests/not_same_key.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 +COQC tests/primitive_records.v +The command did fail as expected with message: +The term "default" has type "nonempty.sort ?t" +while it is expected to have type "nat". 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] -default : nat - : nat +COQC tests/non_forgetful_inheritance.v +bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) + : Type +[1716011937.972924] HB: exporting under the module path [] +[1716011937.973335] 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] +[1716011937.975837] HB: exporting CS instances +[«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] +[1716011937.976416] HB: exporting Abbreviations [addr0, addrNK] 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 -COQC tests/hb_pack.v -The command did fail as expected with message: -The term "default" has type "nonempty.sort ?t" -while it is expected to have type "nat". -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big -COQC tests/declare.v -COQC tests/short.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 -COQC tests/primitive_records.v -[1681601409.716526] HB: start module and section hasA -[1681601409.716806] HB: converting arguments +forall (R : Enclosing.Ring.type) (x : R), x = x + : Prop +0%G + : ?s +where +?s : [ |- Enclosing.Ring.type] +Enclosing.zero : Z + : Z +COQC tests/fix_loop.v +[1716011938.017397] HB: start module SubInhab +[1716011938.017638] HB: declare axioms record +w-params.cons T (sort (typ «HB.tests.subtype.345»)) c0 \ + w-params.cons P (app [global (const «pred»), c0]) c1 \ + w-params.nil sT (sort (typ «HB.tests.subtype.347»)) c2 \ + [triple (indt «is_inhab.axioms_») [] c2, + triple (indt «is_SUB.axioms_») [c0, c1] c2] +[1716011938.017944] HB: typing class field indt «is_inhab.axioms_» +[1716011938.018234] HB: typing class field indt «is_SUB.axioms_» +COQC tests/test_synthesis_params.v +[1716011938.027034] HB: declare type record +[1716011938.035715] HB: structure: new mixins [] +[1716011938.035815] HB: structure: mixin first class [] +[1716011938.035855] HB: declaring clone abbreviation +[1716011938.044652] HB: declaring pack_ constant +[1716011938.047217] HB: declaring pack_ constant = +fun `T` (sort (typ «HB.tests.subtype.345»)) c0 \ + fun `P` (app [global (const «pred»), c0]) c1 \ + fun `sT` (sort (typ «HB.tests.subtype.347»)) 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]] +[1716011938.049662] HB: start module Exports +[1716011938.049862] HB: making coercion from type to target +[1716011938.049937] HB: declare sort coercion +[1716011938.050234] HB: exporting unification hints +[1716011938.052300] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1716011938.053386] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1716011938.061071] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB +[1716011938.069043] HB: declare coercion path compression rules +[1716011938.070975] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1716011938.072080] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1716011938.080412] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab +[1716011938.088875] HB: declare coercion path compression rules +[1716011938.109120] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1716011938.117636] HB: exporting coercions from class to mixins +[1716011938.118222] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1716011938.119906] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1716011938.120983] HB: accumulating various props +[1716011938.135333] HB: stop module Exports +[1716011938.138163] HB: declaring on_ abbreviation +[1716011938.147623] HB: declaring `copy` abbreviation +[1716011938.148517] HB: declaring on abbreviation +[1716011938.150419] HB: eta expanded instances +[1716011938.153813] HB: postulating T +[1716011938.160872] HB: postulating P +[1716011938.163232] HB: postulating sT +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 +[1716011938.187771] HB: declare mixin instance +subtype_SubInhab__to__subtype_is_inhab +[1716011938.208087] HB: declare mixin instance +subtype_SubInhab__to__subtype_is_SUB +[1716011938.224672] HB: skipping already existing subtype_Inhab instance on +eta sT +[1716011938.225702] HB: skipping already existing subtype_Nontrivial +instance on eta sT +[1716011938.226603] HB: skipping already existing subtype_SUB instance on +eta sT +[1716011938.229621] HB: we can build a subtype_SubInhab on eta sT +[1716011938.229879] HB: declare canonical structure instance +structures_eta__canonical__subtype_SubInhab +[1716011938.230743] 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 + |} +|} +[1716011938.239616] HB: structure instance +structures_eta__canonical__subtype_SubInhab declared +[1716011938.239725] HB: closing instance section +[1716011938.241560] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1716011938.245255] HB: export +«HB.tests.subtype.SubInhab.EtaAndMixinExports» +[1716011938.246168] HB: exporting operations +[1716011938.246431] HB: operations meta-data module: ElpiOperations +[1716011938.247559] HB: abbreviation factory-by-classname +[1716011938.262766] HB: start module and section hasA +[1716011938.263061] 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 -[1681601409.716963] HB: processing key parameter -[1681601409.717411] HB: converting factories +[1716011938.263220] HB: processing key parameter +[1716011938.263825] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1681601409.717482] HB: declaring context +[1716011938.263924] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1681601409.717607] HB: declaring parameters and key as section variables +[1716011938.264075] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1681601409.723807] HB: declare mixin or factory -[1681601409.723892] HB: declare record axioms_ +[1716011938.270224] HB: declare mixin or factory +[1716011938.270318] HB: declare record axioms_ +[1716011938.280436] HB: declare notation Build +COQC tests/hnf.v +[1716011938.287873] HB: declare notation axioms +COQC tests/fun_instance.v +[1716011938.302915] HB: start module Exports +[1716011938.314066] HB: end modules and sections; export +«HB.tests.hb_pack.hasA.Exports» +hasA.type not a defined object. +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 tests/issue284.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 +aType + : Type +hasB.type not a defined object. +hasB.type not a defined object. +COQC tests/issue287.v HB.check: forall w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w : Prop -[1681601409.735767] HB: declare notation Build -[1681601409.744144] HB: declare notation axioms -COQC tests/non_forgetful_inheritance.v -[1681601409.761932] HB: start module Exports -[1681601409.777334] HB: end modules and sections; export -«HB.tests.hb_pack.hasA.Exports» -hasA.type not a defined object. -aType - : Type +Query assignments: + Ind = «hasA.axioms_» +COQC examples/demo1/test_0_0.v +COQC examples/demo1/test_1_0.v File "./tests/interleave_context.v", line 16, characters 0-52: Warning: pulling in dependencies: [interleave_context_HasA, interleave_context_HasB] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] -hasB.type not a defined object. Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1397,20 +1450,34 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC tests/fix_loop.v -hasB.type not a defined object. -Query assignments: - Ind = «hasA.axioms_» -COQC tests/test_synthesis_params.v -hasAB.type not a defined object. -hasA'.type not a defined object. +COQC examples/demo1/test_2_0.v +COQC examples/demo1/test_3_0.v +COQC examples/demo1/test_3_3.v Query assignments: Ind = «A.axioms_» -COQC tests/hnf.v -COQC tests/fun_instance.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 +COQC examples/demo1/test_4_0.v +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_4_3.v +COQC examples/demo1/test_5_0.v +hasAB.type not a defined object. hasAB.type not a defined object. hasA'.type not a defined object. -COQC tests/issue284.v +hasA'.type not a defined object. +COQC examples/demo1/test_5_3.v +COQC examples/demo2/stage10.v +COQC examples/demo2/stage11.v +COQC examples/demo3/test_0_0.v Query assignments: Ind = «A.type» forall T : AB.type, @@ -1440,71 +1507,47 @@ : T * T AB3 : AB.type : AB.type -COQC tests/issue287.v +COQC examples/demo3/test_1_0.v +COQC examples/demo3/test_2_0.v +COQC tests/exports2.v erefl ?t : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] -COQC examples/demo1/test_0_0.v X : Foo.type A P : Foo.type A P -COQC examples/demo1/test_1_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_2_0.v -COQC examples/demo1/test_3_0.v T : Fun.type nat : Fun.type nat -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_1_0.v -COQC examples/demo3/test_2_0.v -COQC tests/exports2.v -[1681601415.065080] HB: exporting under the module path [] -[1681601415.065250] HB: exporting modules [] -[1681601415.065330] HB: exporting CS instances [] -[1681601415.065406] HB: exporting Abbreviations [] +[1716011940.341546] HB: exporting under the module path [] +[1716011940.341723] HB: exporting modules [] +[1716011940.341837] HB: exporting CS instances [] +[1716011940.341954] HB: exporting Abbreviations [] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 HB: skipping section opening -[1681601423.057100] HB: declare mixin instance +[1716011945.384788] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1681601423.060279] HB: declare canonical mixin instance +[1716011945.387182] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1681601423.061680] HB: declare mixin instance +[1716011945.388323] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1681601423.084290] HB: declare canonical mixin instance +[1716011945.404389] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1681601423.085742] HB: declare mixin instance +[1716011945.405476] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1681601423.093285] HB: declare canonical mixin instance +[1716011945.410324] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1681601423.094468] HB: declare mixin instance +[1716011945.411171] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1681601423.098733] HB: declare canonical mixin instance +[1716011945.413977] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1681601423.100876] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1716011945.415371] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1681601423.101069] HB: declare canonical structure instance +[1716011945.415580] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1681601423.101262] HB: Giving name HB_unnamed_mixin_92 to mixin instance +[1716011945.415815] 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 -[1681601423.103742] HB: structure instance for +[1716011945.417581] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1514,12 +1557,12 @@ HB_unnamed_mixin_92 |} |} -[1681601423.107156] HB: structure instance +[1716011945.420182] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1681601423.108368] HB: we can build a Stage11_UniformSpace on Qc -[1681601423.108547] HB: declare canonical structure instance +[1716011945.420969] HB: we can build a Stage11_UniformSpace on Qc +[1716011945.421169] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1681601423.109130] HB: structure instance for +[1716011945.421637] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1529,15 +1572,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} -[1681601423.112931] HB: structure instance +[1716011945.424195] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1681601423.114311] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1681601423.114496] HB: declare canonical structure instance +[1716011945.425074] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1716011945.425276] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1681601423.115138] HB: Giving name HB_unnamed_mixin_93 to mixin instance +[1716011945.425789] 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 -[1681601423.117836] HB: structure instance for +[1716011945.427734] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1549,12 +1592,12 @@ HB_unnamed_mixin_93 |} |} -[1681601423.121576] HB: structure instance +[1716011945.430356] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1681601423.123411] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1681601423.123647] HB: declare canonical structure instance +[1716011945.431566] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1716011945.431769] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1681601423.124654] HB: structure instance for +[1716011945.432516] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1569,18 +1612,18 @@ HB_unnamed_mixin_92 |} |} -[1681601423.128930] HB: structure instance +[1716011945.435143] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1681601423.132633] HB: we can build a Stage11_TAddAG on Qc -[1681601423.132880] HB: declare canonical structure instance +[1716011945.437112] HB: we can build a Stage11_TAddAG on Qc +[1716011945.437314] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1681601423.133875] HB: Giving name HB_unnamed_mixin_94 to mixin instance +[1716011945.437977] 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 -[1681601423.137786] HB: Giving name HB_unnamed_mixin_95 to mixin instance +[1716011945.440268] 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 -[1681601423.141451] HB: structure instance for +[1716011945.442424] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1594,13 +1637,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_95 |} |} -[1681601423.146120] HB: structure instance +[1716011945.445302] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 22.868 secs (22.525u,0.327s) (successful) +Finished transaction in 11.705 secs (11.352u,0.352s) (successful) Finished transaction in 0. secs (0.u,0.s) (successful) -Finished transaction in 13.505 secs (13.357u,0.147s) (successful) +Finished transaction in 9.735 secs (9.511u,0.223s) (successful) Module Type new_conceptLocked = Sig @@ -1655,7 +1698,7 @@ create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install - make -j8 install DESTDIR=/build/coq-hierarchy-builder-1.4.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" + make -j15 install DESTDIR=/build/coq-hierarchy-builder-1.4.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-hierarchy-builder-1.4.0' make -f Makefile.coq install make[2]: Entering directory '/build/coq-hierarchy-builder-1.4.0' @@ -1691,14 +1734,14 @@ dh_ocaml W: coq-hierarchy-builder doesn't resolve dependency on unit Hb dh_gencontrol +dpkg-gencontrol: warning: Depends field of package coq-hierarchy-builder: substitution variable ${shlibs:Depends} used, but is not defined 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 dh_builddeb -dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.4.0-2_i386.deb'. dpkg-deb: building package 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.4.0-2_i386.deb'. +dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.4.0-2_i386.deb'. dpkg-genbuildinfo --build=binary -O../coq-hierarchy-builder_1.4.0-2_i386.buildinfo dpkg-genchanges --build=binary -O../coq-hierarchy-builder_1.4.0-2_i386.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -1706,12 +1749,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: not including original source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/100152/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/19587 and its subdirectories -I: Current time: Sat Apr 15 11:30:59 -12 2023 -I: pbuilder-time-stamp: 1681601459 +I: removing directory /srv/workspace/pbuilder/100152 and its subdirectories +I: Current time: Sat May 18 19:59:31 +14 2024 +I: pbuilder-time-stamp: 1716011971