Diff of the two buildlogs: -- --- b1/build.log 2025-01-25 15:50:45.042788487 +0000 +++ b2/build.log 2025-01-25 15:59:14.155929722 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Jan 25 03:27:41 -12 2025 -I: pbuilder-time-stamp: 1737818861 +I: Current time: Sat Feb 28 12:13:47 +14 2026 +I: pbuilder-time-stamp: 1772230427 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -25,52 +25,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/2520217/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1153847/tmp/hooks/D01_modify_environment starting +debug: Running on codethink03-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 Feb 27 22:13 /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/1153847/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1153847/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]="2" [2]="37" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") + BASH_VERSION='5.2.37(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='trixie' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='ba5cbd72ad864b2d856826d6089bf2f0' - 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='2520217' - PS1='# ' - PS2='> ' + INVOCATION_ID=ab34490d18634bcbadb04feb0473f205 + 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=1153847 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.PeLoO5EM/pbuilderrc_5DY3 --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.PeLoO5EM/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='109' - 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.PeLoO5EM/pbuilderrc_wt7d --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.PeLoO5EM/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=109 + 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 codethink04-arm64 6.1.0-30-cloud-arm64 #1 SMP Debian 6.1.124-1 (2025-01-12) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-30-cloud-arm64 #1 SMP Debian 6.1.124-1 (2025-01-12) aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/2520217/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1153847/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -309,7 +341,7 @@ Get: 197 http://deb.debian.org/debian trixie/main arm64 xdg-utils all 1.2.1-2 [75.8 kB] Get: 198 http://deb.debian.org/debian trixie/main arm64 texlive-base all 2024.20241115-1 [22.7 MB] Get: 199 http://deb.debian.org/debian trixie/main arm64 texlive-latex-base all 2024.20241115-1 [1278 kB] -Fetched 181 MB in 1s (146 MB/s) +Fetched 181 MB in 1s (275 MB/s) Preconfiguring packages ... Selecting previously unselected package libapparmor1: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 ... 19970 files and directories currently installed.) @@ -973,8 +1005,8 @@ Setting up tzdata (2024b-6) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Jan 25 15:28:55 UTC 2025. -Universal Time is now: Sat Jan 25 15:28:55 UTC 2025. +Local time is now: Fri Feb 27 22:14:19 UTC 2026. +Universal Time is now: Fri Feb 27 22:14:19 UTC 2026. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.13-1) ... @@ -1176,7 +1208,11 @@ fakeroot is already the newest version (1.36.2-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.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-5_source.changes +I: user script /srv/workspace/pbuilder/1153847/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/1153847/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-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1569,7 +1605,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 25 03:30:49 -12 2025 +Sat Feb 28 12:15:12 +14 2026 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2807,7 +2843,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 # mem = - : (* -> * list -> bool) @@ -2945,7 +2981,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #.............start address -T 0xc45da0 () : void @@ -3104,7 +3140,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #.............start address -T 0xc45da0 () : void @@ -3296,7 +3332,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 # concat = - : (string -> string -> string) @@ -3406,7 +3442,7 @@ start address -T 0xc3bf40 ;; Finished loading "lisp/f-ol-net" start address -T 0xa7ebf0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 25/1/25 + version 2.02 (GCL) created 28/2/26 #...start address -T 0xa963e0 () : void @@ -3735,7 +3771,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 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 ###########################() : void @@ -3748,7 +3784,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 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 ################################################################################################() : void @@ -3893,7 +3929,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 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 ############################() : void @@ -3936,7 +3972,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 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 ############################Theory ind loaded () : void @@ -3973,7 +4009,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4014,7 +4050,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4416,7 +4452,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4484,7 +4520,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4689,7 +4725,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4813,7 +4849,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4899,7 +4935,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -4992,7 +5028,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5061,7 +5097,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5166,7 +5202,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5401,7 +5437,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5427,7 +5463,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5555,7 +5591,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5603,7 +5639,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5670,7 +5706,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5729,7 +5765,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5785,7 +5821,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 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5798,7 +5834,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #() : void @@ -5850,7 +5886,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ##########################() : void @@ -5881,7 +5917,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ##############################() : void @@ -5968,7 +6004,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #######################################################################() : void @@ -6121,7 +6157,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ###########################() : void @@ -6156,7 +6192,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #############################() : void @@ -6217,7 +6253,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ###########################Theory arithmetic loaded () : void @@ -6712,7 +6748,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ##################################() : void @@ -6859,7 +6895,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #################################Theory list loaded () : void @@ -7198,7 +7234,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ###############################Theory list loaded () : void @@ -8695,7 +8731,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #############################() : void @@ -9079,7 +9115,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ############################() : void @@ -9377,7 +9413,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ############################() : void @@ -9517,7 +9553,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ############################################() : void @@ -9614,7 +9650,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 ##################################() : void @@ -9644,7 +9680,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -9661,7 +9697,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #Theory num loaded () : void @@ -9680,7 +9716,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -9837,7 +9873,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 # @@ -9875,7 +9911,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 # @@ -9909,7 +9945,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -9994,7 +10030,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -10035,7 +10071,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -10219,7 +10255,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 # define_load_lib_function = - : (string list -> void -> void) @@ -10295,7 +10331,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 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre10 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10308,7 +10344,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #() : void @@ -10372,11 +10408,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 25 03:35:55 -12 2025 +Sat Feb 28 12:17:10 +14 2026 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 25 03:35:56 -12 2025 +Sat Feb 28 12:17:10 +14 2026 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10399,7 +10435,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -10483,7 +10519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -10589,7 +10625,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11339,7 +11375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11362,7 +11398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11405,7 +11441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11441,7 +11477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11493,7 +11529,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11525,7 +11561,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11563,7 +11599,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11591,7 +11627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11668,7 +11704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11690,7 +11726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11744,7 +11780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11793,7 +11829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11944,7 +11980,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -11988,7 +12024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12063,7 +12099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12113,7 +12149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12176,7 +12212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12229,7 +12265,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12275,7 +12311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12363,7 +12399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12401,7 +12437,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12462,7 +12498,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12526,7 +12562,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12552,7 +12588,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12577,7 +12613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12616,7 +12652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -12692,7 +12728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13429,7 +13465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13452,7 +13488,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13495,7 +13531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13530,7 +13566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13571,7 +13607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13634,7 +13670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13657,7 +13693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13682,7 +13718,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13709,7 +13745,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -13745,7 +13781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14277,7 +14313,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14300,7 +14336,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14334,7 +14370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14389,7 +14425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14480,7 +14516,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14649,7 +14685,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -14845,7 +14881,7 @@ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. less l(z,y) ==> ~P z))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 109 WOSET_TOTAL_LE = @@ -14912,7 +14948,7 @@ (!f g x. (!y. less l(ms y,ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 280 Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... @@ -15040,7 +15076,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -15065,7 +15101,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.0s +Run time: 0.1s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -15102,7 +15138,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1083 () : void @@ -15121,7 +15157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -15252,7 +15288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -15344,7 +15380,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -15423,7 +15459,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2546 () : void @@ -15433,15 +15469,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Jan 25 03:38:00 -12 2025 +===> abs_theory rebuilt on Sat Feb 28 12:17:57 +14 2026 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -15614,7 +15650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -15857,7 +15893,7 @@ TRAT_ADD_ASSOC = |- !h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -16051,7 +16087,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -16306,7 +16342,7 @@ Intermediate theorems generated: 154 HRAT_MEAN = |- !x y. x hrat_lt y ==> (?z. x hrat_lt z /\ z hrat_lt y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 133 isacut = @@ -16439,7 +16475,7 @@ Intermediate theorems generated: 2 hreal_lt = |- !X Y. X hreal_lt Y = ~(X = Y) /\ (!x. cut X x ==> cut Y x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 HREAL_INV_ISACUT = @@ -16509,7 +16545,7 @@ 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 = @@ -16551,7 +16587,7 @@ File hreal.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 10456 #\ @@ -16561,7 +16597,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -16853,7 +16889,7 @@ |- !x y z. x treal_mul (y treal_add z) = (x treal_mul y) treal_add (x treal_mul z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 345 TREAL_ADD_LID = |- !x. (treal_0 treal_add x) treal_eq x @@ -16938,7 +16974,7 @@ TREAL_BIJ_WELLDEF = |- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1446 TREAL_NEG_WELLDEF = @@ -17109,7 +17145,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -17449,7 +17485,7 @@ Intermediate theorems generated: 94 REAL_LET_ANTISYM = |- !x y. ~(x < y /\ y <= x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 32 REAL_LTE_ANTSYM = |- !x y. ~(x <= y /\ y < x) @@ -17609,7 +17645,7 @@ Intermediate theorems generated: 30 REAL_INV_NZ = |- !x. ~(x = & 0) ==> ~(inv x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 REAL_INVINV = |- !x. ~(x = & 0) ==> (inv(inv x) = x) @@ -17629,7 +17665,7 @@ Intermediate theorems generated: 87 REAL_LT_RMUL_0 = |- !x y. (& 0) < y ==> ((& 0) < (x * y) = (& 0) < x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_LT_LMUL = |- !x y z. (& 0) < x ==> ((x * y) < (x * z) = y < z) @@ -17795,7 +17831,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) @@ -17848,7 +17884,7 @@ Intermediate theorems generated: 91 REAL_LT_ADD_SUB = |- !x y z. (x + y) < z = x < (z - y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 23 REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) @@ -17935,7 +17971,7 @@ Intermediate theorems generated: 24 REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 REAL_INV_MUL = @@ -17958,7 +17994,7 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y @@ -18043,7 +18079,7 @@ Intermediate theorems generated: 163 REAL_EQ_NEG = |- !x y. (-- x = -- y) = (x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 36 REAL_DIV_MUL2 = @@ -18076,7 +18112,7 @@ Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) @@ -18237,7 +18273,7 @@ Intermediate theorems generated: 160 POW_M1 = |- !n. abs((--(& 1)) pow n) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 80 POW_MUL = |- !n x y. (x * y) pow n = (x pow n) * (y pow n) @@ -18253,7 +18289,7 @@ Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 62 REAL_LE1_POW2 = |- !x. (& 1) <= x ==> (& 1) <= (x pow 2) @@ -18463,11 +18499,11 @@ 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.0s +Run time: 0.1s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) @@ -18588,13 +18624,13 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2469 SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 () : void @@ -18614,7 +18650,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -18932,7 +18968,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 544 MTOP_OPEN = @@ -19108,7 +19144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -19358,7 +19394,7 @@ Theorem METRIC_TRIANGLE autoloading from theory `TOPOLOGY` ... METRIC_TRIANGLE = |- !m x y z. (dist m(x,z)) <= ((dist m(x,y)) + (dist m(y,z))) -Run time: 0.0s +Run time: 0.1s Theorem REAL_NOT_LT autoloading from theory `REAL` ... REAL_NOT_LT = |- !x y. ~x < y = y <= x @@ -19497,7 +19533,7 @@ Theorem LESS_0 autoloading from theory `prim_rec` ... LESS_0 = |- !n. 0 num_lt (SUC n) -Run time: 0.1s +Run time: 0.0s Theorem REAL_LT autoloading from theory `REAL` ... REAL_LT = |- !m n. (& m) < (& n) = m num_lt n @@ -19833,7 +19869,7 @@ File nets.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 7389 #\ @@ -19843,7 +19879,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -20168,7 +20204,7 @@ Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 182 mono = @@ -20319,7 +20355,7 @@ Theorem REAL_ADD_RINV autoloading from theory `REAL` ... REAL_ADD_RINV = |- !x. x + (-- x) = & 0 -Run time: 0.1s +Run time: 0.0s Definition real_sub autoloading from theory `REAL` ... real_sub = |- !x y. x - y = x + (-- y) @@ -20611,7 +20647,7 @@ Run time: 0.0s SEQ_POWER_ABS = |- !c. (abs c) < (& 1) ==> (\n. (abs c) pow n) --> (& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 573 Theorem POW_ABS autoloading from theory `REAL` ... @@ -20748,7 +20784,7 @@ Theorem REAL_EQ_LMUL_IMP autoloading from theory `REAL` ... REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) -Run time: 0.1s +Run time: 0.0s Theorem REAL_MUL_RID autoloading from theory `REAL` ... REAL_MUL_RID = |- !x. x * (& 1) = x @@ -20882,7 +20918,7 @@ |- !f k. summable f /\ 0 num_lt k ==> (\n. Sum(n num_mul k,k)f) sums (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 258 Theorem MULT_SYM autoloading from theory `arithmetic` ... @@ -20965,7 +21001,7 @@ Theorem SUM_DIFF autoloading from theory `REAL` ... SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) -Run time: 0.1s +Run time: 0.0s SER_CAUCHY = |- !f. @@ -21127,7 +21163,7 @@ File seq.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 18704 #\ @@ -21137,7 +21173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -21393,7 +21429,7 @@ LIM_INV = |- !f l. (f --> l)x /\ ~(l = & 0) ==> ((\x. inv(f x)) --> (inv l))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 Theorem NET_SUB autoloading from theory `NETS` ... @@ -21535,7 +21571,7 @@ Run time: 0.0s DIFF_CONT = |- !f l x. (f diffl l)x ==> f contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 290 Theorem REAL_ADD_SUB autoloading from theory `REAL` ... @@ -21761,7 +21797,7 @@ Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... REAL_NEG_MINUS1 = |- !x. -- x = (--(& 1)) * x -Run time: 0.0s +Run time: 0.1s DIFF_NEG = |- !f l x. (f diffl l)x ==> ((\x. --(f x)) diffl (-- l))x Run time: 0.0s @@ -21867,7 +21903,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -22024,7 +22060,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22221,7 +22257,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -22253,7 +22289,7 @@ File lim.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 21608 #\ @@ -22263,7 +22299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -22495,7 +22531,7 @@ Theorem REAL_NEG_SUB autoloading from theory `REAL` ... REAL_NEG_SUB = |- !x y. --(x - y) = y - x -Run time: 0.0s +Run time: 0.1s Theorem REAL_NEG_LMUL autoloading from theory `REAL` ... REAL_NEG_LMUL = |- !x y. --(x * y) = (-- x) * y @@ -22600,7 +22636,7 @@ Theorem ABS_ABS autoloading from theory `REAL` ... ABS_ABS = |- !x. abs(abs x) = abs x -Run time: 0.1s +Run time: 0.0s Theorem ABS_MUL autoloading from theory `REAL` ... ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) @@ -23115,7 +23151,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 @@ -23135,7 +23171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -23303,7 +23339,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23350,7 +23386,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) + (g x)) diffl (l + m))x -Run time: 0.1s +Run time: 0.0s Theorem DIFF_DIV autoloading from theory `LIM` ... DIFF_DIV = @@ -24159,7 +24195,7 @@ Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 690 Theorem REAL_ADD_RINV autoloading from theory `REAL` ... @@ -24247,7 +24283,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 = @@ -24364,7 +24400,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24460,7 +24496,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 @@ -24488,7 +24524,7 @@ Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -24648,7 +24684,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` ... @@ -24664,7 +24700,7 @@ (cos x = & 0) = (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. ~EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 630 Theorem EVEN_EXISTS autoloading from theory `arithmetic` ... @@ -24888,7 +24924,7 @@ (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) /\ (tan(atn y) = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y @@ -24911,7 +24947,7 @@ File transc.ml loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24924,7 +24960,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -24946,7 +24982,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25012,7 +25048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25044,7 +25080,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25153,7 +25189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25306,7 +25342,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25379,7 +25415,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25459,7 +25495,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25616,7 +25652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25771,7 +25807,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -25988,7 +26024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26010,7 +26046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26029,7 +26065,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26074,7 +26110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26139,7 +26175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26189,7 +26225,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26259,7 +26295,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26329,7 +26365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26365,7 +26401,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26418,7 +26454,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26490,7 +26526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26569,7 +26605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26764,7 +26800,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -26801,7 +26837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -27487,7 +27523,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -27959,7 +27995,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -28223,7 +28259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -28468,7 +28504,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -28932,7 +28968,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29400,7 +29436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29456,7 +29492,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29546,7 +29582,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29745,7 +29781,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29777,7 +29813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -29911,7 +29947,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30214,7 +30250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30246,7 +30282,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30285,7 +30321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30317,7 +30353,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30478,7 +30514,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30611,7 +30647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30800,7 +30836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30860,7 +30896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -30985,7 +31021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -31096,7 +31132,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -31121,7 +31157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -31149,7 +31185,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -31262,7 +31298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -31765,7 +31801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32013,7 +32049,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32239,7 +32275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32281,7 +32317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32313,7 +32349,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32536,7 +32572,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -32929,7 +32965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -33042,7 +33078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -33545,7 +33581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -33793,7 +33829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34019,7 +34055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34054,7 +34090,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34093,7 +34129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34130,7 +34166,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34151,7 +34187,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34248,7 +34284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34270,7 +34306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34766,7 +34802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34789,7 +34825,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34867,7 +34903,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34926,7 +34962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34970,7 +35006,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -34988,7 +35024,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35015,7 +35051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35059,7 +35095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35172,7 +35208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35219,7 +35255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35258,7 +35294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35332,7 +35368,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35421,7 +35457,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35492,7 +35528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35562,7 +35598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35611,7 +35647,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35652,7 +35688,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35693,7 +35729,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35717,7 +35753,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35818,7 +35854,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35839,7 +35875,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -35864,7 +35900,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36490,7 +36526,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36567,7 +36603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36594,7 +36630,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36711,7 +36747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36806,7 +36842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -36892,7 +36928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37007,7 +37043,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37100,7 +37136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37276,7 +37312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37380,7 +37416,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37675,7 +37711,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37778,7 +37814,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37846,7 +37882,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -37908,7 +37944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -38088,7 +38124,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -38129,7 +38165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -38159,7 +38195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -38185,7 +38221,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -38703,7 +38739,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -39240,7 +39276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -39428,7 +39464,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #false : bool @@ -39446,10 +39482,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sat Jan 25 03:43:48 -12 2025 +Sat Feb 28 12:20:42 +14 2026 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Jan 25 03:43:48 -12 2025 +Sat Feb 28 12:20:42 +14 2026 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39469,20 +39505,20 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 25/1/25 + HOL88 Version 2.02 (GCL), built on 28/2/26 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 25/1/25 +BASIC-HOL version 2.02 (GCL) created 28/2/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 25/1/25 +HOL-LCF version 2.02 (GCL) created 28/2/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -40159,7 +40195,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, 338304 bytes). +Output written on tutorial.dvi (114 pages, 338308 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' @@ -42366,7 +42402,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, 1083500 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' @@ -44578,7 +44614,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, 1150940 bytes). +Output written on reference.dvi (669 pages, 1150944 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -52910,7 +52946,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.01.25:0347' -> endpages.ps +' TeX output 2026.02.28:1221' -> endpages.ps @@ -52982,7 +53018,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.01.25:0347' -> titlepages.ps +' TeX output 2026.02.28:1221' -> titlepages.ps @@ -53140,12 +53176,12 @@ dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_arm64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_arm64.changes @@ -53154,12 +53190,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/1153847/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1153847/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/2520217 and its subdirectories -I: Current time: Sat Jan 25 03:50:43 -12 2025 -I: pbuilder-time-stamp: 1737820243 +I: removing directory /srv/workspace/pbuilder/1153847 and its subdirectories +I: Current time: Sat Feb 28 12:22:12 +14 2026 +I: pbuilder-time-stamp: 1772230932