Diff of the two buildlogs: -- --- b1/build.log 2023-05-22 11:34:24.614863657 +0000 +++ b2/build.log 2023-05-22 11:37:06.395825907 +0000 @@ -1,6 +1,7 @@ +W: cgroups are not available on the host, not using them. I: pbuilder: network access will be disabled during build -I: Current time: Sun Jun 23 05:56:12 -12 2024 -I: pbuilder-time-stamp: 1719165372 +I: Current time: Tue May 23 01:34:26 +14 2023 +I: pbuilder-time-stamp: 1684755266 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -17,7 +18,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 @@ -29,137 +30,168 @@ 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/10942/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/25363/tmp/hooks/D01_modify_environment starting +debug: Running on ionos12-i386. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 May 23 01:34 /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/25363/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/25363/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='i386' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=16 ' - DISTRIBUTION='bookworm' - HOME='/root' - HOST_ARCH='i386' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="15" [3]="1" [4]="release" [5]="i686-pc-linux-gnu") + BASH_VERSION='5.2.15(1)-release' + BUILDDIR=/build + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=i386 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=7 ' + DIRSTACK=() + DISTRIBUTION=bookworm + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=i686 + HOST_ARCH=i386 IFS=' ' - INVOCATION_ID='69c1dd8f71d345c7910365e354f03d6a' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - LD_LIBRARY_PATH='/usr/lib/libeatmydata' - LD_PRELOAD='libeatmydata.so' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='10942' - PS1='# ' - PS2='> ' + LANG=C + LANGUAGE=de_CH:de + LC_ALL=C + LD_LIBRARY_PATH=/usr/lib/libeatmydata + LD_PRELOAD=libeatmydata.so + MACHTYPE=i686-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=25363 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.KziOYEV7/pbuilderrc_Wco6 --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.KziOYEV7/b1 --logfile b1/build.log coq-mtac2_1.4+8.16-2.dsc' - SUDO_GID='112' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://85.184.249.68: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.KziOYEV7/pbuilderrc_agHH --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.KziOYEV7/b2 --logfile b2/build.log --extrapackages usrmerge coq-mtac2_1.4+8.16-2.dsc' + SUDO_GID=112 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://78.137.99.97:3128 I: uname -a - Linux ionos16-i386 5.10.0-23-amd64 #1 SMP Debian 5.10.179-1 (2023-05-12) x86_64 GNU/Linux + Linux i-capture-the-hostname 5.10.0-23-686-pae #1 SMP Debian 5.10.179-1 (2023-05-12) i686 GNU/Linux I: ls -l /bin total 6036 - -rwxr-xr-x 1 root root 1408088 Apr 23 2023 bash - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bunzip2 - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bzcat - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzcmp -> bzdiff - -rwxr-xr-x 1 root root 2225 Sep 18 2022 bzdiff - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzegrep -> bzgrep - -rwxr-xr-x 1 root root 4893 Nov 27 2021 bzexe - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzfgrep -> bzgrep - -rwxr-xr-x 1 root root 3775 Sep 18 2022 bzgrep - -rwxr-xr-x 3 root root 38404 Sep 18 2022 bzip2 - -rwxr-xr-x 1 root root 17892 Sep 18 2022 bzip2recover - lrwxrwxrwx 1 root root 6 Sep 18 2022 bzless -> bzmore - -rwxr-xr-x 1 root root 1297 Sep 18 2022 bzmore - -rwxr-xr-x 1 root root 42920 Sep 20 2022 cat - -rwxr-xr-x 1 root root 79816 Sep 20 2022 chgrp - -rwxr-xr-x 1 root root 67496 Sep 20 2022 chmod - -rwxr-xr-x 1 root root 79816 Sep 20 2022 chown - -rwxr-xr-x 1 root root 162024 Sep 20 2022 cp - -rwxr-xr-x 1 root root 136916 Jan 5 2023 dash - -rwxr-xr-x 1 root root 137160 Sep 20 2022 date - -rwxr-xr-x 1 root root 100364 Sep 20 2022 dd - -rwxr-xr-x 1 root root 108940 Sep 20 2022 df - -rwxr-xr-x 1 root root 162152 Sep 20 2022 dir - -rwxr-xr-x 1 root root 87760 Mar 22 2023 dmesg - lrwxrwxrwx 1 root root 8 Dec 19 2022 dnsdomainname -> hostname - lrwxrwxrwx 1 root root 8 Dec 19 2022 domainname -> hostname - -rwxr-xr-x 1 root root 38760 Sep 20 2022 echo - -rwxr-xr-x 1 root root 41 Jan 24 2023 egrep - -rwxr-xr-x 1 root root 34664 Sep 20 2022 false - -rwxr-xr-x 1 root root 41 Jan 24 2023 fgrep - -rwxr-xr-x 1 root root 84272 Mar 22 2023 findmnt - -rwsr-xr-x 1 root root 30240 Mar 22 2023 fusermount - -rwxr-xr-x 1 root root 218680 Jan 24 2023 grep - -rwxr-xr-x 2 root root 2346 Apr 9 2022 gunzip - -rwxr-xr-x 1 root root 6447 Apr 9 2022 gzexe - -rwxr-xr-x 1 root root 100952 Apr 9 2022 gzip - -rwxr-xr-x 1 root root 21916 Dec 19 2022 hostname - -rwxr-xr-x 1 root root 75756 Sep 20 2022 ln - -rwxr-xr-x 1 root root 55600 Mar 22 2023 login - -rwxr-xr-x 1 root root 162152 Sep 20 2022 ls - -rwxr-xr-x 1 root root 214568 Mar 22 2023 lsblk - -rwxr-xr-x 1 root root 96328 Sep 20 2022 mkdir - -rwxr-xr-x 1 root root 84008 Sep 20 2022 mknod - -rwxr-xr-x 1 root root 38792 Sep 20 2022 mktemp - -rwxr-xr-x 1 root root 63016 Mar 22 2023 more - -rwsr-xr-x 1 root root 58912 Mar 22 2023 mount - -rwxr-xr-x 1 root root 13856 Mar 22 2023 mountpoint - -rwxr-xr-x 1 root root 157932 Sep 20 2022 mv - lrwxrwxrwx 1 root root 8 Dec 19 2022 nisdomainname -> hostname - lrwxrwxrwx 1 root root 14 Apr 2 2023 pidof -> /sbin/killall5 - -rwxr-xr-x 1 root root 38792 Sep 20 2022 pwd - lrwxrwxrwx 1 root root 4 Apr 23 2023 rbash -> bash - -rwxr-xr-x 1 root root 51080 Sep 20 2022 readlink - -rwxr-xr-x 1 root root 75720 Sep 20 2022 rm - -rwxr-xr-x 1 root root 51080 Sep 20 2022 rmdir - -rwxr-xr-x 1 root root 22308 Nov 2 2022 run-parts - -rwxr-xr-x 1 root root 133224 Jan 5 2023 sed - lrwxrwxrwx 1 root root 4 Jan 5 2023 sh -> dash - -rwxr-xr-x 1 root root 38760 Sep 20 2022 sleep - -rwxr-xr-x 1 root root 87976 Sep 20 2022 stty - -rwsr-xr-x 1 root root 83492 Mar 22 2023 su - -rwxr-xr-x 1 root root 38792 Sep 20 2022 sync - -rwxr-xr-x 1 root root 598456 Apr 6 2023 tar - -rwxr-xr-x 1 root root 13860 Nov 2 2022 tempfile - -rwxr-xr-x 1 root root 120776 Sep 20 2022 touch - -rwxr-xr-x 1 root root 34664 Sep 20 2022 true - -rwxr-xr-x 1 root root 17892 Mar 22 2023 ulockmgr_server - -rwsr-xr-x 1 root root 30236 Mar 22 2023 umount - -rwxr-xr-x 1 root root 38760 Sep 20 2022 uname - -rwxr-xr-x 2 root root 2346 Apr 9 2022 uncompress - -rwxr-xr-x 1 root root 162152 Sep 20 2022 vdir - -rwxr-xr-x 1 root root 71216 Mar 22 2023 wdctl - lrwxrwxrwx 1 root root 8 Dec 19 2022 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/10942/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1408088 Apr 24 11:24 bash + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bunzip2 + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bzcat + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzcmp -> bzdiff + -rwxr-xr-x 1 root root 2225 Sep 19 2022 bzdiff + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzegrep -> bzgrep + -rwxr-xr-x 1 root root 4893 Nov 28 2021 bzexe + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzfgrep -> bzgrep + -rwxr-xr-x 1 root root 3775 Sep 19 2022 bzgrep + -rwxr-xr-x 3 root root 38404 Sep 19 2022 bzip2 + -rwxr-xr-x 1 root root 17892 Sep 19 2022 bzip2recover + lrwxrwxrwx 1 root root 6 Sep 19 2022 bzless -> bzmore + -rwxr-xr-x 1 root root 1297 Sep 19 2022 bzmore + -rwxr-xr-x 1 root root 42920 Sep 21 2022 cat + -rwxr-xr-x 1 root root 79816 Sep 21 2022 chgrp + -rwxr-xr-x 1 root root 67496 Sep 21 2022 chmod + -rwxr-xr-x 1 root root 79816 Sep 21 2022 chown + -rwxr-xr-x 1 root root 162024 Sep 21 2022 cp + -rwxr-xr-x 1 root root 136916 Jan 6 03:20 dash + -rwxr-xr-x 1 root root 137160 Sep 21 2022 date + -rwxr-xr-x 1 root root 100364 Sep 21 2022 dd + -rwxr-xr-x 1 root root 108940 Sep 21 2022 df + -rwxr-xr-x 1 root root 162152 Sep 21 2022 dir + -rwxr-xr-x 1 root root 87760 Mar 24 00:20 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 38760 Sep 21 2022 echo + -rwxr-xr-x 1 root root 41 Jan 25 04:43 egrep + -rwxr-xr-x 1 root root 34664 Sep 21 2022 false + -rwxr-xr-x 1 root root 41 Jan 25 04:43 fgrep + -rwxr-xr-x 1 root root 84272 Mar 24 00:20 findmnt + -rwsr-xr-x 1 root root 30240 Mar 23 22:38 fusermount + -rwxr-xr-x 1 root root 218680 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 100952 Apr 10 2022 gzip + -rwxr-xr-x 1 root root 21916 Dec 20 03:33 hostname + -rwxr-xr-x 1 root root 75756 Sep 21 2022 ln + -rwxr-xr-x 1 root root 55600 Mar 24 01:43 login + -rwxr-xr-x 1 root root 162152 Sep 21 2022 ls + -rwxr-xr-x 1 root root 214568 Mar 24 00:20 lsblk + -rwxr-xr-x 1 root root 96328 Sep 21 2022 mkdir + -rwxr-xr-x 1 root root 84008 Sep 21 2022 mknod + -rwxr-xr-x 1 root root 38792 Sep 21 2022 mktemp + -rwxr-xr-x 1 root root 63016 Mar 24 00:20 more + -rwsr-xr-x 1 root root 58912 Mar 24 00:20 mount + -rwxr-xr-x 1 root root 13856 Mar 24 00:20 mountpoint + -rwxr-xr-x 1 root root 157932 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 38792 Sep 21 2022 pwd + lrwxrwxrwx 1 root root 4 Apr 24 11:24 rbash -> bash + -rwxr-xr-x 1 root root 51080 Sep 21 2022 readlink + -rwxr-xr-x 1 root root 75720 Sep 21 2022 rm + -rwxr-xr-x 1 root root 51080 Sep 21 2022 rmdir + -rwxr-xr-x 1 root root 22308 Nov 3 2022 run-parts + -rwxr-xr-x 1 root root 133224 Jan 6 09:55 sed + lrwxrwxrwx 1 root root 9 May 23 01:34 sh -> /bin/bash + -rwxr-xr-x 1 root root 38760 Sep 21 2022 sleep + -rwxr-xr-x 1 root root 87976 Sep 21 2022 stty + -rwsr-xr-x 1 root root 83492 Mar 24 00:20 su + -rwxr-xr-x 1 root root 38792 Sep 21 2022 sync + -rwxr-xr-x 1 root root 598456 Apr 7 04:25 tar + -rwxr-xr-x 1 root root 13860 Nov 3 2022 tempfile + -rwxr-xr-x 1 root root 120776 Sep 21 2022 touch + -rwxr-xr-x 1 root root 34664 Sep 21 2022 true + -rwxr-xr-x 1 root root 17892 Mar 23 22:38 ulockmgr_server + -rwsr-xr-x 1 root root 30236 Mar 24 00:20 umount + -rwxr-xr-x 1 root root 38760 Sep 21 2022 uname + -rwxr-xr-x 2 root root 2346 Apr 10 2022 uncompress + -rwxr-xr-x 1 root root 162152 Sep 21 2022 vdir + -rwxr-xr-x 1 root root 71216 Mar 24 00:20 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/25363/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -272,7 +304,7 @@ Get: 61 http://deb.debian.org/debian bookworm/main i386 libzarith-ocaml-dev i386 1.12-1+b1 [93.1 kB] Get: 62 http://deb.debian.org/debian bookworm/main i386 libcoq-core-ocaml-dev i386 8.16.1+dfsg-1+b2 [42.4 MB] Get: 63 http://deb.debian.org/debian bookworm/main i386 libcoq-unicoq i386 1.6-8.16-2+b1 [72.8 kB] -Fetched 310 MB in 5s (61.1 MB/s) +Fetched 310 MB in 8s (39.2 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:i386. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19604 files and directories currently installed.) @@ -540,8 +572,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/25363/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/25363/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 @@ -568,7 +611,7 @@ Warning: in orphan_Mtac2Tests_Mtac2 make[1]: Leaving directory '/build/coq-mtac2-1.4+8.16' dh_auto_build - make -j16 "INSTALL=install --strip-program=true" + make -j7 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-mtac2-1.4+8.16' COQDEP VFILES COQPP src/metaCoqInit.mlg @@ -577,6 +620,7 @@ CAMLDEP src/run.mli 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 @@ -587,7 +631,6 @@ CAMLDEP src/constrs.ml CAMLDEP src/metaCoqTactic.ml CAMLDEP src/metaCoqInit.ml -*** Warning: in file theories/Base.v, declared ML module ././unicoq has not been found! COQC theories/lib/Logic.v COQC theories/lib/Datatypes.v COQC theories/intf/Sorts.v @@ -599,15 +642,14 @@ COQC theories/intf/Name.v COQC theories/intf/Dyn.v COQC theories/intf/DeclarationDefs.v +COQC theories/intf/Goals.v COQC theories/intf/Tm_kind.v -CAMLC -c src/metaCoqInterp.mli +COQC theories/lib/Specif.v +COQC theories/lib/List.v CAMLOPT -c -for-pack MetaCoqPlugin src/constrs.ml CAMLC -c src/mtacNames.mli -COQC theories/lib/List.v +CAMLC -c src/metaCoqInterp.mli COQC theories/intf/Reduction.v -COQC theories/lib/Specif.v -COQC theories/intf/Goals.v -CAMLOPT -c -for-pack MetaCoqPlugin src/mtacNames.ml File "./theories/lib/Specif.v", line 201, characters 0-144: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -621,26 +663,33 @@ Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] COQC theories/intf/MTele.v +CAMLOPT -c -for-pack MetaCoqPlugin src/mtacNames.ml COQC theories/lib/Utils.v COQC theories/intf/Case.v -CAMLOPT -c -for-pack MetaCoqPlugin src/mConstr.ml File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -File "src/mConstr.ml", line 158, characters 21-41: -158 | let isconstant n h = Names.Constant.equal (Lazy.force n) h - ^^^^^^^^^^^^^^^^^^^^ -Alert deprecated: Names.Constant.equal -Use QConstant.equal File "./theories/intf/MTele.v", line 1, characters 0-39: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] COQC theories/intf/Exceptions.v File "./theories/intf/MTele.v", line 151, characters 0-224: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +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 + ^^^^^^^^^^^^^^^^^^^^ +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] CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInterp.ml File "src/metaCoqInterp.ml", line 158, characters 4-12: 158 | nf_enter begin fun gl -> @@ -654,16 +703,10 @@ Normalization is enforced by EConstr, please use [enter] CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqInit.ml CAMLOPT -c -for-pack MetaCoqPlugin src/metaCoqTactic.ml -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 -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 @@ -673,6 +716,11 @@ COQC theories/tactics/TacticsBase.v 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/MTeleMatch.v File "./theories/meta/MFixDef.v", line 1, characters 0-44: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -682,18 +730,12 @@ 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] -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/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/MTeleMatch.v", line 2, characters 0-74: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] @@ -767,6 +809,7 @@ (fun _ : nat => mBase@{Mtac2.meta.MTeleMatch.352})) (fun _ : nat => nat)) COQC theories/meta/MFix.v +COQC theories/tactics/Tactics.v File "./theories/meta/MFix.v", line 86, characters 5-44: Warning: The format modifier is irrelevant for only-parsing rules. [irrelevant-format-only-parsing,parsing] @@ -793,14 +836,14 @@ File "./theories/DecomposeApp.v", line 111, characters 0-185: Warning: This notation contains Ltac expressions: it will not be used for printing. [non-reversible-notation,parsing] -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. -[require-in-module,fragile] COQC theories/tactics/IntroPatt.v COQC theories/tactics/CompoundTactics.v COQC theories/Mtac2.v COQC theories/ideas/DepDestruct.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. +[require-in-module,fragile] File "./theories/tactics/Ttactics.v", line 293, characters 0-20: Warning: This command is just asserting the names of arguments of gbase. If this is what you want, add ': assert' to silence the warning. If you want to @@ -808,16 +851,16 @@ notation scopes, add ': clear scopes' [arguments-assert,vernacular] COQC theories/tactics/ConstrSelector.v COQC theories/ideas/SumRun.v -File "./theories/ideas/SumRun.v", line 67, characters 0-80: -Warning: Notation "[run _ ]" was already used. [notation-overridden,parsing] File "./theories/ideas/DepDestruct.v", line 370, characters 0-32: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] File "./theories/ideas/DepDestruct.v", line 370, characters 0-32: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] +File "./theories/ideas/SumRun.v", line 67, characters 0-80: +Warning: Notation "[run _ ]" was already used. [notation-overridden,parsing] COQC theories/ideas/Transport.v -Finished transaction in 0.092 secs (0.092u,0.s) (successful) +Finished transaction in 0.171 secs (0.171u,0.s) (successful) COQC tests/ConstrSelector.v COQC tests/DepDestruct.v COQC tests/Exhaustive.v @@ -825,54 +868,166 @@ COQC tests/abs.v COQC tests/abs_prod.v COQC tests/binders.v +[DEBUG] (NameExistsInContext (TheName "x")) +[DEBUG] (VarAppearsInValue z) +[OK] tests/abs.v COQC tests/bug_universes.v +[OK] tests/binders.v +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 COQC tests/bugs.v +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 +mmatch 1 +(let ps' := + with _ => M.print "always triggered first"| [# ] 0 | =n> + M.print "O, never triggered"| + [# ] S | _ : nat =n> M.print "S, never triggered" end in + ps') + : idmatcher_return M_InDepMatcher +mmatch (1 :: nil)%list +(let ps' := + with [# ] nil | =n> M.print "nil"| [# ] cons | + (_ : nat) (_ : list nat) =n> + M.print "cons"| + _ => M.print "not in constructor normal form" end in + ps') + : idmatcher_return M_InDepMatcher + = 0 + : nat + = 1 + : nat +mmatch (1 :: nil)%list +(let ps' := + with [# ] nil | =n> M.print "nil"| [# ] cons | + (_ : nat) (_ : list nat) =n> + M.print "cons"| + _ => 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 +[OK] tests/Exhaustive.v +Universes written to file "universes-mtac2.txt". + = let (eval) := ?runner in eval + : nat COQC tests/cevar.v +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] +[DEBUG] (nat -> (fun T : Type => T) Type) +[OK] tests/abs_prod.v +0 + = Z0 + : Z COQC tests/comptactics.v +[DEBUG] Running test +[OK] tests/UnivSanityCheck.v COQC tests/debug_ex.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] +testMmatch@{i j} = +fun x : Type@{i} => x + : Type@{i} -> Type@{max(i,j)} +(* i j |= *) + +Arguments testMmatch _%type_scope +testMmatch'@{i j} = +fun x : Type@{i} => x + : Type@{i} -> Type@{j} +(* i j |= i <= j *) + +Arguments testMmatch' _%type_scope +testret@{u u0} = +fun x : Type@{u} => x + : Type@{u} -> Type@{u0} +(* u u0 |= u <= u0 *) + +Arguments testret _%type_scope +testexact@{u u0} : Type@{u} -> Type@{u0} +(* u u0 |= u <= u0 *) + +testexact is universe polymorphic +Arguments testexact _%type_scope +testexact is opaque +Expands to: Constant Mtac2Tests.bug_universes.testexact +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/bug_universes.v COQC tests/decapp.v +[DEBUG] {| + case_ind := nat; + case_val := 3; + case_return := Dyn (fun _ : nat => bool); + case_branches := [m: Dyn true + | Dyn (fun _ : nat => false)] +|} +[OK] tests/cevar.v COQC tests/declare.v +[OK] tests/DepDestruct.v COQC tests/decompose.v -COQC tests/dependent_let_goals.v [DEBUG] raise ?e Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. [DEBUG] (StuckTerm ?t) -Universes written to file "universes-mtac2.txt". -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 - = 0 - : nat -[OK] tests/decompose.v +[OK] tests/debug_ex.v +[DEBUG] true +[DEBUG] (Metavar Propₛ (1 = 1) ?e) +[OK] tests/ConstrSelector.v +[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) +COQC tests/dependent_let_goals.v +[OK] tests/bugs.v COQC tests/destruct_eq.v - = 1 - : nat +COQC tests/do.v +[OK] tests/decapp.v +COQC tests/dummylang.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] +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] +File "./tests/comptactics.v", line 35, characters 14-21: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/comptactics.v", line 40, characters 5-12: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/comptactics.v", line 41, characters 10-17: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +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] +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] +File "./tests/comptactics.v", line 59, characters 5-12: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/comptactics.v", line 60, characters 10-17: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +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] File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -[OK] tests/debug_ex.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -COQC tests/do.v -[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] [DEBUG] bla - = let (eval) := ?runner in eval - : nat [DEBUG] bla -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 - = let (eval) := ?runner in eval - : nat -[DEBUG] (NameExistsInContext (TheName "x")) = tt : unit bla = fun x : nat => (fun x0 : nat => {| s := x0 |}) x @@ -895,103 +1050,42 @@ Arguments bli {x}%nat_scope = bli : ST -[DEBUG] (VarAppearsInValue z) - = let (eval) := ?runner in eval - : nat = tt : unit = tt : unit -testMmatch@{i j} = -fun x : Type@{i} => x - : Type@{i} -> Type@{max(i,j)} -(* i j |= *) - -Arguments testMmatch _%type_scope -testMmatch'@{i j} = -fun x : Type@{i} => x - : Type@{i} -> Type@{j} -(* i j |= i <= j *) - -Arguments testMmatch' _%type_scope = tt : unit -testret@{u u0} = -fun x : Type@{u} => x - : Type@{u} -> Type@{u0} -(* u u0 |= u <= u0 *) - -Arguments testret _%type_scope = tt : unit -0 = tt : unit -testexact@{u u0} : Type@{u} -> Type@{u0} -(* u u0 |= u <= u0 *) - -testexact is universe polymorphic -Arguments testexact _%type_scope -testexact is opaque -Expands to: Constant Mtac2Tests.bug_universes.testexact - = Z0 - : Z -[OK] tests/abs.v -mmatch 1 -(let ps' := - with _ => M.print "always triggered first"| [# ] 0 | =n> - M.print "O, never triggered"| - [# ] S | _ : nat =n> M.print "S, never triggered" end in - ps') - : idmatcher_return M_InDepMatcher -COQC tests/dummylang.v = tt : unit NAT0 = 0 : nat -[DEBUG] (nat -> (fun T : Type => T) Type) NAT1 = 1 : nat NAT2 = 2 : nat -[OK] tests/decapp.v NAT3 = 3 : nat +[OK] tests/comptactics.v +If ffalse or nil then ;; else If ttrue then ;; else ;; end end + : st COQC tests/exceptions.v -[OK] tests/bug_universes.v -COQC tests/goal_reordering.v -[OK] tests/abs_prod.v -COQC tests/hugo.v -[DEBUG] Running test -[OK] tests/binders.v -COQC tests/initialization.v -[OK] tests/UnivSanityCheck.v -[OK] tests/dependent_let_goals.v -COQC tests/intropatt.v -COQC tests/kind_of_term.v -mmatch (1 :: nil)%list -(let ps' := - with [# ] nil | =n> M.print "nil"| [# ] cons | - (_ : nat) (_ : list nat) =n> - M.print "cons"| - _ => M.print "not in constructor normal form" end in - ps') - : idmatcher_return M_InDepMatcher -[DEBUG] true -[DEBUG] (Metavar Propₛ (1 = 1) ?e) +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] +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] NAT3: nat NAT2: nat NAT1: nat NAT0: nat -[OK] tests/cevar.v -mmatch (1 :: nil)%list -(let ps' := - with [# ] nil | =n> M.print "nil"| [# ] cons | - (_ : nat) (_ : list nat) =n> - M.print "cons"| - _ => M.print "not in constructor normal form" end in - ps') - : idmatcher_return M_InDepMatcher Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for (@M.runner unit ev) without backtracking @@ -1001,7 +1095,6 @@ (@M.runner unit ev), 0 subgoal(s) = tt : unit -COQC tests/lift.v [DEBUG] NAT3 = tt : unit @@ -1015,16 +1108,6 @@ Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. [deprecated-syntactic-definition,deprecated] -[OK] tests/bugs.v -COQC tests/ltac.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] -[OK] tests/Exhaustive.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] -COQC tests/ltac_rewrite.v File "./tests/declare.v", line 92, characters 62-71: Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. @@ -1040,9 +1123,6 @@ Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. [deprecated-syntactic-definition,deprecated] -File "./tests/comptactics.v", line 35, characters 14-21: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] blu = le_n_S : forall n m : nat, n <= m -> S n <= S m @@ -1055,14 +1135,6 @@ : forall n m : nat, n <= m -> S n <= S m Arguments blu (n m)%nat_scope _ -If ffalse or nil then ;; else If ttrue then ;; else ;; end end - : st -File "./tests/comptactics.v", line 40, characters 5-12: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/comptactics.v", line 41, characters 10-17: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] = (MTele_val (curry_sort Typeₛ (fun a' : ArgsOf [tele (_ : Type) (_ : nat) ] => @@ -1087,13 +1159,6 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit))) -> M unit : Type -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] -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] = M.declare_mind [tele (_ : Type) (_ : nat) ] [m:(m:"blubb__"; fun (_ : Type) (k : nat) => @@ -1133,10 +1198,6 @@ (fun (_ : Type -> forall a0 : nat, a0 = a0 -> Type) (_ : Type) (k : nat) => (m:[m:]; tt)) : M unit -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] = tt : unit = (MTele_val @@ -1163,9 +1224,6 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit))) -> M unit : Type -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] = M.declare_mind [tele (_ : Type) (_ : nat) ] [m:(m:"blubb__"; fun (_ : Type) (k : nat) => @@ -1283,17 +1341,8 @@ mexistT (MTele_ConstT S.Sort) [tele ] Propₛ) a))) mt_constr}) *m unit)))) -> M unit : Type -File "./tests/comptactics.v", line 59, characters 5-12: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/comptactics.v", line 60, characters 10-17: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] = tt : unit -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] = (MTele_val (curry_sort Typeₛ (fun a' : ArgsOf [tele (_ : Type) (_ : nat) ] => @@ -1340,24 +1389,8 @@ : Type = tt : unit -[DEBUG] tt -Pum - : Exception -[DEBUG] nat -[OK] tests/do.v -COQC tests/match_goal_context.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] -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/dependent_let_goals.v +COQC tests/goal_reordering.v Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for dummy without backtracking @@ -1374,57 +1407,75 @@ 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/comptactics.v -COQC tests/mctacticstests.v [OK] tests/declare.v -COQC tests/min_bug_univpoly.v +COQC tests/hugo.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] -[DEBUG] {| - case_ind := nat; - case_val := 3; - case_return := Dyn (fun _ : nat => bool); - case_branches := [m: Dyn true - | Dyn (fun _ : nat => false)] -|} -[OK] tests/initialization.v -COQC tests/min_bug_univpoly2.v -[OK] tests/goal_reordering.v -COQC tests/mode.v -[OK] tests/kind_of_term.v -COQC tests/mono_list_issue.v +[DEBUG] tt +Pum + : Exception +[DEBUG] nat +[OK] tests/do.v +COQC tests/initialization.v [OK] tests/destruct_eq.v -COQC tests/mrun.v +COQC tests/intropatt.v [OK] tests/exceptions.v -COQC tests/names.v -[DEBUG] hola -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/lift.v -COQC tests/nu_let.v +COQC tests/kind_of_term.v +[OK] tests/decompose.v +COQC tests/lift.v +[OK] tests/goal_reordering.v +COQC tests/ltac.v +[OK] tests/initialization.v +COQC tests/ltac_rewrite.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/min_bug_univpoly2.v -COQC tests/pretype.v [OK] tests/hugo.v -COQC tests/reduction.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/kind_of_term.v +COQC tests/mctacticstests.v +[DEBUG] hola +[OK] tests/lift.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/min_bug_univpoly.v +[OK] tests/dummylang.v +COQC tests/min_bug_univpoly2.v +[OK] tests/ltac_rewrite.v +COQC tests/mode.v +[OK] tests/ltac.v +COQC tests/mono_list_issue.v +[OK] tests/min_bug_univpoly2.v +COQC tests/mrun.v +[OK] tests/match_goal_context.v +COQC tests/names.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/match_goal_context.v -COQC tests/reif_jason.v -[OK] tests/ltac_rewrite.v -COQC tests/removetest.v -[OK] tests/DepDestruct.v -COQC tests/replace.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 +COQC tests/nu_let.v File "./tests/min_bug_univpoly.v", line 27, characters 0-118: Warning: Notation "_ = _ :> _" was already used in scope type_scope. [notation-overridden,parsing] @@ -1440,91 +1491,133 @@ File "./tests/min_bug_univpoly.v", line 34, characters 0-47: Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing] -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] -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/ConstrSelector.v -[OK] tests/mono_list_issue.v -COQC tests/rew_hd_error.v -COQC tests/selectors.v +[OK] tests/mode.v File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing] File "./tests/min_bug_univpoly.v", line 208, characters 0-72: Warning: Notation "( _ , _ , .. , _ )" was already used in scope core_scope. [notation-overridden,parsing] +COQC tests/pretype.v File "./tests/min_bug_univpoly.v", line 216, characters 0-67: Warning: Notation "_ :: _" was already used in scope list_scope. [notation-overridden,parsing] 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/reduction.v +[OK] tests/intropatt.v +COQC tests/reif_jason.v +[OK] tests/mrun.v +COQC tests/removetest.v [OK] tests/names.v +COQC tests/replace.v +[OK] tests/nu_let.v +[OK] tests/pretype.v +COQC tests/rew_hd_error.v +COQC tests/selectors.v +is_not_breaking_letins = id I + : True +[DEBUG] b +[DEBUG] nat +(fun H : if true then True else False => H) +[DEBUG] b +[DEBUG] nat +[OK] tests/replace.v COQC tests/ssrpattern.v -[OK] tests/mode.v +[DEBUG] b +[DEBUG] nat +[OK] tests/rew_hd_error.v COQC tests/tactics.v -[OK] tests/ltac.v +Finished transaction in 0.724 secs (0.296u,0.064s) (successful) +[OK] tests/removetest.v COQC tests/test_bind.v -[OK] tests/nu_let.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. +[deprecated-syntactic-definition,deprecated] +Finished transaction in 0.034 secs (0.034u,0.s) (successful) +File "./tests/mctacticstests.v", line 278, characters 13-22: +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] +File "./tests/reif_jason.v", line 596, characters 2-322: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +[DEBUG] (fun n : nat => n + n = S (S (S n))) +[DEBUG] (fun n : nat => ?n + n = S (S (S n))) +[OK] tests/reduction.v +[OK] tests/ssrpattern.v COQC tests/test_brackets.v -[OK] tests/min_bug_univpoly.v COQC tests/test_get_name.v -is_not_breaking_letins = id I - : True -[OK] tests/mrun.v +[OK] tests/reif_jason.v COQC tests/test_get_reference.v -[OK] tests/pretype.v +[OK] tests/selectors.v COQC tests/test_goal_match.v -(fun H : if true then True else False => H) -[OK] tests/replace.v +(fun (x : nat) (z : bool) (y : nat) => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return (a =m= (forall z0 : nat, (fun n : nat => n > y) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return + (a =m= + (forall z0 : nat, (fun n : nat => forall x0 : nat, x0 > n) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return + (a =m= + (forall z0 : bool, + (fun _ : bool => forall y0 x0 : nat, x0 > y0) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => ?Goal + end z + end y + end x) +[OK] tests/test_bind.v +[OK] tests/test_get_name.v COQC tests/test_mmatch.v -[OK] tests/rew_hd_error.v COQC tests/test_mtry.v -[OK] tests/dummylang.v +[OK] tests/mctacticstests.v COQC tests/test_munify.v -[DEBUG] (fun n : nat => n + n = S (S (S n))) -[OK] tests/intropatt.v -Finished transaction in 0.296 secs (0.243u,0.051s) (successful) +[OK] tests/test_get_reference.v COQC tests/test_ret.v -[DEBUG] (fun n : nat => ?n + n = S (S (S n))) -[OK] tests/test_bind.v -[OK] tests/ssrpattern.v +[OK] tests/test_brackets.v COQC tests/test_unfold_in.v +[OK] tests/test_goal_match.v +[OK] tests/test_mtry.v COQC tests/timers.v -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/trace.v -Finished transaction in 0.027 secs (0.027u,0.s) (successful) -[OK] tests/selectors.v +Finished transaction in 0.126 secs (0.11u,0.015s) (successful) +[OK] tests/test_munify.v COQC tests/ttactics.v -[OK] tests/test_get_name.v +0.031000 +0.031000 +0.061000 +0.000000 +[OK] tests/timers.v COQC tests/typeclass.v -[OK] tests/reduction.v -COQC tests/typed_term_decomposition.v -[OK] tests/test_get_reference.v -COQC tests/unification.v -[OK] tests/removetest.v -COQC tests/bugs/bug117.v -[OK] tests/test_mtry.v -COQC tests/bugs/bug225.v -[OK] tests/test_munify.v -COQC tests/bugs/bug288.v [OK] tests/test_unfold_in.v -Finished transaction in 0.107 secs (0.083u,0.023s) (successful) [OK] tests/test_ret.v -COQC tests/bugs/bug295.v -COQC tests/bugs/bug297.v -[OK] tests/test_brackets.v -COQC tests/bugs/bug299.v -0.025000 -0.025000 [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -1536,20 +1629,22 @@ [DEBUG] (M.abs_fun ann (fun ann0 : ann => ann0)) [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) +COQC tests/typed_term_decomposition.v [OK] tests/trace.v -COQC tests/bugs/bug302.v -0.051000 -0.000000 -[OK] tests/test_goal_match.v -COQC tests/bugs/bug304.v -[OK] tests/timers.v -COQC examples/basics_tutorial.v +COQC tests/unification.v +[OK] tests/test_mmatch.v +COQC tests/bugs/bug117.v +COQC tests/bugs/bug225.v +[OK] tests/typeclass.v +[OK] tests/tactics.v +COQC tests/bugs/bug288.v +COQC tests/bugs/bug295.v +[OK] tests/ttactics.v +COQC tests/bugs/bug297.v (3, 5) : nat * nat 5 : nat -[OK] tests/typeclass.v -COQC examples/tactics.v (True, False) : Prop * Prop [DEBUG] (3, 5) @@ -1558,35 +1653,28 @@ [DEBUG] (m:Dyn Nat.add; [m: Dyn 3 | Dyn 4]) [OK] tests/typed_term_decomposition.v -COQC examples/tauto.v +COQC tests/bugs/bug299.v +[OK] tests/bugs/bug117.v +[OK] tests/bugs/bug225.v +COQC tests/bugs/bug302.v +COQC tests/bugs/bug304.v [OK] tests/unification.v +COQC examples/basics_tutorial.v +[OK] tests/bugs/bug288.v +COQC examples/tactics.v +[OK] tests/bugs/bug295.v +COQC examples/tauto.v +[OK] tests/bugs/bug297.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. -[OK] tests/ttactics.v -[OK] tests/bugs/bug117.v -[OK] tests/bugs/bug225.v -[OK] tests/bugs/bug288.v -[OK] tests/test_mmatch.v -CLEAN -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -COQDEP VFILES -[DEBUG] b -[DEBUG] nat -make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. -[OK] tests/bugs/bug297.v -[DEBUG] b -[DEBUG] nat -[DEBUG] All good, a was instantiated with b's type (tFalse) -[OK] tests/bugs/bug295.v -[OK] tests/bugs/bug299.v [DEBUG] All good -[DEBUG] b [OK] tests/bugs/bug304.v -[DEBUG] nat +[DEBUG] All good, a was instantiated with b's type (tFalse) +[OK] tests/bugs/bug299.v 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] @@ -1597,7 +1685,6 @@ 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] -COQC lf/Preface.v empty_string = "" : string world_string = "world" @@ -1611,16 +1698,14 @@ the_sequence_6 = 6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil : list nat -[DEBUG] all good inlist : forall (A : Type) (x : A) (x0 : list A), M (In x x0) -[OK] tests/bugs/bug302.v y_in_zyx = fun x y z : nat => eval (inlist y (z :: y :: x :: nil)) : forall x y z : nat, In y (z :: y :: x :: nil) Arguments y_in_zyx (x y z)%nat_scope -COQC lf/Basics.v +CLEAN inlist' = fun (A : Type) (x : A) => mfix1 f s : list A : M In x s := @@ -1697,6 +1782,7 @@ : forall x y z : nat, In x ((y :: z :: nil) ++ x :: z :: nil) Arguments ex_inlist (x y z)%nat_scope +[DEBUG] all good ex_inlist' = fun x y z : nat => (fun (A : Type) (x0 : A) (_ : forall x1 : list A, M (In x0 x1)) @@ -1757,8 +1843,11 @@ : forall x y z : nat, In x ((y :: z :: nil) ++ x :: z :: nil) Arguments ex_inlist'' (x y z)%nat_scope +[OK] tests/bugs/bug302.v +make[3]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. ex1 = conj I (or_intror I) : True /\ (False \/ True) +COQDEP VFILES nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B nu is universe polymorphic @@ -1770,7 +1859,7 @@ : forall p q : Prop, p -> q -> p /\ q Arguments ex_with_implication [p q]%type_scope _ _ -[OK] examples/tauto.v +make[3]: 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. @@ -1796,15 +1885,14 @@ Warning: Notation plus_comm is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition,deprecated] -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. -[deprecated-syntactic-definition,deprecated] -File "./tests/mctacticstests.v", line 278, characters 13-22: -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] [OK] examples/basics_tutorial.v +[OK] examples/tauto.v +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] @@ -1812,7 +1900,6 @@ : day = tuesday : day -[OK] tests/tactics.v true : bool negb true @@ -1833,50 +1920,6 @@ : nat 0 + 1 + 1 : nat -(fun (x : nat) (z : bool) (y : nat) => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return (a =m= (forall z0 : nat, (fun n : nat => n > y) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return - (a =m= - (forall z0 : nat, (fun n : nat => forall x0 : nat, x0 > n) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return - (a =m= - (forall z0 : bool, - (fun _ : bool => forall y0 x0 : nat, x0 > y0) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => ?Goal - end z - end y - end x) -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 -[OK] tests/mctacticstests.v COQC lf/Induction.v leb : nat -> nat -> bool @@ -1953,7 +1996,7 @@ (_ : 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 -j16 test + make -j7 test make[1]: Entering directory '/build/coq-mtac2-1.4+8.16' COQC tests/ConstrSelector.v COQC tests/DepDestruct.v @@ -1962,55 +2005,192 @@ COQC tests/abs.v COQC tests/abs_prod.v COQC tests/binders.v +[DEBUG] (nat -> (fun T : Type => T) Type) +[OK] tests/abs_prod.v COQC tests/bug_universes.v + = 0 + : nat +Universes written to file "universes-mtac2.txt". + = 1 + : nat + = let (eval) := ?runner in eval + : nat + = let (eval) := ?runner in eval + : nat + = let (eval) := ?runner in eval + : nat +[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] +0 + = Z0 + : Z +[DEBUG] (NameExistsInContext (TheName "x")) +[DEBUG] (VarAppearsInValue z) +[OK] tests/abs.v COQC tests/bugs.v +[OK] tests/binders.v +[DEBUG] Running test COQC tests/cevar.v +[OK] tests/UnivSanityCheck.v COQC tests/comptactics.v +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 +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] +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] {| + case_ind := nat; + case_val := 3; + case_return := Dyn (fun _ : nat => bool); + case_branches := [m: Dyn true + | Dyn (fun _ : nat => false)] +|} +mmatch 1 +(let ps' := + with _ => M.print "always triggered first"| [# ] 0 | =n> + M.print "O, never triggered"| + [# ] S | _ : nat =n> M.print "S, never triggered" end in + ps') + : idmatcher_return M_InDepMatcher +mmatch (1 :: nil)%list +(let ps' := + with [# ] nil | =n> M.print "nil"| [# ] cons | + (_ : nat) (_ : list nat) =n> + M.print "cons"| + _ => M.print "not in constructor normal form" end in + ps') + : idmatcher_return M_InDepMatcher +mmatch (1 :: nil)%list +(let ps' := + with [# ] nil | =n> M.print "nil"| [# ] cons | + (_ : nat) (_ : list nat) =n> + M.print "cons"| + _ => M.print "not in constructor normal form" end in + ps') + : idmatcher_return M_InDepMatcher +[OK] tests/Exhaustive.v COQC tests/debug_ex.v +testMmatch@{i j} = +fun x : Type@{i} => x + : Type@{i} -> Type@{max(i,j)} +(* i j |= *) + +Arguments testMmatch _%type_scope +testMmatch'@{i j} = +fun x : Type@{i} => x + : Type@{i} -> Type@{j} +(* i j |= i <= j *) + +Arguments testMmatch' _%type_scope +testret@{u u0} = +fun x : Type@{u} => x + : Type@{u} -> Type@{u0} +(* u u0 |= u <= u0 *) + +Arguments testret _%type_scope +testexact@{u u0} : Type@{u} -> Type@{u0} +(* u u0 |= u <= u0 *) + +testexact is universe polymorphic +Arguments testexact _%type_scope +testexact is opaque +Expands to: Constant Mtac2Tests.bug_universes.testexact +[OK] tests/bug_universes.v COQC tests/decapp.v +[OK] tests/DepDestruct.v +[OK] tests/cevar.v COQC tests/declare.v COQC tests/decompose.v +[OK] tests/ConstrSelector.v COQC tests/dependent_let_goals.v -[DEBUG] (NameExistsInContext (TheName "x")) -[DEBUG] (VarAppearsInValue z) -[OK] tests/binders.v -COQC tests/destruct_eq.v -[OK] tests/dependent_let_goals.v -COQC tests/do.v [DEBUG] raise ?e Debug: ?t is not evaluable. Context: Monadic. Not reduced to let-in. [DEBUG] (StuckTerm ?t) -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 - = 0 - : nat [OK] tests/debug_ex.v +[DEBUG] true +[DEBUG] (Metavar Propₛ (1 = 1) ?e) +COQC tests/destruct_eq.v +[OK] tests/bugs.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] +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] +File "./tests/comptactics.v", line 35, characters 14-21: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +COQC tests/do.v +File "./tests/comptactics.v", line 40, characters 5-12: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/comptactics.v", line 41, characters 10-17: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +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] +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] +File "./tests/comptactics.v", line 59, characters 5-12: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +File "./tests/comptactics.v", line 60, characters 10-17: +Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. +[deprecated-syntactic-definition,deprecated] +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/dummylang.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] +[OK] tests/decompose.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] +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] +If ffalse or nil then ;; else If ttrue then ;; else ;; end end + : st +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] +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] +[OK] tests/destruct_eq.v +COQC tests/goal_reordering.v File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "{ _ } + { _ }" was already used in scope type_scope. [notation-overridden,parsing] File "./tests/declare.v", line 1, characters 0-51: Warning: Notation "_ + { _ }" was already used in scope type_scope. [notation-overridden,parsing] -COQC tests/dummylang.v - = 1 - : nat [DEBUG] bla -[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) [DEBUG] bla - = 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"| - _ => M.print "not in constructor normal form" end in - ps') - : idmatcher_return M_InDepMatcher +[DEBUG] (Specif.msigT (MTele.MTele_Const nat)) = tt : unit bla = fun x : nat => (fun x0 : nat => {| s := x0 |}) x @@ -2018,7 +2198,6 @@ Arguments bla x%nat_scope S.selem_of elemr T.of_M S.stype_of -Universes written to file "universes-mtac2.txt". M.t <- predicate_pred ( M_Predicate ) gtactic <- predicate_pred ( T_Predicate ) _ <- s ( bla ) @@ -2034,8 +2213,6 @@ Arguments bli {x}%nat_scope = bli : ST - = let (eval) := ?runner in eval - : nat = tt : unit = tt @@ -2046,100 +2223,30 @@ : unit = tt : unit -[DEBUG] [ $(egrep "Coq.*Mtac2" universes-mtac2.txt | wc -l | tr -d ' ') = "0" ] +[OK] tests/decapp.v = tt : unit NAT0 = 0 : nat -mmatch 1 -(let ps' := - with _ => M.print "always triggered first"| [# ] 0 | =n> - M.print "O, never triggered"| - [# ] S | _ : nat =n> M.print "S, never triggered" end in - ps') - : idmatcher_return M_InDepMatcher -testMmatch@{i j} = -fun x : Type@{i} => x - : Type@{i} -> Type@{max(i,j)} -(* i j |= *) - -Arguments testMmatch _%type_scope NAT1 = 1 : nat -testMmatch'@{i j} = -fun x : Type@{i} => x - : Type@{i} -> Type@{j} -(* i j |= i <= j *) - -Arguments testMmatch' _%type_scope NAT2 = 2 : nat NAT3 = 3 : nat -0 -testret@{u u0} = -fun x : Type@{u} => x - : Type@{u} -> Type@{u0} -(* u u0 |= u <= u0 *) - -Arguments testret _%type_scope - = Z0 - : Z -[DEBUG] (nat -> (fun T : Type => T) Type) -testexact@{u u0} : Type@{u} -> Type@{u0} -(* u u0 |= u <= u0 *) - -testexact is universe polymorphic -Arguments testexact _%type_scope -testexact is opaque -Expands to: Constant Mtac2Tests.bug_universes.testexact -[OK] tests/decapp.v -COQC tests/exceptions.v -[OK] tests/decompose.v -COQC tests/goal_reordering.v -[OK] tests/abs_prod.v COQC tests/hugo.v -[OK] tests/bug_universes.v -[DEBUG] Running test +[OK] tests/dependent_let_goals.v +[DEBUG] tt +Pum + : Exception +[DEBUG] nat +[OK] tests/do.v COQC tests/initialization.v -[OK] tests/abs.v COQC tests/intropatt.v -[OK] tests/cevar.v -COQC tests/kind_of_term.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] -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] -File "./tests/comptactics.v", line 35, characters 14-21: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -[DEBUG] true -mmatch (1 :: nil)%list -(let ps' := - with [# ] nil | =n> M.print "nil"| [# ] cons | - (_ : nat) (_ : list nat) =n> - M.print "cons"| - _ => M.print "not in constructor normal form" end in - ps') - : idmatcher_return M_InDepMatcher -[DEBUG] (Metavar Propₛ (1 = 1) ?e) -[OK] tests/UnivSanityCheck.v -File "./tests/comptactics.v", line 40, characters 5-12: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/comptactics.v", line 41, characters 10-17: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -COQC tests/lift.v NAT3: nat NAT2: nat NAT1: nat NAT0: nat -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] Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for (@M.runner unit ev) without backtracking @@ -2149,8 +2256,6 @@ (@M.runner unit ev), 0 subgoal(s) = tt : unit -If ffalse or nil then ;; else If ttrue then ;; else ;; end end - : st [DEBUG] NAT3 = tt : unit @@ -2164,23 +2269,6 @@ Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. [deprecated-syntactic-definition,deprecated] -mmatch (1 :: nil)%list -(let ps' := - with [# ] nil | =n> M.print "nil"| [# ] cons | - (_ : nat) (_ : list nat) =n> - M.print "cons"| - _ => M.print "not in constructor normal form" end in - ps') - : idmatcher_return M_InDepMatcher -[OK] tests/bugs.v -COQC tests/ltac.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] -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] File "./tests/declare.v", line 92, characters 62-71: Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. @@ -2189,10 +2277,6 @@ Warning: Notation Le.le_n_S is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.succ_le_mono instead. [deprecated-syntactic-definition,deprecated] -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] blu = tt : unit @@ -2204,12 +2288,10 @@ : forall n m : nat, n <= m -> S n <= S m Arguments blu (n m)%nat_scope _ -[OK] tests/Exhaustive.v = tt : unit newone = tt : unit -COQC tests/ltac_rewrite.v blu = le_n_S : forall n m : nat, n <= m -> S n <= S m @@ -2238,12 +2320,6 @@ _ : k = k ] (fun _ : k = k => Propₛ)) a))) mt_constr}) *m unit))) -> M unit : Type -File "./tests/comptactics.v", line 59, characters 5-12: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] -File "./tests/comptactics.v", line 60, characters 10-17: -Warning: Notation beq_nat is deprecated since 8.16. Use Nat.eqb instead. -[deprecated-syntactic-definition,deprecated] = M.declare_mind [tele (_ : Type) (_ : nat) ] [m:(m:"blubb__"; fun (_ : Type) (k : nat) => @@ -2283,9 +2359,6 @@ (fun (_ : Type -> forall a0 : nat, a0 = a0 -> Type) (_ : Type) (k : nat) => (m:[m:]; tt)) : M unit -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] = tt : unit = (MTele_val @@ -2431,8 +2504,6 @@ : Type = tt : unit -[OK] tests/comptactics.v -COQC tests/match_goal_context.v = (MTele_val (curry_sort Typeₛ (fun a' : ArgsOf [tele (_ : Type) (_ : nat) ] => @@ -2479,30 +2550,12 @@ : Type = tt : unit -[DEBUG] tt -Pum - : Exception -[DEBUG] nat -[OK] tests/do.v -COQC tests/mctacticstests.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] -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] Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false Debug: 1: looking for dummy without backtracking Debug: 1.1: exact test_local1 on dummy, 0 subgoal(s) Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false -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] Debug: 1: looking for Inner.dummy without backtracking Debug: 1.1: exact Inner.test_global5 on Inner.dummy, 0 subgoal(s) Debug: @@ -2514,58 +2567,40 @@ 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/min_bug_univpoly.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] -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] -[DEBUG] hola +COQC tests/kind_of_term.v +[OK] tests/exceptions.v +COQC tests/lift.v [OK] tests/initialization.v -COQC tests/min_bug_univpoly2.v -[DEBUG] {| - case_ind := nat; - case_val := 3; - case_return := Dyn (fun _ : nat => bool); - case_branches := [m: Dyn true - | Dyn (fun _ : nat => false)] -|} -[OK] tests/kind_of_term.v -COQC tests/mode.v -[OK] tests/lift.v -COQC tests/mono_list_issue.v +COQC tests/ltac.v [OK] tests/goal_reordering.v -COQC tests/mrun.v -[OK] tests/destruct_eq.v -COQC tests/names.v -[OK] tests/exceptions.v -COQC tests/nu_let.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] +COQC tests/ltac_rewrite.v +[DEBUG] hola +[OK] tests/lift.v +COQC tests/match_goal_context.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] +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/kind_of_term.v +COQC tests/mctacticstests.v [OK] tests/hugo.v -COQC tests/pretype.v -[OK] tests/min_bug_univpoly2.v -COQC tests/reduction.v +COQC tests/min_bug_univpoly.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/reif_jason.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] +COQC tests/mode.v +[OK] tests/min_bug_univpoly2.v +COQC tests/mono_list_issue.v [OK] tests/ltac_rewrite.v -COQC tests/removetest.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] +COQC tests/mrun.v +[OK] tests/intropatt.v +COQC tests/names.v File "./tests/min_bug_univpoly.v", line 27, characters 0-118: Warning: Notation "_ = _ :> _" was already used in scope type_scope. [notation-overridden,parsing] @@ -2581,15 +2616,22 @@ File "./tests/min_bug_univpoly.v", line 34, characters 0-47: Warning: Notation "_ <> _" was already used in scope type_scope. [notation-overridden,parsing] -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] +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/dummylang.v +COQC tests/nu_let.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 -COQC tests/replace.v -[OK] tests/DepDestruct.v -COQC tests/rew_hd_error.v -[OK] tests/ConstrSelector.v -COQC tests/selectors.v +COQC tests/pretype.v +[OK] tests/mode.v +COQC tests/reduction.v File "./tests/min_bug_univpoly.v", line 207, characters 0-44: Warning: Notation "_ * _" was already used in scope type_scope. [notation-overridden,parsing] @@ -2602,60 +2644,115 @@ 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/mode.v -COQC tests/ssrpattern.v -[OK] tests/mrun.v -COQC tests/tactics.v +[OK] tests/min_bug_univpoly.v +COQC tests/reif_jason.v [OK] tests/nu_let.v -COQC tests/test_bind.v +COQC tests/removetest.v [OK] tests/names.v -COQC tests/test_brackets.v -[OK] tests/ltac.v -COQC tests/test_get_name.v +COQC tests/replace.v +[OK] tests/mrun.v +COQC tests/rew_hd_error.v [OK] tests/pretype.v -[OK] tests/min_bug_univpoly.v -COQC tests/test_get_reference.v -COQC tests/test_goal_match.v +COQC tests/selectors.v is_not_breaking_letins = id I : True -[OK] tests/rew_hd_error.v -COQC tests/test_mmatch.v -(fun H : if true then True else False => H) -[OK] tests/replace.v -COQC tests/test_mtry.v File "./tests/reif_jason.v", line 596, characters 2-322: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -Finished transaction in 0.284 secs (0.24u,0.044s) (successful) +[OK] tests/reif_jason.v +COQC tests/ssrpattern.v +(fun H : if true then True else False => H) +[OK] tests/replace.v +COQC tests/tactics.v +[OK] tests/rew_hd_error.v +COQC tests/test_bind.v +Finished transaction in 0.694 secs (0.287u,0.098s) (successful) +Finished transaction in 0.034 secs (0.033u,0.s) (successful) +[OK] tests/selectors.v +COQC tests/test_brackets.v +[OK] tests/reduction.v +COQC tests/test_get_name.v [DEBUG] (fun n : nat => n + n = S (S (S n))) -[OK] tests/intropatt.v -COQC tests/test_munify.v [DEBUG] (fun n : nat => ?n + n = S (S (S n))) +[OK] tests/removetest.v [OK] tests/ssrpattern.v +COQC tests/test_get_reference.v +COQC tests/test_goal_match.v +[DEBUG] b +[DEBUG] nat +[DEBUG] b +[DEBUG] nat +[DEBUG] b +[DEBUG] nat [OK] tests/test_bind.v +COQC tests/test_mmatch.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. +[deprecated-syntactic-definition,deprecated] +File "./tests/mctacticstests.v", line 278, characters 13-22: +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] +[OK] tests/test_brackets.v +COQC tests/test_mtry.v +[OK] tests/test_get_name.v +COQC tests/test_munify.v +[OK] tests/test_get_reference.v COQC tests/test_ret.v +[OK] tests/test_mtry.v COQC tests/test_unfold_in.v -[OK] tests/test_get_name.v +(fun (x : nat) (z : bool) (y : nat) => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return (a =m= (forall z0 : nat, (fun n : nat => n > y) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return + (a =m= + (forall z0 : nat, (fun n : nat => forall x0 : nat, x0 > n) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => + match + reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) + match + meq_refl in (_ =m= a) + return + (a =m= + (forall z0 : bool, + (fun _ : bool => forall y0 x0 : nat, x0 > y0) z0)) + with + | meq_refl => meq_refl + end in (_ =m= Q) return Q + with + | meq_refl => ?Goal + end z + end y + end x) +[OK] tests/test_goal_match.v COQC tests/timers.v -[OK] tests/dummylang.v +[OK] tests/tactics.v COQC tests/trace.v -Finished transaction in 0.026 secs (0.026u,0.s) (successful) -[OK] tests/reif_jason.v +[OK] tests/test_munify.v COQC tests/ttactics.v -[OK] tests/selectors.v +[OK] tests/test_ret.v COQC tests/typeclass.v -[OK] tests/reduction.v +Finished transaction in 0.271 secs (0.124u,0.012s) (successful) +[OK] tests/test_unfold_in.v COQC tests/typed_term_decomposition.v -[OK] tests/test_get_reference.v +[OK] tests/mctacticstests.v COQC tests/unification.v -[OK] tests/removetest.v -COQC tests/bugs/bug117.v -[OK] tests/test_mtry.v -COQC tests/bugs/bug225.v -Finished transaction in 0.105 secs (0.093u,0.012s) (successful) -[OK] tests/test_brackets.v -COQC tests/bugs/bug288.v -[DEBUG] b -[DEBUG] nat [DEBUG] (M.nu Generate mNone (fun P : Type => M.nu Generate mNone @@ -2667,70 +2764,56 @@ [DEBUG] (M.abs_fun ann (fun ann0 : ann => ann0)) [DEBUG] (M.set_trace false) [DEBUG] (M.set_trace false) -[OK] tests/test_ret.v -COQC tests/bugs/bug295.v [OK] tests/trace.v -[OK] tests/test_munify.v -COQC tests/bugs/bug297.v -COQC tests/bugs/bug299.v -[OK] tests/test_unfold_in.v -COQC tests/bugs/bug302.v -[DEBUG] b -[DEBUG] nat -[OK] tests/test_goal_match.v -COQC tests/bugs/bug304.v -0.021000 -0.021000 -0.037000 +COQC tests/bugs/bug117.v +[OK] tests/typeclass.v +COQC tests/bugs/bug225.v +[OK] tests/ttactics.v +COQC tests/bugs/bug288.v +0.066000 +0.066000 +0.128000 0.000000 [OK] tests/timers.v -COQC examples/basics_tutorial.v -[DEBUG] b -[DEBUG] nat (3, 5) : nat * nat -[OK] tests/typeclass.v -COQC examples/tactics.v 5 : nat (True, False) : Prop * Prop -[OK] tests/ttactics.v -COQC examples/tauto.v -[OK] tests/unification.v -cd tests/sf-5; ./configure.sh; make clean; make +COQC tests/bugs/bug295.v [DEBUG] (3, 5) -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. -[OK] tests/bugs/bug117.v [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 +[OK] tests/bugs/bug117.v +COQC tests/bugs/bug297.v +[OK] tests/unification.v +COQC tests/bugs/bug299.v +COQC tests/bugs/bug302.v +[OK] tests/test_mmatch.v +COQC tests/bugs/bug304.v [OK] tests/bugs/bug225.v +COQC examples/basics_tutorial.v [OK] tests/bugs/bug288.v -CLEAN -[OK] tests/test_mmatch.v -[DEBUG] All good, a was instantiated with b's type (tFalse) -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. -[OK] tests/bugs/bug299.v -[DEBUG] All good -[OK] tests/bugs/bug304.v +COQC examples/tactics.v [OK] tests/bugs/bug297.v -COQDEP VFILES -make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +COQC examples/tauto.v [OK] tests/bugs/bug295.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. +[DEBUG] all good +[OK] tests/bugs/bug302.v 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] -[DEBUG] all good produces_a_value : M nat the_value_tactic = 1 @@ -2738,7 +2821,6 @@ 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/bug302.v empty_string = "" : string world_string = "world" @@ -2752,22 +2834,16 @@ the_sequence_6 = 6 :: 3 :: 10 :: 5 :: 16 :: 8 :: 4 :: 2 :: 1 :: nil : list nat -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. -[deprecated-syntactic-definition,deprecated] -COQC lf/Preface.v +[DEBUG] All good, a was instantiated with b's type (tFalse) inlist : forall (A : Type) (x : A) (x0 : list A), M (In x x0) -File "./tests/mctacticstests.v", line 278, characters 13-22: -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] +[OK] tests/bugs/bug299.v y_in_zyx = fun x y z : nat => eval (inlist y (z :: y :: x :: nil)) : forall x y z : nat, In y (z :: y :: x :: nil) Arguments y_in_zyx (x y z)%nat_scope +[DEBUG] All good inlist' = fun (A : Type) (x : A) => mfix1 f s : list A : M In x s := @@ -2827,7 +2903,8 @@ : 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 -COQC lf/Basics.v +CLEAN +[OK] tests/bugs/bug304.v ex_inlist = fun x y z : nat => in_cons y x @@ -2907,6 +2984,9 @@ Arguments ex_inlist'' (x y z)%nat_scope ex1 = conj I (or_intror I) : True /\ (False \/ True) +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. nu@{u u0 u1} : forall {A B : Type}, name -> moption A -> (A -> M B) -> M B nu is universe polymorphic @@ -2918,46 +2998,7 @@ : forall p q : Prop, p -> q -> p /\ q Arguments ex_with_implication [p q]%type_scope _ _ -(fun (x : nat) (z : bool) (y : nat) => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return (a =m= (forall z0 : nat, (fun n : nat => n > y) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return - (a =m= - (forall z0 : nat, (fun n : nat => forall x0 : nat, x0 > n) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => - match - reduce (RedWhd [rl:RedBeta; RedDelta; RedMatch]) - match - meq_refl in (_ =m= a) - return - (a =m= - (forall z0 : bool, - (fun _ : bool => forall y0 x0 : nat, x0 > y0) z0)) - with - | meq_refl => meq_refl - end in (_ =m= Q) return Q - with - | meq_refl => ?Goal - end z - end y - end x) -[OK] examples/tauto.v +COQDEP VFILES 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. @@ -2984,7 +3025,10 @@ The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition,deprecated] [OK] examples/basics_tutorial.v -[OK] tests/tactics.v +make[2]: warning: jobserver unavailable: using -j1. Add '+' to parent make rule. +COQC lf/Preface.v +[OK] examples/tauto.v +COQC lf/Basics.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] @@ -2998,6 +3042,9 @@ : bool negb : bool -> bool +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] 4 : nat = 2 @@ -3008,15 +3055,11 @@ : nat -> nat minustwo : nat -> nat +[OK] examples/tactics.v = 5 : nat 0 + 1 + 1 : nat -[OK] tests/mctacticstests.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 COQC lf/Induction.v leb : nat -> nat -> bool @@ -3253,8 +3296,8 @@ dpkg-gencontrol: warning: Depends field of package libcoq-mtac2: substitution variable ${shlibs:Depends} used, but is not defined dh_md5sums dh_builddeb -dpkg-deb: building package 'libcoq-mtac2' in '../libcoq-mtac2_1.4+8.16-2_i386.deb'. dpkg-deb: building package 'libcoq-mtac2-dbgsym' in '../libcoq-mtac2-dbgsym_1.4+8.16-2_i386.deb'. +dpkg-deb: building package 'libcoq-mtac2' in '../libcoq-mtac2_1.4+8.16-2_i386.deb'. dpkg-genbuildinfo --build=binary -O../coq-mtac2_1.4+8.16-2_i386.buildinfo dpkg-genchanges --build=binary -O../coq-mtac2_1.4+8.16-2_i386.changes dpkg-genchanges: info: binary-only upload (no source code included) @@ -3262,12 +3305,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/25363/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/25363/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/10942 and its subdirectories -I: Current time: Sun Jun 23 05:57:24 -12 2024 -I: pbuilder-time-stamp: 1719165444 +I: removing directory /srv/workspace/pbuilder/25363 and its subdirectories +I: Current time: Tue May 23 01:37:05 +14 2023 +I: pbuilder-time-stamp: 1684755425