Diff of the two buildlogs: -- --- b1/build.log 2025-10-30 02:09:41.702825542 +0000 +++ b2/build.log 2025-10-30 02:18:34.147435260 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Dec 1 20:18:28 -12 2026 -I: pbuilder-time-stamp: 1796199508 +I: Current time: Thu Oct 30 16:09:44 +14 2025 +I: pbuilder-time-stamp: 1761790184 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,53 +26,85 @@ dpkg-source: info: applying function_representation I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3655472/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3840426/tmp/hooks/D01_modify_environment starting +debug: Running on codethink04-arm64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Oct 30 02:09 /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/3840426/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3840426/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='arm64' - DEBIAN_FRONTEND='noninteractive' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="3" [2]="3" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") + BASH_VERSION='5.3.3(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='dc0c967e0200438d82efa99ed3ffe952' - 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='3655472' - PS1='# ' - PS2='> ' + INVOCATION_ID=2e74ca0ef13447439a0c96e7a74cf6d8 + LANG=C + LANGUAGE=nl_BE:nl + LC_ALL=C + MACHTYPE=aarch64-unknown-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=3840426 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.XBKdBm9J/pbuilderrc_AZE8 --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.XBKdBm9J/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-8.dsc' - SUDO_GID='109' - SUDO_HOME='/var/lib/jenkins' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.4: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.XBKdBm9J/pbuilderrc_sLWI --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.XBKdBm9J/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-8.dsc' + SUDO_GID=109 + SUDO_HOME=/var/lib/jenkins + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://192.168.101.4:3128 I: uname -a - Linux codethink03-arm64 6.12.48+deb13-cloud-arm64 #1 SMP Debian 6.12.48-1 (2025-09-20) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.12.48+deb13-cloud-arm64 #1 SMP Debian 6.12.48-1 (2025-09-20) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Aug 10 2025 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/3655472/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Aug 10 12:30 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/3840426/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -211,7 +243,7 @@ Get: 97 http://deb.debian.org/debian unstable/main arm64 texlive-base all 2025.20250927-4 [23.1 MB] Get: 98 http://deb.debian.org/debian unstable/main arm64 texlive-luatex all 2025.20250927-4 [36.0 MB] Get: 99 http://deb.debian.org/debian unstable/main arm64 texlive-latex-base all 2025.20250927-4 [1319 kB] -Fetched 177 MB in 2s (86.7 MB/s) +Fetched 177 MB in 1s (224 MB/s) Preconfiguring packages ... Selecting previously unselected package libexpat1:arm64. (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 ... 19964 files and directories currently installed.) @@ -648,7 +680,11 @@ Solving dependencies... 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.19940316dfsg/ && 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.19940316dfsg-8_source.changes +I: user script /srv/workspace/pbuilder/3840426/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/3840426/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && 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.19940316dfsg-8_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-8 dpkg-buildpackage: info: source distribution unstable @@ -1057,7 +1093,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Dec 2 08:20:37 2026 +Thu Oct 30 02:11:14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -1999,8 +2035,8 @@ ;; Compiling lisp/f-freadth.l. ;;; Including lisp/f-macro;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/lisp/f-macro.o 0x2a81d20 ;; When compiling (DEFUN THY-READ) -;; inlining (#<@0000000002812640> # ...) -;; inlining (#<@0000000002802EA0> # ...) +;; inlining (#<@0000000002812650> # ...) +;; inlining (#<@0000000002802EB0> # ...) STYLE-WARNING: The variable ERTOK is not used. ;; End of Pass 1. @@ -2334,7 +2370,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 # mem = - : (* -> * list -> bool) @@ -2503,7 +2539,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x2b1e1e0 .............() : void @@ -2694,7 +2730,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x2b1e1e0 .............() : void @@ -2919,7 +2955,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 # concat = - : (string -> string -> string) @@ -3060,7 +3096,7 @@ ;; Finished loading "lisp/f-ol-net" ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 2/12/26 + version 2.02 (GCL) created 30/10/25 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/site_ml.o 0x2b1e1e0 ...() : void @@ -3409,7 +3445,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 ###########################() : void @@ -3422,7 +3458,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 ################################################################################################() : void @@ -3567,7 +3603,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 ############################() : void @@ -3610,7 +3646,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 ############################Theory ind loaded () : void @@ -3647,7 +3683,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3688,7 +3724,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4090,7 +4126,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4158,7 +4194,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4363,7 +4399,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4487,7 +4523,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4573,7 +4609,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4666,7 +4702,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4735,7 +4771,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -4840,7 +4876,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5075,7 +5111,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5101,7 +5137,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5229,7 +5265,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5277,7 +5313,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5344,7 +5380,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5403,7 +5439,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5459,7 +5495,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 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre7 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5471,7 +5507,7 @@ Temporary directory for compiler files set to /tmp/ > -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #() : void @@ -5523,7 +5559,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ##########################() : void @@ -5554,7 +5590,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ##############################() : void @@ -5641,7 +5677,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #######################################################################() : void @@ -5794,7 +5830,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ###########################() : void @@ -5829,7 +5865,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #############################() : void @@ -5890,7 +5926,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ###########################Theory arithmetic loaded () : void @@ -6385,7 +6421,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ##################################() : void @@ -6532,7 +6568,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #################################Theory list loaded () : void @@ -6871,7 +6907,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ###############################Theory list loaded () : void @@ -8368,7 +8404,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #############################() : void @@ -8752,7 +8788,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ############################() : void @@ -9050,7 +9086,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ############################() : void @@ -9190,7 +9226,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ############################################() : void @@ -9287,7 +9323,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 ##################################() : void @@ -9317,7 +9353,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -9334,7 +9370,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #Theory num loaded () : void @@ -9353,7 +9389,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -9510,7 +9546,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 # @@ -9548,7 +9584,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 # @@ -9582,7 +9618,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -9667,7 +9703,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -9708,7 +9744,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -9892,7 +9928,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 # define_load_lib_function = - : (string list -> void -> void) @@ -9968,7 +10004,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 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre7 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -9980,7 +10016,7 @@ Temporary directory for compiler files set to /tmp/ > -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #() : void @@ -10044,11 +10080,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Dec 2 08:24:25 2026 +Thu Oct 30 02:13:30 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Dec 2 08:24:26 2026 +Thu Oct 30 02:13:30 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10071,7 +10107,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -10155,7 +10191,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -10261,7 +10297,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11011,7 +11047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11034,7 +11070,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11077,7 +11113,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11113,7 +11149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11165,7 +11201,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11197,7 +11233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11235,7 +11271,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11263,7 +11299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11340,7 +11376,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11362,7 +11398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11416,7 +11452,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11465,7 +11501,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11616,7 +11652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11660,7 +11696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11735,7 +11771,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11785,7 +11821,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11848,7 +11884,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11901,7 +11937,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -11947,7 +11983,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12035,7 +12071,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12073,7 +12109,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12134,7 +12170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12198,7 +12234,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12224,7 +12260,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12249,7 +12285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12288,7 +12324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -12364,7 +12400,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13101,7 +13137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13124,7 +13160,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13167,7 +13203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13202,7 +13238,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13243,7 +13279,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13306,7 +13342,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13329,7 +13365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13354,7 +13390,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13381,7 +13417,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13417,7 +13453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13949,7 +13985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -13972,7 +14008,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14006,7 +14042,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14061,7 +14097,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14152,7 +14188,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14321,7 +14357,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14554,7 +14590,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14678,12 +14714,12 @@ EXTEND_FL = |- !l x. woset l ==> (fl(\(x,y). l(x,y) /\ l(y,a))x = l(x,a)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 143 EXTEND_INSEG = |- !l a. woset l /\ fl l a ==> (\(x,y). l(x,y) /\ l(y,a)) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 EXTEND_LINSEG = @@ -14737,7 +14773,7 @@ WO_FL_RESTRICT = |- !l. woset l ==> (!P. fl(\(x,y). P x /\ P y /\ l(x,y))x = P x /\ fl l x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -14793,7 +14829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -14924,7 +14960,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -15016,7 +15052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -15108,12 +15144,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Wed Dec 2 08:25:41 2026 +===> abs_theory rebuilt on Thu Oct 30 02:14:23 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -15286,7 +15322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -15550,7 +15586,7 @@ |- !h i j. (h trat_mul (i trat_add j)) trat_eq ((h trat_mul i) trat_add (h trat_mul j)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 611 TRAT_MUL_LID = |- !h. (trat_1 trat_mul h) trat_eq h @@ -15622,7 +15658,7 @@ Run time: 0.0s TRAT_ARCH = |- !h. ?n d. (trat_sucint n) trat_eq (h trat_add d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 395 TRAT_SUCINT = @@ -15713,7 +15749,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 11032 #\ @@ -15723,7 +15759,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -16076,7 +16112,7 @@ CUT_NEARTOP_MUL = |- !X u. hrat_1 hrat_lt u ==> (?x. cut X x /\ ~cut X(u hrat_mul x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 234 hreal_1 = |- hreal_1 = hreal(cut_of_hrat hrat_1) @@ -16181,12 +16217,12 @@ HREAL_SUB_ISACUT = |- !X Y. X hreal_lt Y ==> isacut(\w. ?x. ~cut X x /\ cut Y(x hrat_add w)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 400 HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16233,7 +16269,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -16568,12 +16604,12 @@ Intermediate theorems generated: 48 TREAL_LT_REFL = |- !x. ~x treal_lt x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16781,7 +16817,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -17153,7 +17189,7 @@ Intermediate theorems generated: 73 REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) @@ -17337,7 +17373,7 @@ Intermediate theorems generated: 19 REAL_LE_ADDR = |- !x y. x <= (x + y) = (& 0) <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 20 REAL_LE_ADDL = |- !x y. y <= (x + y) = (& 0) <= x @@ -17516,7 +17552,7 @@ Intermediate theorems generated: 145 REAL_SUB_SUB = |- !x y. (x - y) - x = -- y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) @@ -17532,7 +17568,7 @@ Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 38 REAL_LE_SUB_RADD = |- !x y z. (x - y) <= z = x <= (z + y) @@ -17626,7 +17662,7 @@ REAL_SUB_INV2 = |- !x y. ~(x = & 0) /\ ~(y = & 0) ==> ((inv x) - (inv y) = (y - x) / (x * y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y @@ -17728,7 +17764,7 @@ Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) @@ -17814,7 +17850,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -17848,7 +17884,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -17909,7 +17945,7 @@ Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -17925,7 +17961,7 @@ Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -18024,11 +18060,11 @@ REAL_SUP_UBOUND_LE = |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 342 Theorem PRE autoloading from theory `prim_rec` ... @@ -18135,7 +18171,7 @@ SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) @@ -18143,7 +18179,7 @@ Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 89 SUM_SUB = @@ -18229,7 +18265,7 @@ Theorem LESS_ADD_SUC autoloading from theory `arithmetic` ... LESS_ADD_SUC = |- !m n. m num_lt (m num_add (SUC n)) -Run time: 0.1s +Run time: 0.0s Theorem LESS_MONO_EQ autoloading from theory `arithmetic` ... LESS_MONO_EQ = |- !m n. (SUC m) num_lt (SUC n) = m num_lt n @@ -18266,7 +18302,7 @@ SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 () : void @@ -18286,7 +18322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -18780,7 +18816,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -19094,7 +19130,7 @@ (!x. (& 0) < (dist m1(x,x0)) /\ (dist m1(x,x0)) <= d ==> (dist m2(f x,y0)) < e)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 459 Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... @@ -19363,7 +19399,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 NET_SUB = @@ -19432,7 +19468,7 @@ Theorem REAL_MUL_RINV autoloading from theory `REAL` ... REAL_MUL_RINV = |- !x. ~(x = & 0) ==> (x * (inv x) = & 1) -Run time: 0.0s +Run time: 0.1s Theorem REAL_MUL_RID autoloading from theory `REAL` ... REAL_MUL_RID = |- !x. x * (& 1) = x @@ -19515,7 +19551,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -20451,7 +20487,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20471,7 +20507,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) @@ -20647,7 +20683,7 @@ Intermediate theorems generated: 412 SER_ZERO = |- !f. summable f ==> f --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 121 Theorem SUM_LE autoloading from theory `REAL` ... @@ -20726,7 +20762,7 @@ Theorem REAL_DIV_LZERO autoloading from theory `REAL` ... REAL_DIV_LZERO = |- !x. (& 0) / x = & 0 -Run time: 0.1s +Run time: 0.0s GP_FINITE = |- !x. @@ -20799,7 +20835,7 @@ File seq.ml loaded () : void -Run time: 0.4s +Run time: 0.3s Intermediate theorems generated: 18704 #\ @@ -20809,7 +20845,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -21485,7 +21521,7 @@ (?k d. (& 0) < d /\ (!x. (& 0) < (abs(x - x0)) /\ (abs(x - x0)) < d ==> (abs(f x)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 362 Theorem REAL_MUL_LID autoloading from theory `REAL` ... @@ -21539,7 +21575,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21696,7 +21732,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -21753,7 +21789,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -21935,7 +21971,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -22044,7 +22080,7 @@ Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22506,7 +22542,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -22578,7 +22614,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22787,7 +22823,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2494 () : void @@ -22807,7 +22843,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -22975,7 +23011,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.1s +Run time: 0.0s basic_diffs = [] : thm list Run time: 0.0s @@ -23233,7 +23269,7 @@ EXP_CONVERGES = |- !x. (\n. ((\n. inv(&(FACT n)))n) * (x pow n)) sums (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 628 Theorem REAL_INV_POS autoloading from theory `REAL` ... @@ -23525,7 +23561,7 @@ Theorem REAL_NEG_RMUL autoloading from theory `REAL` ... REAL_NEG_RMUL = |- !x y. --(x * y) = x * (-- y) -Run time: 0.1s +Run time: 0.0s Theorem DIFF_ISCONST_ALL autoloading from theory `LIM` ... DIFF_ISCONST_ALL = |- !f. (!x. (f diffl (& 0))x) ==> (!x y. f x = f y) @@ -23813,7 +23849,7 @@ Run time: 0.0s SIN_0 = |- sin(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -23935,7 +23971,7 @@ SIN_ADD = |- !x y. sin(x + y) = ((sin x) * (cos y)) + ((cos x) * (sin y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 51 COS_ADD = @@ -24076,7 +24112,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` ... @@ -24132,7 +24168,7 @@ Intermediate theorems generated: 2 PI2 = |- pi / (& 2) = (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 117 COS_PI2 = |- cos(pi / (& 2)) = & 0 @@ -24244,7 +24280,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (& 0) <= x /\ x <= pi /\ (cos x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 766 Theorem REAL_EQ_RADD autoloading from theory `REAL` ... @@ -24336,7 +24372,7 @@ (cos x = & 0) = (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. ~EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 630 Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... @@ -24461,7 +24497,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 = @@ -24583,7 +24619,7 @@ File transc.ml loaded () : void -Run time: 0.7s +Run time: 0.6s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24596,7 +24632,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -24618,7 +24654,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -24684,7 +24720,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -24716,7 +24752,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -24825,7 +24861,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -24978,7 +25014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25051,7 +25087,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25131,7 +25167,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25288,7 +25324,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25443,7 +25479,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25660,7 +25696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25682,7 +25718,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25701,7 +25737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25746,7 +25782,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25811,7 +25847,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25861,7 +25897,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -25931,7 +25967,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26001,7 +26037,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26037,7 +26073,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26090,7 +26126,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26162,7 +26198,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26241,7 +26277,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26436,7 +26472,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -26473,7 +26509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -27159,7 +27195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -27631,7 +27667,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -27895,7 +27931,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -28140,7 +28176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -28604,7 +28640,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29072,7 +29108,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29128,7 +29164,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29218,7 +29254,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29417,7 +29453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29449,7 +29485,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29583,7 +29619,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29886,7 +29922,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29918,7 +29954,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29957,7 +29993,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -29989,7 +30025,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30150,7 +30186,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30283,7 +30319,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30472,7 +30508,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30532,7 +30568,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30657,7 +30693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30768,7 +30804,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30793,7 +30829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30821,7 +30857,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -30934,7 +30970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -31437,7 +31473,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -31685,7 +31721,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -31911,7 +31947,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -31953,7 +31989,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -31985,7 +32021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -32208,7 +32244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -32601,7 +32637,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -32714,7 +32750,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33217,7 +33253,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33465,7 +33501,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33691,7 +33727,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33726,7 +33762,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33765,7 +33801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33802,7 +33838,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33823,7 +33859,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33920,7 +33956,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -33942,7 +33978,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34438,7 +34474,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34461,7 +34497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34539,7 +34575,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34598,7 +34634,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34642,7 +34678,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34660,7 +34696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34687,7 +34723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34731,7 +34767,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34844,7 +34880,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34891,7 +34927,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -34930,7 +34966,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35004,7 +35040,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35093,7 +35129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35164,7 +35200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35234,7 +35270,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35283,7 +35319,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35324,7 +35360,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35365,7 +35401,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35389,7 +35425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35490,7 +35526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35511,7 +35547,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -35536,7 +35572,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36162,7 +36198,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36239,7 +36275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36266,7 +36302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36383,7 +36419,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36478,7 +36514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36564,7 +36600,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36679,7 +36715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36772,7 +36808,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -36948,7 +36984,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37052,7 +37088,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37347,7 +37383,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37450,7 +37486,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37518,7 +37554,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37580,7 +37616,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37760,7 +37796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37801,7 +37837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37831,7 +37867,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -37857,7 +37893,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -38375,7 +38411,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -38912,7 +38948,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -39100,7 +39136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #false : bool @@ -39118,10 +39154,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Wed Dec 2 08:30:01 2026 +Thu Oct 30 02:17:03 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Dec 2 08:30:01 2026 +Thu Oct 30 02:17:03 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39141,20 +39177,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 2/12/26 + HOL88 Version 2.02 (GCL), built on 30/10/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 2/12/26 +BASIC-HOL version 2.02 (GCL) created 30/10/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 2/12/26 +HOL-LCF version 2.02 (GCL) created 30/10/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39203,8 +39239,8 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-8_arm64.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-8_arm64.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-8_arm64.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' for i in Manual/Tutorial/ack.tex Manual/Reference/ack.tex Manual/Description/ack.tex; do\ ln -snf ../Latex/ack.tex $i ; done @@ -39658,7 +39694,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, 316564 bytes). +Output written on tutorial.dvi (112 pages, 316560 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' @@ -39877,7 +39913,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (114 pages, 338308 bytes). +Output written on tutorial.dvi (114 pages, 338304 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' @@ -42084,7 +42120,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, 1083512 bytes). +Output written on description.dvi (353 pages, 1083508 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -46486,7 +46522,7 @@ [663]) (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1155388 bytes). +Output written on reference.dvi (669 pages, 1155384 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -52557,7 +52593,7 @@ [1] [2]) (./preface.tex) [3] (./libraries.aux (./title.aux) (./preface.aux)) ) -Output written on libraries.dvi (3 pages, 2296 bytes). +Output written on libraries.dvi (3 pages, 2292 bytes). Transcript written on libraries.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Libraries' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Libraries' @@ -52628,7 +52664,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2025.1 (TeX Live 2025) Copyright 2025 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.12.02:0832' -> endpages.ps +' TeX output 2025.10.30:0218' -> endpages.ps @@ -52700,7 +52736,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2025.1 (TeX Live 2025) Copyright 2025 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.12.02:0832' -> titlepages.ps +' TeX output 2025.10.30:0218' -> titlepages.ps @@ -52761,13 +52797,13 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-8_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-8_all.deb'. -dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-8_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-8_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-8_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-8_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-8_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-8_arm64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-8_arm64.changes @@ -52776,12 +52812,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/3840426/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3840426/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/3655472 and its subdirectories -I: Current time: Tue Dec 1 20:32:40 -12 2026 -I: pbuilder-time-stamp: 1796200360 +I: removing directory /srv/workspace/pbuilder/3840426 and its subdirectories +I: Current time: Thu Oct 30 16:18:33 +14 2025 +I: pbuilder-time-stamp: 1761790713