Diff of the two buildlogs: -- --- b1/build.log 2024-01-07 00:41:29.769701735 +0000 +++ b2/build.log 2024-01-07 01:10:24.325478493 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Jan 6 12:24:02 -12 2024 -I: pbuilder-time-stamp: 1704587042 +I: Current time: Sat Feb 8 21:04:35 +14 2025 +I: pbuilder-time-stamp: 1738998275 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bullseye-reproducible-base.tgz] I: copying local configuration @@ -17,7 +17,7 @@ I: copying [./hol88_2.02.19940316-35.1.debian.tar.xz] I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' -gpgv: keyblock resource '/tmp/dpkg-verify-sig.ytijO5a2/trustedkeys.kbx': General error +gpgv: keyblock resource '/tmp/dpkg-verify-sig.gbOnPJHN/trustedkeys.kbx': General error gpgv: Signature made Tue Jan 5 11:49:56 2021 gpgv: using RSA key B8BF54137B09D35CF026FE9D091AB856069AAA1C gpgv: Can't check signature: No public key @@ -30,49 +30,80 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/4155929/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/D01_modify_environment starting +debug: Running on ionos15-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Feb 8 07:04 /bin/sh -> /bin/bash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all,-fixfilepath parallel=15 ' - DISTRIBUTION='bullseye' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="1" [2]="4" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.1.4(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all,-fixfilepath parallel=16 ' + DIRSTACK=() + DISTRIBUTION=bullseye + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='e66b79abeb624f5da7d01f2458b00ff4' - 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='4155929' - PS1='# ' - PS2='> ' + INVOCATION_ID=8a6f3f55534d43ec9cadb8d67e55be06 + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=2936086 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.o5qHkzFS/pbuilderrc_MHNw --distribution bullseye --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.o5qHkzFS/b1 --logfile b1/build.log hol88_2.02.19940316-35.1.dsc' - SUDO_GID='111' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://78.137.99.97:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.o5qHkzFS/pbuilderrc_hueL --distribution bullseye --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.o5qHkzFS/b2 --logfile b2/build.log hol88_2.02.19940316-35.1.dsc' + SUDO_GID=111 + SUDO_UID=106 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://85.184.249.68:3128 I: uname -a - Linux ionos11-amd64 6.1.0-17-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.69-1 (2023-12-30) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.5.0-0.deb12.4-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.5.10-1~bpo12+1 (2023-11-23) x86_64 GNU/Linux I: ls -l /bin total 5476 -rwxr-xr-x 1 root root 1234376 Mar 27 2022 bash @@ -132,7 +163,7 @@ -rwxr-xr-x 1 root root 52032 Sep 24 2020 rmdir -rwxr-xr-x 1 root root 27472 Sep 27 2020 run-parts -rwxr-xr-x 1 root root 122224 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Dec 7 09:30 sh -> dash + lrwxrwxrwx 1 root root 9 Feb 8 07:04 sh -> /bin/bash -rwxr-xr-x 1 root root 43808 Sep 24 2020 sleep -rwxr-xr-x 1 root root 84928 Sep 24 2020 stty -rwsr-xr-x 1 root root 71912 Jan 20 2022 su @@ -158,7 +189,7 @@ -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew -I: user script /srv/workspace/pbuilder/4155929/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -334,7 +365,7 @@ Get: 126 http://deb.debian.org/debian bullseye/main amd64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 127 http://deb.debian.org/debian bullseye/main amd64 texlive-base all 2020.20210202-3 [20.8 MB] Get: 128 http://deb.debian.org/debian bullseye/main amd64 texlive-latex-base all 2020.20210202-3 [1120 kB] -Fetched 130 MB in 31s (4133 kB/s) +Fetched 130 MB in 4s (33.3 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package bsdextrautils. (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 ... 17743 files and directories currently installed.) @@ -756,8 +787,8 @@ Setting up tzdata (2021a-1+deb11u10) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Jan 7 00:25:50 UTC 2024. -Universal Time is now: Sun Jan 7 00:25:50 UTC 2024. +Local time is now: Sat Feb 8 07:06:11 UTC 2025. +Universal Time is now: Sat Feb 8 07:06:11 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up xtrans-dev (1.4.0-1) ... @@ -936,7 +967,11 @@ fakeroot is already the newest version (1.25.3-1.1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316-35.1_source.changes +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bullseye +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/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 && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../hol88_2.02.19940316-35.1_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316-35.1 dpkg-buildpackage: info: source distribution unstable @@ -1329,7 +1364,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:26:46 -12 2024 +Sat Feb 8 21:07:55 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2503,7 +2538,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # mem = - : (* -> * list -> bool) @@ -2641,7 +2676,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #.............start address -T 0xb89450 () : void @@ -2800,7 +2835,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #.............start address -T 0xb89450 () : void @@ -2992,7 +3027,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # concat = - : (string -> string -> string) @@ -3102,7 +3137,7 @@ start address -T 0xb7d110 ;; Finished loading "lisp/f-ol-net" start address -T 0x9e3630 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 6/1/24 + version 2.02 (GCL) created 8/2/25 #...start address -T 0x9f44a0 () : void @@ -3415,7 +3450,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ###########################() : void @@ -3428,7 +3463,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ################################################################################################() : void @@ -3573,7 +3608,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ############################() : void @@ -3616,7 +3651,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 ############################Theory ind loaded () : void @@ -3653,7 +3688,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3694,7 +3729,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4096,7 +4131,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4164,7 +4199,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4369,7 +4404,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4493,7 +4528,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4579,7 +4614,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4672,7 +4707,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4741,7 +4776,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -4846,7 +4881,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5081,7 +5116,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5107,7 +5142,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5235,7 +5270,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5283,7 +5318,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5350,7 +5385,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5409,7 +5444,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5465,7 +5500,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 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #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) @@ -5478,7 +5513,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #() : void @@ -5530,7 +5565,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##########################() : void @@ -5561,7 +5596,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##############################() : void @@ -5648,7 +5683,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #######################################################################() : void @@ -5801,7 +5836,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###########################() : void @@ -5836,7 +5871,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #############################() : void @@ -5897,7 +5932,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###########################Theory arithmetic loaded () : void @@ -6392,7 +6427,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##################################() : void @@ -6539,7 +6574,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #################################Theory list loaded () : void @@ -6878,7 +6913,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ###############################Theory list loaded () : void @@ -8375,7 +8410,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #############################() : void @@ -8759,7 +8794,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################() : void @@ -9057,7 +9092,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################() : void @@ -9197,7 +9232,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ############################################() : void @@ -9294,7 +9329,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 ##################################() : void @@ -9324,7 +9359,7 @@ | /build/reproducible-path/hol88-2.02.19940316/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9341,7 +9376,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #Theory num loaded () : void @@ -9360,7 +9395,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9517,7 +9552,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # @@ -9555,7 +9590,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # @@ -9589,7 +9624,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9674,7 +9709,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9715,7 +9750,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -9899,7 +9934,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 # define_load_lib_function = - : (string list -> void -> void) @@ -9973,7 +10008,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 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #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) @@ -9986,7 +10021,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #() : void @@ -10050,11 +10085,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:32:05 -12 2024 +Sat Feb 8 21:15:05 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:32:05 -12 2024 +Sat Feb 8 21:15:06 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10077,7 +10112,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -10161,7 +10196,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -10267,7 +10302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11017,7 +11052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11040,7 +11075,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11083,7 +11118,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11119,7 +11154,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11171,7 +11206,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11203,7 +11238,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11241,7 +11276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11269,7 +11304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11346,7 +11381,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11368,7 +11403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11422,7 +11457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11471,7 +11506,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11622,7 +11657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11666,7 +11701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11741,7 +11776,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11791,7 +11826,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11854,7 +11889,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11907,7 +11942,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -11953,7 +11988,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12041,7 +12076,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12079,7 +12114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12140,7 +12175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12204,7 +12239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12230,7 +12265,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12255,7 +12290,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12294,7 +12329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -12370,7 +12405,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13107,7 +13142,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13130,7 +13165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13173,7 +13208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13208,7 +13243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13249,7 +13284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13312,7 +13347,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13335,7 +13370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13360,7 +13395,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13387,7 +13422,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13423,7 +13458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13955,7 +13990,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -13978,7 +14013,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14012,7 +14047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14067,7 +14102,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14158,7 +14193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14327,7 +14362,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14491,7 +14526,7 @@ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. P z ==> l(y,z)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1294 PAIRED_EXT = |- !l m. (!x y. l(x,y) = m(x,y)) = (l = m) @@ -14570,7 +14605,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.1s +Run time: 0.0s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14590,7 +14625,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.0s +Run time: 0.1s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... @@ -14646,7 +14681,7 @@ Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m @@ -14679,7 +14714,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1172 EXTEND_FL = @@ -14697,7 +14732,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 = @@ -14718,7 +14753,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -14790,7 +14825,7 @@ File mk_wellorder loaded () : void -Run time: 0.7s +Run time: 0.5s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder' @@ -14799,7 +14834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -14930,7 +14965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15022,7 +15057,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15084,7 +15119,7 @@ Intermediate theorems generated: 732 |- !a. I(I a) = a -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1106 concrete_rep = "group(\x y. x = y)T I" : term @@ -15101,7 +15136,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2546 () : void @@ -15114,12 +15149,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Jan 6 12:34:03 -12 2024 +===> abs_theory rebuilt on Sat Feb 8 21:17:21 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15292,7 +15327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15514,7 +15549,7 @@ TRAT_MUL_WELLDEFINED = |- !p q r. p trat_eq q ==> (p trat_mul r) trat_eq (q trat_mul r) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 207 TRAT_MUL_WELLDEFINED2 = @@ -15596,7 +15631,7 @@ Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 233 Theorem LESS_ADD_NONZERO autoloading from theory `arithmetic` ... @@ -15668,7 +15703,7 @@ HRAT_ADD_ASSOC = |- !h i j. h hrat_add (i hrat_add j) = (h hrat_add i) hrat_add j -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 7 HRAT_MUL_SYM = |- !h i. h hrat_mul i = i hrat_mul h @@ -15729,7 +15764,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -15998,11 +16033,11 @@ Intermediate theorems generated: 2 cut_of_hrat = |- !x. cut_of_hrat x = (\y. y hrat_lt x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ISACUT_HRAT = |- !h. isacut(cut_of_hrat h) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 221 hreal_tydef = |- ?rep. TYPE_DEFINITION isacut rep @@ -16130,12 +16165,12 @@ HREAL_ADD_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 521 HREAL_MUL_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X @@ -16172,7 +16207,7 @@ Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 155 hreal_sub = @@ -16239,7 +16274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -16493,7 +16528,7 @@ Intermediate theorems generated: 1147 TREAL_EQ_EQUIV = |- !p q. p treal_eq q = ($treal_eq p = $treal_eq q) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 TREAL_EQ_AP = |- !p q. (p = q) ==> p treal_eq q @@ -16501,7 +16536,7 @@ Intermediate theorems generated: 8 TREAL_10 = |- ~treal_1 treal_eq treal_0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 32 TREAL_ADD_SYM = |- !x y. x treal_add y = y treal_add x @@ -16591,7 +16626,7 @@ |- !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 @@ -16657,7 +16692,7 @@ TREAL_LT_WELLDEFL = |- !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 612 TREAL_LT_WELLDEF = @@ -16727,12 +16762,12 @@ (?z. !x. P x ==> x real_lt z) ==> (?X. (\h. P(real_of_hreal h))X) /\ (?Y. !X. (\h. P(real_of_hreal h))X ==> X hreal_lt Y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 135 SUP_ALLPOS_LEMMA4 = |- !y. ~r0 real_lt y ==> (!x. y real_lt (real_of_hreal x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 75 Theorem HREAL_SUP autoloading from theory `HREAL` ... @@ -16787,7 +16822,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -17059,7 +17094,7 @@ Intermediate theorems generated: 116 REAL_LT_LADD = |- !x y z. (x + y) < (x + z) = y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 REAL_LT_RADD = |- !x y z. (x + z) < (y + z) = x < y @@ -17099,7 +17134,7 @@ Intermediate theorems generated: 21 REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) @@ -17171,7 +17206,7 @@ Intermediate theorems generated: 6 REAL_LT_01 = |- (& 0) < (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 REAL_LE_LADD = |- !x y z. (x + y) <= (x + z) = y <= z @@ -17409,7 +17444,7 @@ Intermediate theorems generated: 1 REAL_ADD = |- !m n. (& m) + (& n) = &(m num_add n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 131 Theorem MULT_CLAUSES autoloading from theory `arithmetic` ... @@ -17473,7 +17508,7 @@ Run time: 0.0s REAL_LT_MULTIPLE = |- !n d. 1 num_lt n ==> (d < ((& n) * d) = (& 0) < d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) @@ -17530,7 +17565,7 @@ Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -17566,7 +17601,7 @@ Intermediate theorems generated: 22 REAL_LET_ADD2 = |- !w x y z. w <= x /\ y < z ==> (w + y) < (x + z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 58 REAL_LTE_ADD2 = |- !w x y z. w < x /\ y <= z ==> (w + y) < (x + z) @@ -17636,7 +17671,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 @@ -17697,7 +17732,7 @@ Intermediate theorems generated: 36 REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 Theorem FACT_LESS autoloading from theory `arithmetic` ... @@ -17754,7 +17789,7 @@ Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) @@ -17766,7 +17801,7 @@ Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 385 ABS_LT_MUL2 = @@ -17799,7 +17834,7 @@ Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 21 ABS_BETWEEN = @@ -17841,7 +17876,7 @@ Intermediate theorems generated: 61 REAL_SUB_ABS = |- !x y. ((abs x) - (abs y)) <= (abs(x - y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) @@ -17895,7 +17930,7 @@ Run time: 0.0s POW_ADD = |- !c m n. c pow (m num_add n) = (c pow m) * (c pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 152 POW_1 = |- !x. x pow 1 = x @@ -17907,7 +17942,7 @@ Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) @@ -17943,7 +17978,7 @@ Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -17977,7 +18012,7 @@ |- !d. (!y. (?x. (\x. P(x + d))x /\ y < x) = y < s) ==> (!y. (?x. P x /\ y < x) = y < (s + d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) @@ -18004,7 +18039,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 31 REAL_SUP_UBOUND = @@ -18064,7 +18099,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18195,7 +18230,7 @@ SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18266,7 +18301,7 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2469 SUM_CANCEL = @@ -18282,7 +18317,7 @@ File real.ml loaded () : void -Run time: 1.3s +Run time: 1.8s Intermediate theorems generated: 23746 #\ @@ -18292,7 +18327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -18465,7 +18500,7 @@ Intermediate theorems generated: 2 OPEN_OWN_NEIGH = |- !S top x. open top S /\ S x ==> neigh top(S,x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 OPEN_UNOPEN = @@ -18476,7 +18511,7 @@ OPEN_SUBOPEN = |- !S top. open top S = (!x. S x ==> (?P. P x /\ open top P /\ P re_subset S)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 245 OPEN_NEIGH = @@ -18610,7 +18645,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18652,7 +18687,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -18786,7 +18821,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -19160,7 +19195,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19335,7 +19370,7 @@ |- !g k x. (x --> (& 0))(mtop mr1,g) ==> ((\n. k * (x n)) --> (& 0))(mtop mr1,g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 506 Theorem REAL_ADD_ASSOC autoloading from theory `REAL` ... @@ -19454,7 +19489,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 = @@ -19505,13 +19540,13 @@ Intermediate theorems generated: 400 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File nets.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 7389 #\ @@ -19521,7 +19556,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -19827,7 +19862,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.0s +Run time: 0.1s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -20326,7 +20361,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20477,7 +20512,7 @@ Intermediate theorems generated: 16 SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) @@ -20529,7 +20564,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) < (f m)) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 209 Theorem LESS_REFL autoloading from theory `prim_rec` ... @@ -20671,7 +20706,7 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 395 SER_COMPARA = @@ -20805,7 +20840,7 @@ File seq.ml loaded () : void -Run time: 0.5s +Run time: 0.6s Intermediate theorems generated: 18704 #\ @@ -20815,7 +20850,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -21039,7 +21074,7 @@ (!x y x0 y0. (x tends x0)(mtop mr1,g) /\ (y tends y0)(mtop mr1,g) ==> ((\n. (x n) * (y n)) tends (x0 * y0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s LIM_MUL = |- !f g l m. @@ -21086,7 +21121,7 @@ LIM_SUB = |- !f g l m. (f --> l)x /\ (g --> m)x ==> ((\x. (f x) - (g x)) --> (l - m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 Theorem NET_DIV autoloading from theory `NETS` ... @@ -21491,7 +21526,7 @@ (?k d. (& 0) < d /\ (!x. (& 0) < (abs(x - x0)) /\ (abs(x - x0)) < d ==> (abs(f x)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 362 Theorem REAL_MUL_LID autoloading from theory `REAL` ... @@ -21628,7 +21663,7 @@ DIFF_XM1 = |- !x. ~(x = & 0) ==> ((\x. inv x) diffl (--((inv x) pow 2)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 818 Theorem POW_INV autoloading from theory `REAL` ... @@ -21722,7 +21757,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -21822,7 +21857,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f y) <= (f x))) ==> (l = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 572 Theorem REAL_NEG_EQ0 autoloading from theory `REAL` ... @@ -21867,7 +21902,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> f differentiable x) ==> (?z. a < z /\ z < b /\ (f diffl (& 0))z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3178 gfn = "\x. (f x) - ((((f b) - (f a)) / (b - a)) * x)" : term @@ -21931,7 +21966,7 @@ File lim.ml loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 21608 #\ @@ -21941,7 +21976,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -22336,7 +22371,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (abs(f n)) * (z pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22375,7 +22410,7 @@ Sum(0,n)(\n'. (diffs c n') * (x pow n')) = (Sum(0,n)(\n'. (& n') * ((c n') * (x pow (n' num_sub 1))))) + ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 229 Theorem REAL_EQ_SUB_LADD autoloading from theory `REAL` ... @@ -22626,11 +22661,11 @@ Theorem REAL_LE_ANTISYM autoloading from theory `REAL` ... REAL_LE_ANTISYM = |- !x y. x <= y /\ y <= x = (x = y) -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... REAL_LT_HALF2 = |- !d. (d / (& 2)) < d = (& 0) < d -Run time: 0.0s +Run time: 0.1s Definition abs autoloading from theory `REAL` ... abs = |- !x. abs x = ((& 0) <= x => x | -- x) @@ -22793,7 +22828,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -22803,7 +22838,7 @@ File powser.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 8507 #\ @@ -22813,7 +22848,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -22899,7 +22934,7 @@ Theory POWSER loaded () : void -Run time: 0.0s +Run time: 0.1s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -23264,7 +23299,7 @@ Theorem REAL_MUL_LZERO autoloading from theory `REAL` ... REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 -Run time: 0.0s +Run time: 0.1s Theorem ABS_0 autoloading from theory `REAL` ... ABS_0 = |- abs(& 0) = & 0 @@ -23424,7 +23459,7 @@ Intermediate theorems generated: 144 DIFF_SIN = |- !x. (sin diffl (cos x))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 200 Theorem DIFFS_NEG autoloading from theory `POWSER` ... @@ -23718,7 +23753,7 @@ Intermediate theorems generated: 53 LN_1 = |- ln(& 1) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 27 Theorem REAL_POS_NZ autoloading from theory `REAL` ... @@ -23873,7 +23908,7 @@ Run time: 0.0s SIN_BOUND = |- !x. (abs(sin x)) <= (& 1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 212 Theorem ABS_BOUNDS autoloading from theory `REAL` ... @@ -23925,7 +23960,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.1s +Run time: 0.0s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -23941,7 +23976,7 @@ SIN_ADD = |- !x y. sin(x + y) = ((sin x) * (cos y)) + ((cos x) * (sin y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 COS_ADD = @@ -24051,7 +24086,7 @@ (((--(& 1)) pow n) / (&(FACT(2 num_mul n)))) * (x pow (2 num_mul n))) sums (cos x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 163 Theorem LESS_MONO_EQ autoloading from theory `arithmetic` ... @@ -24082,7 +24117,7 @@ Run time: 0.0s COS_2 = |- (cos(& 2)) < (& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3794 Theorem REAL_LET_TRANS autoloading from theory `REAL` ... @@ -24130,7 +24165,7 @@ Run time: 0.0s COS_ISZERO = |- ?! x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24178,7 +24213,7 @@ Intermediate theorems generated: 84 SIN_PI = |- sin pi = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 SIN_COS = |- !x. sin x = cos((pi / (& 2)) - x) @@ -24214,7 +24249,7 @@ Intermediate theorems generated: 137 SIN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 COS_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) @@ -24326,7 +24361,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` ... @@ -24421,7 +24456,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24467,7 +24502,7 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1046 TAN_TOTAL_POS = @@ -24521,7 +24556,7 @@ (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) /\ (sin(asn y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 ASN_SIN = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (sin(asn y) = y) @@ -24570,7 +24605,7 @@ Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) @@ -24589,7 +24624,7 @@ File transc.ml loaded () : void -Run time: 0.9s +Run time: 1.2s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/theories' @@ -24602,7 +24637,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24624,7 +24659,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24690,7 +24725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24722,7 +24757,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24831,7 +24866,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -24984,7 +25019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25057,7 +25092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25137,7 +25172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25294,7 +25329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25449,7 +25484,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25666,7 +25701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25688,7 +25723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25707,7 +25742,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25752,7 +25787,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25817,7 +25852,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25867,7 +25902,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -25937,7 +25972,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26007,7 +26042,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26043,7 +26078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26096,7 +26131,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26168,7 +26203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26247,7 +26282,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26442,7 +26477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -26479,7 +26514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -27165,7 +27200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -27637,7 +27672,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -27901,7 +27936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -28146,7 +28181,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -28610,7 +28645,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29078,7 +29113,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29134,7 +29169,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29224,7 +29259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29423,7 +29458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29455,7 +29490,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29589,7 +29624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29892,7 +29927,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29924,7 +29959,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29963,7 +29998,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -29995,7 +30030,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30156,7 +30191,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30289,7 +30324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30478,7 +30513,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30538,7 +30573,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30663,7 +30698,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30774,7 +30809,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30799,7 +30834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30827,7 +30862,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -30940,7 +30975,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31443,7 +31478,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31691,7 +31726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31917,7 +31952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31959,7 +31994,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -31991,7 +32026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32214,7 +32249,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32607,7 +32642,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -32720,7 +32755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33223,7 +33258,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33471,7 +33506,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33697,7 +33732,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33732,7 +33767,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33771,7 +33806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33808,7 +33843,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33829,7 +33864,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33926,7 +33961,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -33948,7 +33983,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34444,7 +34479,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34467,7 +34502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34545,7 +34580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34604,7 +34639,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34648,7 +34683,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34666,7 +34701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34693,7 +34728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34737,7 +34772,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34850,7 +34885,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34897,7 +34932,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -34936,7 +34971,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35010,7 +35045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35099,7 +35134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35170,7 +35205,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35240,7 +35275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35289,7 +35324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35330,7 +35365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35371,7 +35406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35395,7 +35430,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35496,7 +35531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35517,7 +35552,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -35542,7 +35577,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36168,7 +36203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36245,7 +36280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36272,7 +36307,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36389,7 +36424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36484,7 +36519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36570,7 +36605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36685,7 +36720,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36778,7 +36813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -36954,7 +36989,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37058,7 +37093,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37353,7 +37388,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37456,7 +37491,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37524,7 +37559,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37586,7 +37621,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37766,7 +37801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37807,7 +37842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37837,7 +37872,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -37863,7 +37898,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38381,7 +38416,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -38918,7 +38953,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -39106,7 +39141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #false : bool @@ -39124,10 +39159,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library' date -Sat Jan 6 12:38:23 -12 2024 +Sat Feb 8 21:26:09 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Sat Jan 6 12:38:23 -12 2024 +Sat Feb 8 21:26:09 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39147,20 +39182,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 6/1/24 + HOL88 Version 2.02 (GCL), built on 8/2/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 6/1/24 +BASIC-HOL version 2.02 (GCL) created 8/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -HOL-LCF version 2.02 (GCL) created 6/1/24 +HOL-LCF version 2.02 (GCL) created 8/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -39508,7 +39543,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, 313732 bytes). +Output written on tutorial.dvi (112 pages, 313736 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Tutorial' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Tutorial' @@ -40897,7 +40932,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -41104,7 +41139,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, 1079640 bytes). +Output written on description.dvi (353 pages, 1079644 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' @@ -42663,7 +42698,7 @@ make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44407,7 +44442,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44662,7 +44697,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44899,7 +44934,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45077,7 +45112,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45266,7 +45301,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45385,7 +45420,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45501,7 +45536,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45741,7 +45776,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46082,7 +46117,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46289,7 +46324,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46632,7 +46667,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46824,7 +46859,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47092,7 +47127,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47253,7 +47288,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47398,7 +47433,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47550,7 +47585,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47706,7 +47741,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47884,7 +47919,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48080,7 +48115,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48305,7 +48340,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48566,7 +48601,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:1240' -> endpages.ps +' TeX output 2025.02.08:2130' -> endpages.ps @@ -48629,7 +48664,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.06:1240' -> titlepages.ps +' TeX output 2025.02.08:2130' -> titlepages.ps @@ -48780,10 +48815,10 @@ dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316-35.1_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316-35.1_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35.1_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316-35.1_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316-35.1_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316-35.1_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' dpkg-genbuildinfo --build=binary dpkg-genchanges --build=binary >../hol88_2.02.19940316-35.1_amd64.changes @@ -48792,12 +48827,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: not including original source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/2936086/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/2936086/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/4155929 and its subdirectories -I: Current time: Sat Jan 6 12:41:29 -12 2024 -I: pbuilder-time-stamp: 1704588089 +I: removing directory /srv/workspace/pbuilder/2936086 and its subdirectories +I: Current time: Sat Feb 8 21:33:26 +14 2025 +I: pbuilder-time-stamp: 1739000006