Diff of the two buildlogs: -- --- b1/build.log 2023-05-30 07:11:06.656316258 +0000 +++ b2/build.log 2023-05-30 07:22:58.033197758 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Mon May 29 19:01:33 -12 2023 -I: pbuilder-time-stamp: 1685430093 +I: Current time: Tue May 30 21:11:22 +14 2023 +I: pbuilder-time-stamp: 1685430682 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-mtac2_1.4+8.16.orig.tar.gz] I: copying [./coq-mtac2_1.4+8.16-2.debian.tar.xz] I: Extracting source -gpgv: Signature made Wed Jan 25 00:09:05 2023 -12 +gpgv: Signature made Thu Jan 26 02:09:05 2023 +14 gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 gpgv: issuer "jpuydt@debian.org" gpgv: Can't check signature: No public key @@ -28,135 +28,167 @@ dpkg-source: info: applying fix_configure.sh.patch I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/12391/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/12848/tmp/hooks/D01_modify_environment starting +debug: Running on jtx1b. +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 30 21:11 /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/12848/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/12848/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='armhf' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 ' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='armhf' + 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]="arm-unknown-linux-gnueabihf") + 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=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4 ' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='4c13c87e2185484ca35778c099d083a8' - 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='12391' - PS1='# ' - PS2='> ' + INVOCATION_ID=3cc539bb1a114a5c8d7ac40e605f9a40 + LANG=C + LANGUAGE=it_CH:it + LC_ALL=C + MACHTYPE=arm-unknown-linux-gnueabihf + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnueabihf + 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=12848 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.BrOaOMS5/pbuilderrc_4jxt --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.BrOaOMS5/b1 --logfile b1/build.log coq-mtac2_1.4+8.16-2.dsc' - SUDO_GID='112' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://10.0.0.15:3142/' + 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.BrOaOMS5/pbuilderrc_oNRg --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.BrOaOMS5/b2 --logfile b2/build.log --extrapackages usrmerge coq-mtac2_1.4+8.16-2.dsc' + SUDO_GID=114 + SUDO_UID=110 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://10.0.0.15:3142/ I: uname -a - Linux virt32b 5.10.0-23-armmp-lpae #1 SMP Debian 5.10.179-1 (2023-05-12) armv7l GNU/Linux + Linux i-capture-the-hostname 5.10.0-23-arm64 #1 SMP Debian 5.10.179-1 (2023-05-12) aarch64 GNU/Linux I: ls -l /bin total 5072 - -rwxr-xr-x 1 root root 838488 Apr 23 09:24 bash - -rwxr-xr-x 3 root root 67144 Sep 18 2022 bunzip2 - -rwxr-xr-x 3 root root 67144 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 67144 Sep 18 2022 bzip2 - -rwxr-xr-x 1 root root 67112 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 67632 Sep 20 2022 cat - -rwxr-xr-x 1 root root 67676 Sep 20 2022 chgrp - -rwxr-xr-x 1 root root 67644 Sep 20 2022 chmod - -rwxr-xr-x 1 root root 67684 Sep 20 2022 chown - -rwxr-xr-x 1 root root 133532 Sep 20 2022 cp - -rwxr-xr-x 1 root root 132868 Jan 5 01:20 dash - -rwxr-xr-x 1 root root 133220 Sep 20 2022 date - -rwxr-xr-x 1 root root 67732 Sep 20 2022 dd - -rwxr-xr-x 1 root root 68104 Sep 20 2022 df - -rwxr-xr-x 1 root root 133632 Sep 20 2022 dir - -rwxr-xr-x 1 root root 59128 Mar 22 21: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 67560 Sep 20 2022 echo - -rwxr-xr-x 1 root root 41 Jan 24 02:43 egrep - -rwxr-xr-x 1 root root 67548 Sep 20 2022 false - -rwxr-xr-x 1 root root 41 Jan 24 02:43 fgrep - -rwxr-xr-x 1 root root 55748 Mar 22 21:02 findmnt - -rwsr-xr-x 1 root root 26208 Mar 22 20:15 fusermount - -rwxr-xr-x 1 root root 128608 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 64220 Apr 9 2022 gzip - -rwxr-xr-x 1 root root 67032 Dec 19 01:33 hostname - -rwxr-xr-x 1 root root 67720 Sep 20 2022 ln - -rwxr-xr-x 1 root root 35132 Mar 22 21:51 login - -rwxr-xr-x 1 root root 133632 Sep 20 2022 ls - -rwxr-xr-x 1 root root 136808 Mar 22 21:02 lsblk - -rwxr-xr-x 1 root root 67800 Sep 20 2022 mkdir - -rwxr-xr-x 1 root root 67764 Sep 20 2022 mknod - -rwxr-xr-x 1 root root 67596 Sep 20 2022 mktemp - -rwxr-xr-x 1 root root 38504 Mar 22 21:02 more - -rwsr-xr-x 1 root root 38496 Mar 22 21:02 mount - -rwxr-xr-x 1 root root 9824 Mar 22 21:02 mountpoint - -rwxr-xr-x 1 root root 133532 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 67608 Sep 20 2022 pwd - lrwxrwxrwx 1 root root 4 Apr 23 09:24 rbash -> bash - -rwxr-xr-x 1 root root 67600 Sep 20 2022 readlink - -rwxr-xr-x 1 root root 67672 Sep 20 2022 rm - -rwxr-xr-x 1 root root 67600 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 67400 Nov 2 2022 run-parts - -rwxr-xr-x 1 root root 133372 Jan 5 07:55 sed - lrwxrwxrwx 1 root root 4 Jan 5 01:20 sh -> dash - -rwxr-xr-x 1 root root 67584 Sep 20 2022 sleep - -rwxr-xr-x 1 root root 67644 Sep 20 2022 stty - -rwsr-xr-x 1 root root 50800 Mar 22 21:02 su - -rwxr-xr-x 1 root root 67584 Sep 20 2022 sync - -rwxr-xr-x 1 root root 336764 Apr 6 02:25 tar - -rwxr-xr-x 1 root root 67144 Nov 2 2022 tempfile - -rwxr-xr-x 1 root root 133224 Sep 20 2022 touch - -rwxr-xr-x 1 root root 67548 Sep 20 2022 true - -rwxr-xr-x 1 root root 9768 Mar 22 20:15 ulockmgr_server - -rwsr-xr-x 1 root root 22108 Mar 22 21:02 umount - -rwxr-xr-x 1 root root 67572 Sep 20 2022 uname - -rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress - -rwxr-xr-x 1 root root 133632 Sep 20 2022 vdir - -rwxr-xr-x 1 root root 42608 Mar 22 21: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/12391/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 838488 Apr 24 11:24 bash + -rwxr-xr-x 3 root root 67144 Sep 19 2022 bunzip2 + -rwxr-xr-x 3 root root 67144 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 67144 Sep 19 2022 bzip2 + -rwxr-xr-x 1 root root 67112 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 67632 Sep 21 2022 cat + -rwxr-xr-x 1 root root 67676 Sep 21 2022 chgrp + -rwxr-xr-x 1 root root 67644 Sep 21 2022 chmod + -rwxr-xr-x 1 root root 67684 Sep 21 2022 chown + -rwxr-xr-x 1 root root 133532 Sep 21 2022 cp + -rwxr-xr-x 1 root root 132868 Jan 6 03:20 dash + -rwxr-xr-x 1 root root 133220 Sep 21 2022 date + -rwxr-xr-x 1 root root 67732 Sep 21 2022 dd + -rwxr-xr-x 1 root root 68104 Sep 21 2022 df + -rwxr-xr-x 1 root root 133632 Sep 21 2022 dir + -rwxr-xr-x 1 root root 59128 Mar 23 23:02 dmesg + lrwxrwxrwx 1 root root 8 Dec 20 03:33 dnsdomainname -> hostname + lrwxrwxrwx 1 root root 8 Dec 20 03:33 domainname -> hostname + -rwxr-xr-x 1 root root 67560 Sep 21 2022 echo + -rwxr-xr-x 1 root root 41 Jan 25 04:43 egrep + -rwxr-xr-x 1 root root 67548 Sep 21 2022 false + -rwxr-xr-x 1 root root 41 Jan 25 04:43 fgrep + -rwxr-xr-x 1 root root 55748 Mar 23 23:02 findmnt + -rwsr-xr-x 1 root root 26208 Mar 23 22:15 fusermount + -rwxr-xr-x 1 root root 128608 Jan 25 04:43 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 64220 Apr 10 2022 gzip + -rwxr-xr-x 1 root root 67032 Dec 20 03:33 hostname + -rwxr-xr-x 1 root root 67720 Sep 21 2022 ln + -rwxr-xr-x 1 root root 35132 Mar 23 23:51 login + -rwxr-xr-x 1 root root 133632 Sep 21 2022 ls + -rwxr-xr-x 1 root root 136808 Mar 23 23:02 lsblk + -rwxr-xr-x 1 root root 67800 Sep 21 2022 mkdir + -rwxr-xr-x 1 root root 67764 Sep 21 2022 mknod + -rwxr-xr-x 1 root root 67596 Sep 21 2022 mktemp + -rwxr-xr-x 1 root root 38504 Mar 23 23:02 more + -rwsr-xr-x 1 root root 38496 Mar 23 23:02 mount + -rwxr-xr-x 1 root root 9824 Mar 23 23:02 mountpoint + -rwxr-xr-x 1 root root 133532 Sep 21 2022 mv + lrwxrwxrwx 1 root root 8 Dec 20 03:33 nisdomainname -> hostname + lrwxrwxrwx 1 root root 14 Apr 3 20:25 pidof -> /sbin/killall5 + -rwxr-xr-x 1 root root 67608 Sep 21 2022 pwd + lrwxrwxrwx 1 root root 4 Apr 24 11:24 rbash -> bash + -rwxr-xr-x 1 root root 67600 Sep 21 2022 readlink + -rwxr-xr-x 1 root root 67672 Sep 21 2022 rm + -rwxr-xr-x 1 root root 67600 Sep 21 2022 rmdir + -rwxr-xr-x 1 root root 67400 Nov 3 2022 run-parts + -rwxr-xr-x 1 root root 133372 Jan 6 09:55 sed + lrwxrwxrwx 1 root root 9 May 30 21:11 sh -> /bin/bash + -rwxr-xr-x 1 root root 67584 Sep 21 2022 sleep + -rwxr-xr-x 1 root root 67644 Sep 21 2022 stty + -rwsr-xr-x 1 root root 50800 Mar 23 23:02 su + -rwxr-xr-x 1 root root 67584 Sep 21 2022 sync + -rwxr-xr-x 1 root root 336764 Apr 7 04:25 tar + -rwxr-xr-x 1 root root 67144 Nov 3 2022 tempfile + -rwxr-xr-x 1 root root 133224 Sep 21 2022 touch + -rwxr-xr-x 1 root root 67548 Sep 21 2022 true + -rwxr-xr-x 1 root root 9768 Mar 23 22:15 ulockmgr_server + -rwsr-xr-x 1 root root 22108 Mar 23 23:02 umount + -rwxr-xr-x 1 root root 67572 Sep 21 2022 uname + -rwxr-xr-x 2 root root 2346 Apr 10 2022 uncompress + -rwxr-xr-x 1 root root 133632 Sep 21 2022 vdir + -rwxr-xr-x 1 root root 42608 Mar 23 23:02 wdctl + lrwxrwxrwx 1 root root 8 Dec 20 03:33 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/12848/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -269,7 +301,7 @@ Get: 61 http://deb.debian.org/debian bookworm/main armhf libzarith-ocaml-dev armhf 1.12-1+b1 [90.2 kB] Get: 62 http://deb.debian.org/debian bookworm/main armhf libcoq-core-ocaml-dev armhf 8.16.1+dfsg-1+b2 [43.1 MB] Get: 63 http://deb.debian.org/debian bookworm/main armhf libcoq-unicoq armhf 1.6-8.16-2+b1 [77.9 kB] -Fetched 310 MB in 33s (9307 kB/s) +Fetched 310 MB in 28s (11.0 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:armhf. (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 ... 19324 files and directories currently installed.) @@ -537,8 +569,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-mtac2-1.4+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-mtac2_1.4+8.16-2_source.changes +I: user script /srv/workspace/pbuilder/12848/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/12848/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/coq-mtac2-1.4+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-mtac2_1.4+8.16-2_source.changes dpkg-buildpackage: info: source package coq-mtac2 dpkg-buildpackage: info: source version 1.4+8.16-2 dpkg-buildpackage: info: source distribution unstable @@ -565,16 +608,16 @@ Warning: in orphan_Mtac2Tests_Mtac2 make[1]: Leaving directory '/build/coq-mtac2-1.4+8.16' dh_auto_build - make -j3 "INSTALL=install --strip-program=true" + make -j4 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-mtac2-1.4+8.16' COQDEP VFILES COQPP src/metaCoqInit.mlg COQPP src/metaCoqTactic.mlg CAMLDEP src/metaCoqInterp.mli CAMLDEP src/run.mli -*** Warning: in file theories/Base.v, declared ML module ././unicoq has not been found! CAMLDEP src/mConstr.mli CAMLDEP src/mtacNames.mli +*** Warning: in file theories/Base.v, declared ML module ././unicoq has not been found! CAMLDEP src/constrs.mli CAMLDEP src/metaCoqInstr.mli OCAMLLIBDEP src/MetaCoqPlugin.mlpack @@ -585,8 +628,8 @@ CAMLDEP src/constrs.ml CAMLDEP src/metaCoqTactic.ml CAMLDEP src/metaCoqInit.ml -COQC theories/lib/Datatypes.v COQC theories/lib/Logic.v +COQC theories/lib/Datatypes.v COQC theories/intf/Sorts.v CAMLC -c src/constrs.mli CAMLC -c src/mConstr.mli @@ -600,6 +643,7 @@ COQC theories/intf/Tm_kind.v COQC theories/lib/Specif.v COQC theories/lib/List.v +CAMLOPT -c -for-pack MetaCoqPlugin src/constrs.ml File "./theories/lib/Specif.v", line 201, characters 0-144: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -609,27 +653,25 @@ File "./theories/lib/Specif.v", line 214, characters 0-144: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -CAMLOPT -c -for-pack MetaCoqPlugin src/constrs.ml File "./theories/lib/Specif.v", line 214, characters 0-144: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] CAMLC -c src/mtacNames.mli CAMLC -c src/metaCoqInterp.mli COQC theories/intf/MTele.v -COQC theories/intf/Exceptions.v COQC theories/intf/Reduction.v +COQC theories/intf/Case.v File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -File "./theories/intf/MTele.v", line 151, characters 0-224: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -COQC theories/intf/Case.v COQC theories/lib/Utils.v CAMLOPT -c -for-pack MetaCoqPlugin src/mtacNames.ml -COQC theories/Pattern.v +File "./theories/intf/MTele.v", line 151, characters 0-224: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +COQC theories/intf/Exceptions.v CAMLOPT -c -for-pack MetaCoqPlugin src/mConstr.ml File "src/mConstr.ml", line 158, characters 21-41: 158 | let isconstant n h = Names.Constant.equal (Lazy.force n) h @@ -637,20 +679,20 @@ Alert deprecated: Names.Constant.equal Use QConstant.equal CAMLOPT -c -for-pack MetaCoqPlugin src/run.ml +COQC theories/Pattern.v COQC theories/intf/M.v -File "./theories/intf/M.v", line 3, characters 0-80: -Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. -[notation-overridden,parsing] -File "./theories/intf/M.v", line 3, characters 0-80: -Warning: Notation "_ + { _ }" was already used in scope type_scope. -[notation-overridden,parsing] -COQC theories/intf/Lift.v CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInterp.ml File "src/metaCoqInterp.ml", line 158, characters 4-12: 158 | nf_enter begin fun gl -> ^^^^^^^^ Alert deprecated: Proofview.Goal.nf_enter Normalization is enforced by EConstr, please use [enter] +File "./theories/intf/M.v", line 3, characters 0-80: +Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. +[notation-overridden,parsing] +File "./theories/intf/M.v", line 3, characters 0-80: +Warning: Notation "_ + { _ }" was already used in scope type_scope. +[notation-overridden,parsing] File "src/metaCoqInterp.ml", line 184, characters 4-12: 184 | nf_enter begin fun gl -> ^^^^^^^^ @@ -661,36 +703,36 @@ CAMLOPT -pack -o src/MetaCoqPlugin.cmx CAMLOPT -a -o src/MetaCoqPlugin.cmxa CAMLOPT -shared -o src/MetaCoqPlugin.cmxs +COQC theories/intf/Lift.v COQC theories/Base.v File "./theories/Base.v", line 37, characters 0-124: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] -COQC theories/meta/MTeleMatchDef.v COQC theories/meta/MFixDef.v +COQC theories/meta/MTeleMatchDef.v COQC theories/tactics/TacticsBase.v +COQC theories/ideas/Abstract.v File "./theories/meta/MFixDef.v", line 1, characters 0-44: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] File "./theories/meta/MFixDef.v", line 1, characters 0-44: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -COQC theories/ideas/Abstract.v +COQC theories/meta/Exhaustive.v File "./theories/meta/MTeleMatchDef.v", line 67, characters 0-12: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. [require-in-module,fragile] -COQC theories/meta/Exhaustive.v +COQC theories/meta/MTeleMatch.v File "./theories/tactics/TacticsBase.v", line 298, characters 7-9: Warning: Unused variable l' catches more than one case. [unused-pattern-matching-variable,pattern-matching] File "./theories/tactics/TacticsBase.v", line 298, characters 4-5: Warning: Unused variable l catches more than one case. [unused-pattern-matching-variable,pattern-matching] -COQC theories/tactics/Tactics.v File "./theories/meta/Exhaustive.v", line 61, characters 0-259: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] -COQC theories/meta/MTeleMatch.v File "./theories/meta/MTeleMatch.v", line 2, characters 0-74: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -763,6 +805,7 @@ (mTele@{Mtac2.meta.MTeleMatch.352} (fun _ : nat => mBase@{Mtac2.meta.MTeleMatch.352})) (fun _ : nat => nat)) +COQC theories/tactics/Tactics.v COQC theories/meta/MFix.v File "./theories/meta/MFix.v", line 86, characters 5-44: Warning: The format modifier is irrelevant for only-parsing rules. @@ -791,6 +834,8 @@ Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] COQC theories/tactics/IntroPatt.v +COQC theories/tactics/CompoundTactics.v +COQC theories/Mtac2.v File "./theories/tactics/Ttactics.v", line 182, characters 0-30: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. @@ -800,8 +845,6 @@ this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes' [arguments-assert,vernacular] -COQC theories/tactics/CompoundTactics.v -COQC theories/Mtac2.v COQC theories/ideas/DepDestruct.v COQC theories/tactics/ConstrSelector.v COQC theories/ideas/SumRun.v @@ -814,26 +857,27 @@ Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] COQC theories/ideas/Transport.v -Finished transaction in 0.512 secs (0.347u,0.s) (successful) +Finished transaction in 0.694 secs (0.306u,0.s) (successful) COQC tests/ConstrSelector.v COQC tests/DepDestruct.v COQC tests/Exhaustive.v +COQC tests/UnivSanityCheck.v = 0 : nat = 1 : nat = let (eval) := ?runner in eval : nat - = let (eval) := ?runner in eval - : nat - = let (eval) := ?runner in eval - : nat mmatch 1 (let ps' := with [# ] S | _ : nat =n> M.print "S"| [# ] 0 | =n> M.print "O"| _ => M.print "not in constructor normal form" end in ps') : idmatcher_return M_InDepMatcher + = let (eval) := ?runner in eval + : nat + = let (eval) := ?runner in eval + : nat mmatch 1 (let ps' := with [# ] 0 | =n> M.print "O"| [# ] S | _ : nat =n> M.print "S"| @@ -847,6 +891,11 @@ [# ] S | _ : nat =n> M.print "S, never triggered" end in ps') : idmatcher_return M_InDepMatcher +Universes written to file "universes-mtac2.txt". +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] +0 + = Z0 + : Z mmatch (1 :: nil)%list (let ps' := with [# ] nil | =n> M.print "nil"| [# ] cons | @@ -855,6 +904,7 @@ _ => M.print "not in constructor normal form" end in ps') : idmatcher_return M_InDepMatcher +[DEBUG] Running test mmatch (1 :: nil)%list (let ps' := with [# ] nil | =n> M.print "nil"| [# ] cons | @@ -864,7 +914,9 @@ ps') : idmatcher_return M_InDepMatcher [OK] tests/Exhaustive.v -COQC tests/UnivSanityCheck.v +COQC tests/abs.v +[OK] tests/UnivSanityCheck.v +COQC tests/abs_prod.v File "./tests/ConstrSelector.v", line 47, characters 22-29: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -878,27 +930,19 @@ case_branches := [m: Dyn true | Dyn (fun _ : nat => false)] |} -Universes written to file "universes-mtac2.txt". -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] -0 - = Z0 - : Z -[DEBUG] Running test -[OK] tests/UnivSanityCheck.v -COQC tests/abs.v -[OK] tests/DepDestruct.v -COQC tests/abs_prod.v -[OK] tests/ConstrSelector.v -COQC tests/binders.v -[OK] tests/abs.v -COQC tests/bug_universes.v [DEBUG] (nat -> (fun T : Type => T) Type) +[OK] tests/abs.v [OK] tests/abs_prod.v +COQC tests/binders.v +COQC tests/bug_universes.v +[OK] tests/ConstrSelector.v COQC tests/bugs.v +[OK] tests/DepDestruct.v +COQC tests/cevar.v [DEBUG] (NameExistsInContext (TheName "x")) [DEBUG] (VarAppearsInValue z) [OK] tests/binders.v -COQC tests/cevar.v +COQC tests/comptactics.v testMmatch@{i j} = fun x : Type@{i} => x : Type@{i} -> Type@{max(i,j)} @@ -925,11 +969,18 @@ testexact is opaque Expands to: Constant Mtac2Tests.bug_universes.testexact [OK] tests/bug_universes.v -COQC tests/comptactics.v +COQC tests/debug_ex.v [DEBUG] true [DEBUG] (Metavar Propₛ (1 = 1) ?e) [OK] tests/bugs.v -COQC tests/debug_ex.v +COQC tests/decapp.v +[OK] tests/cevar.v +COQC tests/declare.v +[DEBUG] raise ?e +Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. +[DEBUG] (StuckTerm ?t) +[OK] tests/debug_ex.v +COQC tests/decompose.v File "./tests/comptactics.v", line 32, characters 28-35: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -948,8 +999,6 @@ File "./tests/comptactics.v", line 48, characters 15-22: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/cevar.v -COQC tests/decapp.v File "./tests/comptactics.v", line 52, characters 15-22: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -962,16 +1011,7 @@ File "./tests/comptactics.v", line 77, characters 15-22: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/comptactics.v -COQC tests/declare.v [DEBUG] (Specif.msigT (MTele.MTele_Const nat)) -[DEBUG] raise ?e -[OK] tests/decapp.v -Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. -[DEBUG] (StuckTerm ?t) -COQC tests/decompose.v -[OK] tests/debug_ex.v -COQC tests/dependent_let_goals.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -980,6 +1020,8 @@ [notation-overridden,parsing] [DEBUG] bla [DEBUG] bla +[OK] tests/decapp.v +COQC tests/dependent_let_goals.v = tt : unit bla = fun x : nat => (fun x0 : nat => {| s := x0 |}) x @@ -1022,13 +1064,17 @@ : nat NAT3 = 3 : nat +[OK] tests/comptactics.v +COQC tests/destruct_eq.v NAT3: nat NAT2: nat NAT1: nat NAT0: nat +[OK] tests/decompose.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for (@M.runner unit ev) without backtracking +COQC tests/do.v [DEBUG] _ Debug: 1.1: (*external*) mrun (@M.bind _ _ f (fun eres => @M.ret _ (@M.Build_runner _ f eres))) on @@ -1327,12 +1373,8 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit)))) -> M unit : Type -[OK] tests/decompose.v -COQC tests/destruct_eq.v = tt : unit -[OK] tests/dependent_let_goals.v -COQC tests/do.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for dummy without backtracking @@ -1341,38 +1383,40 @@ Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) +[OK] tests/dependent_let_goals.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) +COQC tests/dummylang.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) [OK] tests/declare.v -COQC tests/dummylang.v +COQC tests/exceptions.v +File "./tests/destruct_eq.v", line 4, characters 34-41: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/destruct_eq.v", line 7, characters 18-25: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] If ffalse or nil then ;; else If ttrue then ;; else ;; end end : st +[DEBUG] tt +Pum + : Exception +[DEBUG] nat +[OK] tests/do.v File "./tests/dummylang.v", line 69, characters 0-70: Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] +COQC tests/goal_reordering.v File "./tests/dummylang.v", line 75, characters 2-21: Warning: "intros until 0" is deprecated, use "intros *"; instead of "induction 0" and "destruct 0" use explicitly a name." [deprecated-intros-until-0,tactics] -[DEBUG] tt -Pum - : Exception -[DEBUG] nat -File "./tests/destruct_eq.v", line 4, characters 34-41: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/destruct_eq.v", line 7, characters 18-25: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -[OK] tests/do.v -COQC tests/exceptions.v File "./tests/destruct_eq.v", line 12, characters 39-46: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -1380,40 +1424,40 @@ Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] [OK] tests/destruct_eq.v -COQC tests/goal_reordering.v -[OK] tests/exceptions.v COQC tests/hugo.v -[OK] tests/goal_reordering.v +[OK] tests/exceptions.v COQC tests/initialization.v +[OK] tests/goal_reordering.v +COQC tests/intropatt.v File "./tests/hugo.v", line 19, characters 11-20: Warning: Notation Lt.lt_n_S is deprecated since 8.16. The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/initialization.v -COQC tests/intropatt.v [OK] tests/hugo.v COQC tests/kind_of_term.v -[OK] tests/kind_of_term.v +[OK] tests/initialization.v COQC tests/lift.v -[OK] tests/dummylang.v -COQC tests/ltac.v -File "./tests/ltac.v", line 7, characters 0-32: -Warning: The Ltac name induction may be unusable because of a conflict with a -notation. [unusable-identifier,parsing] [DEBUG] hola [OK] tests/lift.v +COQC tests/ltac.v +[OK] tests/kind_of_term.v COQC tests/ltac_rewrite.v -File "./tests/ltac.v", line 60, characters 0-32: -Warning: The Ltac name injection may be unusable because of a conflict with a -notation. [unusable-identifier,parsing] -[OK] tests/ltac.v +[OK] tests/dummylang.v COQC tests/match_goal_context.v +File "./tests/ltac.v", line 7, characters 0-32: +Warning: The Ltac name induction may be unusable because of a conflict with a +notation. [unusable-identifier,parsing] [OK] tests/intropatt.v COQC tests/mctacticstests.v [OK] tests/ltac_rewrite.v COQC tests/min_bug_univpoly.v -[OK] tests/match_goal_context.v +File "./tests/ltac.v", line 60, characters 0-32: +Warning: The Ltac name injection may be unusable because of a conflict with a +notation. [unusable-identifier,parsing] +[OK] tests/ltac.v COQC tests/min_bug_univpoly2.v +[OK] tests/match_goal_context.v +COQC tests/mode.v File "./tests/min_bug_univpoly.v", line 27, characters 0-118: Warning: Notation "_ = _ :> _" was already used in scope type_scope. [notation-overridden,parsing] @@ -1430,7 +1474,7 @@ Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing] [OK] tests/min_bug_univpoly2.v -COQC tests/mode.v +COQC tests/mono_list_issue.v File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing] @@ -1443,38 +1487,51 @@ File "./tests/min_bug_univpoly.v", line 234, characters 0-66: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing] -[OK] tests/min_bug_univpoly.v -COQC tests/mono_list_issue.v File "./tests/mono_list_issue.v", line 3, characters 0-29: Warning: Use of “Require” inside a module is fragile. It is not recommended to use this functionality in finished proof scripts. [require-in-module,fragile] -[OK] tests/mode.v +[OK] tests/min_bug_univpoly.v COQC tests/mrun.v File "./tests/mono_list_issue.v", line 26, characters 0-67: Warning: Notation "_ :: _" was already used in scope list_scope. [notation-overridden,parsing] +[OK] tests/mode.v File "./tests/mono_list_issue.v", line 39, characters 0-66: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing] -[OK] tests/mono_list_issue.v COQC tests/names.v -[OK] tests/names.v +[OK] tests/mono_list_issue.v COQC tests/nu_let.v -[OK] tests/mrun.v +[OK] tests/nu_let.v COQC tests/pretype.v +[OK] tests/names.v +COQC tests/reduction.v +[OK] tests/mrun.v +COQC tests/reif_jason.v +[OK] tests/pretype.v +COQC tests/removetest.v +is_not_breaking_letins = id I + : True +Finished transaction in 1.218 secs (0.37u,0.072s) (successful) +Finished transaction in 0.042 secs (0.042u,0.s) (successful) [DEBUG] b [DEBUG] nat +[OK] tests/reduction.v +COQC tests/replace.v [DEBUG] b [DEBUG] nat [DEBUG] b -[OK] tests/nu_let.v [DEBUG] nat -COQC tests/reduction.v -[OK] tests/pretype.v -COQC tests/reif_jason.v -is_not_breaking_letins = id I - : True +File "./tests/reif_jason.v", line 596, characters 2-322: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +[OK] tests/reif_jason.v +COQC tests/rew_hd_error.v +(fun H : if true then True else False => H) +[OK] tests/replace.v +COQC tests/selectors.v +[OK] tests/removetest.v +COQC tests/ssrpattern.v File "./tests/mctacticstests.v", line 271, characters 8-17: Warning: Notation Gt.gt_n_S is deprecated since 8.16. The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. @@ -1483,7 +1540,12 @@ Warning: Notation Gt.gt_n_S is deprecated since 8.16. The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. [deprecated-syntactic-definition,deprecated] -Finished transaction in 1.668 secs (0.586u,0.055s) (successful) +[OK] tests/rew_hd_error.v +COQC tests/tactics.v +[DEBUG] (fun n : nat => n + n = S (S (S n))) +[DEBUG] (fun n : nat => ?n + n = S (S (S n))) +[OK] tests/ssrpattern.v +COQC tests/test_bind.v (fun (x : nat) (z : bool) (y : nat) => match reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) @@ -1523,51 +1585,39 @@ end z end y end x) -File "./tests/reif_jason.v", line 596, characters 2-322: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -Finished transaction in 0.122 secs (0.061u,0.s) (successful) -[OK] tests/reif_jason.v -COQC tests/removetest.v -[OK] tests/reduction.v -COQC tests/replace.v -(fun H : if true then True else False => H) -[OK] tests/replace.v -COQC tests/rew_hd_error.v -[OK] tests/mctacticstests.v -COQC tests/selectors.v -[OK] tests/removetest.v -COQC tests/ssrpattern.v -[OK] tests/rew_hd_error.v -COQC tests/tactics.v [OK] tests/selectors.v -COQC tests/test_bind.v -[DEBUG] (fun n : nat => n + n = S (S (S n))) -[DEBUG] (fun n : nat => ?n + n = S (S (S n))) -[OK] tests/ssrpattern.v COQC tests/test_brackets.v [OK] tests/test_bind.v COQC tests/test_get_name.v -[OK] tests/test_get_name.v +[OK] tests/mctacticstests.v COQC tests/test_get_reference.v -[OK] tests/test_brackets.v +[OK] tests/test_get_name.v COQC tests/test_goal_match.v [OK] tests/test_get_reference.v COQC tests/test_mmatch.v -[OK] tests/test_goal_match.v +[OK] tests/test_brackets.v COQC tests/test_mtry.v -Finished transaction in 0.474 secs (0.21u,0.014s) (successful) [OK] tests/test_mtry.v COQC tests/test_munify.v -[OK] tests/tactics.v +[OK] tests/test_goal_match.v COQC tests/test_ret.v -[OK] tests/test_mmatch.v +Finished transaction in 0.825 secs (0.229u,0.021s) (successful) +[OK] tests/tactics.v COQC tests/test_unfold_in.v [OK] tests/test_munify.v COQC tests/timers.v [OK] tests/test_ret.v COQC tests/trace.v -[OK] tests/test_unfold_in.v +[OK] tests/test_mmatch.v COQC tests/ttactics.v +[OK] tests/test_unfold_in.v +COQC tests/typeclass.v +0.206000 +0.206000 +0.367000 +0.000000 +[OK] tests/timers.v +COQC tests/typed_term_decomposition.v [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -1580,51 +1630,53 @@ [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) [OK] tests/trace.v -COQC tests/typeclass.v -0.148000 -0.148000 -0.292000 -0.000000 -[OK] tests/timers.v -COQC tests/typed_term_decomposition.v -[OK] tests/typeclass.v COQC tests/unification.v [OK] tests/ttactics.v COQC tests/bugs/bug117.v +[OK] tests/typeclass.v +COQC tests/bugs/bug225.v (3, 5) : nat * nat 5 : nat (True, False) : Prop * Prop +[OK] tests/unification.v +COQC tests/bugs/bug288.v [DEBUG] (3, 5) [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [OK] tests/typed_term_decomposition.v -COQC tests/bugs/bug225.v -[OK] tests/unification.v -COQC tests/bugs/bug288.v -[OK] tests/bugs/bug117.v COQC tests/bugs/bug295.v [OK] tests/bugs/bug225.v COQC tests/bugs/bug297.v -[OK] tests/bugs/bug288.v +[OK] tests/bugs/bug117.v COQC tests/bugs/bug299.v -[OK] tests/bugs/bug295.v -[OK] tests/bugs/bug297.v +[OK] tests/bugs/bug288.v COQC tests/bugs/bug302.v +[OK] tests/bugs/bug295.v COQC tests/bugs/bug304.v +[OK] tests/bugs/bug297.v +COQC examples/basics_tutorial.v [DEBUG] All good, a was instantiated with b's type (tFalse) [OK] tests/bugs/bug299.v -COQC examples/basics_tutorial.v -[DEBUG] All good -[OK] tests/bugs/bug304.v COQC examples/tactics.v +[DEBUG] All good [DEBUG] all good -[OK] tests/bugs/bug302.v +[OK] tests/bugs/bug304.v COQC examples/tauto.v +[OK] tests/bugs/bug302.v +cd tests/sf-5; ./configure.sh; make clean; make +Warning: No common logical root. +Warning: In this case the -docroot option should be given. +Warning: Otherwise the install-doc target is going to install files +Warning: in orphan_lf_Mtac2 +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +CLEAN +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +COQDEP VFILES File "./examples/basics_tutorial.v", line 55, characters 22-29: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -1635,6 +1687,7 @@ File "./examples/basics_tutorial.v", line 97, characters 0-47: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. empty_string = "" : string world_string = "world" @@ -1655,6 +1708,7 @@ : forall x y z : nat, In y (z :: y :: x :: nil) Arguments y_in_zyx (x y z)%nat_scope +COQC lf/Preface.v inlist' = fun (A : Type) (x : A) => mfix1 f s : list A : M In x s := @@ -1791,6 +1845,7 @@ : forall x y z : nat, In x ((y :: z :: nil) ++ x :: z :: nil) Arguments ex_inlist'' (x y z)%nat_scope +COQC lf/Basics.v ex1 = conj I (or_intror I) : True /\ (False \/ True) nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B @@ -1830,23 +1885,7 @@ The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition,deprecated] [OK] examples/basics_tutorial.v -cd tests/sf-5; ./configure.sh; make clean; make -Warning: No common logical root. -Warning: In this case the -docroot option should be given. -Warning: Otherwise the install-doc target is going to install files -Warning: in orphan_lf_Mtac2 -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -CLEAN -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. [OK] examples/tauto.v -COQDEP VFILES -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQC lf/Preface.v -COQC lf/Basics.v -File "./examples/tactics.v", line 208, characters 0-55: -Warning: This notation contains Ltac expressions: it will not be used for -printing. [non-reversible-notation,parsing] -[OK] examples/tactics.v File "./lf/Basics.v", line 15, characters 0-38: Warning: There is no flag or option with this name: "Global Default Proof Using". [unknown-option,option] @@ -1874,6 +1913,10 @@ : nat 0 + 1 + 1 : nat +File "./examples/tactics.v", line 208, characters 0-55: +Warning: This notation contains Ltac expressions: it will not be used for +printing. [non-reversible-notation,parsing] +[OK] examples/tactics.v COQC lf/Induction.v leb : nat -> nat -> bool @@ -1950,33 +1993,40 @@ (_ : forall x : X, @eq Y (f x) (g x)), @eq (forall _ : X, Y) f g make[1]: Leaving directory '/build/coq-mtac2-1.4+8.16' dh_auto_test - make -j3 test + make -j4 test make[1]: Entering directory '/build/coq-mtac2-1.4+8.16' COQC tests/ConstrSelector.v COQC tests/DepDestruct.v COQC tests/Exhaustive.v +COQC tests/UnivSanityCheck.v +Universes written to file "universes-mtac2.txt". = 0 : nat = 1 : nat = let (eval) := ?runner in eval : nat - = let (eval) := ?runner in eval - : nat - = let (eval) := ?runner in eval - : nat mmatch 1 (let ps' := with [# ] S | _ : nat =n> M.print "S"| [# ] 0 | =n> M.print "O"| _ => M.print "not in constructor normal form" end in ps') : idmatcher_return M_InDepMatcher +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] + = let (eval) := ?runner in eval + : nat + = let (eval) := ?runner in eval + : nat +0 + = Z0 + : Z mmatch 1 (let ps' := with [# ] 0 | =n> M.print "O"| [# ] S | _ : nat =n> M.print "S"| _ => M.print "not in constructor normal form" end in ps') : idmatcher_return M_InDepMatcher +[DEBUG] Running test mmatch 1 (let ps' := with _ => M.print "always triggered first"| [# ] 0 | =n> @@ -1984,6 +2034,8 @@ [# ] S | _ : nat =n> M.print "S, never triggered" end in ps') : idmatcher_return M_InDepMatcher +[OK] tests/UnivSanityCheck.v +COQC tests/abs.v mmatch (1 :: nil)%list (let ps' := with [# ] nil | =n> M.print "nil"| [# ] cons | @@ -2001,13 +2053,15 @@ ps') : idmatcher_return M_InDepMatcher [OK] tests/Exhaustive.v -COQC tests/UnivSanityCheck.v +COQC tests/abs_prod.v File "./tests/ConstrSelector.v", line 47, characters 22-29: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] File "./tests/ConstrSelector.v", line 85, characters 19-26: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] +[OK] tests/abs.v +COQC tests/binders.v [DEBUG] {| case_ind := nat; case_val := 3; @@ -2015,27 +2069,17 @@ case_branches := [m: Dyn true | Dyn (fun _ : nat => false)] |} -Universes written to file "universes-mtac2.txt". -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] -0 - = Z0 - : Z -[DEBUG] Running test -[OK] tests/UnivSanityCheck.v -COQC tests/abs.v -[OK] tests/ConstrSelector.v -COQC tests/abs_prod.v -[OK] tests/DepDestruct.v -COQC tests/binders.v -[OK] tests/abs.v -COQC tests/bug_universes.v [DEBUG] (nat -> (fun T : Type => T) Type) [OK] tests/abs_prod.v +COQC tests/bug_universes.v +[OK] tests/ConstrSelector.v COQC tests/bugs.v +[OK] tests/DepDestruct.v [DEBUG] (NameExistsInContext (TheName "x")) +COQC tests/cevar.v [DEBUG] (VarAppearsInValue z) [OK] tests/binders.v -COQC tests/cevar.v +COQC tests/comptactics.v testMmatch@{i j} = fun x : Type@{i} => x : Type@{i} -> Type@{max(i,j)} @@ -2062,16 +2106,21 @@ testexact is opaque Expands to: Constant Mtac2Tests.bug_universes.testexact [OK] tests/bug_universes.v -COQC tests/comptactics.v +COQC tests/debug_ex.v [DEBUG] true [DEBUG] (Metavar Propₛ (1 = 1) ?e) [OK] tests/bugs.v -COQC tests/debug_ex.v +COQC tests/decapp.v [OK] tests/cevar.v +COQC tests/declare.v +[DEBUG] raise ?e +Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. +[DEBUG] (StuckTerm ?t) +[OK] tests/debug_ex.v +COQC tests/decompose.v File "./tests/comptactics.v", line 32, characters 28-35: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] -COQC tests/decapp.v File "./tests/comptactics.v", line 34, characters 13-20: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] @@ -2099,16 +2148,7 @@ File "./tests/comptactics.v", line 77, characters 15-22: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/comptactics.v -COQC tests/declare.v -[DEBUG] raise ?e -Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. -[DEBUG] (StuckTerm ?t) -[OK] tests/debug_ex.v -COQC tests/decompose.v [DEBUG] (Specif.msigT (MTele.MTele_Const nat)) -[OK] tests/decapp.v -COQC tests/dependent_let_goals.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -2145,8 +2185,10 @@ : unit = tt : unit +[OK] tests/decapp.v = tt : unit +COQC tests/dependent_let_goals.v = tt : unit = tt @@ -2159,10 +2201,12 @@ : nat NAT3 = 3 : nat +[OK] tests/comptactics.v NAT3: nat NAT2: nat NAT1: nat NAT0: nat +COQC tests/destruct_eq.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for (@M.runner unit ev) without backtracking @@ -2277,8 +2321,6 @@ : M unit = tt : unit -[OK] tests/decompose.v -COQC tests/destruct_eq.v = (MTele_val (curry_sort Typeₛ (fun a' : ArgsOf [tele (_ : Type) (_ : nat) ] => @@ -2303,6 +2345,8 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit))) -> M unit : Type +[OK] tests/decompose.v +COQC tests/do.v = M.declare_mind [tele (_ : Type) (_ : nat) ] [m:(m:"blubb__"; fun (_ : Type) (k : nat) => @@ -2420,8 +2464,6 @@ mexistT (MTele_ConstT S.Sort) [tele ] Propₛ) a))) mt_constr}) *m unit)))) -> M unit : Type -[OK] tests/dependent_let_goals.v -COQC tests/do.v = tt : unit = (MTele_val @@ -2486,8 +2528,16 @@ Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) -[OK] tests/declare.v +[OK] tests/dependent_let_goals.v COQC tests/dummylang.v +[OK] tests/declare.v +COQC tests/exceptions.v +File "./tests/destruct_eq.v", line 4, characters 34-41: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/destruct_eq.v", line 7, characters 18-25: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] If ffalse or nil then ;; else If ttrue then ;; else ;; end end : st File "./tests/dummylang.v", line 69, characters 0-70: @@ -2498,39 +2548,31 @@ Warning: "intros until 0" is deprecated, use "intros *"; instead of "induction 0" and "destruct 0" use explicitly a name." [deprecated-intros-until-0,tactics] -[DEBUG] tt -Pum - : Exception -[DEBUG] nat -[OK] tests/do.v -COQC tests/exceptions.v -File "./tests/destruct_eq.v", line 4, characters 34-41: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/destruct_eq.v", line 7, characters 18-25: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] File "./tests/destruct_eq.v", line 12, characters 39-46: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] File "./tests/destruct_eq.v", line 15, characters 18-25: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/destruct_eq.v +[DEBUG] tt +Pum + : Exception +[DEBUG] nat +[OK] tests/do.v COQC tests/goal_reordering.v -[OK] tests/exceptions.v +[OK] tests/destruct_eq.v COQC tests/hugo.v -[OK] tests/goal_reordering.v +[OK] tests/exceptions.v COQC tests/initialization.v +[OK] tests/goal_reordering.v +COQC tests/intropatt.v File "./tests/hugo.v", line 19, characters 11-20: Warning: Notation Lt.lt_n_S is deprecated since 8.16. The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. [deprecated-syntactic-definition,deprecated] [OK] tests/hugo.v -COQC tests/intropatt.v -[OK] tests/initialization.v COQC tests/kind_of_term.v -[OK] tests/dummylang.v +[OK] tests/initialization.v COQC tests/lift.v [OK] tests/kind_of_term.v COQC tests/ltac.v @@ -2540,17 +2582,25 @@ File "./tests/ltac.v", line 7, characters 0-32: Warning: The Ltac name induction may be unusable because of a conflict with a notation. [unusable-identifier,parsing] -[OK] tests/ltac_rewrite.v +[OK] tests/dummylang.v +COQC tests/match_goal_context.v File "./tests/ltac.v", line 60, characters 0-32: Warning: The Ltac name injection may be unusable because of a conflict with a notation. [unusable-identifier,parsing] -COQC tests/match_goal_context.v [OK] tests/intropatt.v COQC tests/mctacticstests.v [OK] tests/ltac.v COQC tests/min_bug_univpoly.v -[OK] tests/match_goal_context.v +[OK] tests/ltac_rewrite.v COQC tests/min_bug_univpoly2.v +[OK] tests/min_bug_univpoly2.v +COQC tests/mode.v +[OK] tests/match_goal_context.v +COQC tests/mono_list_issue.v +File "./tests/mono_list_issue.v", line 3, characters 0-29: +Warning: Use of “Require” inside a module is fragile. It is not recommended +to use this functionality in finished proof scripts. +[require-in-module,fragile] File "./tests/min_bug_univpoly.v", line 27, characters 0-118: Warning: Notation "_ = _ :> _" was already used in scope type_scope. [notation-overridden,parsing] @@ -2566,8 +2616,12 @@ File "./tests/min_bug_univpoly.v", line 34, characters 0-47: Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing] -[OK] tests/min_bug_univpoly2.v -COQC tests/mode.v +File "./tests/mono_list_issue.v", line 26, characters 0-67: +Warning: Notation "_ :: _" was already used in scope list_scope. +[notation-overridden,parsing] +File "./tests/mono_list_issue.v", line 39, characters 0-66: +Warning: Notation "_ ++ _" was already used in scope list_scope. +[notation-overridden,parsing] File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing] @@ -2577,41 +2631,41 @@ File "./tests/min_bug_univpoly.v", line 216, characters 0-67: Warning: Notation "_ :: _" was already used in scope list_scope. [notation-overridden,parsing] +[OK] tests/mono_list_issue.v File "./tests/min_bug_univpoly.v", line 234, characters 0-66: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing] -[OK] tests/min_bug_univpoly.v -COQC tests/mono_list_issue.v -File "./tests/mono_list_issue.v", line 3, characters 0-29: -Warning: Use of “Require” inside a module is fragile. It is not recommended -to use this functionality in finished proof scripts. -[require-in-module,fragile] -[OK] tests/mode.v COQC tests/mrun.v -File "./tests/mono_list_issue.v", line 26, characters 0-67: -Warning: Notation "_ :: _" was already used in scope list_scope. -[notation-overridden,parsing] -File "./tests/mono_list_issue.v", line 39, characters 0-66: -Warning: Notation "_ ++ _" was already used in scope list_scope. -[notation-overridden,parsing] -[OK] tests/mono_list_issue.v +[OK] tests/mode.v COQC tests/names.v -[OK] tests/mrun.v +[OK] tests/min_bug_univpoly.v COQC tests/nu_let.v [OK] tests/names.v COQC tests/pretype.v +[OK] tests/mrun.v +COQC tests/reduction.v +[OK] tests/nu_let.v +COQC tests/reif_jason.v +[OK] tests/pretype.v +COQC tests/removetest.v +is_not_breaking_letins = id I + : True [DEBUG] b [DEBUG] nat [DEBUG] b [DEBUG] nat [DEBUG] b [DEBUG] nat -[OK] tests/pretype.v -COQC tests/reduction.v -[OK] tests/nu_let.v -COQC tests/reif_jason.v -is_not_breaking_letins = id I - : True +Finished transaction in 1.453 secs (0.373u,0.075s) (successful) +File "./tests/reif_jason.v", line 596, characters 2-322: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +Finished transaction in 0.147 secs (0.043u,0.s) (successful) +[OK] tests/reduction.v +COQC tests/replace.v +[OK] tests/reif_jason.v +COQC tests/rew_hd_error.v +[OK] tests/removetest.v +COQC tests/selectors.v File "./tests/mctacticstests.v", line 271, characters 8-17: Warning: Notation Gt.gt_n_S is deprecated since 8.16. The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. @@ -2620,12 +2674,11 @@ Warning: Notation Gt.gt_n_S is deprecated since 8.16. The Arith.Gt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead. [deprecated-syntactic-definition,deprecated] -Finished transaction in 0.772 secs (0.578u,0.055s) (successful) -File "./tests/reif_jason.v", line 596, characters 2-322: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -Finished transaction in 0.117 secs (0.068u,0.s) (successful) -[OK] tests/reif_jason.v -COQC tests/removetest.v +(fun H : if true then True else False => H) +[OK] tests/replace.v +COQC tests/ssrpattern.v +[OK] tests/rew_hd_error.v +COQC tests/tactics.v (fun (x : nat) (z : bool) (y : nat) => match reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) @@ -2665,46 +2718,43 @@ end z end y end x) -[OK] tests/reduction.v -COQC tests/replace.v -(fun H : if true then True else False => H) -[OK] tests/replace.v -COQC tests/rew_hd_error.v -[OK] tests/mctacticstests.v -COQC tests/selectors.v -[OK] tests/removetest.v -[OK] tests/rew_hd_error.v -COQC tests/ssrpattern.v -COQC tests/tactics.v [OK] tests/selectors.v COQC tests/test_bind.v [DEBUG] (fun n : nat => n + n = S (S (S n))) [DEBUG] (fun n : nat => ?n + n = S (S (S n))) [OK] tests/ssrpattern.v COQC tests/test_brackets.v -[OK] tests/test_bind.v +[OK] tests/mctacticstests.v COQC tests/test_get_name.v -[OK] tests/test_brackets.v +[OK] tests/test_bind.v COQC tests/test_get_reference.v [OK] tests/test_get_name.v COQC tests/test_goal_match.v -[OK] tests/test_get_reference.v +[OK] tests/test_brackets.v COQC tests/test_mmatch.v -[OK] tests/tactics.v +[OK] tests/test_get_reference.v COQC tests/test_mtry.v -[OK] tests/test_goal_match.v -COQC tests/test_munify.v [OK] tests/test_mtry.v +COQC tests/test_munify.v +Finished transaction in 0.823 secs (0.211u,0.039s) (successful) +[OK] tests/test_goal_match.v +[OK] tests/tactics.v COQC tests/test_ret.v -Finished transaction in 0.298 secs (0.237u,0.007s) (successful) -[OK] tests/test_munify.v COQC tests/test_unfold_in.v -[OK] tests/test_ret.v +[OK] tests/test_munify.v COQC tests/timers.v -[OK] tests/test_unfold_in.v -COQC tests/trace.v [OK] tests/test_mmatch.v +COQC tests/trace.v +[OK] tests/test_ret.v COQC tests/ttactics.v +[OK] tests/test_unfold_in.v +COQC tests/typeclass.v +0.198000 +0.198000 +0.392000 +0.000000 +[OK] tests/timers.v +COQC tests/typed_term_decomposition.v [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -2717,19 +2767,13 @@ [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) [OK] tests/trace.v -COQC tests/typeclass.v -0.079000 -0.079000 -0.152000 -0.000000 -[OK] tests/timers.v -COQC tests/typed_term_decomposition.v -[OK] tests/ttactics.v COQC tests/unification.v [OK] tests/typeclass.v COQC tests/bugs/bug117.v +[OK] tests/ttactics.v (3, 5) : nat * nat +COQC tests/bugs/bug225.v 5 : nat (True, False) @@ -2740,23 +2784,25 @@ [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [OK] tests/typed_term_decomposition.v -COQC tests/bugs/bug225.v -[OK] tests/bugs/bug117.v COQC tests/bugs/bug288.v [OK] tests/unification.v COQC tests/bugs/bug295.v -[OK] tests/bugs/bug225.v -[OK] tests/bugs/bug288.v +[OK] tests/bugs/bug117.v COQC tests/bugs/bug297.v +[OK] tests/bugs/bug225.v COQC tests/bugs/bug299.v -[OK] tests/bugs/bug295.v +[OK] tests/bugs/bug288.v COQC tests/bugs/bug302.v +[OK] tests/bugs/bug297.v +COQC tests/bugs/bug304.v +[OK] tests/bugs/bug295.v +COQC examples/basics_tutorial.v [DEBUG] All good, a was instantiated with b's type (tFalse) [OK] tests/bugs/bug299.v -COQC tests/bugs/bug304.v +COQC examples/tactics.v [DEBUG] all good -[OK] tests/bugs/bug297.v -COQC examples/basics_tutorial.v +[OK] tests/bugs/bug302.v +COQC examples/tauto.v [DEBUG] All good File "./examples/basics_tutorial.v", line 55, characters 22-29: Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. @@ -2768,12 +2814,20 @@ File "./examples/basics_tutorial.v", line 97, characters 0-47: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] +[OK] tests/bugs/bug304.v +cd tests/sf-5; ./configure.sh; make clean; make +Warning: No common logical root. +Warning: In this case the -docroot option should be given. +Warning: Otherwise the install-doc target is going to install files +Warning: in orphan_lf_Mtac2 empty_string = "" : string world_string = "world" : string other_string = "other" : string +make[2]: Entering directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. File "./examples/basics_tutorial.v", line 207, characters 11-15: Warning: Notation div2 is deprecated since 8.16. The Arith.Div2 file is obsolete. Use Nat.div2 instead. @@ -2847,8 +2901,6 @@ : forall (A : Type) (x : A) (l r : list A), In x r -> In x (l ++ r) Arguments inlist'_obligation_2 [A]%type_scope x (l r)%list_scope ir -[OK] tests/bugs/bug302.v -COQC examples/tactics.v ex_inlist = fun x y z : nat => in_cons y x @@ -2866,6 +2918,7 @@ : forall x y z : nat, In x ((y :: z :: nil) ++ x :: z :: nil) Arguments ex_inlist (x y z)%nat_scope +CLEAN ex_inlist' = fun x y z : nat => (fun (A : Type) (x0 : A) (_ : forall x1 : list A, M (In x0 x1)) @@ -2928,8 +2981,10 @@ Arguments ex_inlist'' (x y z)%nat_scope ex1 = conj I (or_intror I) : True /\ (False \/ True) -[OK] tests/bugs/bug304.v -COQC examples/tauto.v +make[2]: Leaving directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' +make[2]: Entering directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +COQDEP VFILES nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B nu is universe polymorphic @@ -2941,6 +2996,7 @@ : forall p q : Prop, p -> q -> p /\ q Arguments ex_with_implication [p q]%type_scope _ _ +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. File "./examples/basics_tutorial.v", line 673, characters 8-20: Warning: Notation beq_nat_refl is deprecated since 8.16. Use Nat.eqb_refl (with symmetry of equality) instead. @@ -2966,27 +3022,10 @@ Warning: Notation plus_comm is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition,deprecated] -[OK] examples/basics_tutorial.v -cd tests/sf-5; ./configure.sh; make clean; make -Warning: No common logical root. -Warning: In this case the -docroot option should be given. -Warning: Otherwise the install-doc target is going to install files -Warning: in orphan_lf_Mtac2 -make[2]: Entering directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -CLEAN -File "./examples/tactics.v", line 208, characters 0-55: -Warning: This notation contains Ltac expressions: it will not be used for -printing. [non-reversible-notation,parsing] -[OK] examples/tactics.v -make[2]: Leaving directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' -make[2]: Entering directory '/build/coq-mtac2-1.4+8.16/tests/sf-5' -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQDEP VFILES -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. COQC lf/Preface.v -[OK] examples/tauto.v +[OK] examples/basics_tutorial.v COQC lf/Basics.v +[OK] examples/tauto.v File "./lf/Basics.v", line 15, characters 0-38: Warning: There is no flag or option with this name: "Global Default Proof Using". [unknown-option,option] @@ -3014,6 +3053,10 @@ : nat 0 + 1 + 1 : nat +File "./examples/tactics.v", line 208, characters 0-55: +Warning: This notation contains Ltac expressions: it will not be used for +printing. [non-reversible-notation,parsing] +[OK] examples/tactics.v COQC lf/Induction.v leb : nat -> nat -> bool @@ -3257,12 +3300,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/12848/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/12848/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/12391 and its subdirectories -I: Current time: Mon May 29 19:11:00 -12 2023 -I: pbuilder-time-stamp: 1685430660 +I: removing directory /srv/workspace/pbuilder/12848 and its subdirectories +I: Current time: Tue May 30 21:22:53 +14 2023 +I: pbuilder-time-stamp: 1685431373