Diff of the two buildlogs: -- --- b1/build.log 2023-06-05 05:27:15.093480760 +0000 +++ b2/build.log 2023-06-05 05:28:47.473437620 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Jun 4 17:25:37 -12 2023 -I: pbuilder-time-stamp: 1685942737 +I: Current time: Mon Jul 8 01:50:25 +14 2024 +I: pbuilder-time-stamp: 1720353025 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-unicoq_1.6-8.16.orig.tar.gz] I: copying [./coq-unicoq_1.6-8.16-2.debian.tar.xz] I: Extracting source -gpgv: Signature made Tue Jan 24 19:51:39 2023 -12 +gpgv: Signature made Wed Jan 25 21:51:39 2023 +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-unicoq_1.6-8.16-2.debian.tar.xz I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/2443067/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3603484/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 Jul 8 01:50 /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/3603484/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3603484/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='f7afb16b065b44f7a63a53620141d28d' - 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='2443067' - PS1='# ' - PS2='> ' + INVOCATION_ID=ae4db5a5b53843feaff6c4938989e828 + 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=3603484 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.lJibK9Xq/pbuilderrc_hR34 --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.lJibK9Xq/b1 --logfile b1/build.log coq-unicoq_1.6-8.16-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.lJibK9Xq/pbuilderrc_kLOm --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.lJibK9Xq/b2 --logfile b2/build.log --extrapackages usrmerge coq-unicoq_1.6-8.16-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-23-amd64 #1 SMP Debian 5.10.179-1 (2023-05-12) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-0.deb11.7-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.20-2~bpo11+1 (2023-04-23) 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 2022 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 2022 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/2443067/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 Jul 8 01:50 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/3603484/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -262,7 +294,7 @@ Get: 60 http://deb.debian.org/debian bookworm/main amd64 libgmp3-dev amd64 2:6.2.1+dfsg1-1.1 [331 kB] Get: 61 http://deb.debian.org/debian bookworm/main amd64 libzarith-ocaml-dev amd64 1.12-1+b1 [90.8 kB] Get: 62 http://deb.debian.org/debian bookworm/main amd64 libcoq-core-ocaml-dev amd64 8.16.1+dfsg-1+b2 [42.7 MB] -Fetched 317 MB in 5s (69.3 MB/s) +Fetched 317 MB in 4s (88.1 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 ... 19591 files and directories currently installed.) @@ -526,8 +558,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-unicoq-1.6-8.16/ && 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-unicoq_1.6-8.16-2_source.changes +I: user script /srv/workspace/pbuilder/3603484/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/3603484/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/coq-unicoq-1.6-8.16/ && 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-unicoq_1.6-8.16-2_source.changes dpkg-buildpackage: info: source package coq-unicoq dpkg-buildpackage: info: source version 1.6-8.16-2 dpkg-buildpackage: info: source distribution unstable @@ -552,7 +595,7 @@ coq_makefile -f _CoqProject -o Makefile make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16' dh_auto_build - make -j15 "INSTALL=install --strip-program=true" + make -j16 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-unicoq-1.6-8.16' COQDEP VFILES COQPP src/unitactics.mlg @@ -662,45 +705,7 @@ _?x =?= (?n 0) (Meta-Inst) OK __nat =<= nat (Reduce-Same) OK ?A =<= nat (Meta-Inst) OK -_Set =<= Type (Reduce-Same)Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst) -?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -(0 = 0) =<= (?n x = 0) (App-FO) -_@eq =<= @eq (Rigid-Same) -_nat =?= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -_(?n x) =?= 0 (Meta-Inst) -__(nat -> nat) =<= (nat -> nat) (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -_0 =?= 0 (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -inst1 = eq_refl - : (fun _ : nat => 0) x = 0 - OK +_Set =<= Type (Reduce-Same) OK (?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK _@eq =<= @eq (Rigid-Same) OK _?A =?= nat (Meta-Inst) OK @@ -710,7 +715,7 @@ _((fun x : nat => ?n) 0) =?= 0 (Meta-Specialize) OK __?n =?= 0 (Meta-DelDeps) OK ___?n =?= 0 (Meta-Inst) OK -____nat =<= nat (Reduce-Same)?T =<= nat (Meta-Inst) OK +____nat =<= nat (Reduce-Same) OK ?A =<= nat (Meta-Inst) OK _Set =<= Type (Reduce-Same) OK (?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK @@ -730,11 +735,6 @@ ?T@\{x:=x; x0:=x; x1:=x\} =<= ?A (Meta-Inst) ERR _?A =<= ?T@\{x:=x; x0:=x; x1:=x\} (Meta-Inst) OK ?T@\{x:=x; x0:=x; x1:=x\} =<= nat (Meta-Inst) OK -_Set =<= Type (Reduce-Same) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst) -?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) _Set =<= Type (Reduce-Same) OK (?x = ?x) =<= (?n x x = S x) (App-FO) ERR _@eq =<= @eq (Rigid-Same) OK @@ -745,81 +745,22 @@ __nat =<= nat (Reduce-Same) OK _(?n x x) =?= (S x) (Meta-Inst) ERR _(?n x x) =?= (S x) (Meta-DelDeps) ERR -__(?n x x) =?= (S x) (Meta-Inst) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -(x = x) =<= (?n x = x) (App-FO) -_@eq =<= @eq (Rigid-Same) -_nat =?= nat (Reduce-Same) -_(?n x) =?= x (Meta-Inst) -_(?n x) =?= x (Meta-DelDeps) ERR +__(?n x x) =?= (S x) (Meta-Inst) ERR (?x = ?x) =<= (?n x x = S x) (App-FO) ERR _@eq =<= @eq (Rigid-Same) OK -_?A =?= nat (Meta-Inst) -__(?n x) =?= x (Meta-Inst) OK +_?A =?= nat (Meta-Inst) OK __Set =<= Type (Reduce-Same) OK _(?n x x) =?= ?x (Meta-Inst) ERR _?x =?= (?n x x) (Meta-Inst) OK __nat =<= nat (Reduce-Same) OK _(?n x x) =?= (S x) (Meta-Inst) ERR _(?n x x) =?= (S x) (Meta-DelDeps) ERR -__(?n x x) =?= (S x) (Meta-Inst) -___(nat -> nat) =<= (nat -> nat) (Reduce-Same) -_x =?= x (Reduce-Same) -inst2 = eq_refl - : (fun n : nat => n) x = x -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) ERR +__(?n x x) =?= (S x) (Meta-Inst) ERR 0 =?= 0 (App-FO) OK -_0 =?= 0 (Rigid-Same) -?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst) -?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -(x = x) =<= (?n x y z = x) (App-FO) -_@eq =<= @eq (Rigid-Same) -_nat =?= nat (Reduce-Same) -_(?n x y z) =?= x (Meta-Inst) -_(?n x y z) =?= x (Meta-DelDeps) -__(?n x y z) =?= x (Meta-Inst) -___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same) -_x =?= x (Reduce-Same) OK +_0 =?= 0 (Rigid-Same) OK Decimal.uint n) x y z = x -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst) -?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -(z = z) =<= (?n x y z = z) (App-FO) -_@eq =<= @eq (Rigid-Same) -_nat =?= nat (Reduce-Same) -_(?n x y z) =?= z (Meta-Inst) -_(?n x y z) =?= z (Meta-DelDeps) -__(?n x y z) =?= z (Meta-Inst) -___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same) -_z =?= z (Reduce-Same) -inst4 = eq_refl - : (fun _ _ n1 : nat => n1) x y z = z -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same)Number.uint O in X x) =?= O (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst) -?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -(@eq ?A ?x ?x) =<= (@eq nat ((fun w : forall _ : nat, nat => w) ?w x) O) (App-FO) -_@eq =<= @eq (Rigid-Same) -_?A =?= nat (Meta-Inst) -__Set =<= Type (Reduce-Same) -_?x =?= ((fun w : forall _ : nat, nat => w) ?w x) (Meta-Inst) -__nat =<= nat (Reduce-Same) -_(?w x) =?= O (Meta-Inst) -__(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -nat =<= nat (Reduce-Same) -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same)(let x := True in ?Goal) - -?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst) -_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst) -(@eq ?T@\{x:=x; x0:=x\} ((fun w : forall x0 : nat, ?T => w) ?w x) - ((fun w : forall x0 : nat, ?T => w) ?w x)) =<= (@eq nat O O) (App-FO) -_@eq =<= @eq (Rigid-Same) -_?T@\{x:=x; x0:=x\} =?= nat (Meta-Inst) -__Set =<= Type (Reduce-Same) -_((fun w : forall _ : nat, nat => w) ?w x) =?= O (Lam-BetaL) -__(?w x) =?= O (Meta-Inst) -___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) -_((fun w : forall _ : nat, nat => w) (fun _ : nat => O) x) =?= O (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same)Number.uint ?n - | S _ => O - end x) (App-FO) -_@eq =<= @eq (Rigid-Same) -_?A =?= nat (Meta-Inst) -__Set =<= Type (Reduce-Same) -_?x =?= match O return nat with -| O => ?n -| S _ => O -end (Meta-Inst) -__nat =<= nat (Reduce-Same) -_match O return nat with -| O => ?n -| S _ => O -end =?= x (App-FO) -_match O return nat with -| O => ?n -| S _ => O -end =?= x (Case-IotaL) -__?n =?= x (Meta-Inst) -___nat =<= nat (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Decimal.uint =<= Decimal.uint (Reduce-Same) -Number.uint =<= Number.uint (Reduce-Same) -Type =<= Type (Reduce-Same) -?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps) -_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst) -__Type =<= Type (Reduce-Same) -?T =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -?A =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -nat =<= nat (Reduce-Same) -(@eq ?A ?x ?x) =<= (@eq nat - (match O return (forall _ : nat, nat) with - | O => ?n - | S _ => fun _ : nat => O - end x) x) (App-FO) -_@eq =<= @eq (Rigid-Same) -_?A =?= nat (Meta-Inst) -__Set =<= Type (Reduce-Same)tt - : unit nat ?n - | S _ => fun _ : nat => O - end x) (Meta-Inst)Decimal.uint ?n - | S _ => fun _ : nat => O - end x) =?= x (Case-IotaL) -__(?n x) =?= x (Meta-Inst)nat m | S p => S (add p m) end) 0 0)) - -Type =<= Type (Reduce-Same)nat ?n - | S _ => fun _ : nat => O - end x) - (match O return (forall _ : nat, nat) with - | O => ?n - | S _ => fun _ : nat => O - end x)) =<= (@eq nat x x) (App-FO) -_@eq =<= @eq (Rigid-Same) -_nat =?= nat (Reduce-Same) -_(match O return (forall _ : nat, nat) with - | O => ?n - | S _ => fun _ : nat => O - end x) =?= x (Case-IotaL) -__(?n x) =?= x (Meta-Inst) -__(?n x) =?= x (Meta-DelDeps) -___(?n x) =?= x (Meta-Inst) -____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)nat fun n : nat => n - | S _ => fun _ : nat => O - end x) =?= x (Reduce-Same)(nat -> nat) nat) nat) =<= nat (App-FO) ERR (nat -> nat) nat) =<= nat (App-FO) ERR @@ -1163,42 +908,20 @@ | 0 => m | S p => S (add p m) end) 0 0) (Meta-Inst) OK -___nat =<= nat (Reduce-Same) -nat =<= nat (Reduce-Same) -?A0 =<= nat (Meta-Inst) -_Set =<= Type (Reduce-Same) -nat =<= nat (Reduce-Same) -?B =<= nat (Meta-Inst) OK +___nat =<= nat (Reduce-Same) OK +Decimal.uint x) 1) - -____Prop =<= Prop (Reduce-Same)nat x) 1) +nat nat) nat) =<= nat (App-FO) ERR @@ -1296,7 +961,7 @@ nat x) 1) (Cons-DeltaNotStuckR) OK @@ -1323,20 +988,37 @@ Decimal.uint nat) =<= (nat -> nat) (Reduce-Same) +nat =<= nat (Reduce-Same) +nat =<= nat (Reduce-Same) +nat =<= nat (Reduce-Same) OK Decimal.uint nat) nat) =<= (forall x0 : nat, ?T) (App-FO) OK -__(nat -> nat) =<= (forall x0 : nat, ?T) (Prod-Same) OK +__(nat -> nat) =<= (forall x0 : nat, ?T) (Prod-Same) +inst1 = eq_refl + : (fun _ : nat => 0) x = 0 + OK ___nat =?= nat (Reduce-Same) OK ___?T@\{x0:=n\} =<= nat (Meta-Inst) OK ____Set =<= Type (Reduce-Same) OK nat nat) =<= (forall x1 : nat, ?T@\{x0:=n\}) (Prod-Same) OK _______nat =?= nat (Reduce-Same) OK _______?T@\{x0:=n; x1:=n\} =<= nat (Meta-Inst) OK -________Set =<= Type (Reduce-Same) OK +________Set =<= Type (Reduce-Same) +_Set =<= Type (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +(x = x) =<= (?n x = x) (App-FO) +_@eq =<= @eq (Rigid-Same) +_nat =?= nat (Reduce-Same) +_(?n x) =?= x (Meta-Inst) +_(?n x) =?= x (Meta-DelDeps) +__(?n x) =?= x (Meta-Inst) +___(nat -> nat) =<= (nat -> nat) (Reduce-Same) +_x =?= x (Reduce-Same) +inst2 = eq_refl + : (fun n : nat => n) x = x +?T =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst) +_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst) +?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +(x = x) =<= (?n x y z = x) (App-FO) +_@eq =<= @eq (Rigid-Same) +_nat =?= nat (Reduce-Same) +_(?n x y z) =?= x (Meta-Inst) +_(?n x y z) =?= x (Meta-DelDeps) +__(?n x y z) =?= x (Meta-Inst) +___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same) +_x =?= x (Reduce-Same) +inst3 = eq_refl + : (fun n _ _ : nat => n) x y z = x +?T =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst) +_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst) +?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +(z = z) =<= (?n x y z = z) (App-FO) OK nat ?n) x = x) + +___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same) +_z =?= z (Reduce-Same) +inst4 = eq_refl + : (fun _ _ n1 : nat => n1) x y z = z +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +nat =<= nat (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +nat =<= nat (Reduce-Same) +(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in @eq nat (X x) O) (Let-ZetaR) +_(@eq ?A ?x ?x) =<= (@eq nat (?n x) O) (App-FO) +__@eq =<= @eq (Rigid-Same) +__?A =?= nat (Meta-Inst) +___Set =<= Type (Reduce-Same) +__(?n x) =?= ?x (Meta-Inst) +__?x =?= (?n x) (Meta-Inst) +___nat =<= nat (Reduce-Same) +__(?n x) =?= O (Meta-Inst) +___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same)(?x = ?x) ?n) x = x) ?A =?= nat Set ?n) x) @@ -1478,18 +1263,36 @@ ?n@{z:=x} =?= (Nat.add x) (nat -> nat) nat) y =?= y -aggressive_double_var' = + +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +nat =<= nat (Reduce-Same)aggressive_double_var' = fun x y : nat => eq_refl : forall x y : nat, (fun z : nat => Nat.add z) x y = x + y Arguments aggressive_double_var' (x y)%nat_scope -Decimal.uint O in X x) =?= O (Reduce-Same)Set ?n) x 0 y) nat w) ?w x) O) (App-FO) +_@eq =<= @eq (Rigid-Same) +_?A =?= nat (Meta-Inst)?n@{u:=x; w:=y} =?= x + +__Set =<= Type (Reduce-Same)nat w) ?w x) (Meta-Inst)nat eq_refl @@ -1537,32 +1354,125 @@ nat ?n) 0 x y = x) -nat ?n) 0 x y = x) + +?A =<= nat (Meta-Inst)nat ?n) 0 x y) + +(@eq ?T@\{x:=x; x0:=x\} ((fun w : forall x0 : nat, ?T => w) ?w x) + ((fun w : forall x0 : nat, ?T => w) ?w x)) =<= (@eq nat O O) (App-FO)nat w) ?w x) =?= O (Lam-BetaL)nat ?n) 0 x y = x) (App-FO) OK + +___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) +_((fun w : forall _ : nat, nat => w) (fun _ : nat => O) x) =?= O (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Type =<= Type (Reduce-Same) +?T =<= nat (Meta-DelDeps) +_?T =<= nat (Meta-Inst) +__Set =<= Type (Reduce-Same) +nat =<= nat (Reduce-Same) +nat =<= nat (Reduce-Same) +(@eq ?A ?x ?x) =<= (@eq nat match O return nat with + | O => ?n + | S _ => O + end x) (App-FO) +_@eq =<= @eq (Rigid-Same) +_?A =?= nat (Meta-Inst) +__Set =<= Type (Reduce-Same) +_?x =?= match O return nat with +| O => ?n +| S _ => O +end (Meta-Inst) +__nat =<= nat (Reduce-Same) +_match O return nat with +| O => ?n +| S _ => O +end =?= x (App-FO) +_match O return nat with +| O => ?n +| S _ => O +end =?= x (Case-IotaL) +__?n =?= x (Meta-Inst) +___nat =<= nat (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Decimal.uint =<= Decimal.uint (Reduce-Same)?n@{x:=x; y:=y; u:=0; v:=x; w:=y} =?= x + +Decimal.uint =<= Decimal.uint (Reduce-Same) +Number.uint =<= Number.uint (Reduce-Same) +Type =<= Type (Reduce-Same) +?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps) +_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst) +__Type =<= Type (Reduce-Same) +?T =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +?A =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +nat =<= nat (Reduce-Same) +(@eq ?A ?x ?x) =<= (@eq nat + (match O return (forall _ : nat, nat) with + | O => ?n + | S _ => fun _ : nat => O + end x) x) (App-FO) +_@eq =<= @eq (Rigid-Same) +_?A =?= nat (Meta-Inst)?n@{v:=x; w:=y} =?= x + +__Set =<= Type (Reduce-Same) +_?x =?= (match O return (forall _ : nat, nat) with + | O => ?n + | S _ => fun _ : nat => O + end x) (Meta-Inst)nat ?n) 0 x y = x) (App-FO) OK _@eq =<= @eq (Rigid-Same) OK _?A =?= nat (Meta-Inst) OK __Set =<= Type (Reduce-Same) OK @@ -1570,7 +1480,15 @@ __nat =<= nat (Reduce-Same) OK _?n@\{v:=x; w:=y\} =?= x (Meta-DelDeps) OK __?n@\{v:=x; w:=y\} =?= x (Meta-Inst) OK -___nat =<= nat (Reduce-Same) OK +___nat =<= nat (Reduce-Same) +_(match O return (forall _ : nat, nat) with + | O => ?n + | S _ => fun _ : nat => O + end x) =?= x (Case-IotaL) +__(?n x) =?= x (Meta-Inst) +__(?n x) =?= x (Meta-DelDeps) +___(?n x) =?= x (Meta-Inst) +____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same) OK nat ?n + | S _ => fun _ : nat => O + end x) + (match O return (forall _ : nat, nat) with + | O => ?n + | S _ => fun _ : nat => O + end x)) =<= (@eq nat x x) (App-FO) +_@eq =<= @eq (Rigid-Same)Set ?n) y x 0 = x) +__Set =<= Type (Reduce-Same) +_(match O return (forall _ : nat, nat) with + | O => ?n + | S _ => fun _ : nat => O + end x) =?= x (Case-IotaL) +__(?n x) =?= x (Meta-Inst) +__(?n x) =?= x (Meta-DelDeps) OK nat ?n) y x 0 = x) nat fun n : nat => n + | S _ => fun _ : nat => O + end x) =?= x (Reduce-Same)nat eq_refl : forall x y : nat, nat -> (fun _ v _ : nat => v) y x 0 = x Arguments aggressive_const'' (x y z)%nat_scope -Type B -> Prop) B -> Prop) + +?B =<= nat (Meta-Inst) +_Set =<= Type (Reduce-Same) +(prod nat nat) =<= (prod nat nat) (Reduce-Same)(B -> B -> Prop) B -> Prop) ((A -> B) -> (A -> B) -> Prop) ?B -> Prop) -(A -> B) =?= ?B -Type B) -> Prop) B) -> Prop) -((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (App-FO) OK + +(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in + @eq (prod nat nat) (@pair nat nat (X x) (X x)) (@pair nat nat (X x) x)) (Let-ZetaR) +_(@eq ?A ?x ?x) =<= (@eq (prod nat nat) (@pair nat nat (?n x) (?n x)) (@pair nat nat (?n x) x)) (App-FO) +__@eq =<= @eq (Rigid-Same)(A -> B) =?= ?B + +__?A =?= (prod nat nat) (Meta-Inst) +___Set =<= Type (Reduce-Same) +__?x =?= (@pair nat nat (?n x) (?n x)) (Meta-Inst) +___(prod nat nat) =<= (prod nat nat) (Reduce-Same)Type B) -> Prop) B) -> Prop) + +___nat =?= nat (Reduce-Same) +___nat =?= nat (Reduce-Same) +___(?n x) =?= (?n x) (Meta-Same-Same)((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (App-FO) OK _((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (Prod-Same) OK __?B =?= (A -> B) (Meta-Inst) OK ___Type =<= Type (Reduce-Same) OK -__((A -> B) -> Prop) =<= ((A -> B) -> Prop) (Reduce-Same) OK +__((A -> B) -> Prop) =<= ((A -> B) -> Prop) (Reduce-Same) +____x =?= x (Reduce-Same) OK Prop B -> Prop) -> Prop) B -> Prop) -> Prop) -(forall B : Type, (B -> B -> Prop) -> Prop) B -> Prop) -> Prop) + +___(?n x) =?= x (Meta-Inst) +___(?n x) =?= x (Meta-DelDeps)((B -> B -> Prop) -> Prop) B -> Prop) -> Prop) + +____(?n x) =?= x (Meta-Inst) +_____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)(forall B : Type, (B -> B -> Prop) -> Prop) B -> Prop) -> Prop) Prop B -> Prop) -> Prop) -> Prop) B -> Prop) -> Prop) -> Prop) ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) B -> Prop) -> Prop) -> Prop) -(nat -> nat) nat) -(nat -> nat -> nat) nat -> nat) -(nat -> nat -> nat -> nat) nat -> nat -> nat) -nat nat) nat) + +_(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (App-FO) +__(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (Prod-Same) +___?T =?= Type (Meta-Inst)(nat -> nat -> nat) nat -> nat) + +____Type =<= Type (Reduce-Same) +___(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (App-FO)(nat -> nat -> nat -> nat) nat -> nat -> nat) + +____(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (Prod-Same) +_____?T =?= T (Meta-Inst) +______Type =<= Type (Reduce-Same)nat ?n) y y x) ?n =?= ?n@{x:=y; y:=y; z:=x} (?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = y) +tt + : unit ?A =?= nat Set ?n) x y z) @@ -2464,7 +2507,7 @@ ___nat =<= nat (Reduce-Same) OK __?n =?= y (Meta-Inst) ERR STATS: 902 165 -Finished transaction in 5.46 secs (5.043u,0.12s) (successful) +Finished transaction in 10.452 secs (5.436u,0.124s) (successful) make[1]: Leaving directory '/build/coq-unicoq-1.6-8.16' dh_auto_test create-stamp debian/debhelper-build-stamp @@ -2532,8 +2575,8 @@ dpkg-gencontrol: warning: package libcoq-unicoq: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums dh_builddeb -dpkg-deb: building package 'libcoq-unicoq-dbgsym' in '../libcoq-unicoq-dbgsym_1.6-8.16-2_amd64.deb'. dpkg-deb: building package 'libcoq-unicoq' in '../libcoq-unicoq_1.6-8.16-2_amd64.deb'. +dpkg-deb: building package 'libcoq-unicoq-dbgsym' in '../libcoq-unicoq-dbgsym_1.6-8.16-2_amd64.deb'. dpkg-genbuildinfo --build=binary -O../coq-unicoq_1.6-8.16-2_amd64.buildinfo dpkg-genchanges --build=binary -O../coq-unicoq_1.6-8.16-2_amd64.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -2541,12 +2584,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/3603484/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3603484/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/2443067 and its subdirectories -I: Current time: Sun Jun 4 17:27:14 -12 2023 -I: pbuilder-time-stamp: 1685942834 +I: removing directory /srv/workspace/pbuilder/3603484 and its subdirectories +I: Current time: Mon Jul 8 01:51:55 +14 2024 +I: pbuilder-time-stamp: 1720353115