Diff of the two buildlogs: -- --- b1/build.log 2020-08-25 14:29:32.675828236 +0000 +++ b2/build.log 2020-08-25 14:46:00.721690793 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Mon Sep 27 08:35:46 -12 2021 -I: pbuilder-time-stamp: 1632774946 +I: Current time: Wed Aug 26 04:29:44 +14 2020 +I: pbuilder-time-stamp: 1598365784 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 '/var/lib/jenkins/.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/21747/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/14963/tmp/hooks/D01_modify_environment starting +debug: Running on codethink-sled16-arm64. +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/14963/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/14963/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='arm64' - DEBIAN_FRONTEND='noninteractive' + 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]="aarch64-unknown-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=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=8' - DISTRIBUTION='' - HOME='/var/lib/jenkins' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION= + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/var/lib/jenkins + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - 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='21747' - PS1='# ' - PS2='> ' + LANG=C + LANGUAGE=nl_BE:nl + LC_ALL=C + MACHTYPE=aarch64-unknown-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=14963 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.K2mZO4bmcG/pbuilderrc_r7Vd --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.K2mZO4bmcG/b1 --logfile b1/build.log hol88_2.02.19940316-35.dsc' - SUDO_GID='117' - SUDO_UID='110' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - USERNAME='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.16: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.K2mZO4bmcG/pbuilderrc_ApKQ --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.K2mZO4bmcG/b2 --logfile b2/build.log hol88_2.02.19940316-35.dsc' + SUDO_GID=117 + SUDO_UID=110 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + USERNAME=root + _='I: set' + http_proxy=http://192.168.101.16:3128 I: uname -a - Linux codethink-sled15-arm64 4.4.0-187-generic #217-Ubuntu SMP Tue Jul 21 04:16:35 UTC 2020 aarch64 GNU/Linux + Linux i-capture-the-hostname 4.4.0-187-generic #217-Ubuntu SMP Tue Jul 21 04:16:35 UTC 2020 aarch64 GNU/Linux I: ls -l /bin total 4928 - -rwxr-xr-x 1 root root 1216928 Apr 17 2019 bash - -rwxr-xr-x 3 root root 34808 Jul 10 2019 bunzip2 - -rwxr-xr-x 3 root root 34808 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 34808 Jul 10 2019 bzip2 - -rwxr-xr-x 1 root root 14264 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 35576 Feb 28 2019 cat - -rwxr-xr-x 1 root root 60256 Feb 28 2019 chgrp - -rwxr-xr-x 1 root root 56096 Feb 28 2019 chmod - -rwxr-xr-x 1 root root 64368 Feb 28 2019 chown - -rwxr-xr-x 1 root root 134632 Feb 28 2019 cp - -rwxr-xr-x 1 root root 129536 Jan 17 2019 dash - -rwxr-xr-x 1 root root 97136 Feb 28 2019 date - -rwxr-xr-x 1 root root 76736 Feb 28 2019 dd - -rwxr-xr-x 1 root root 93752 Feb 28 2019 df - -rwxr-xr-x 1 root root 138848 Feb 28 2019 dir - -rwxr-xr-x 1 root root 75984 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 31368 Feb 28 2019 echo - -rwxr-xr-x 1 root root 28 Jan 7 2019 egrep - -rwxr-xr-x 1 root root 27256 Feb 28 2019 false - -rwxr-xr-x 1 root root 28 Jan 7 2019 fgrep - -rwxr-xr-x 1 root root 68792 Jan 9 2019 findmnt - -rwsr-xr-x 1 root root 34824 Apr 22 2020 fusermount - -rwxr-xr-x 1 root root 174304 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 89656 Jan 5 2019 gzip - -rwxr-xr-x 1 root root 18440 Sep 26 2018 hostname - -rwxr-xr-x 1 root root 64472 Feb 28 2019 ln - -rwxr-xr-x 1 root root 52544 Jul 26 2018 login - -rwxr-xr-x 1 root root 138848 Feb 28 2019 ls - -rwxr-xr-x 1 root root 108552 Jan 9 2019 lsblk - -rwxr-xr-x 1 root root 76840 Feb 28 2019 mkdir - -rwxr-xr-x 1 root root 64480 Feb 28 2019 mknod - -rwxr-xr-x 1 root root 39736 Feb 28 2019 mktemp - -rwxr-xr-x 1 root root 38840 Jan 9 2019 more - -rwsr-xr-x 1 root root 47112 Jan 9 2019 mount - -rwxr-xr-x 1 root root 14344 Jan 9 2019 mountpoint - -rwxr-xr-x 1 root root 138736 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 35560 Feb 28 2019 pwd - lrwxrwxrwx 1 root root 4 Apr 17 2019 rbash -> bash - -rwxr-xr-x 1 root root 43712 Feb 28 2019 readlink - -rwxr-xr-x 1 root root 68440 Feb 28 2019 rm - -rwxr-xr-x 1 root root 39624 Feb 28 2019 rmdir - -rwxr-xr-x 1 root root 19144 Jan 21 2019 run-parts - -rwxr-xr-x 1 root root 114016 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Sep 26 02:48 sh -> dash - -rwxr-xr-x 1 root root 31384 Feb 28 2019 sleep - -rwxr-xr-x 1 root root 72480 Feb 28 2019 stty - -rwsr-xr-x 1 root root 59424 Jan 9 2019 su - -rwxr-xr-x 1 root root 31416 Feb 28 2019 sync - -rwxr-xr-x 1 root root 449416 Apr 23 2019 tar - -rwxr-xr-x 1 root root 10560 Jan 21 2019 tempfile - -rwxr-xr-x 1 root root 88968 Feb 28 2019 touch - -rwxr-xr-x 1 root root 27256 Feb 28 2019 true - -rwxr-xr-x 1 root root 14264 Apr 22 2020 ulockmgr_server - -rwsr-xr-x 1 root root 30728 Jan 9 2019 umount - -rwxr-xr-x 1 root root 31384 Feb 28 2019 uname - -rwxr-xr-x 2 root root 2345 Jan 5 2019 uncompress - -rwxr-xr-x 1 root root 138848 Feb 28 2019 vdir - -rwxr-xr-x 1 root root 34824 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/21747/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 1216928 Apr 18 2019 bash + -rwxr-xr-x 3 root root 34808 Jul 11 2019 bunzip2 + -rwxr-xr-x 3 root root 34808 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 34808 Jul 11 2019 bzip2 + -rwxr-xr-x 1 root root 14264 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 35576 Mar 1 2019 cat + -rwxr-xr-x 1 root root 60256 Mar 1 2019 chgrp + -rwxr-xr-x 1 root root 56096 Mar 1 2019 chmod + -rwxr-xr-x 1 root root 64368 Mar 1 2019 chown + -rwxr-xr-x 1 root root 134632 Mar 1 2019 cp + -rwxr-xr-x 1 root root 129536 Jan 18 2019 dash + -rwxr-xr-x 1 root root 97136 Mar 1 2019 date + -rwxr-xr-x 1 root root 76736 Mar 1 2019 dd + -rwxr-xr-x 1 root root 93752 Mar 1 2019 df + -rwxr-xr-x 1 root root 138848 Mar 1 2019 dir + -rwxr-xr-x 1 root root 75984 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 31368 Mar 1 2019 echo + -rwxr-xr-x 1 root root 28 Jan 8 2019 egrep + -rwxr-xr-x 1 root root 27256 Mar 1 2019 false + -rwxr-xr-x 1 root root 28 Jan 8 2019 fgrep + -rwxr-xr-x 1 root root 68792 Jan 10 2019 findmnt + -rwsr-xr-x 1 root root 34824 Apr 23 09:38 fusermount + -rwxr-xr-x 1 root root 174304 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 89656 Jan 6 2019 gzip + -rwxr-xr-x 1 root root 18440 Sep 27 2018 hostname + -rwxr-xr-x 1 root root 64472 Mar 1 2019 ln + -rwxr-xr-x 1 root root 52544 Jul 27 2018 login + -rwxr-xr-x 1 root root 138848 Mar 1 2019 ls + -rwxr-xr-x 1 root root 108552 Jan 10 2019 lsblk + -rwxr-xr-x 1 root root 76840 Mar 1 2019 mkdir + -rwxr-xr-x 1 root root 64480 Mar 1 2019 mknod + -rwxr-xr-x 1 root root 39736 Mar 1 2019 mktemp + -rwxr-xr-x 1 root root 38840 Jan 10 2019 more + -rwsr-xr-x 1 root root 47112 Jan 10 2019 mount + -rwxr-xr-x 1 root root 14344 Jan 10 2019 mountpoint + -rwxr-xr-x 1 root root 138736 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 35560 Mar 1 2019 pwd + lrwxrwxrwx 1 root root 4 Apr 18 2019 rbash -> bash + -rwxr-xr-x 1 root root 43712 Mar 1 2019 readlink + -rwxr-xr-x 1 root root 68440 Mar 1 2019 rm + -rwxr-xr-x 1 root root 39624 Mar 1 2019 rmdir + -rwxr-xr-x 1 root root 19144 Jan 22 2019 run-parts + -rwxr-xr-x 1 root root 114016 Dec 23 2018 sed + lrwxrwxrwx 1 root root 4 Aug 26 04:29 sh -> bash + lrwxrwxrwx 1 root root 4 Aug 24 22:25 sh.distrib -> dash + -rwxr-xr-x 1 root root 31384 Mar 1 2019 sleep + -rwxr-xr-x 1 root root 72480 Mar 1 2019 stty + -rwsr-xr-x 1 root root 59424 Jan 10 2019 su + -rwxr-xr-x 1 root root 31416 Mar 1 2019 sync + -rwxr-xr-x 1 root root 449416 Apr 24 2019 tar + -rwxr-xr-x 1 root root 10560 Jan 22 2019 tempfile + -rwxr-xr-x 1 root root 88968 Mar 1 2019 touch + -rwxr-xr-x 1 root root 27256 Mar 1 2019 true + -rwxr-xr-x 1 root root 14264 Apr 23 09:38 ulockmgr_server + -rwsr-xr-x 1 root root 30728 Jan 10 2019 umount + -rwxr-xr-x 1 root root 31384 Mar 1 2019 uname + -rwxr-xr-x 2 root root 2345 Jan 6 2019 uncompress + -rwxr-xr-x 1 root root 138848 Mar 1 2019 vdir + -rwxr-xr-x 1 root root 34824 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/14963/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -433,7 +467,7 @@ Get: 225 http://deb.debian.org/debian buster/main arm64 xdg-utils all 1.1.3-1+deb10u1 [73.7 kB] Get: 226 http://deb.debian.org/debian buster/main arm64 texlive-base all 2018.20190227-2 [19.7 MB] Get: 227 http://deb.debian.org/debian buster/main arm64 texlive-latex-base all 2018.20190227-2 [984 kB] -Fetched 162 MB in 17s (9447 kB/s) +Fetched 162 MB in 11s (14.1 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 ... 19168 files and directories currently installed.) @@ -1409,7 +1443,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 @@ -1801,7 +1835,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/hol88-2.02.19940316' date -Mon Sep 27 08:37:48 -12 2021 +Wed Aug 26 04:31:59 +14 2020 /usr/bin/make hol make[2]: Entering directory '/build/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2975,7 +3009,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 # mem = - : (* -> * list -> bool) @@ -3113,7 +3147,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #.............start address -T 0xe081a0 () : void @@ -3272,7 +3306,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #.............start address -T 0xe081a0 () : void @@ -3464,7 +3498,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 # concat = - : (string -> string -> string) @@ -3570,7 +3604,7 @@ start address -T 0xdfe350 ;; Finished loading "lisp/f-ol-net" start address -T 0xc65300 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 27/9/21 + version 2.02 (GCL) created 26/8/20 #...start address -T 0xe0a3d0 () : void @@ -3883,7 +3917,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 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 ###########################() : void @@ -3896,7 +3930,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 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 ################################################################################################() : void @@ -4041,7 +4075,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 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 ############################() : void @@ -4084,7 +4118,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 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 ############################Theory ind loaded () : void @@ -4121,7 +4155,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4162,7 +4196,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -4564,7 +4598,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -4632,7 +4666,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -4837,7 +4871,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -4961,7 +4995,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5047,7 +5081,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5140,7 +5174,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5209,7 +5243,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5314,7 +5348,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5549,7 +5583,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5575,7 +5609,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5703,7 +5737,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5751,7 +5785,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5818,7 +5852,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5877,7 +5911,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5933,7 +5967,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 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #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) @@ -5946,7 +5980,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #() : void @@ -5998,7 +6032,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ##########################() : void @@ -6029,7 +6063,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ##############################() : void @@ -6116,7 +6150,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #######################################################################() : void @@ -6269,7 +6303,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ###########################() : void @@ -6304,7 +6338,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #############################() : void @@ -6365,7 +6399,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ###########################Theory arithmetic loaded () : void @@ -6860,7 +6894,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ##################################() : void @@ -7007,7 +7041,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #################################Theory list loaded () : void @@ -7346,7 +7380,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ###############################Theory list loaded () : void @@ -8843,7 +8877,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #############################() : void @@ -9227,7 +9261,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ############################() : void @@ -9525,7 +9559,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ############################() : void @@ -9665,7 +9699,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ############################################() : void @@ -9762,7 +9796,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 ##################################() : void @@ -9792,7 +9826,7 @@ | /build/hol88-2.02.19940316/basic-hol;\ cd /build/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -9809,7 +9843,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #Theory num loaded () : void @@ -9828,7 +9862,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -9985,7 +10019,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 # @@ -10023,7 +10057,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 # @@ -10057,7 +10091,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -10142,7 +10176,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -10183,7 +10217,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -10367,7 +10401,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 # define_load_lib_function = - : (string list -> void -> void) @@ -10441,7 +10475,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 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #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) @@ -10454,7 +10488,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #() : void @@ -10518,11 +10552,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Mon Sep 27 08:42:39 -12 2021 +Wed Aug 26 04:36:10 +14 2020 /usr/bin/make library make[2]: Entering directory '/build/hol88-2.02.19940316' date -Mon Sep 27 08:42:39 -12 2021 +Wed Aug 26 04:36:10 +14 2020 (cd /build/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10545,7 +10579,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -10629,7 +10663,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -10735,7 +10769,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11485,7 +11519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11508,7 +11542,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11551,7 +11585,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11587,7 +11621,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11639,7 +11673,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11671,7 +11705,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11709,7 +11743,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11737,7 +11771,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11814,7 +11848,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11836,7 +11870,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11890,7 +11924,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -11939,7 +11973,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12090,7 +12124,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12134,7 +12168,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12209,7 +12243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12259,7 +12293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12322,7 +12356,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12375,7 +12409,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12421,7 +12455,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12509,7 +12543,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12547,7 +12581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12608,7 +12642,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12672,7 +12706,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12698,7 +12732,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12723,7 +12757,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12762,7 +12796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -12838,7 +12872,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13575,7 +13609,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13598,7 +13632,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13641,7 +13675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13676,7 +13710,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13717,7 +13751,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13780,7 +13814,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13803,7 +13837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13828,7 +13862,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13855,7 +13889,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -13891,7 +13925,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14423,7 +14457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14446,7 +14480,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14480,7 +14514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14535,7 +14569,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14626,7 +14660,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -14795,7 +14829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15028,7 +15062,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 = @@ -15038,7 +15072,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 = @@ -15058,7 +15092,7 @@ (!f g x. (!y. less l(ms y,ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... @@ -15098,7 +15132,7 @@ |- !h ms. (!f g x. (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) @@ -15165,7 +15199,7 @@ woset l /\ fl l a ==> (\(x,y). linseg l a(x,y) \/ (y = a) /\ (fl(linseg l a)x \/ (x = a))) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 489 ORDINAL_CHAINED = @@ -15177,7 +15211,7 @@ |- !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 = @@ -15186,7 +15220,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -15215,21 +15249,21 @@ Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 403 HP = |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2506 ZL = |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -15248,7 +15282,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1083 () : void @@ -15258,7 +15292,7 @@ File mk_wellorder loaded () : void -Run time: 0.9s +Run time: 0.8s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/hol88-2.02.19940316/Library/wellorder' @@ -15267,7 +15301,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15398,7 +15432,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15452,7 +15486,7 @@ IDENTITY_UNIQUE = ... |- !f. (!a. (fn g a f = a) /\ (fn g f a = a)) ==> (f = id g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 144 ":(*)group" : type @@ -15464,7 +15498,7 @@ Intermediate theorems generated: 6 LEFT_CANCELLATION = ... |- !x y a. (fn g a x = fn g a y) ==> (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 67 INVERSE_INVERSE_LEMMA = |- !g. IS_GROUP g ==> (!a. inv g(inv g a) = a) @@ -15490,7 +15524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15544,11 +15578,11 @@ Intermediate theorems generated: 378 |- !f. (!a. (~(a = f) = a) /\ (~(f = a) = a)) ==> ~f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 732 |- !a. I(I a) = a @@ -15582,12 +15616,12 @@ Run time: 0.2s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Mon Sep 27 08:44:34 -12 2021 +===> abs_theory rebuilt on Wed Aug 26 04:38:03 +14 2020 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15747,7 +15781,7 @@ File abs_theory compiled () : void -Run time: 0.0s +Run time: 0.1s make[4]: Leaving directory '/build/hol88-2.02.19940316/Library/abs_theory' make[4]: Entering directory '/build/hol88-2.02.19940316/Library/reals' @@ -15760,7 +15794,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -15940,7 +15974,7 @@ Run time: 0.0s TRAT_EQ_TRANS = |- !p q r. p trat_eq q /\ q trat_eq r ==> p trat_eq r -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 152 TRAT_EQ_AP = |- !p q. (p = q) ==> p trat_eq q @@ -16032,7 +16066,7 @@ Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 Theorem ADD_INV_0_EQ autoloading from theory `arithmetic` ... @@ -16040,7 +16074,7 @@ Run time: 0.0s TRAT_NOZERO = |- !h i. ~(h trat_add i) trat_eq h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... @@ -16197,7 +16231,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -16383,7 +16417,7 @@ HRAT_LT_LADD = |- !x y z. (z hrat_add x) hrat_lt (z hrat_add y) = x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 77 HRAT_LT_RADD = @@ -16399,7 +16433,7 @@ HRAT_LT_LMUL = |- !x y z. (z hrat_mul x) hrat_lt (z hrat_mul y) = x hrat_lt y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 149 HRAT_LT_RMUL = @@ -16519,7 +16553,7 @@ Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 137 Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... @@ -16538,7 +16572,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.0s +Run time: 0.1s Theorem HRAT_ARCH autoloading from theory `HRAT` ... HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16598,7 +16632,7 @@ HREAL_ADD_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 521 HREAL_MUL_ISACUT = @@ -16616,7 +16650,7 @@ HREAL_ADD_ASSOC = |- !X Y Z. X hreal_add (Y hreal_add Z) = (X hreal_add Y) hreal_add Z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 490 HREAL_MUL_ASSOC = @@ -16632,7 +16666,7 @@ Intermediate theorems generated: 935 HREAL_MUL_LID = |- !X. hreal_1 hreal_mul X = X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 @@ -16649,7 +16683,7 @@ Intermediate theorems generated: 2 HREAL_LT_LEMMA = |- !X Y. X hreal_lt Y ==> (?x. ~cut X x /\ cut Y x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 210 HREAL_SUB_ISACUT = @@ -16660,7 +16694,7 @@ HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16687,7 +16721,7 @@ |- !P. (?X. P X) /\ (?Y. !X. P X ==> X hreal_lt Y) ==> (!Y. (?X. P X /\ Y hreal_lt X) = Y hreal_lt (hreal_sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 553 () : void @@ -16707,7 +16741,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -16882,7 +16916,7 @@ |- !x1 x2 y1 y2. x1 hreal_lt y1 /\ x2 hreal_lt y2 ==> (x1 hreal_add x2) hreal_lt (y1 hreal_add y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 HREAL_LT_LADD = @@ -17015,7 +17049,7 @@ Intermediate theorems generated: 217 TREAL_ADD_LINV = |- !x. ((treal_neg x) treal_add x) treal_eq treal_0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 Theorem HREAL_SUB_ADD autoloading from theory `HREAL` ... @@ -17052,14 +17086,14 @@ 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 = |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -17166,12 +17200,12 @@ (!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.2s +Run time: 0.3s Intermediate theorems generated: 7766 REAL_ISO_EQ = |- !h i. h hreal_lt i = (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 98 REAL_POS = |- !X. r0 real_lt (real_of_hreal X) @@ -17255,7 +17289,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -17495,7 +17529,7 @@ Intermediate theorems generated: 18 REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 101 REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -17691,7 +17725,7 @@ Intermediate theorems generated: 20 REAL_SUB_0 = |- !x y. (x - y = & 0) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LE_DOUBLE = |- !x. (& 0) <= (x + x) = (& 0) <= x @@ -17771,7 +17805,7 @@ Intermediate theorems generated: 133 REAL_LT_LMUL_0 = |- !x y. (& 0) < x ==> ((& 0) < (x * y) = (& 0) < y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 87 REAL_LT_RMUL_0 = |- !x y. (& 0) < y ==> ((& 0) < (x * y) = (& 0) < x) @@ -17840,7 +17874,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 @@ -17851,7 +17885,7 @@ Run time: 0.0s REAL_LE = |- !m n. (& m) <= (& n) = m num_le n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -17929,7 +17963,7 @@ REAL_LT_FRACTION_0 = |- !n d. ~(n = 0) ==> ((& 0) < (d / (& n)) = (& 0) < d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 44 Theorem LESS_TRANS autoloading from theory `arithmetic` ... @@ -17994,7 +18028,7 @@ Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) @@ -18053,11 +18087,11 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 < x2 /\ y1 < y2 ==> (x1 * y1) < (x2 * y2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -18104,7 +18138,7 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y @@ -18112,7 +18146,7 @@ Intermediate theorems generated: 36 REAL_MEAN = |- !x y. x < y ==> (?z. x < z /\ z < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) @@ -18153,11 +18187,11 @@ Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) @@ -18202,11 +18236,11 @@ Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) @@ -18276,11 +18310,11 @@ Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) @@ -18395,11 +18429,11 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -18492,13 +18526,13 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 15 REAL_SUP_UBOUND_LE = |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) @@ -18581,11 +18615,11 @@ SUM_ABS = |- !f m n. abs(Sum(m,n)(\m. abs(f m))) = Sum(m,n)(\m. abs(f m)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 105 Theorem ADD_ASSOC autoloading from theory `arithmetic` ... @@ -18677,7 +18711,7 @@ SUM_OFFSET = |- !f n k. Sum(0,n)(\m. f(m num_add k)) = (Sum(0,n num_add k)f) - (Sum(0,k)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 141 SUM_REINDEX = @@ -18760,7 +18794,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -18901,11 +18935,11 @@ L re_universe /\ (!a b. L a /\ L b ==> L(a re_intersect b)) /\ (!P. P re_subset L ==> L(re_Union P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 topology_tydef = |- ?rep. TYPE_DEFINITION istopology rep -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 86 topology_tybij = @@ -19038,7 +19072,7 @@ Run time: 0.0s METRIC_SYM = |- !m x y. dist m(x,y) = dist m(y,x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 99 METRIC_TRIANGLE = @@ -19157,11 +19191,11 @@ Run time: 0.0s ISMET_R1 = |- ismet(\(x,y). abs(y - x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 204 mr1 = |- mr1 = metric(\(x,y). abs(y - x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 MR1_DEF = |- !x y. dist mr1(x,y) = abs(y - x) @@ -19254,7 +19288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -19369,7 +19403,7 @@ dorder g = (!x y. g x x /\ g y y ==> (?z. g z z /\ (!w. g w z ==> g w x /\ g w y))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 tends = @@ -19420,7 +19454,7 @@ (?n. g n n /\ (!m. g m n ==> P m)) /\ (?n. g n n /\ (!m. g m n ==> Q m)) ==> (?n. g n n /\ (!m. g m n ==> P m /\ Q m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 312 DORDER_THEN = - : ((thm -> *) -> thm -> *) @@ -19531,7 +19565,7 @@ dorder g ==> (x --> x0)(mtop d,g) /\ (x --> x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 313 SEQ_TENDS = @@ -19568,7 +19602,7 @@ (!x. (& 0) < (dist m1(x,x0)) /\ (dist m1(x,x0)) <= d ==> (dist m2(f x,y0)) < e)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 459 Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... @@ -19638,7 +19672,7 @@ NET_NULL = |- !g x x0. (x --> x0)(mtop mr1,g) = ((\n. (x n) - x0) --> (& 0))(mtop mr1,g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 151 Theorem LESS_0 autoloading from theory `prim_rec` ... @@ -19767,7 +19801,7 @@ (!x y. bounded(mr1,g)x /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) * (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 484 Theorem REAL_LT_LMUL autoloading from theory `REAL` ... @@ -19922,7 +19956,7 @@ (!x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) --> (inv x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1253 NET_DIV = @@ -19979,7 +20013,7 @@ File nets.ml loaded () : void -Run time: 0.5s +Run time: 0.4s Intermediate theorems generated: 7389 #\ @@ -19989,7 +20023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -20508,7 +20542,7 @@ Theorem REAL_NEGNEG autoloading from theory `REAL` ... REAL_NEGNEG = |- !x. --(-- x) = x -Run time: 0.1s +Run time: 0.0s SEQ_NEG_CONV = |- !f. convergent f = convergent(\n. --(f n)) Run time: 0.0s @@ -20516,7 +20550,7 @@ Theorem ABS_NEG autoloading from theory `REAL` ... ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.0s +Run time: 0.1s SEQ_NEG_BOUNDED = |- !f. bounded(mr1,$num_ge)(\n. --(f n)) = bounded(mr1,$num_ge)f @@ -20612,7 +20646,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20635,7 +20669,7 @@ Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.1s +Run time: 0.0s SEQ_SUC = |- !f l. f --> l = (\n. f(SUC n)) --> l Run time: 0.0s @@ -20949,7 +20983,7 @@ Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 69 Theorem SUM_ZERO autoloading from theory `REAL` ... @@ -20985,7 +21019,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: 220 Theorem Sum autoloading from theory `REAL` ... @@ -21069,7 +21103,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -21173,7 +21207,7 @@ Run time: 0.0s SER_ACONV = |- !f. summable(\n. abs(f n)) ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 126 Theorem SUM_ABS_LE autoloading from theory `REAL` ... @@ -21263,7 +21297,7 @@ c < (& 1) /\ (!n. n num_ge N ==> (abs(f(SUC n))) <= (c * (abs(f n)))) ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 683 () : void @@ -21273,7 +21307,7 @@ File seq.ml loaded () : void -Run time: 1.0s +Run time: 0.9s Intermediate theorems generated: 18704 #\ @@ -21283,7 +21317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -21605,7 +21639,7 @@ LIM_EQUAL = |- !f g l x0. (!x. ~(x = x0) ==> (f x = g x)) ==> ((f --> l)x0 = (g --> l)x0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 171 Theorem REAL_LT_TRANS autoloading from theory `REAL` ... @@ -21652,7 +21686,7 @@ LIM_TRANSFORM = |- !f g x0 l. ((\x. (f x) - (g x)) --> (& 0))x0 /\ (g --> l)x0 ==> (f --> l)x0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 473 diffl = @@ -21813,7 +21847,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21862,7 +21896,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) + (g x)) diffl (l + m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 150 Theorem REAL_MUL_SYM autoloading from theory `REAL` ... @@ -21897,7 +21931,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) * (g x)) diffl ((l * (g x)) + (m * (f x))))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 567 DIFF_CMUL = @@ -22170,7 +22204,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.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22227,7 +22261,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -22236,7 +22270,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -22317,7 +22351,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -22353,7 +22387,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -22367,7 +22401,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 = @@ -22409,7 +22443,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -22514,11 +22548,11 @@ Run time: 0.0s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22671,7 +22705,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.1s +Run time: 0.0s Intermediate theorems generated: 235 Theorem REAL_LT_IMP_NE autoloading from theory `REAL` ... @@ -22980,7 +23014,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -23281,7 +23315,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -23751,7 +23785,7 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.1s +Run time: 0.0s SIN_CONVERGES = |- !x. @@ -23981,7 +24015,7 @@ Run time: 0.0s EXP_LE_X = |- !x. (& 0) <= x ==> ((& 1) + x) <= (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 420 EXP_LT_1 = |- !x. (& 0) < x ==> (& 1) < (exp x) @@ -24078,7 +24112,7 @@ Intermediate theorems generated: 152 EXP_SUB = |- !x y. exp(x - y) = (exp x) / (exp y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 38 Theorem REAL_LT_RMUL autoloading from theory `REAL` ... @@ -24239,7 +24273,7 @@ ROOT_LN = |- !n x. (& 0) < x ==> (!n. root(SUC n)x = exp((ln x) / (&(SUC n)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 282 Theorem REAL_ENTIRE autoloading from theory `REAL` ... @@ -24341,7 +24375,7 @@ Run time: 0.0s SIN_BOUND = |- !x. (abs(sin x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem ABS_BOUNDS autoloading from theory `REAL` ... @@ -24393,7 +24427,7 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -24414,7 +24448,7 @@ COS_ADD = |- !x y. cos(x + y) = ((cos x) * (cos y)) - ((sin x) * (sin y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 Theorem REAL_LNEG_UNIQ autoloading from theory `REAL` ... @@ -24577,7 +24611,7 @@ Definition differentiable autoloading from theory `LIM` ... differentiable = |- !f x. f differentiable x = (?l. (f diffl l)x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem REAL_LT_TOTAL autoloading from theory `REAL` ... @@ -24622,7 +24656,7 @@ Run time: 0.0s PI_POS = |- (& 0) < pi -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 31 Theorem REAL_LT_GT autoloading from theory `REAL` ... @@ -24654,7 +24688,7 @@ Intermediate theorems generated: 66 COS_SIN = |- !x. cos x = sin((pi / (& 2)) - x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 56 SIN_PERIODIC_PI = |- !x. sin(x + pi) = --(sin x) @@ -24700,7 +24734,7 @@ Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -24718,7 +24752,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (& 0) <= x /\ x <= pi /\ (cos x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 766 Theorem REAL_EQ_RADD autoloading from theory `REAL` ... @@ -24794,7 +24828,7 @@ |- !x. (& 0) <= x /\ (sin x = & 0) ==> (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 305 Theorem REAL_NEG_EQ autoloading from theory `REAL` ... @@ -24810,7 +24844,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` ... @@ -24941,7 +24975,7 @@ TAN_TOTAL_POS = |- !y. (& 0) <= y ==> (?x. (& 0) <= x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 372 Theorem POW_NZ autoloading from theory `REAL` ... @@ -24993,7 +25027,7 @@ Intermediate theorems generated: 79 ASN_SIN = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (sin(asn y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 ASN_BOUNDS = @@ -25012,7 +25046,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi /\ (cos(acs y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) @@ -25057,7 +25091,7 @@ File transc.ml loaded () : void -Run time: 1.7s +Run time: 1.6s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/hol88-2.02.19940316/Library/reals/theories' @@ -25070,7 +25104,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25092,7 +25126,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25158,7 +25192,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25190,7 +25224,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25299,7 +25333,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25452,7 +25486,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25525,7 +25559,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25605,7 +25639,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25762,7 +25796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -25917,7 +25951,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26134,7 +26168,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26156,7 +26190,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26175,7 +26209,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26220,7 +26254,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26285,7 +26319,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26335,7 +26369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26405,7 +26439,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26475,7 +26509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26511,7 +26545,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26564,7 +26598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26636,7 +26670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26715,7 +26749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26910,7 +26944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -26947,7 +26981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -27633,7 +27667,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -28105,7 +28139,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -28369,7 +28403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -28614,7 +28648,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29078,7 +29112,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29546,7 +29580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29602,7 +29636,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29692,7 +29726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29891,7 +29925,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -29923,7 +29957,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30057,7 +30091,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30360,7 +30394,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30392,7 +30426,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30431,7 +30465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30463,7 +30497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30624,7 +30658,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30757,7 +30791,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -30946,7 +30980,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31006,7 +31040,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31131,7 +31165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31242,7 +31276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31267,7 +31301,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31295,7 +31329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31408,7 +31442,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -31911,7 +31945,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -32159,7 +32193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -32385,7 +32419,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -32427,7 +32461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -32459,7 +32493,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -32682,7 +32716,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -33075,7 +33109,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -33188,7 +33222,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -33691,7 +33725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -33939,7 +33973,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34165,7 +34199,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34200,7 +34234,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34239,7 +34273,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34276,7 +34310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34297,7 +34331,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34394,7 +34428,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34416,7 +34450,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34912,7 +34946,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -34935,7 +34969,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35013,7 +35047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35072,7 +35106,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35116,7 +35150,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35134,7 +35168,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35161,7 +35195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35205,7 +35239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35318,7 +35352,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35365,7 +35399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35404,7 +35438,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35478,7 +35512,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35567,7 +35601,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35638,7 +35672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35708,7 +35742,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35757,7 +35791,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35798,7 +35832,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35839,7 +35873,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35863,7 +35897,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35964,7 +35998,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -35985,7 +36019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36010,7 +36044,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36636,7 +36670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36713,7 +36747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36740,7 +36774,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36857,7 +36891,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -36952,7 +36986,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37038,7 +37072,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37153,7 +37187,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37246,7 +37280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37422,7 +37456,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37526,7 +37560,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37821,7 +37855,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37924,7 +37958,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -37992,7 +38026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38054,7 +38088,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38234,7 +38268,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38275,7 +38309,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38305,7 +38339,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38331,7 +38365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -38849,7 +38883,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -39386,7 +39420,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -39574,7 +39608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #false : bool @@ -39592,10 +39626,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/hol88-2.02.19940316/Library' date -Mon Sep 27 08:50:42 -12 2021 +Wed Aug 26 04:44:13 +14 2020 make[2]: Leaving directory '/build/hol88-2.02.19940316' date -Mon Sep 27 08:50:42 -12 2021 +Wed Aug 26 04:44:13 +14 2020 make permissions make[2]: Entering directory '/build/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39615,20 +39649,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 27/9/21 + HOL88 Version 2.02 (GCL), built on 26/8/20 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 27/9/21 +BASIC-HOL version 2.02 (GCL) created 26/8/20 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -HOL-LCF version 2.02 (GCL) created 27/9/21 +HOL-LCF version 2.02 (GCL) created 26/8/20 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -39975,7 +40009,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' @@ -40084,7 +40118,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' @@ -41357,12 +41391,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 . @@ -41567,7 +41601,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' @@ -43119,12 +43153,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 . @@ -44650,7 +44684,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' @@ -44865,7 +44899,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 . @@ -45118,7 +45152,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 . @@ -45353,7 +45387,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 . @@ -45528,7 +45562,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 . @@ -45714,7 +45748,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 . @@ -45832,7 +45866,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 . @@ -45947,7 +45981,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 . @@ -46185,7 +46219,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 . @@ -46524,7 +46558,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 . @@ -46729,7 +46763,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 . @@ -47067,7 +47101,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 . @@ -47256,7 +47290,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 . @@ -47522,7 +47556,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 . @@ -47681,7 +47715,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 . @@ -47824,7 +47858,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 . @@ -47974,7 +48008,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 . @@ -48128,7 +48162,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 . @@ -48304,7 +48338,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 . @@ -48497,7 +48531,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 . @@ -48719,7 +48753,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 . @@ -48910,7 +48944,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' @@ -48976,7 +49010,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2021.09.27:0851' -> endpages.ps +' TeX output 2020.08.26:0445' -> endpages.ps . @@ -49037,7 +49071,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 5.998 Copyright 2018 Radical Eye Software (www.radicaleye.com) -' TeX output 2021.09.27:0851' -> titlepages.ps +' TeX output 2020.08.26:0445' -> titlepages.ps . @@ -49140,13 +49174,13 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_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-source' in '../hol88-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-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-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'. make[1]: Leaving directory '/build/hol88-2.02.19940316' dpkg-genbuildinfo --build=binary dpkg-genchanges --build=binary >../hol88_2.02.19940316-35_arm64.changes @@ -49154,12 +49188,14 @@ dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: copying local configuration +I: user script /srv/workspace/pbuilder/14963/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/14963/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/21747 and its subdirectories -I: Current time: Mon Sep 27 08:52:30 -12 2021 -I: pbuilder-time-stamp: 1632775950 +I: removing directory /srv/workspace/pbuilder/14963 and its subdirectories +I: Current time: Wed Aug 26 04:45:59 +14 2020 +I: pbuilder-time-stamp: 1598366759