Diff of the two buildlogs: -- --- b1/build.log 2023-04-29 03:07:05.855577455 +0000 +++ b2/build.log 2023-04-29 03:09:07.922181899 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Fri Apr 28 14:57:23 -12 2023 -I: pbuilder-time-stamp: 1682737043 +I: Current time: Fri May 31 23:30:09 +14 2024 +I: pbuilder-time-stamp: 1717147809 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -16,7 +16,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 @@ -26,135 +26,167 @@ 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/1697223/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/2803668/tmp/hooks/D01_modify_environment starting +debug: Running on ionos5-amd64. +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 31 23:30 /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/2803668/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/2803668/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='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=15' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='amd64' + 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]="x86_64-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=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=16' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='ff0d9e7e6b044ca9b48a5ce059b370df' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - 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='1697223' - PS1='# ' - PS2='> ' + INVOCATION_ID=148df9b255694dcba49b306fedef1b8a + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-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=2803668 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.3AjtH8k6/pbuilderrc_m9XI --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.3AjtH8k6/b1 --logfile b1/build.log coq-hierarchy-builder_1.4.0-2.dsc' - SUDO_GID='110' - SUDO_UID='105' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - 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.3AjtH8k6/pbuilderrc_4k2o --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.3AjtH8k6/b2 --logfile b2/build.log --extrapackages usrmerge coq-hierarchy-builder_1.4.0-2.dsc' + SUDO_GID=110 + SUDO_UID=105 + 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 ionos1-amd64 5.10.0-21-amd64 #1 SMP Debian 5.10.162-1 (2023-01-21) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-0.deb11.6-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.15-1~bpo11+1 (2023-03-16) x86_64 GNU/Linux I: ls -l /bin total 5632 - -rwxr-xr-x 1 root root 1265648 Apr 23 09:23 bash - -rwxr-xr-x 3 root root 39224 Sep 18 2022 bunzip2 - -rwxr-xr-x 3 root root 39224 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 39224 Sep 18 2022 bzip2 - -rwxr-xr-x 1 root root 14568 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 44016 Sep 20 2022 cat - -rwxr-xr-x 1 root root 68656 Sep 20 2022 chgrp - -rwxr-xr-x 1 root root 64496 Sep 20 2022 chmod - -rwxr-xr-x 1 root root 72752 Sep 20 2022 chown - -rwxr-xr-x 1 root root 151152 Sep 20 2022 cp - -rwxr-xr-x 1 root root 125640 Jan 5 01:20 dash - -rwxr-xr-x 1 root root 121904 Sep 20 2022 date - -rwxr-xr-x 1 root root 89240 Sep 20 2022 dd - -rwxr-xr-x 1 root root 102200 Sep 20 2022 df - -rwxr-xr-x 1 root root 151344 Sep 20 2022 dir - -rwxr-xr-x 1 root root 88656 Mar 22 22:02 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 43856 Sep 20 2022 echo - -rwxr-xr-x 1 root root 41 Jan 24 02:43 egrep - -rwxr-xr-x 1 root root 35664 Sep 20 2022 false - -rwxr-xr-x 1 root root 41 Jan 24 02:43 fgrep - -rwxr-xr-x 1 root root 85600 Mar 22 22:02 findmnt - -rwsr-xr-x 1 root root 35128 Mar 22 20:35 fusermount - -rwxr-xr-x 1 root root 203152 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 98136 Apr 9 2022 gzip - -rwxr-xr-x 1 root root 22680 Dec 19 01:33 hostname - -rwxr-xr-x 1 root root 72824 Sep 20 2022 ln - -rwxr-xr-x 1 root root 53024 Mar 23 00:40 login - -rwxr-xr-x 1 root root 151344 Sep 20 2022 ls - -rwxr-xr-x 1 root root 207168 Mar 22 22:02 lsblk - -rwxr-xr-x 1 root root 97552 Sep 20 2022 mkdir - -rwxr-xr-x 1 root root 72912 Sep 20 2022 mknod - -rwxr-xr-x 1 root root 43952 Sep 20 2022 mktemp - -rwxr-xr-x 1 root root 59712 Mar 22 22:02 more - -rwsr-xr-x 1 root root 59704 Mar 22 22:02 mount - -rwxr-xr-x 1 root root 18744 Mar 22 22:02 mountpoint - -rwxr-xr-x 1 root root 142968 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 43952 Sep 20 2022 pwd - lrwxrwxrwx 1 root root 4 Apr 23 09:23 rbash -> bash - -rwxr-xr-x 1 root root 52112 Sep 20 2022 readlink - -rwxr-xr-x 1 root root 72752 Sep 20 2022 rm - -rwxr-xr-x 1 root root 56240 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 27560 Nov 2 04:31 run-parts - -rwxr-xr-x 1 root root 126424 Jan 5 07:55 sed - lrwxrwxrwx 1 root root 4 Jan 5 01:20 sh -> dash - -rwxr-xr-x 1 root root 43888 Sep 20 2022 sleep - -rwxr-xr-x 1 root root 85008 Sep 20 2022 stty - -rwsr-xr-x 1 root root 72000 Mar 22 22:02 su - -rwxr-xr-x 1 root root 39824 Sep 20 2022 sync - -rwxr-xr-x 1 root root 531984 Apr 6 02:25 tar - -rwxr-xr-x 1 root root 14520 Nov 2 04:31 tempfile - -rwxr-xr-x 1 root root 109616 Sep 20 2022 touch - -rwxr-xr-x 1 root root 35664 Sep 20 2022 true - -rwxr-xr-x 1 root root 14568 Mar 22 20:35 ulockmgr_server - -rwsr-xr-x 1 root root 35128 Mar 22 22:02 umount - -rwxr-xr-x 1 root root 43888 Sep 20 2022 uname - -rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress - -rwxr-xr-x 1 root root 151344 Sep 20 2022 vdir - -rwxr-xr-x 1 root root 72024 Mar 22 22:02 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/1697223/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1265648 Apr 24 2023 bash + -rwxr-xr-x 3 root root 39224 Sep 19 2022 bunzip2 + -rwxr-xr-x 3 root root 39224 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 39224 Sep 19 2022 bzip2 + -rwxr-xr-x 1 root root 14568 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 44016 Sep 21 2022 cat + -rwxr-xr-x 1 root root 68656 Sep 21 2022 chgrp + -rwxr-xr-x 1 root root 64496 Sep 21 2022 chmod + -rwxr-xr-x 1 root root 72752 Sep 21 2022 chown + -rwxr-xr-x 1 root root 151152 Sep 21 2022 cp + -rwxr-xr-x 1 root root 125640 Jan 6 2023 dash + -rwxr-xr-x 1 root root 121904 Sep 21 2022 date + -rwxr-xr-x 1 root root 89240 Sep 21 2022 dd + -rwxr-xr-x 1 root root 102200 Sep 21 2022 df + -rwxr-xr-x 1 root root 151344 Sep 21 2022 dir + -rwxr-xr-x 1 root root 88656 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 43856 Sep 21 2022 echo + -rwxr-xr-x 1 root root 41 Jan 25 2023 egrep + -rwxr-xr-x 1 root root 35664 Sep 21 2022 false + -rwxr-xr-x 1 root root 41 Jan 25 2023 fgrep + -rwxr-xr-x 1 root root 85600 Mar 24 2023 findmnt + -rwsr-xr-x 1 root root 35128 Mar 23 2023 fusermount + -rwxr-xr-x 1 root root 203152 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 98136 Apr 10 2022 gzip + -rwxr-xr-x 1 root root 22680 Dec 20 2022 hostname + -rwxr-xr-x 1 root root 72824 Sep 21 2022 ln + -rwxr-xr-x 1 root root 53024 Mar 24 2023 login + -rwxr-xr-x 1 root root 151344 Sep 21 2022 ls + -rwxr-xr-x 1 root root 207168 Mar 24 2023 lsblk + -rwxr-xr-x 1 root root 97552 Sep 21 2022 mkdir + -rwxr-xr-x 1 root root 72912 Sep 21 2022 mknod + -rwxr-xr-x 1 root root 43952 Sep 21 2022 mktemp + -rwxr-xr-x 1 root root 59712 Mar 24 2023 more + -rwsr-xr-x 1 root root 59704 Mar 24 2023 mount + -rwxr-xr-x 1 root root 18744 Mar 24 2023 mountpoint + -rwxr-xr-x 1 root root 142968 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 43952 Sep 21 2022 pwd + lrwxrwxrwx 1 root root 4 Apr 24 2023 rbash -> bash + -rwxr-xr-x 1 root root 52112 Sep 21 2022 readlink + -rwxr-xr-x 1 root root 72752 Sep 21 2022 rm + -rwxr-xr-x 1 root root 56240 Sep 21 2022 rmdir + -rwxr-xr-x 1 root root 27560 Nov 3 2022 run-parts + -rwxr-xr-x 1 root root 126424 Jan 6 2023 sed + lrwxrwxrwx 1 root root 9 May 31 23:30 sh -> /bin/bash + -rwxr-xr-x 1 root root 43888 Sep 21 2022 sleep + -rwxr-xr-x 1 root root 85008 Sep 21 2022 stty + -rwsr-xr-x 1 root root 72000 Mar 24 2023 su + -rwxr-xr-x 1 root root 39824 Sep 21 2022 sync + -rwxr-xr-x 1 root root 531984 Apr 7 2023 tar + -rwxr-xr-x 1 root root 14520 Nov 3 2022 tempfile + -rwxr-xr-x 1 root root 109616 Sep 21 2022 touch + -rwxr-xr-x 1 root root 35664 Sep 21 2022 true + -rwxr-xr-x 1 root root 14568 Mar 23 2023 ulockmgr_server + -rwsr-xr-x 1 root root 35128 Mar 24 2023 umount + -rwxr-xr-x 1 root root 43888 Sep 21 2022 uname + -rwxr-xr-x 2 root root 2346 Apr 10 2022 uncompress + -rwxr-xr-x 1 root root 151344 Sep 21 2022 vdir + -rwxr-xr-x 1 root root 72024 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/2803668/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -279,7 +311,7 @@ Get: 75 http://deb.debian.org/debian bookworm/main amd64 libelpi-ocaml-dev amd64 1.16.8-1+b2 [10.4 MB] Get: 76 http://deb.debian.org/debian bookworm/main amd64 libcoq-elpi amd64 1.16.0-2+b1 [2429 kB] Get: 77 http://deb.debian.org/debian bookworm/main amd64 wdiff amd64 1.2.2-5 [119 kB] -Fetched 355 MB in 10s (34.4 MB/s) +Fetched 355 MB in 4s (96.7 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:amd64. (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 ... 19596 files and directories currently installed.) @@ -603,8 +635,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/2803668/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/2803668/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 @@ -614,7 +657,7 @@ debian/rules clean dh clean --with coq,ocaml dh_auto_clean - make -j15 distclean + make -j16 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 @@ -629,7 +672,7 @@ dh_ocamlinit dh_auto_configure dh_auto_build - make -j15 "INSTALL=install --strip-program=true" + make -j16 "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' @@ -647,8 +690,8 @@ make test-suite make[2]: Entering directory '/build/coq-hierarchy-builder-1.4.0' make -f Makefile.coq -make[3]: Entering directory '/build/coq-hierarchy-builder-1.4.0' /usr/bin/coq_makefile -f _CoqProject.test-suite -o Makefile.test-suite.coq +make[3]: Entering directory '/build/coq-hierarchy-builder-1.4.0' Warning: . and tests overlap (used in -R or -Q) Warning: . and examples overlap (used in -R or -Q) @@ -673,8 +716,9 @@ COQC examples/demo4/hierarchy_0.v COQC examples/demo5/hierarchy_0.v COQC examples/FSCD2020_material/V1.v -[1682737334.123373] HB: start module and section AddComoid_of_Type -[1682737334.123820] HB: converting arguments +COQC examples/FSCD2020_material/V2.v +[1717147867.022236] HB: start module and section AddComoid_of_Type +[1717147867.022655] HB: converting arguments indt-decl (parameter A explicit X0 c0 \ record AddComoid_of_Type (sort (typ X1)) Build_AddComoid_of_Type @@ -700,31 +744,19 @@ app [global (indt «eq»), X10 c0 c1 c2 c3 c4 c5, app [c2, c1, c5], c5]) c5 \ end-record)) to factories -[1682737334.125008] HB: processing key parameter -[1682737334.125884] HB: converting factories +[1717147867.023239] HB: processing key parameter +[1717147867.023858] HB: converting factories w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] to mixins -[1682737334.126057] HB: declaring context +[1717147867.023933] HB: declaring context w-params.nil A (sort (typ «HB.examples.readme.2»)) c0 \ [] -[1682737335.045606] HB: declaring parameters and key as section variables -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] +[1717147867.024073] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1682737343.721522] HB: declare mixin or factory -[1682737343.721677] HB: declare record axioms_ -[1682737343.968095] HB: declare notation Build -[1682737344.742296] HB: declare notation axioms -[1682737344.786584] HB: start module Exports -[1682737345.746566] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_AddAG_of_AddComoid -[1682737345.746772] HB: declare builder from hierarchy_2_Ring_of_AddComoid -to hierarchy_2_Ring_of_AddAG -COQC examples/FSCD2020_material/V2.v -[1682737364.311154] HB: end modules and sections; export +[1717147867.041035] HB: declare mixin or factory +[1717147867.041140] HB: declare record axioms_ +[1717147867.080864] HB: declare notation Build +[1717147867.102580] HB: declare notation axioms +[1717147867.141047] HB: start module Exports +[1717147867.177957] HB: end modules and sections; export «HB.examples.readme.AddComoid_of_Type.Exports» (* @@ -781,72 +813,65 @@ Notation AddComoid_of_Type X1 := ( AddComoid_of_Type.phant_axioms X1). *) -[1682737366.748203] HB: start module AddComoid -[1682737366.748680] HB: declare axioms record +[1717147867.311067] HB: start module AddComoid +[1717147867.311520] HB: declare axioms record w-params.nil A (sort (typ «HB.examples.readme.25»)) c0 \ [triple (indt «AddComoid_of_Type.axioms_») [] c0] -[1682737366.749136] HB: typing class field +[1717147867.311768] HB: typing class field indt «AddComoid_of_Type.axioms_» -COQC examples/FSCD2020_material/V3.v -COQC examples/FSCD2020_material/V4.v -inhab - : ?s -where -?T : [ |- Type] -?s : [ |- s1.type ?T] -[1682737372.924802] HB: declare type record -[1682737373.131429] HB: structure: new mixins +[1717147867.431774] HB: declare type record +[1717147867.447812] HB: structure: new mixins [indt «AddComoid_of_Type.axioms_»] -[1682737373.131609] HB: structure: mixin first class +[1717147867.448019] HB: structure: mixin first class [mixin-first-class (indt «AddComoid_of_Type.axioms_») (indt «axioms_»)] -[1682737373.131697] HB: declaring clone abbreviation -[1682737373.245429] HB: declaring pack_ constant -[1682737373.277162] HB: declaring pack_ constant = +[1717147867.448101] HB: declaring clone abbreviation +[1717147867.464931] HB: declaring pack_ constant +[1717147867.467051] 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]] -[1682737373.280816] HB: start module Exports -[1682737373.281145] HB: making coercion from type to target -[1682737373.281204] HB: declare sort coercion -[1682737373.482052] HB: exporting unification hints -[1682737373.482370] HB: exporting coercions from class to mixins -[1682737373.482765] HB: export class to mixin coercion for mixin +[1717147867.471582] HB: start module Exports +[1717147867.471944] HB: making coercion from type to target +[1717147867.472002] HB: declare sort coercion +[1717147867.472458] HB: exporting unification hints +[1717147867.472759] HB: exporting coercions from class to mixins +[1717147867.473176] HB: export class to mixin coercion for mixin readme_AddComoid_of_Type -[1682737373.483285] HB: accumulating various props -[1682737373.533780] HB: stop module Exports -[1682737373.534698] HB: declaring on_ abbreviation -[1682737373.550190] HB: declaring `copy` abbreviation -[1682737373.551780] HB: declaring on abbreviation -[1682737373.553379] HB: eta expanded instances -[1682737373.555724] HB: postulating A -[1682737374.761366] HB: declare mixin instance +[1717147867.473691] HB: accumulating various props +[1717147867.493327] HB: stop module Exports +[1717147867.496382] HB: declaring on_ abbreviation +[1717147867.511522] HB: declaring `copy` abbreviation +[1717147867.512494] HB: declaring on abbreviation +[1717147867.513776] HB: eta expanded instances +[1717147867.516611] HB: postulating A +[1717147867.545483] HB: declare mixin instance readme_AddComoid__to__readme_AddComoid_of_Type -[1682737374.776778] HB: we can build a readme_AddComoid on eta A -[1682737374.777308] HB: declare canonical structure instance +[1717147867.555437] HB: we can build a readme_AddComoid on eta A +[1717147867.555873] HB: declare canonical structure instance structures_eta__canonical__readme_AddComoid -[1682737374.777766] HB: Giving name HB_unnamed_mixin_4 to mixin instance +[1717147867.556570] HB: Giving name HB_unnamed_mixin_4 to mixin instance readme_AddComoid_of_Type_mixin (eta A) HB_unnamed_factory_2 -[1682737374.781286] HB: structure instance for +[1717147867.562263] HB: structure instance for structures_eta__canonical__readme_AddComoid is {| sort := eta A; class := {| readme_AddComoid_of_Type_mixin := HB_unnamed_mixin_4 |} |} -[1682737374.788134] HB: structure instance +[1717147867.569512] HB: structure instance structures_eta__canonical__readme_AddComoid declared -[1682737374.788277] HB: closing instance section -[1682737374.790718] HB: end modules; export +[1717147867.569789] HB: closing instance section +[1717147867.572266] HB: end modules; export «HB.examples.readme.AddComoid.Exports» -[1682737374.792338] HB: export +[1717147867.575263] HB: export «HB.examples.readme.AddComoid.EtaAndMixinExports» -[1682737374.793771] HB: exporting operations -[1682737374.795364] HB: export operation zero -[1682737374.799984] HB: export operation add -[1682737374.805334] HB: export operation addrA -[1682737374.811631] HB: export operation addrC -[1682737374.817456] HB: export operation add0r -[1682737374.821921] HB: operations meta-data module: ElpiOperations -[1682737374.833243] HB: abbreviation factory-by-classname +[1717147867.577641] HB: exporting operations +[1717147867.579586] HB: export operation zero +[1717147867.583970] HB: export operation add +[1717147867.591050] HB: export operation addrA +[1717147867.597684] HB: export operation addrC +[1717147867.603040] HB: export operation add0r +[1717147867.608211] HB: operations meta-data module: ElpiOperations +[1717147867.620075] HB: abbreviation factory-by-classname (* Module AddComoid. @@ -961,30 +986,36 @@ *) forall (M : AddComoid.type) (x : M), x + x = 0 : Prop -[1682737374.850162] HB: begin module for builders -[1682737374.851009] HB: postulating factories -[1682737374.851233] HB: processing key context-item -[1682737374.851631] HB: processing mixin parameter a -[1682737374.852075] HB: declaring parameters and key as section variables -Here is the list of mixins to declare (the order matters): [] -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_talk/V1.v +COQC examples/FSCD2020_material/V3.v +COQC examples/FSCD2020_material/V4.v +inhab + : ?s +where +?T : [ |- Type] +?s : [ |- s1.type ?T] eq_refl : inhab = 7 : inhab = 7 +AbelianGrp.phant_on_ BinNums_Z__canonical__readme_AbelianGrp + (Phant BinNums_Z__canonical__readme_AbelianGrp) + : AbelianGrp.axioms_ Z + : AbelianGrp.axioms_ Z 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) +HB: Z is canonically equipped with structures: + - AbelianGrp + (from "./examples/readme.v", line 32) + - AddComoid + (from "./examples/readme.v", line 31) +COQC examples/FSCD2020_talk/V1.v +[1717147869.074326] HB: begin module for builders +[1717147869.074737] HB: postulating factories +[1717147869.074846] HB: processing key context-item +[1717147869.075231] HB: processing mixin parameter a +[1717147869.075604] HB: declaring parameters and key as section variables +Here is the list of mixins to declare (the order matters): [] COQC examples/FSCD2020_talk/V2.v fun X : s2.type nat => inhab : X : forall X : s2.type nat, X @@ -992,16 +1023,6 @@ : forall X : s2.type nat, nat -> X s2_to_s1 not a defined object. COQC examples/FSCD2020_talk/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,6 +1031,7 @@ @addNr : forall s : Ring.type, left_inverse 0 opp 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 @@ -1019,11 +1041,50 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC examples/Coq2020_material/CoqWS_abstract.v COQC examples/Coq2020_material/CoqWS_expansion/withHB.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_expansion/withoutHB.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] +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 +HB: A is canonically equipped with structures: + - Equality + Singleton + (from "./examples/hulk.v", line 216) + 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] +COQC tests/instance_params_no_type.v +[1717147872.060008] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_AddAG_of_AddComoid +[1717147872.060342] HB: declare builder from hierarchy_2_Ring_of_AddComoid +to hierarchy_2_Ring_of_AddAG +add + : ?s -> ?s -> ?s +where +?s : [ |- CMonoid.type] +addrC + : commutative add +where +?s : [ |- CMonoid.type] Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1033,64 +1094,39 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -COQC tests/instance_params_no_type.v -COQC tests/test_CS_db_filtering.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/subtype.v -add - : ?s -> ?s -> ?s -where -?s : [ |- CMonoid.type] addrC : commutative add where ?s : [ |- CMonoid.type] -File "./examples/FSCD2020_talk/V2.v", line 17, characters 0-66: +COQC tests/test_CS_db_filtering.v +File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: Warning: -pulling in dependencies: [V2_is_semigroup] +pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] -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/infer.v -File "./examples/Coq2020_material/CoqWS_demo.v", line 73, characters 0-73: +COQC tests/subtype.v +File "./examples/Coq2020_material/CoqWS_abstract.v", line 23, characters 0-71: Warning: -pulling in dependencies: [CoqWS_demo_CMonoid_of_Type] +pulling in dependencies: [CoqWS_abstract_CMonoid_of_Type] Please list them or end the declaration with '&' [HB.implicit-structure-dependency,HB] -COQC tests/exports.v -addrC - : commutative add -where -?s : [ |- CMonoid.type] -COQC tests/log_impargs_record.v forall x y : ?t, x - (y + 0) = x : Prop where ?t : [x : ?t y : ?t |- AbelianGrp.type] (x, y cannot be used) +COQC tests/infer.v +COQC tests/exports.v +COQC tests/log_impargs_record.v COQC tests/compress_coe.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/funclass.v +COQC tests/grefclass.v +COQC tests/local_instance.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/grefclass.v -COQC tests/local_instance.v (* Module A. @@ -1149,6 +1185,7 @@ ?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/lock.v A.p : forall [T : Type] (record : A.axioms_ T) [x : T], A.f record x = x -> True @@ -1156,75 +1193,30 @@ Arguments A.p [T]%type_scope record [x] _ A.p is transparent Expands to: Constant HB.tests.log_impargs_record.A.p +COQC tests/interleave_context.v +p : pred nat + : pred nat +COQC tests/not_same_key.v forall x : Z, x * - (1 + x) = 0 + 1 : Prop -COQC tests/lock.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 -add - : A -> A -> A -COQC tests/interleave_context.v -[1682737398.312910] HB: start module SubInhab -[1682737398.313191] 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] -[1682737398.313564] HB: typing class field indt «is_inhab.axioms_» -[1682737398.313953] HB: typing class field indt «is_SUB.axioms_» -[1682737398.380300] HB: declare type record -[1682737398.431858] HB: structure: new mixins [] -[1682737398.432072] HB: structure: mixin first class [] -[1682737398.432124] HB: declaring clone abbreviation -[1682737398.484283] HB: declaring pack_ constant -[1682737398.500264] 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]] -[1682737398.516207] HB: start module Exports -[1682737398.516597] HB: making coercion from type to target -[1682737398.516716] HB: declare sort coercion -[1682737398.517160] HB: exporting unification hints -[1682737398.529711] HB: declare coercion subtype_SubInhab__to__subtype_SUB -[1682737398.535577] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_SUB_class -[1682737398.579395] HB: declare unification hint -subtype_SubInhab__to__subtype_SUB +default : nat + : nat forall x : Z, x * - (1 + x) = 0 + 1 : Prop -[1682737398.619783] HB: declare coercion path compression rules -[1682737398.630923] HB: declare coercion subtype_SubInhab__to__subtype_Inhab -[1682737398.632470] HB: declare coercion hint -subtype_SubInhab_class__to__subtype_Inhab_class -[1682737398.686831] HB: declare unification hint -subtype_SubInhab__to__subtype_Inhab -[1682737398.727624] HB: declare coercion path compression rules -[1682737398.817903] HB: declare unification hint -join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB -COQC tests/not_same_key.v -[1682737398.875941] HB: exporting coercions from class to mixins -[1682737398.876718] HB: export class to mixin coercion for mixin -subtype_is_inhab -[1682737398.895738] HB: export class to mixin coercion for mixin -subtype_is_SUB -[1682737398.897356] HB: accumulating various props -[1682737398.999526] HB: stop module Exports -[1682737399.016097] HB: declaring on_ abbreviation +The command did fail as expected with message: +The term "default" has type "nonempty.sort ?t" +while it is expected to have type "nat". +add + : A -> A -> A +COQC tests/hb_pack.v HB.check: bar.type_ bool Datatypes_nat__canonical__infer_foo bool : Type -[1682737399.067734] HB: declaring `copy` abbreviation -[1682737399.069024] HB: declaring on abbreviation -[1682737399.072209] HB: eta expanded instances -[1682737399.085778] HB: postulating T +COQC tests/declare.v 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 = @@ -1240,46 +1232,24 @@ bar.phant_type bool Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) bool : Type -[1682737399.125057] HB: postulating P -[1682737399.136762] HB: postulating sT -[1682737399.243234] HB: declare mixin instance -subtype_SubInhab__to__subtype_is_inhab -[1682737399.316486] HB: declare mixin instance -subtype_SubInhab__to__subtype_is_SUB -p : pred nat - : pred nat -[1682737399.385192] HB: skipping already existing subtype_Inhab instance on -eta sT -[1682737399.399193] HB: skipping already existing subtype_Nontrivial -instance on eta sT -[1682737399.400606] HB: skipping already existing subtype_SUB instance on -eta sT -[1682737399.416887] HB: we can build a subtype_SubInhab on eta sT -[1682737399.417391] HB: declare canonical structure instance -structures_eta__canonical__subtype_SubInhab -[1682737399.423152] 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 - |} -|} -[1682737399.457764] HB: structure instance -structures_eta__canonical__subtype_SubInhab declared -[1682737399.457949] HB: closing instance section -[1682737399.468575] HB: end modules; export -«HB.tests.subtype.SubInhab.Exports» -default : nat - : nat -[1682737399.494428] HB: export -«HB.tests.subtype.SubInhab.EtaAndMixinExports» -[1682737399.496675] HB: exporting operations -[1682737399.497089] HB: operations meta-data module: ElpiOperations -[1682737399.507399] HB: abbreviation factory-by-classname -COQC tests/hb_pack.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 +Notation big := big.body +Expands to: Notation HB.tests.lock.X.big +COQC tests/short.v +COQC tests/primitive_records.v Record type : Type := Pack { sort : Type; class : Monoid.axioms_ sort }. Arguments Monoid.Pack sort%type_scope class @@ -1289,72 +1259,145 @@ : forall s : AbelianGroup.type, left_inverse 0 opp add @addrC : forall s : AbelianGroup.type, commutative add -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 +[1717147875.893157] HB: start module SubInhab +[1717147875.893651] 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] +[1717147875.894557] HB: typing class field indt «is_inhab.axioms_» +[1717147875.895043] HB: typing class field indt «is_SUB.axioms_» +[1717147875.911415] HB: declare type record +[1717147875.925282] HB: structure: new mixins [] +[1717147875.925457] HB: structure: mixin first class [] +[1717147875.925515] HB: declaring clone abbreviation +[1717147875.939416] HB: declaring pack_ constant +[1717147875.943394] 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]] +[1717147875.947087] HB: start module Exports +[1717147875.947422] HB: making coercion from type to target +[1717147875.947513] HB: declare sort coercion +[1717147875.947906] HB: exporting unification hints +[1717147875.952845] HB: declare coercion subtype_SubInhab__to__subtype_SUB +[1717147875.955713] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_SUB_class +[1717147875.979525] HB: declare unification hint +subtype_SubInhab__to__subtype_SUB +[1717147876.013596] HB: declare coercion path compression rules +[1717147876.028415] HB: declare coercion subtype_SubInhab__to__subtype_Inhab +[1717147876.035194] HB: declare coercion hint +subtype_SubInhab_class__to__subtype_Inhab_class +[1717147876.068348] HB: declare unification hint +subtype_SubInhab__to__subtype_Inhab forall x : Z, x * - (1 + x) = 0 + 1 : Prop -COQC tests/declare.v -COQC tests/short.v -COQC tests/primitive_records.v -COQC tests/non_forgetful_inheritance.v -Notation big := big.body -Expands to: Notation HB.tests.lock.X.big +[1717147876.115967] HB: declare coercion path compression rules COQC tests/fix_loop.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 bar1.phant_type Datatypes_nat__canonical__infer_foo (ssreflect.Phant nat) : Type +[1717147876.160751] HB: declare unification hint +join_subtype_SubInhab_between_subtype_Inhab_and_subtype_SUB +[1717147876.181143] HB: exporting coercions from class to mixins +[1717147876.182652] HB: export class to mixin coercion for mixin +subtype_is_inhab +[1717147876.185811] HB: export class to mixin coercion for mixin +subtype_is_SUB +[1717147876.188086] HB: accumulating various props COQC tests/test_synthesis_params.v -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 -[1682737403.074171] HB: start module and section hasA -[1682737403.074757] HB: converting arguments +COQC tests/hnf.v +[1717147876.220948] HB: stop module Exports +[1717147876.227190] HB: declaring on_ abbreviation +[1717147876.227919] HB: start module and section hasA +[1717147876.228421] 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 -[1682737403.075057] HB: processing key parameter -[1682737403.075878] HB: converting factories +[1717147876.228658] HB: processing key parameter +[1717147876.230671] HB: converting factories w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] to mixins -[1682737403.076020] HB: declaring context +[1717147876.230844] HB: declaring context w-params.nil T (sort (typ «HB.tests.hb_pack.8»)) c0 \ [] -[1682737403.076270] HB: declaring parameters and key as section variables +[1717147876.231033] HB: declaring parameters and key as section variables Here is the list of mixins to declare (the order matters): [] -[1682737403.104979] HB: declare mixin or factory -[1682737403.105075] HB: declare record axioms_ -COQC tests/hnf.v -[1682737403.167890] HB: declare notation Build -[1682737403.223617] HB: declare notation axioms -[1682737403.321141] HB: start module Exports -[1682737403.417509] HB: end modules and sections; export +[1717147876.239818] HB: declare mixin or factory +[1717147876.239913] HB: declare record axioms_ +[1717147876.245947] HB: declaring `copy` abbreviation +[1717147876.247731] HB: declaring on abbreviation +[1717147876.251212] HB: eta expanded instances +[1717147876.256975] HB: postulating T +COQC tests/fun_instance.v +[1717147876.257960] HB: declare notation Build +[1717147876.270909] HB: postulating P +[1717147876.271103] HB: declare notation axioms +[1717147876.276428] HB: postulating sT +[1717147876.298612] HB: start module Exports +[1717147876.325458] HB: declare mixin instance +subtype_SubInhab__to__subtype_is_inhab +[1717147876.333931] HB: end modules and sections; export «HB.tests.hb_pack.hasA.Exports» hasA.type not a defined object. +[1717147876.365800] HB: declare mixin instance +subtype_SubInhab__to__subtype_is_SUB +[1717147876.398728] HB: skipping already existing subtype_Inhab instance on +eta sT +[1717147876.400043] HB: skipping already existing subtype_Nontrivial +instance on eta sT +[1717147876.401190] HB: skipping already existing subtype_SUB instance on +eta sT +[1717147876.405517] HB: we can build a subtype_SubInhab on eta sT +[1717147876.405899] HB: declare canonical structure instance +structures_eta__canonical__subtype_SubInhab +[1717147876.407495] 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 + |} +|} +[1717147876.421236] HB: structure instance +structures_eta__canonical__subtype_SubInhab declared +[1717147876.421443] HB: closing instance section +[1717147876.424077] HB: end modules; export +«HB.tests.subtype.SubInhab.Exports» +[1717147876.429041] HB: export +«HB.tests.subtype.SubInhab.EtaAndMixinExports» +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 +[1717147876.430739] HB: exporting operations +[1717147876.431042] HB: operations meta-data module: ElpiOperations +[1717147876.432962] HB: abbreviation factory-by-classname +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 -COQC tests/fun_instance.v -COQC tests/issue284.v -[1682737405.109126] HB: exporting under the module path [] -[1682737405.119932] HB: exporting modules +[1717147876.794435] HB: exporting under the module path [] +[1717147876.795167] 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] -[1682737405.123258] HB: exporting CS instances +[1717147876.799165] HB: exporting CS instances [«Z_ring_axioms», «BinNums_Z__canonical__Enclosing_Ring»] -[1682737405.124127] HB: exporting Abbreviations [addr0, addrNK] +[1717147876.800061] HB: exporting Abbreviations [addr0, addrNK] forall (R : Enclosing.Ring.type) (x : R), x = x : Prop 0%G @@ -1364,25 +1407,26 @@ Enclosing.zero : Z : Z COQC tests/issue287.v -aType - : Type +hasB.type not a defined object. HB.check: forall w : wp.phant_type nat Nat_mul__canonical__funclass_Monoid (Phantom (nat -> nat -> nat) Init.Nat.mul), w = w : Prop -hasB.type not a defined object. +aType + : Type COQC examples/demo1/test_0_0.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] -hasB.type not a defined object. +COQC examples/demo1/test_1_0.v +COQC examples/demo1/test_2_0.v Query assignments: Ind = «hasA.axioms_» -COQC examples/demo1/test_1_0.v Datatypes_prod__canonical__compress_coe_D = fun D D' : D.type => {| @@ -1404,37 +1448,32 @@ : D.type -> D.type -> D.type Arguments Datatypes_prod__canonical__compress_coe_D D D' -COQC examples/demo1/test_2_0.v -Query assignments: - Ind = «A.axioms_» COQC examples/demo1/test_3_0.v COQC examples/demo1/test_3_3.v COQC examples/demo1/test_4_0.v +hasAB.type not a defined object. 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_3.v +hasAB.type not a defined object. 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_5_0.v -hasAB.type not a defined object. -hasAB.type not a defined object. -COQC examples/demo1/test_5_3.v hasA'.type not a defined object. hasA'.type not a defined object. +COQC examples/demo1/test_4_3.v +COQC examples/demo1/test_5_0.v +COQC examples/demo1/test_5_3.v Query assignments: - Ind = «A.type» + Ind = «A.axioms_» COQC examples/demo2/stage10.v COQC examples/demo2/stage11.v -COQC examples/demo3/test_0_0.v -COQC examples/demo3/test_1_0.v forall T : AB.type, unkeyed {| @@ -1454,54 +1493,58 @@ : A.type AB1 : hasB.phant_axioms A -> AB.type : hasB.phant_axioms A -> AB.type -COQC examples/demo3/test_2_0.v Bm : hasB.phant_axioms A : hasB.phant_axioms A AB2 : AB.type : AB.type +COQC examples/demo3/test_0_0.v pB : T * T : T * T AB3 : AB.type : AB.type +COQC examples/demo3/test_1_0.v +COQC examples/demo3/test_2_0.v +Query assignments: + Ind = «A.type» COQC tests/exports2.v +X : Foo.type A P + : Foo.type A P erefl ?t : ?t = ?t : ?t = ?t where ?t : [ |- Sq.type] -X : Foo.type A P - : Foo.type A P -[1682737419.545960] HB: exporting under the module path [] -[1682737419.558298] HB: exporting modules [] -[1682737419.558486] HB: exporting CS instances [] -[1682737419.558687] HB: exporting Abbreviations [] T : Fun.type nat : Fun.type nat +[1717147880.463202] HB: exporting under the module path [] +[1717147880.463374] HB: exporting modules [] +[1717147880.463445] HB: exporting CS instances [] +[1717147880.463510] HB: exporting Abbreviations [] Qcplus_opp_r: forall q : Qc, q + - q = Q2Qc 0 HB: skipping section opening -[1682737454.398353] HB: declare mixin instance +[1717147889.110970] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology -[1682737454.407662] HB: declare canonical mixin instance +[1717147889.114710] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Uniform_wo_Topology» -[1682737454.409894] HB: declare mixin instance +[1717147889.116444] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology -[1682737454.448309] HB: declare canonical mixin instance +[1717147889.123573] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_Uniform_Topology» -[1682737454.459086] HB: declare mixin instance +[1717147889.125526] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform -[1682737454.491181] HB: declare canonical mixin instance +[1717147889.135002] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_Join_TAddAG_Uniform» -[1682737454.493177] HB: declare mixin instance +[1717147889.136460] HB: declare mixin instance Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform -[1682737454.508231] HB: declare canonical mixin instance +[1717147889.141557] HB: declare canonical mixin instance «Stage11_JoinTAddAG__to__Stage11_JoinTAddAG_wo_Uniform» -[1682737454.530158] HB: we can build a Stage11_UniformSpace_wo_Topology on +[1717147889.144446] HB: we can build a Stage11_UniformSpace_wo_Topology on Qc -[1682737454.530703] HB: declare canonical structure instance +[1717147889.144766] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology -[1682737454.531133] HB: Giving name HB_unnamed_mixin_92 to mixin instance +[1717147889.145009] 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 -[1682737454.543688] HB: structure instance for +[1717147889.148246] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology is {| UniformSpace_wo_Topology.sort := Qc; @@ -1511,12 +1554,12 @@ HB_unnamed_mixin_92 |} |} -[1682737454.562333] HB: structure instance +[1717147889.152776] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace_wo_Topology declared -[1682737454.564336] HB: we can build a Stage11_UniformSpace on Qc -[1682737454.564703] HB: declare canonical structure instance +[1717147889.154291] HB: we can build a Stage11_UniformSpace on Qc +[1717147889.154561] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_UniformSpace -[1682737454.565751] HB: structure instance for +[1717147889.155359] HB: structure instance for Qcanon_Qc__canonical__Stage11_UniformSpace is {| UniformSpace.sort := Qc; @@ -1526,15 +1569,15 @@ UniformSpace.Stage11_Uniform_wo_Topology_mixin := HB_unnamed_mixin_92 |} |} -[1682737454.589158] HB: structure instance +[1717147889.160587] HB: structure instance Qcanon_Qc__canonical__Stage11_UniformSpace declared -[1682737454.596333] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc -[1682737454.596728] HB: declare canonical structure instance +[1717147889.162438] HB: we can build a Stage11_TAddAG_wo_Uniform on Qc +[1717147889.162733] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform -[1682737454.597611] HB: Giving name HB_unnamed_mixin_93 to mixin instance +[1717147889.163658] 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 -[1682737454.618732] HB: structure instance for +[1717147889.167308] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform is {| TAddAG_wo_Uniform.sort := Qc; @@ -1546,12 +1589,12 @@ HB_unnamed_mixin_93 |} |} -[1682737454.642199] HB: structure instance +[1717147889.171754] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG_wo_Uniform declared -[1682737454.645420] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc -[1682737454.645793] HB: declare canonical structure instance +[1717147889.173694] HB: we can build a Stage11_Uniform_TAddAG_unjoined on Qc +[1717147889.173906] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined -[1682737454.651654] HB: structure instance for +[1717147889.175072] HB: structure instance for Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined is {| Uniform_TAddAG_unjoined.sort := Qc; @@ -1566,18 +1609,18 @@ HB_unnamed_mixin_92 |} |} -[1682737454.675086] HB: structure instance +[1717147889.180391] HB: structure instance Qcanon_Qc__canonical__Stage11_Uniform_TAddAG_unjoined declared -[1682737454.689032] HB: we can build a Stage11_TAddAG on Qc -[1682737454.689448] HB: declare canonical structure instance +[1717147889.183992] HB: we can build a Stage11_TAddAG on Qc +[1717147889.184245] HB: declare canonical structure instance Qcanon_Qc__canonical__Stage11_TAddAG -[1682737454.703376] HB: Giving name HB_unnamed_mixin_94 to mixin instance +[1717147889.185342] 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 -[1682737454.709725] HB: Giving name HB_unnamed_mixin_95 to mixin instance +[1717147889.189849] 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 -[1682737454.732070] HB: structure instance for +[1717147889.193436] HB: structure instance for Qcanon_Qc__canonical__Stage11_TAddAG is {| TAddAG.sort := Qc; @@ -1591,13 +1634,13 @@ TAddAG.Stage11_Join_TAddAG_Uniform_mixin := HB_unnamed_mixin_95 |} |} -[1682737454.756388] HB: structure instance +[1717147889.198589] HB: structure instance Qcanon_Qc__canonical__Stage11_TAddAG declared entourage : set (set (Qc * Qc)) : set (set (Qc * Qc)) -Finished transaction in 76.782 secs (24.437u,1.239s) (successful) -Finished transaction in 0.001 secs (0.001u,0.s) (successful) -Finished transaction in 66.78 secs (25.339u,1.311s) (successful) +Finished transaction in 19.827 secs (18.785u,0.599s) (successful) +Finished transaction in 0. secs (0.u,0.s) (successful) +Finished transaction in 15.729 secs (15.346u,0.38s) (successful) Module Type new_conceptLocked = Sig @@ -1652,7 +1695,7 @@ create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install - make -j15 install DESTDIR=/build/coq-hierarchy-builder-1.4.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" + make -j16 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' @@ -1688,14 +1731,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 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.4.0-2_amd64.deb'. dpkg-deb: building package 'libcoq-hierarchy-builder' in '../libcoq-hierarchy-builder_1.4.0-2_amd64.deb'. +dpkg-deb: building package 'coq-hierarchy-builder' in '../coq-hierarchy-builder_1.4.0-2_amd64.deb'. dpkg-genbuildinfo --build=binary -O../coq-hierarchy-builder_1.4.0-2_amd64.buildinfo dpkg-genchanges --build=binary -O../coq-hierarchy-builder_1.4.0-2_amd64.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -1703,12 +1746,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/2803668/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/2803668/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/1697223 and its subdirectories -I: Current time: Fri Apr 28 15:07:04 -12 2023 -I: pbuilder-time-stamp: 1682737624 +I: removing directory /srv/workspace/pbuilder/2803668 and its subdirectories +I: Current time: Fri May 31 23:32:09 +14 2024 +I: pbuilder-time-stamp: 1717147929