Diff of the two buildlogs: -- --- b1/build.log 2021-08-09 13:16:27.407435472 +0000 +++ b2/build.log 2021-08-09 13:30:29.911826806 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sun Sep 11 07:31:32 -12 2022 -I: pbuilder-time-stamp: 1662924692 +I: Current time: Tue Aug 10 03:16:29 +14 2021 +I: pbuilder-time-stamp: 1628514989 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/buster-reproducible-base.tgz] I: copying local configuration @@ -17,7 +17,7 @@ I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' gpgv: keyblock resource '/root/.gnupg/trustedkeys.kbx': General error -gpgv: Signature made Tue Aug 29 11:05:09 2017 -12 +gpgv: Signature made Wed Aug 30 13:05:09 2017 +14 gpgv: using RSA key B845CE510F9B714D gpgv: Can't check signature: No public key dpkg-source: warning: failed to verify signature on ./hol88_2.02.19940316-35.dsc @@ -29,136 +29,170 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/40510/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/32824/tmp/hooks/D01_modify_environment starting +debug: Running on ionos1-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +Removing 'diversion of /bin/sh to /bin/sh.distrib by dash' +Adding 'diversion of /bin/sh to /bin/sh.distrib by bash' +Removing 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by dash' +Adding 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by 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/32824/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/32824/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=16' - DISTRIBUTION='' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="0" [2]="3" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.0.3(1)-release' + BUILDDIR=/build + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=15' + DIRSTACK=() + DISTRIBUTION= + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='42f453cb083f424380124f9dd254dc17' - 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='40510' - PS1='# ' - PS2='> ' + INVOCATION_ID=139f0c0ddea9451487c64ce6d9269bef + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=32824 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/tmp.17mcOTX5eX/pbuilderrc_Lp40 --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.17mcOTX5eX/b1 --logfile b1/build.log hol88_2.02.19940316-35.dsc' - SUDO_GID='111' - SUDO_UID='106' - 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/tmp.17mcOTX5eX/pbuilderrc_6ybV --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.17mcOTX5eX/b2 --logfile b2/build.log hol88_2.02.19940316-35.dsc' + SUDO_GID=110 + SUDO_UID=105 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://78.137.99.97:3128 I: uname -a - Linux ionos15-amd64 5.10.0-0.bpo.8-amd64 #1 SMP Debian 5.10.46-2~bpo10+1 (2021-07-22) x86_64 GNU/Linux + Linux i-capture-the-hostname 4.19.0-17-amd64 #1 SMP Debian 4.19.194-3 (2021-07-18) x86_64 GNU/Linux I: ls -l /bin total 5116 - -rwxr-xr-x 1 root root 1168776 Apr 17 2019 bash - -rwxr-xr-x 3 root root 38984 Jul 10 2019 bunzip2 - -rwxr-xr-x 3 root root 38984 Jul 10 2019 bzcat - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzcmp -> bzdiff - -rwxr-xr-x 1 root root 2227 Jul 10 2019 bzdiff - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzegrep -> bzgrep - -rwxr-xr-x 1 root root 4877 Jun 24 2019 bzexe - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzfgrep -> bzgrep - -rwxr-xr-x 1 root root 3641 Jul 10 2019 bzgrep - -rwxr-xr-x 3 root root 38984 Jul 10 2019 bzip2 - -rwxr-xr-x 1 root root 14328 Jul 10 2019 bzip2recover - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzless -> bzmore - -rwxr-xr-x 1 root root 1297 Jul 10 2019 bzmore - -rwxr-xr-x 1 root root 43744 Feb 28 2019 cat - -rwxr-xr-x 1 root root 64320 Feb 28 2019 chgrp - -rwxr-xr-x 1 root root 64288 Feb 28 2019 chmod - -rwxr-xr-x 1 root root 72512 Feb 28 2019 chown - -rwxr-xr-x 1 root root 146880 Feb 28 2019 cp - -rwxr-xr-x 1 root root 121464 Jan 17 2019 dash - -rwxr-xr-x 1 root root 109408 Feb 28 2019 date - -rwxr-xr-x 1 root root 76712 Feb 28 2019 dd - -rwxr-xr-x 1 root root 93744 Feb 28 2019 df - -rwxr-xr-x 1 root root 138856 Feb 28 2019 dir - -rwxr-xr-x 1 root root 84288 Jan 9 2019 dmesg - lrwxrwxrwx 1 root root 8 Sep 26 2018 dnsdomainname -> hostname - lrwxrwxrwx 1 root root 8 Sep 26 2018 domainname -> hostname - -rwxr-xr-x 1 root root 39520 Feb 28 2019 echo - -rwxr-xr-x 1 root root 28 Jan 7 2019 egrep - -rwxr-xr-x 1 root root 35424 Feb 28 2019 false - -rwxr-xr-x 1 root root 28 Jan 7 2019 fgrep - -rwxr-xr-x 1 root root 68880 Jan 9 2019 findmnt - -rwsr-xr-x 1 root root 34896 Apr 22 2020 fusermount - -rwxr-xr-x 1 root root 198976 Jan 7 2019 grep - -rwxr-xr-x 2 root root 2345 Jan 5 2019 gunzip - -rwxr-xr-x 1 root root 6375 Jan 5 2019 gzexe - -rwxr-xr-x 1 root root 98048 Jan 5 2019 gzip - -rwxr-xr-x 1 root root 26696 Sep 26 2018 hostname - -rwxr-xr-x 1 root root 68552 Feb 28 2019 ln - -rwxr-xr-x 1 root root 56760 Jul 26 2018 login - -rwxr-xr-x 1 root root 138856 Feb 28 2019 ls - -rwxr-xr-x 1 root root 108624 Jan 9 2019 lsblk - -rwxr-xr-x 1 root root 89088 Feb 28 2019 mkdir - -rwxr-xr-x 1 root root 68544 Feb 28 2019 mknod - -rwxr-xr-x 1 root root 43808 Feb 28 2019 mktemp - -rwxr-xr-x 1 root root 43008 Jan 9 2019 more - -rwsr-xr-x 1 root root 51280 Jan 9 2019 mount - -rwxr-xr-x 1 root root 14408 Jan 9 2019 mountpoint - -rwxr-xr-x 1 root root 138728 Feb 28 2019 mv - lrwxrwxrwx 1 root root 8 Sep 26 2018 nisdomainname -> hostname - lrwxrwxrwx 1 root root 14 Feb 14 2019 pidof -> /sbin/killall5 - -rwxr-xr-x 1 root root 39616 Feb 28 2019 pwd - lrwxrwxrwx 1 root root 4 Apr 17 2019 rbash -> bash - -rwxr-xr-x 1 root root 47776 Feb 28 2019 readlink - -rwxr-xr-x 1 root root 68416 Feb 28 2019 rm - -rwxr-xr-x 1 root root 47776 Feb 28 2019 rmdir - -rwxr-xr-x 1 root root 23312 Jan 21 2019 run-parts - -rwxr-xr-x 1 root root 122224 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Sep 9 02:47 sh -> dash - -rwxr-xr-x 1 root root 39552 Feb 28 2019 sleep - -rwxr-xr-x 1 root root 80672 Feb 28 2019 stty - -rwsr-xr-x 1 root root 63568 Jan 9 2019 su - -rwxr-xr-x 1 root root 35488 Feb 28 2019 sync - -rwxr-xr-x 1 root root 445560 Apr 23 2019 tar - -rwxr-xr-x 1 root root 14440 Jan 21 2019 tempfile - -rwxr-xr-x 1 root root 97152 Feb 28 2019 touch - -rwxr-xr-x 1 root root 35424 Feb 28 2019 true - -rwxr-xr-x 1 root root 14328 Apr 22 2020 ulockmgr_server - -rwsr-xr-x 1 root root 34888 Jan 9 2019 umount - -rwxr-xr-x 1 root root 39584 Feb 28 2019 uname - -rwxr-xr-x 2 root root 2345 Jan 5 2019 uncompress - -rwxr-xr-x 1 root root 138856 Feb 28 2019 vdir - -rwxr-xr-x 1 root root 34896 Jan 9 2019 wdctl - -rwxr-xr-x 1 root root 946 Jan 21 2019 which - lrwxrwxrwx 1 root root 8 Sep 26 2018 ypdomainname -> hostname - -rwxr-xr-x 1 root root 1983 Jan 5 2019 zcat - -rwxr-xr-x 1 root root 1677 Jan 5 2019 zcmp - -rwxr-xr-x 1 root root 5879 Jan 5 2019 zdiff - -rwxr-xr-x 1 root root 29 Jan 5 2019 zegrep - -rwxr-xr-x 1 root root 29 Jan 5 2019 zfgrep - -rwxr-xr-x 1 root root 2080 Jan 5 2019 zforce - -rwxr-xr-x 1 root root 7584 Jan 5 2019 zgrep - -rwxr-xr-x 1 root root 2205 Jan 5 2019 zless - -rwxr-xr-x 1 root root 1841 Jan 5 2019 zmore - -rwxr-xr-x 1 root root 4552 Jan 5 2019 znew -I: user script /srv/workspace/pbuilder/40510/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1168776 Apr 18 2019 bash + -rwxr-xr-x 3 root root 38984 Jul 11 2019 bunzip2 + -rwxr-xr-x 3 root root 38984 Jul 11 2019 bzcat + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzcmp -> bzdiff + -rwxr-xr-x 1 root root 2227 Jul 11 2019 bzdiff + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzegrep -> bzgrep + -rwxr-xr-x 1 root root 4877 Jun 25 2019 bzexe + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzfgrep -> bzgrep + -rwxr-xr-x 1 root root 3641 Jul 11 2019 bzgrep + -rwxr-xr-x 3 root root 38984 Jul 11 2019 bzip2 + -rwxr-xr-x 1 root root 14328 Jul 11 2019 bzip2recover + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzless -> bzmore + -rwxr-xr-x 1 root root 1297 Jul 11 2019 bzmore + -rwxr-xr-x 1 root root 43744 Mar 1 2019 cat + -rwxr-xr-x 1 root root 64320 Mar 1 2019 chgrp + -rwxr-xr-x 1 root root 64288 Mar 1 2019 chmod + -rwxr-xr-x 1 root root 72512 Mar 1 2019 chown + -rwxr-xr-x 1 root root 146880 Mar 1 2019 cp + -rwxr-xr-x 1 root root 121464 Jan 18 2019 dash + -rwxr-xr-x 1 root root 109408 Mar 1 2019 date + -rwxr-xr-x 1 root root 76712 Mar 1 2019 dd + -rwxr-xr-x 1 root root 93744 Mar 1 2019 df + -rwxr-xr-x 1 root root 138856 Mar 1 2019 dir + -rwxr-xr-x 1 root root 84288 Jan 10 2019 dmesg + lrwxrwxrwx 1 root root 8 Sep 27 2018 dnsdomainname -> hostname + lrwxrwxrwx 1 root root 8 Sep 27 2018 domainname -> hostname + -rwxr-xr-x 1 root root 39520 Mar 1 2019 echo + -rwxr-xr-x 1 root root 28 Jan 8 2019 egrep + -rwxr-xr-x 1 root root 35424 Mar 1 2019 false + -rwxr-xr-x 1 root root 28 Jan 8 2019 fgrep + -rwxr-xr-x 1 root root 68880 Jan 10 2019 findmnt + -rwsr-xr-x 1 root root 34896 Apr 23 2020 fusermount + -rwxr-xr-x 1 root root 198976 Jan 8 2019 grep + -rwxr-xr-x 2 root root 2345 Jan 6 2019 gunzip + -rwxr-xr-x 1 root root 6375 Jan 6 2019 gzexe + -rwxr-xr-x 1 root root 98048 Jan 6 2019 gzip + -rwxr-xr-x 1 root root 26696 Sep 27 2018 hostname + -rwxr-xr-x 1 root root 68552 Mar 1 2019 ln + -rwxr-xr-x 1 root root 56760 Jul 27 2018 login + -rwxr-xr-x 1 root root 138856 Mar 1 2019 ls + -rwxr-xr-x 1 root root 108624 Jan 10 2019 lsblk + -rwxr-xr-x 1 root root 89088 Mar 1 2019 mkdir + -rwxr-xr-x 1 root root 68544 Mar 1 2019 mknod + -rwxr-xr-x 1 root root 43808 Mar 1 2019 mktemp + -rwxr-xr-x 1 root root 43008 Jan 10 2019 more + -rwsr-xr-x 1 root root 51280 Jan 10 2019 mount + -rwxr-xr-x 1 root root 14408 Jan 10 2019 mountpoint + -rwxr-xr-x 1 root root 138728 Mar 1 2019 mv + lrwxrwxrwx 1 root root 8 Sep 27 2018 nisdomainname -> hostname + lrwxrwxrwx 1 root root 14 Feb 15 2019 pidof -> /sbin/killall5 + -rwxr-xr-x 1 root root 39616 Mar 1 2019 pwd + lrwxrwxrwx 1 root root 4 Apr 18 2019 rbash -> bash + -rwxr-xr-x 1 root root 47776 Mar 1 2019 readlink + -rwxr-xr-x 1 root root 68416 Mar 1 2019 rm + -rwxr-xr-x 1 root root 47776 Mar 1 2019 rmdir + -rwxr-xr-x 1 root root 23312 Jan 22 2019 run-parts + -rwxr-xr-x 1 root root 122224 Dec 23 2018 sed + lrwxrwxrwx 1 root root 4 Aug 10 03:16 sh -> bash + lrwxrwxrwx 1 root root 4 Aug 7 22:25 sh.distrib -> dash + -rwxr-xr-x 1 root root 39552 Mar 1 2019 sleep + -rwxr-xr-x 1 root root 80672 Mar 1 2019 stty + -rwsr-xr-x 1 root root 63568 Jan 10 2019 su + -rwxr-xr-x 1 root root 35488 Mar 1 2019 sync + -rwxr-xr-x 1 root root 445560 Apr 24 2019 tar + -rwxr-xr-x 1 root root 14440 Jan 22 2019 tempfile + -rwxr-xr-x 1 root root 97152 Mar 1 2019 touch + -rwxr-xr-x 1 root root 35424 Mar 1 2019 true + -rwxr-xr-x 1 root root 14328 Apr 23 2020 ulockmgr_server + -rwsr-xr-x 1 root root 34888 Jan 10 2019 umount + -rwxr-xr-x 1 root root 39584 Mar 1 2019 uname + -rwxr-xr-x 2 root root 2345 Jan 6 2019 uncompress + -rwxr-xr-x 1 root root 138856 Mar 1 2019 vdir + -rwxr-xr-x 1 root root 34896 Jan 10 2019 wdctl + -rwxr-xr-x 1 root root 946 Jan 22 2019 which + lrwxrwxrwx 1 root root 8 Sep 27 2018 ypdomainname -> hostname + -rwxr-xr-x 1 root root 1983 Jan 6 2019 zcat + -rwxr-xr-x 1 root root 1677 Jan 6 2019 zcmp + -rwxr-xr-x 1 root root 5879 Jan 6 2019 zdiff + -rwxr-xr-x 1 root root 29 Jan 6 2019 zegrep + -rwxr-xr-x 1 root root 29 Jan 6 2019 zfgrep + -rwxr-xr-x 1 root root 2080 Jan 6 2019 zforce + -rwxr-xr-x 1 root root 7584 Jan 6 2019 zgrep + -rwxr-xr-x 1 root root 2205 Jan 6 2019 zless + -rwxr-xr-x 1 root root 1841 Jan 6 2019 zmore + -rwxr-xr-x 1 root root 4552 Jan 6 2019 znew +I: user script /srv/workspace/pbuilder/32824/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -434,7 +468,7 @@ Get: 226 http://deb.debian.org/debian buster/main amd64 xdg-utils all 1.1.3-1+deb10u1 [73.7 kB] Get: 227 http://deb.debian.org/debian buster/main amd64 texlive-base all 2018.20190227-2 [19.7 MB] Get: 228 http://deb.debian.org/debian buster/main amd64 texlive-latex-base all 2018.20190227-2 [984 kB] -Fetched 170 MB in 2s (75.7 MB/s) +Fetched 170 MB in 2s (69.7 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package install-info. (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 ... 19195 files and directories currently installed.) @@ -1414,7 +1448,7 @@ fakeroot is already the newest version (1.23-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/hol88-2.02.19940316/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b +I: Running cd /build/hol88-2.02.19940316/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316-35 dpkg-buildpackage: info: source distribution unstable @@ -1806,7 +1840,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/hol88-2.02.19940316' date -Sun Sep 11 07:32:33 -12 2022 +Tue Aug 10 03:17:32 +14 2021 /usr/bin/make hol make[2]: Entering directory '/build/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2980,7 +3014,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 # mem = - : (* -> * list -> bool) @@ -3118,7 +3152,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #.............start address -T 0xb8ee00 () : void @@ -3277,7 +3311,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #.............start address -T 0xb8ee00 () : void @@ -3469,7 +3503,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 # concat = - : (string -> string -> string) @@ -3575,7 +3609,7 @@ start address -T 0xb85ea0 ;; Finished loading "lisp/f-ol-net" start address -T 0x9eb060 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 11/9/22 + version 2.02 (GCL) created 10/8/21 #...start address -T 0xb92030 () : void @@ -3888,7 +3922,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_PPLAMB.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 ###########################() : void @@ -3901,7 +3935,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_bool.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 ################################################################################################() : void @@ -4046,7 +4080,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_ind.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 ############################() : void @@ -4089,7 +4123,7 @@ /build/hol88-2.02.19940316/hol-lcf < /build/hol88-2.02.19940316/theories/mk_BASIC-HOL.ml;\ cd /build/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 ############################Theory ind loaded () : void @@ -4126,7 +4160,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4167,7 +4201,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -4569,7 +4603,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -4637,7 +4671,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -4842,7 +4876,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -4966,7 +5000,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5052,7 +5086,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5145,7 +5179,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5214,7 +5248,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5319,7 +5353,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5554,7 +5588,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5580,7 +5614,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5708,7 +5742,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5756,7 +5790,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5823,7 +5857,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5882,7 +5916,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -5938,7 +5972,7 @@ 'lisp `(setup)`;;' >foo1 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(ml-save "basic-hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo1") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "basic-hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(ml-save \"basic-hol\")(quit))" "" nil)(with-open-file (s "bm.l" :direction :output) (prin1 si::*binary-modules* s))(quit))`;;' | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5951,7 +5985,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #() : void @@ -6003,7 +6037,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_combin.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ##########################() : void @@ -6034,7 +6068,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_num.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ##############################() : void @@ -6121,7 +6155,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_prim_rec.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #######################################################################() : void @@ -6274,7 +6308,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_fun.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ###########################() : void @@ -6309,7 +6343,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_arith_thms.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #############################() : void @@ -6370,7 +6404,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ###########################Theory arithmetic loaded () : void @@ -6865,7 +6899,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_list_thms.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ##################################() : void @@ -7012,7 +7046,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #################################Theory list loaded () : void @@ -7351,7 +7385,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ###############################Theory list loaded () : void @@ -8848,7 +8882,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_tree.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #############################() : void @@ -9232,7 +9266,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_ltree.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ############################() : void @@ -9530,7 +9564,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_tydefs.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ############################() : void @@ -9670,7 +9704,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_sum.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ############################################() : void @@ -9767,7 +9801,7 @@ /build/hol88-2.02.19940316/basic-hol < /build/hol88-2.02.19940316/theories/mk_one.ml;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 ##################################() : void @@ -9797,7 +9831,7 @@ | /build/hol88-2.02.19940316/basic-hol;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -9814,7 +9848,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #Theory num loaded () : void @@ -9833,7 +9867,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -9990,7 +10024,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 # @@ -10028,7 +10062,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 # @@ -10062,7 +10096,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -10147,7 +10181,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -10188,7 +10222,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -10372,7 +10406,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 # define_load_lib_function = - : (string list -> void -> void) @@ -10446,7 +10480,7 @@ 'lisp `(setup)`;;' >foo2 echo 'lisp `(throw (quote eof) t)`;; #+native-reloc(progn (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(ml-save "hol")) #-native-reloc(let ((si::*collect-binary-modules* t)(si::*binary-modules* (with-open-file (s "bm.l") (read s)))) (with-open-file (s "foo2") (let ((*standard-input* s)) (tml)))(compiler::link (remove-duplicates si::*binary-modules* :test (function equal)) "hol" "(progn (load \"debian/gcl_patch.l\")(load \"foo\")(with-open-file (s \"foo1\") (let ((*standard-input* s)) (tml)))(with-open-file (s \"foo2\") (let ((*standard-input* s)) (tml)))(ml-save \"hol\")(quit))" "" nil)(quit))`;;' | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10459,7 +10493,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #() : void @@ -10523,11 +10557,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Sun Sep 11 07:34:33 -12 2022 +Tue Aug 10 03:19:20 +14 2021 /usr/bin/make library make[2]: Entering directory '/build/hol88-2.02.19940316' date -Sun Sep 11 07:34:33 -12 2022 +Tue Aug 10 03:19:20 +14 2021 (cd /build/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10550,7 +10584,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -10634,7 +10668,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -10740,7 +10774,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11490,7 +11524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11513,7 +11547,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11556,7 +11590,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11592,7 +11626,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11644,7 +11678,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11676,7 +11710,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11714,7 +11748,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11742,7 +11776,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11819,7 +11853,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11841,7 +11875,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11895,7 +11929,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -11944,7 +11978,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12095,7 +12129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12139,7 +12173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12214,7 +12248,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12264,7 +12298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12327,7 +12361,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12380,7 +12414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12426,7 +12460,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12514,7 +12548,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12552,7 +12586,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12613,7 +12647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12677,7 +12711,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12703,7 +12737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12728,7 +12762,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12767,7 +12801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -12843,7 +12877,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13580,7 +13614,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13603,7 +13637,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13646,7 +13680,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13681,7 +13715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13722,7 +13756,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13785,7 +13819,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13808,7 +13842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13833,7 +13867,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13860,7 +13894,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -13896,7 +13930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14428,7 +14462,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14451,7 +14485,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14485,7 +14519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14540,7 +14574,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14631,7 +14665,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -14800,7 +14834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -15033,7 +15067,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -15043,7 +15077,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (!n. ?f. !x. l(ms x,n) ==> (f x = h f x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -15119,11 +15153,11 @@ Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -15175,14 +15209,14 @@ ORDINAL_CHAINED = |- !l m. ordinal l /\ ordinal m ==> m inseg l \/ l inseg m -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 997 FL_SUC = |- !l a. fl(\(x,y). l(x,y) \/ (y = a) /\ (fl l x \/ (x = a)))x = fl l x \/ (x = a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -15253,7 +15287,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1083 () : void @@ -15272,7 +15306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -15403,7 +15437,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -15495,7 +15529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -15587,12 +15621,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sun Sep 11 07:35:19 -12 2022 +===> abs_theory rebuilt on Tue Aug 10 03:20:06 +14 2021 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -15765,7 +15799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -16029,11 +16063,11 @@ |- !h i j. (h trat_mul (i trat_add j)) trat_eq ((h trat_mul i) trat_add (h trat_mul j)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 @@ -16202,7 +16236,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -16520,7 +16554,7 @@ Intermediate theorems generated: 42 CUT_UBOUND = |- !X x y. ~cut X x /\ x hrat_lt y ==> ~cut X y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y @@ -16633,7 +16667,7 @@ |- !X Y Z. X hreal_mul (Y hreal_add Z) = (X hreal_mul Y) hreal_add (X hreal_mul Z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 HREAL_MUL_LID = |- !X. hreal_1 hreal_mul X = X @@ -16702,7 +16736,7 @@ File hreal.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 10456 #\ @@ -16712,7 +16746,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -17057,7 +17091,7 @@ TREAL_LT_ADD = |- !x y z. y treal_lt z ==> (x treal_add y) treal_lt (x treal_add z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1045 TREAL_LT_MUL = @@ -17125,7 +17159,7 @@ TREAL_LT_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_lt y = x2 treal_lt y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 519 TREAL_LT_WELLDEFL = @@ -17171,7 +17205,7 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -17205,7 +17239,7 @@ SUP_ALLPOS_LEMMA4 = |- !y. ~r0 real_lt y ==> (!x. y real_lt (real_of_hreal x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 75 Theorem HREAL_SUP autoloading from theory `HREAL` ... @@ -17260,7 +17294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -17536,7 +17570,7 @@ Intermediate theorems generated: 54 REAL_LT_RADD = |- !x y z. (x + z) < (y + z) = x < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 REAL_NOT_LT = |- !x y. ~x < y = y <= x @@ -17548,7 +17582,7 @@ Intermediate theorems generated: 24 REAL_LT_GT = |- !x y. x < y ==> ~y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 26 REAL_NOT_LE = |- !x y. ~x <= y = y < x @@ -17668,7 +17702,7 @@ Intermediate theorems generated: 22 REAL_LT_ADD = |- !x y. (& 0) < x /\ (& 0) < y ==> (& 0) < (x + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 REAL_LT_ADDNEG = |- !x y z. y < (x + (-- z)) = (y + z) < x @@ -17804,7 +17838,7 @@ Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17845,7 +17879,7 @@ Theorem NOT_LESS autoloading from theory `arithmetic` ... NOT_LESS = |- !m n. ~m num_lt n = n num_le m -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... LESS_EQ_MONO = |- !n m. (SUC n) num_le (SUC m) = n num_le m @@ -17946,7 +17980,7 @@ Run time: 0.0s REAL_LT_MULTIPLE = |- !n d. 1 num_lt n ==> (d < ((& n) * d) = (& 0) < d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) @@ -18003,7 +18037,7 @@ Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -18190,7 +18224,7 @@ Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) @@ -18219,7 +18253,7 @@ Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 @@ -18260,7 +18294,7 @@ Intermediate theorems generated: 105 ABS_ABS = |- !x. abs(abs x) = abs x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 27 ABS_LE = |- !x. x <= (abs x) @@ -18293,7 +18327,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -18335,7 +18369,7 @@ Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 @@ -18372,7 +18406,7 @@ Intermediate theorems generated: 152 POW_1 = |- !x. x pow 1 = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x @@ -18404,7 +18438,7 @@ Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -18466,7 +18500,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) @@ -18537,7 +18571,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18652,7 +18686,7 @@ SUM_NSUB = |- !n f c. (Sum(0,n)f) - ((& n) * c) = Sum(0,n)(\p. (f p) - c) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 239 Theorem LESS_SUC autoloading from theory `prim_rec` ... @@ -18672,7 +18706,7 @@ Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) @@ -18739,13 +18773,13 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2469 SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 () : void @@ -18755,7 +18789,7 @@ File real.ml loaded () : void -Run time: 1.5s +Run time: 1.2s Intermediate theorems generated: 23746 #\ @@ -18765,7 +18799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -18970,7 +19004,7 @@ Intermediate theorems generated: 2 CLOSED_LIMPT = |- !top S. closed top S = (!x. limpt top x S ==> S x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 433 ismet = @@ -19006,7 +19040,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 560 metric_tybij = @@ -19178,7 +19212,7 @@ Run time: 0.0s MR1_ADD = |- !x d. dist mr1(x,x + d) = abs d -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 Theorem REAL_SUB_SUB autoloading from theory `REAL` ... @@ -19249,7 +19283,7 @@ File topology.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 4132 #\ @@ -19259,7 +19293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -19513,7 +19547,7 @@ Theorem REAL_NOT_LT autoloading from theory `REAL` ... REAL_NOT_LT = |- !x y. ~x < y = y <= x -Run time: 0.0s +Run time: 0.1s Theorem REAL_HALF_DOUBLE autoloading from theory `REAL` ... REAL_HALF_DOUBLE = |- !x. (x / (& 2)) + (x / (& 2)) = x @@ -19573,7 +19607,7 @@ (!x. (& 0) < (dist m1(x,x0)) /\ (dist m1(x,x0)) <= d ==> (dist m2(f x,y0)) < e)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 459 Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... @@ -19830,7 +19864,7 @@ (!x x0 y y0. (x --> x0)(mtop mr1,g) /\ (y --> y0)(mtop mr1,g) ==> ((\n. (x n) + (y n)) --> (x0 + y0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 167 Theorem REAL_SUB_NEG2 autoloading from theory `REAL` ... @@ -19994,7 +20028,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -20319,7 +20353,7 @@ Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 182 mono = @@ -20353,7 +20387,7 @@ MONO_SUC = |- !f. mono f = (!n. (f(SUC n)) >= (f n)) \/ (!n. (f(SUC n)) <= (f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 528 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -20567,7 +20601,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20617,7 +20651,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20799,7 +20833,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20930,7 +20964,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -21002,7 +21036,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) < (f m)) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 209 Theorem LESS_REFL autoloading from theory `prim_rec` ... @@ -21093,7 +21127,7 @@ Run time: 0.0s SER_CMUL = |- !x x0 c. x sums x0 ==> (\n. c * (x n)) sums (c * x0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 82 Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... @@ -21178,7 +21212,7 @@ Run time: 0.0s SER_ACONV = |- !f. summable(\n. abs(f n)) ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 126 Theorem SUM_ABS_LE autoloading from theory `REAL` ... @@ -21288,7 +21322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -22018,7 +22052,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -22175,7 +22209,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22322,7 +22356,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -22372,7 +22406,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22381,7 +22415,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -22414,7 +22448,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -22676,7 +22710,7 @@ |- !n x y. Sum(0,SUC n)(\p. (x pow p) * (y pow (n num_sub p))) = Sum(0,SUC n)(\p. (x pow (n num_sub p)) * (y pow p)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 235 Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... @@ -23286,7 +23320,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -23388,7 +23422,7 @@ Theorem MULT_SYM autoloading from theory `arithmetic` ... MULT_SYM = |- !m n. m * n = n * m -Run time: 0.1s +Run time: 0.0s MULT_DIV_2 = |- !n. (2 * n) DIV 2 = n Run time: 0.0s @@ -23897,7 +23931,7 @@ Intermediate theorems generated: 144 DIFF_SIN = |- !x. (sin diffl (cos x))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 200 Theorem DIFFS_NEG autoloading from theory `POWSER` ... @@ -23948,7 +23982,7 @@ Run time: 0.0s EXP_0 = |- exp(& 0) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 274 Theorem REAL_LE_REFL autoloading from theory `REAL` ... @@ -24410,7 +24444,7 @@ Theorem REAL_SUMSQ autoloading from theory `REAL` ... REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) -Run time: 0.0s +Run time: 0.1s SIN_ADD = |- !x y. sin(x + y) = ((sin x) * (cos y)) + ((cos x) * (sin y)) @@ -24501,7 +24535,7 @@ Theorem REAL_LT_RMUL_IMP autoloading from theory `REAL` ... REAL_LT_RMUL_IMP = |- !x y z. x < y /\ (& 0) < z ==> (x * z) < (y * z) -Run time: 0.1s +Run time: 0.0s Theorem SER_POS_LT autoloading from theory `SEQ` ... SER_POS_LT = @@ -24815,7 +24849,7 @@ (cos x = & 0) = (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. ~EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 630 Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... @@ -24894,7 +24928,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24940,7 +24974,7 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1046 TAN_TOTAL_POS = @@ -25039,7 +25073,7 @@ (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) /\ (tan(atn y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y @@ -25047,7 +25081,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 TAN_ATN = @@ -25062,7 +25096,7 @@ File transc.ml loaded () : void -Run time: 1.0s +Run time: 0.8s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/hol88-2.02.19940316/Library/reals/theories' @@ -25075,7 +25109,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25097,7 +25131,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25163,7 +25197,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25195,7 +25229,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25304,7 +25338,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25457,7 +25491,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25530,7 +25564,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25610,7 +25644,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25767,7 +25801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -25922,7 +25956,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26139,7 +26173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26161,7 +26195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26180,7 +26214,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26225,7 +26259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26290,7 +26324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26340,7 +26374,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26410,7 +26444,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26480,7 +26514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26516,7 +26550,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26569,7 +26603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26641,7 +26675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26720,7 +26754,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26915,7 +26949,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -26952,7 +26986,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -27638,7 +27672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -28110,7 +28144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -28374,7 +28408,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -28619,7 +28653,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29083,7 +29117,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29551,7 +29585,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29607,7 +29641,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29697,7 +29731,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29896,7 +29930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -29928,7 +29962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30062,7 +30096,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30365,7 +30399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30397,7 +30431,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30436,7 +30470,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30468,7 +30502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30629,7 +30663,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30762,7 +30796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -30951,7 +30985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31011,7 +31045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31136,7 +31170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31247,7 +31281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31272,7 +31306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31300,7 +31334,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31413,7 +31447,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -31916,7 +31950,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -32164,7 +32198,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -32390,7 +32424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -32432,7 +32466,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -32464,7 +32498,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -32687,7 +32721,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -33080,7 +33114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -33193,7 +33227,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -33696,7 +33730,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -33944,7 +33978,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34170,7 +34204,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34205,7 +34239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34244,7 +34278,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34281,7 +34315,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34302,7 +34336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34399,7 +34433,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34421,7 +34455,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34917,7 +34951,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -34940,7 +34974,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35018,7 +35052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35077,7 +35111,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35121,7 +35155,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35139,7 +35173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35166,7 +35200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35210,7 +35244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35323,7 +35357,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35370,7 +35404,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35409,7 +35443,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35483,7 +35517,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35572,7 +35606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35643,7 +35677,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35713,7 +35747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35762,7 +35796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35803,7 +35837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35844,7 +35878,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35868,7 +35902,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35969,7 +36003,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -35990,7 +36024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36015,7 +36049,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36641,7 +36675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36718,7 +36752,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36745,7 +36779,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36862,7 +36896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -36957,7 +36991,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37043,7 +37077,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37158,7 +37192,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37251,7 +37285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37427,7 +37461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37531,7 +37565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37826,7 +37860,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37929,7 +37963,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -37997,7 +38031,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38059,7 +38093,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38239,7 +38273,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38280,7 +38314,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38310,7 +38344,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38336,7 +38370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -38854,7 +38888,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -39391,7 +39425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -39579,7 +39613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #false : bool @@ -39597,10 +39631,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/hol88-2.02.19940316/Library' date -Sun Sep 11 07:37:58 -12 2022 +Tue Aug 10 03:22:38 +14 2021 make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Sun Sep 11 07:37:58 -12 2022 +Tue Aug 10 03:22:38 +14 2021 make permissions make[2]: Entering directory '/build/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39620,20 +39654,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/9/22 + HOL88 Version 2.02 (GCL), built on 10/8/21 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 11/9/22 +BASIC-HOL version 2.02 (GCL) created 10/8/21 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -HOL-LCF version 2.02 (GCL) created 11/9/22 +HOL-LCF version 2.02 (GCL) created 10/8/21 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -39980,7 +40014,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (112 pages, 310280 bytes). +Output written on tutorial.dvi (112 pages, 310272 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Tutorial' @@ -40089,7 +40123,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (114 pages, 332088 bytes). +Output written on tutorial.dvi (114 pages, 332080 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Tutorial' @@ -41362,12 +41396,12 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 995628 bytes). +Output written on description.dvi (346 pages, 995620 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: ../LaTeX/makeindex: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -41572,7 +41606,7 @@ (./drules.aux) (./conv.aux) (./tactics.aux) (./see.aux) (./references.aux) (./version2.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on description.dvi (353 pages, 1078856 bytes). +Output written on description.dvi (353 pages, 1078848 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Description' @@ -43124,12 +43158,12 @@ (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1132384 bytes). +Output written on reference.dvi (669 pages, 1132372 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' make[4]: Entering directory '/build/hol88-2.02.19940316/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: ../LaTeX/makeindex: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44655,7 +44689,7 @@ (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1136852 bytes). +Output written on reference.dvi (669 pages, 1136848 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Reference' @@ -44870,7 +44904,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45123,7 +45157,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/arith/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45358,7 +45392,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45533,7 +45567,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45719,7 +45753,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45837,7 +45871,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/pair/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45952,7 +45986,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/parser/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46190,7 +46224,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46529,7 +46563,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46734,7 +46768,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47072,7 +47106,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47261,7 +47295,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47527,7 +47561,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/sets/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47686,7 +47720,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/string/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47829,7 +47863,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/taut/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47979,7 +48013,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/trs/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48133,7 +48167,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/unwind/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48309,7 +48343,7 @@ make[6]: Entering directory '/build/hol88-2.02.19940316/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48502,7 +48536,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/window/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48724,7 +48758,7 @@ make[6]: Leaving directory '/build/hol88-2.02.19940316/Library/word/Manual' make[6]: Entering directory '/build/hol88-2.02.19940316/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: ../../../Manual/LaTeX/makeindex: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48915,7 +48949,7 @@ ) (/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd) [1] [2]) (./preface.tex) [3] (./libraries.aux (./title.aux) (./preface.aux)) ) -Output written on libraries.dvi (3 pages, 2244 bytes). +Output written on libraries.dvi (3 pages, 2232 bytes). Transcript written on libraries.log. make[4]: Leaving directory '/build/hol88-2.02.19940316/Manual/Libraries' make[3]: Leaving directory '/build/hol88-2.02.19940316/Manual/Libraries' @@ -48981,7 +49015,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2022.09.11:0738' -> endpages.ps +' TeX output 2021.08.10:0326' -> endpages.ps . @@ -49042,7 +49076,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2022.09.11:0738' -> titlepages.ps +' TeX output 2021.08.10:0326' -> titlepages.ps . @@ -49146,12 +49180,12 @@ dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35_all.deb'. dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35_all.deb'. -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35_all.deb'. make[1]: Leaving directory '/build/hol88-2.02.19940316' dpkg-genbuildinfo --build=binary dpkg-genchanges --build=binary >../hol88_2.02.19940316-35_amd64.changes @@ -49159,12 +49193,14 @@ dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: copying local configuration +I: user script /srv/workspace/pbuilder/32824/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/32824/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/40510 and its subdirectories -I: Current time: Sun Sep 11 07:39:27 -12 2022 -I: pbuilder-time-stamp: 1662925167 +I: removing directory /srv/workspace/pbuilder/32824 and its subdirectories +I: Current time: Tue Aug 10 03:30:29 +14 2021 +I: pbuilder-time-stamp: 1628515829