Diff of the two buildlogs: -- --- b1/build.log 2025-09-03 06:45:25.824925734 +0000 +++ b2/build.log 2025-09-03 07:01:38.290118923 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Sep 2 18:23:06 -12 2025 -I: pbuilder-time-stamp: 1756880586 +I: Current time: Wed Oct 7 03:08:26 +14 2026 +I: pbuilder-time-stamp: 1791292106 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/forky-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/1080000/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/2997414/tmp/hooks/D01_modify_environment starting +debug: Running on ionos5-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Oct 6 13:08 /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/2997414/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/2997414/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=40 ' - DISTRIBUTION='forky' - HOME='/root' - HOST_ARCH='amd64' + 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]="x86_64-pc-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=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 ' + DIRSTACK=() + DISTRIBUTION=forky + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='4727cff57d914819a6ea3d86f268ba9a' - 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='1080000' - PS1='# ' - PS2='> ' + INVOCATION_ID=6b40a0f8a7024961b7a7fdf4a67f99de + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=2997414 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.qW6SAgar/pbuilderrc_6RPS --distribution forky --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/forky-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.qW6SAgar/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-8.dsc' - SUDO_GID='111' - SUDO_HOME='/var/lib/jenkins' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://46.16.76.132: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.qW6SAgar/pbuilderrc_G5PU --distribution forky --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/forky-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.qW6SAgar/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-8.dsc' + SUDO_GID=110 + SUDO_HOME=/var/lib/jenkins + SUDO_UID=105 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://213.165.73.152:3128 I: uname -a - Linux ionos11-amd64 6.12.41+deb13-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.41-1 (2025-08-12) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.12.41+deb13-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.41-1 (2025-08-12) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Aug 10 12:30 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/1080000/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Aug 10 2025 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/2997414/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -206,7 +238,7 @@ Get: 92 http://deb.debian.org/debian forky/main amd64 xdg-utils all 1.2.1-2 [75.8 kB] Get: 93 http://deb.debian.org/debian forky/main amd64 texlive-base all 2025.20250727-3 [23.1 MB] Get: 94 http://deb.debian.org/debian forky/main amd64 texlive-latex-base all 2025.20250727-3 [1318 kB] -Fetched 135 MB in 3s (46.2 MB/s) +Fetched 135 MB in 2s (74.8 MB/s) Preconfiguring packages ... Selecting previously unselected package libexpat1:amd64. (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 ... 19897 files and directories currently installed.) @@ -622,7 +654,11 @@ fakeroot is already the newest version (1.37.1.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-8_source.changes +I: user script /srv/workspace/pbuilder/2997414/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for forky +I: user script /srv/workspace/pbuilder/2997414/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 @@ -876,79 +912,65 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ +printf '\\begin{theindex}' >index.tex; \ +printf '\\mbox{}' >>index.tex; \ +printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' @@ -959,15 +981,29 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ -printf '\\begin{theindex}' >index.tex; \ -printf '\\mbox{}' >>index.tex; \ -printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' find -name X.tex -exec rm -rf {} \; dh_clean -X./ml/site.ml.orig -X./contrib/tooltool/Makefile.orig \ -X./contrib/tooltool/events.c.orig -X./contrib/tooltool/func_fix.c.orig \ @@ -1031,7 +1067,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Sep 3 06:28:04 2025 +Tue Oct 6 13:11:11 2026 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2308,7 +2344,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 # mem = - : (* -> * list -> bool) @@ -2477,7 +2513,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x27254a0 .............() : void @@ -2668,7 +2704,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x27254a0 .............() : void @@ -2893,7 +2929,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 # concat = - : (string -> string -> string) @@ -3034,7 +3070,7 @@ ;; Finished loading "lisp/f-ol-net" ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 3/9/25 + version 2.02 (GCL) created 6/10/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/site_ml.o 0x27254a0 ...() : void @@ -3383,7 +3419,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 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 ###########################() : void @@ -3396,7 +3432,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 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 ################################################################################################() : void @@ -3541,7 +3577,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 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 ############################() : void @@ -3584,7 +3620,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 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 ############################Theory ind loaded () : void @@ -3621,7 +3657,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3662,7 +3698,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4064,7 +4100,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4132,7 +4168,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4337,7 +4373,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4461,7 +4497,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4547,7 +4583,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4640,7 +4676,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4709,7 +4745,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -4814,7 +4850,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5049,7 +5085,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5075,7 +5111,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5203,7 +5239,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5251,7 +5287,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5318,7 +5354,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5377,7 +5413,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5433,7 +5469,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 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre6 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5445,7 +5481,7 @@ Temporary directory for compiler files set to /tmp/ > -HOL-LCF version 2.02 (GCL) created 3/9/25 +HOL-LCF version 2.02 (GCL) created 6/10/26 #() : void @@ -5497,7 +5533,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ##########################() : void @@ -5528,7 +5564,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ##############################() : void @@ -5615,7 +5651,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #######################################################################() : void @@ -5768,7 +5804,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ###########################() : void @@ -5803,7 +5839,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #############################() : void @@ -5864,7 +5900,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ###########################Theory arithmetic loaded () : void @@ -6359,7 +6395,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ##################################() : void @@ -6506,7 +6542,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #################################Theory list loaded () : void @@ -6845,7 +6881,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ###############################Theory list loaded () : void @@ -8342,7 +8378,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #############################() : void @@ -8726,7 +8762,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ############################() : void @@ -9024,7 +9060,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ############################() : void @@ -9164,7 +9200,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ############################################() : void @@ -9261,7 +9297,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 ##################################() : void @@ -9291,7 +9327,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -9308,7 +9344,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #Theory num loaded () : void @@ -9327,7 +9363,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -9484,7 +9520,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 # @@ -9522,7 +9558,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 # @@ -9556,7 +9592,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -9641,7 +9677,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -9682,7 +9718,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -9866,7 +9902,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 # define_load_lib_function = - : (string list -> void -> void) @@ -9942,7 +9978,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 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre6 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -9954,7 +9990,7 @@ Temporary directory for compiler files set to /tmp/ > -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #() : void @@ -10018,11 +10054,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Sep 3 06:34:49 2025 +Tue Oct 6 13:15:48 2026 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Sep 3 06:34:49 2025 +Tue Oct 6 13:15:48 2026 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10045,7 +10081,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -10129,7 +10165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -10235,7 +10271,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -10985,7 +11021,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11008,7 +11044,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11051,7 +11087,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11087,7 +11123,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11139,7 +11175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11171,7 +11207,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11209,7 +11245,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11237,7 +11273,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11314,7 +11350,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11336,7 +11372,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11390,7 +11426,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11439,7 +11475,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11590,7 +11626,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11634,7 +11670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11709,7 +11745,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11759,7 +11795,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11822,7 +11858,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11875,7 +11911,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -11921,7 +11957,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12009,7 +12045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12047,7 +12083,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12108,7 +12144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12172,7 +12208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12198,7 +12234,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12223,7 +12259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12262,7 +12298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -12338,7 +12374,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13075,7 +13111,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13098,7 +13134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13141,7 +13177,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13176,7 +13212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13217,7 +13253,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13280,7 +13316,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13303,7 +13339,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13328,7 +13364,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13355,7 +13391,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13391,7 +13427,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13923,7 +13959,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13946,7 +13982,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -13980,7 +14016,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14035,7 +14071,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14126,7 +14162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14295,7 +14331,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14528,7 +14564,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14563,7 +14599,7 @@ Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... LESS_EQ_REFL = |- !m. m <= m -Run time: 0.1s +Run time: 0.0s FL_NUM = |- !n. fl(\(m,n). m <= n)n Run time: 0.0s @@ -14647,7 +14683,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1172 EXTEND_FL = @@ -14670,7 +14706,7 @@ ORDINAL_CHAINED = |- !l m. ordinal l /\ ordinal m ==> m inseg l \/ l inseg m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 997 FL_SUC = @@ -14686,7 +14722,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) @@ -14715,14 +14751,14 @@ Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 403 HP = |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2506 ZL = @@ -14758,7 +14794,7 @@ File mk_wellorder loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -14767,7 +14803,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14898,7 +14934,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -14990,7 +15026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -15048,7 +15084,7 @@ Intermediate theorems generated: 733 |- !x y a. (~(a = x) = ~(a = y)) ==> (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 732 |- !a. I(I a) = a @@ -15059,7 +15095,7 @@ Run time: 0.0s GROUP_THOBS = |- IS_GROUP(group(\x y. x = y)T I) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 356 inst_func = - : (string -> thm) @@ -15082,12 +15118,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Wed Sep 3 06:37:00 2025 +===> abs_theory rebuilt on Tue Oct 6 13:17:28 2026 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -15247,7 +15283,7 @@ File abs_theory compiled () : void -Run time: 0.3s +Run time: 0.2s make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals' @@ -15260,7 +15296,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -15503,7 +15539,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.1s +Run time: 0.0s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -15532,7 +15568,7 @@ Intermediate theorems generated: 127 TRAT_MUL_LINV = |- !h. ((trat_inv h) trat_mul h) trat_eq trat_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 Theorem ADD_INV_0_EQ autoloading from theory `arithmetic` ... @@ -15640,7 +15676,7 @@ Intermediate theorems generated: 7 HRAT_MUL_SYM = |- !h i. h hrat_mul i = i hrat_mul h -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 5 HRAT_MUL_ASSOC = @@ -15678,7 +15714,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -15687,7 +15723,7 @@ File hrat.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 11032 #\ @@ -15697,7 +15733,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -15948,7 +15984,7 @@ Intermediate theorems generated: 45 HRAT_DOWN2 = |- !x y. ?z. z hrat_lt x /\ z hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 154 HRAT_MEAN = |- !x y. x hrat_lt y ==> (?z. x hrat_lt z /\ z hrat_lt y) @@ -16136,7 +16172,7 @@ Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) @@ -16191,13 +16227,13 @@ Intermediate theorems generated: 553 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File hreal.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 10456 #\ @@ -16207,7 +16243,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -16457,7 +16493,7 @@ TREAL_EQ_TRANS = |- !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1147 TREAL_EQ_EQUIV = |- !p q. p treal_eq q = ($treal_eq p = $treal_eq q) @@ -16547,7 +16583,7 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16559,7 +16595,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -16608,7 +16644,7 @@ TREAL_MUL_WELLDEFR = |- !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 TREAL_MUL_WELLDEF = @@ -16736,16 +16772,16 @@ |- !x y z. y real_lt z ==> (x real_add y) real_lt (x real_add z); |- !x y. r0 real_lt x /\ r0 real_lt y ==> r0 real_lt (x real_mul y)] : thm list -Run time: 0.0s +Run time: 0.1s () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File realax.ml loaded () : void -Run time: 0.5s +Run time: 0.6s Intermediate theorems generated: 26795 #\ @@ -16755,7 +16791,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -16995,7 +17031,7 @@ Intermediate theorems generated: 18 REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 101 REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -17067,7 +17103,7 @@ Intermediate theorems generated: 21 REAL_LE_LT = |- !x y. x <= y = x < y \/ (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 93 REAL_LT_LE = |- !x y. x < y = x <= y /\ ~(x = y) @@ -17199,7 +17235,7 @@ Intermediate theorems generated: 72 REAL_LE_NEGL = |- !x. (-- x) <= x = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_LE_NEGR = |- !x. x <= (-- x) = x <= (& 0) @@ -17219,7 +17255,7 @@ Intermediate theorems generated: 32 REAL_SUB_LT = |- !x y. (& 0) < (x - y) = y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 REAL_SUB_LE = |- !x y. (& 0) <= (x - y) = y <= x @@ -17283,7 +17319,7 @@ Intermediate theorems generated: 57 REAL_LT_RMUL = |- !x y z. (& 0) < z ==> ((x * z) < (y * z) = x < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_LT_RMUL_IMP = |- !x y z. x < y /\ (& 0) < z ==> (x * z) < (y * z) @@ -17299,7 +17335,7 @@ Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) @@ -17396,7 +17432,7 @@ Intermediate theorems generated: 148 REAL_INV1 = |- inv(& 1) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 26 REAL_OVER1 = |- !x. x / (& 1) = x @@ -17408,7 +17444,7 @@ Intermediate theorems generated: 19 REAL_DIV_LZERO = |- !x. (& 0) / x = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 REAL_LT_NZ = |- !n. ~(& n = & 0) = (& 0) < (& n) @@ -17546,7 +17582,7 @@ Intermediate theorems generated: 33 REAL_LTE_ADD = |- !x y. (& 0) < x /\ (& 0) <= y ==> (& 0) < (x + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LT_MUL2 = @@ -17573,7 +17609,7 @@ Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 93 REAL_EQ_SUB_LADD = |- !x y z. (x = y - z) = (x + z = y) @@ -17604,7 +17640,7 @@ Intermediate theorems generated: 153 REAL_SUB_SUB2 = |- !x y. x - (x - y) = y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_ADD_SUB2 = |- !x y. x - (x + y) = -- y @@ -17657,7 +17693,7 @@ Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 REAL_EQ_RMUL_IMP = |- !x y z. ~(z = & 0) /\ (x * z = y * z) ==> (x = y) @@ -17698,7 +17734,7 @@ Intermediate theorems generated: 169 REAL_MIDDLE1 = |- !a b. a <= b ==> a <= ((a + b) / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b @@ -17710,7 +17746,7 @@ Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 52 ABS_0 = |- abs(& 0) = & 0 @@ -17788,7 +17824,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -17800,7 +17836,7 @@ Intermediate theorems generated: 68 ABS_DIV = |- !y. ~(y = & 0) ==> (!x. abs(x / y) = (abs x) / (abs y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 41 ABS_CIRCLE = @@ -17830,7 +17866,7 @@ Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 @@ -17871,7 +17907,7 @@ Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) @@ -17907,11 +17943,11 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -17961,7 +17997,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) @@ -17972,7 +18008,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (!y. (?x. P x /\ y < x) = y < (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 31 REAL_SUP_UBOUND = @@ -18032,7 +18068,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18040,7 +18076,7 @@ Intermediate theorems generated: 109 SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) @@ -18085,7 +18121,7 @@ Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 105 Theorem ADD_ASSOC autoloading from theory `arithmetic` ... @@ -18104,7 +18140,7 @@ |- !f N. (!n. n num_ge N ==> (f n = & 0)) ==> (!m n. m num_ge N ==> (Sum(m,n)f = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 145 SUM_ADD = @@ -18158,12 +18194,12 @@ |- !f K m n. (!p. m num_le p /\ p num_lt (m num_add n) ==> (f p) <= K) ==> (Sum(m,n)f) <= ((& n) * K) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 226 SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18250,7 +18286,7 @@ File real.ml loaded () : void -Run time: 1.7s +Run time: 2.0s Intermediate theorems generated: 23746 #\ @@ -18260,7 +18296,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -18433,7 +18469,7 @@ Intermediate theorems generated: 2 OPEN_OWN_NEIGH = |- !S top x. open top S /\ S x ==> neigh top(S,x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 OPEN_UNOPEN = @@ -18461,7 +18497,7 @@ |- !top x S. limpt top x S = (!N. neigh top(N,x) ==> (?y. ~(x = y) /\ S y /\ N y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 CLOSED_LIMPT = |- !top S. closed top S = (!x. limpt top x S ==> S x) @@ -18585,7 +18621,7 @@ |- !m. open(mtop m)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: 38 ball = |- !m x e. B m(x,e) = (\y. (dist m(x,y)) < e) @@ -18609,7 +18645,7 @@ Run time: 0.0s BALL_OPEN = |- !m x e. (& 0) < e ==> open(mtop m)(B m(x,e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 161 BALL_NEIGH = |- !m x e. (& 0) < e ==> neigh(mtop m)(B m(x,e),x) @@ -18754,7 +18790,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -18948,7 +18984,7 @@ Theorem REAL_LE_TRANS autoloading from theory `REAL` ... REAL_LE_TRANS = |- !x y z. x <= y /\ y <= z ==> x <= z -Run time: 0.1s +Run time: 0.0s Theorem REAL_LE_TOTAL autoloading from theory `REAL` ... REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x @@ -18959,7 +18995,7 @@ Run time: 0.0s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 257 Definition re_subset autoloading from theory `TOPOLOGY` ... @@ -19170,7 +19206,7 @@ |- !g x x0. (x --> x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> (?N. g N N /\ (!n. g n N ==> ~(x n = & 0))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 165 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -19389,7 +19425,7 @@ Theorem ABS_LT_MUL2 autoloading from theory `REAL` ... ABS_LT_MUL2 = |- !w x y z. (abs w) < y /\ (abs x) < z ==> (abs(w * x)) < (y * z) -Run time: 0.1s +Run time: 0.0s Definition LESS_OR_EQ autoloading from theory `arithmetic` ... LESS_OR_EQ = |- !m n. m num_le n = m num_lt n \/ (m = n) @@ -19473,13 +19509,13 @@ Intermediate theorems generated: 400 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File nets.ml loaded () : void -Run time: 0.3s +Run time: 0.4s Intermediate theorems generated: 7389 #\ @@ -19489,7 +19525,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -19765,7 +19801,7 @@ Intermediate theorems generated: 28 convergent = |- !f. convergent f = (?l. f --> l) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 cauchy = @@ -20020,7 +20056,7 @@ SEQ_NEG_BOUNDED = |- !f. bounded(mr1,$num_ge)(\n. --(f n)) = bounded(mr1,$num_ge)f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 39 SEQ_BCONV = |- !f. bounded(mr1,$num_ge)f /\ mono f ==> convergent f @@ -20112,7 +20148,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20294,7 +20330,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20555,7 +20591,7 @@ Theorem REAL_EQ_IMP_LE autoloading from theory `REAL` ... REAL_EQ_IMP_LE = |- !x y. (x = y) ==> x <= y -Run time: 0.1s +Run time: 0.0s Theorem ADD_ASSOC autoloading from theory `arithmetic` ... ADD_ASSOC = |- !m n p. m num_add (n num_add p) = (m num_add n) num_add p @@ -20606,7 +20642,7 @@ Intermediate theorems generated: 43 SER_CDIV = |- !x x0 c. x sums x0 ==> (\n. (x n) / c) sums (x0 / c) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 Theorem SUM_DIFF autoloading from theory `REAL` ... @@ -20673,7 +20709,7 @@ Run time: 0.0s SER_ACONV = |- !f. summable(\n. abs(f n)) ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 126 Theorem SUM_ABS_LE autoloading from theory `REAL` ... @@ -20743,7 +20779,7 @@ ABS_NEG_LEMMA = |- !c. c <= (& 0) ==> (!x y. (abs x) <= (c * (abs y)) ==> (x = & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 114 Theorem REAL_LE_LMUL autoloading from theory `REAL` ... @@ -20773,7 +20809,7 @@ File seq.ml loaded () : void -Run time: 0.6s +Run time: 0.8s Intermediate theorems generated: 18704 #\ @@ -20783,7 +20819,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -20885,7 +20921,7 @@ Intermediate theorems generated: 43 () : void -Run time: 0.0s +Run time: 0.1s () : void Run time: 0.0s @@ -20978,7 +21014,7 @@ Run time: 0.0s LIM_CONST = |- !k x. ((\x. k) --> k)x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 193 Theorem DORDER_TENDSTO autoloading from theory `NETS` ... @@ -21313,7 +21349,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21596,7 +21632,7 @@ DIFF_XM1 = |- !x. ~(x = & 0) ==> ((\x. inv x) diffl (--((inv x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 818 Theorem POW_INV autoloading from theory `REAL` ... @@ -21690,7 +21726,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -21727,7 +21763,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -21802,7 +21838,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f x) <= (f y))) ==> (l = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 88 DIFF_LCONST = @@ -21817,7 +21853,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -21876,7 +21912,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -21899,7 +21935,7 @@ File lim.ml loaded () : void -Run time: 0.7s +Run time: 0.8s Intermediate theorems generated: 21608 #\ @@ -21909,7 +21945,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -22332,7 +22368,7 @@ Theorem SUC_SUB1 autoloading from theory `arithmetic` ... SUC_SUB1 = |- !m. (SUC m) num_sub 1 = m -Run time: 0.0s +Run time: 0.1s Theorem REAL_MUL_LZERO autoloading from theory `REAL` ... REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -22627,7 +22663,7 @@ (& 0) < k /\ (!h. (& 0) < (abs h) /\ (abs h) < k ==> (abs(f h)) <= (K * (abs h))) ==> (f tends_real_real (& 0))(& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 917 Theorem SER_LE autoloading from theory `SEQ` ... @@ -22781,7 +22817,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -22867,7 +22903,7 @@ Theory POWSER loaded () : void -Run time: 0.1s +Run time: 0.0s Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... ADD_CLAUSES = @@ -22949,7 +22985,7 @@ Intermediate theorems generated: 48 () : void -Run time: 0.0s +Run time: 0.1s basic_diffs = [] : thm list Run time: 0.0s @@ -23400,7 +23436,7 @@ Run time: 0.0s DIFF_COS = |- !x. (cos diffl (--(sin x)))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 283 [|- !x. (exp diffl (exp x))x; @@ -23506,7 +23542,7 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 @@ -23707,7 +23743,7 @@ LN_MONO_LT = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x) < (ln y) = x < y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 LN_MONO_LE = @@ -23787,7 +23823,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` ... @@ -23943,7 +23979,7 @@ Theorem ODD_DOUBLE autoloading from theory `arithmetic` ... ODD_DOUBLE = |- !n. ODD(SUC(2 num_mul n)) -Run time: 0.1s +Run time: 0.0s Theorem EVEN_DOUBLE autoloading from theory `arithmetic` ... EVEN_DOUBLE = |- !n. EVEN(2 num_mul n) @@ -23964,7 +24000,7 @@ (((--(& 1)) pow n) / (&(FACT((2 num_mul n) num_add 1)))) * (x pow ((2 num_mul n) num_add 1))) sums (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... @@ -24150,7 +24186,7 @@ Intermediate theorems generated: 79 SIN_COS = |- !x. sin x = cos((pi / (& 2)) - x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 66 COS_SIN = |- !x. cos x = sin((pi / (& 2)) - x) @@ -24162,7 +24198,7 @@ Intermediate theorems generated: 59 COS_PERIODIC_PI = |- !x. cos(x + pi) = --(cos x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 59 SIN_PERIODIC = |- !x. sin(x + ((& 2) * pi)) = sin x @@ -24186,7 +24222,7 @@ Intermediate theorems generated: 53 COS_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (cos x) -Run time: 0.0s +Run time: 0.7s Intermediate theorems generated: 450 Theorem REAL_LT_NEG autoloading from theory `REAL` ... @@ -24283,7 +24319,7 @@ |- !x. (& 0) <= x /\ (cos x = & 0) ==> (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 675 Theorem REAL_LE_ADDR autoloading from theory `REAL` ... @@ -24370,7 +24406,7 @@ |- !x y. ~(cos x = & 0) /\ ~(cos y = & 0) /\ ~(cos(x + y) = & 0) ==> (tan(x + y) = ((tan x) + (tan y)) / ((& 1) - ((tan x) * (tan y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 869 TAN_DOUBLE = @@ -24489,7 +24525,7 @@ (--(pi / (& 2))) <= (asn y) /\ (asn y) <= (pi / (& 2)) /\ (sin(asn y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 ASN_SIN = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (sin(asn y) = y) @@ -24538,7 +24574,7 @@ Intermediate theorems generated: 76 ATN_TAN = |- !y. tan(atn y) = y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) @@ -24570,7 +24606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -24592,7 +24628,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -24658,7 +24694,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -24690,7 +24726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -24799,7 +24835,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -24952,7 +24988,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25025,7 +25061,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25105,7 +25141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25262,7 +25298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25417,7 +25453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25634,7 +25670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25656,7 +25692,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25675,7 +25711,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25720,7 +25756,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25785,7 +25821,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25835,7 +25871,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25905,7 +25941,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -25975,7 +26011,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26011,7 +26047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26064,7 +26100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26136,7 +26172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26215,7 +26251,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26410,7 +26446,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -26447,7 +26483,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -27133,7 +27169,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -27605,7 +27641,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -27869,7 +27905,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -28114,7 +28150,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -28578,7 +28614,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29046,7 +29082,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29102,7 +29138,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29192,7 +29228,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29391,7 +29427,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29423,7 +29459,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29557,7 +29593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29860,7 +29896,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29892,7 +29928,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29931,7 +29967,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -29963,7 +29999,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30124,7 +30160,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30257,7 +30293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30446,7 +30482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30506,7 +30542,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30631,7 +30667,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30742,7 +30778,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30767,7 +30803,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30795,7 +30831,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -30908,7 +30944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -31411,7 +31447,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -31659,7 +31695,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -31885,7 +31921,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -31927,7 +31963,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -31959,7 +31995,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -32182,7 +32218,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -32575,7 +32611,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -32688,7 +32724,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33191,7 +33227,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33439,7 +33475,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33665,7 +33701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33700,7 +33736,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33739,7 +33775,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33776,7 +33812,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33797,7 +33833,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33894,7 +33930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -33916,7 +33952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34412,7 +34448,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34435,7 +34471,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34513,7 +34549,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34572,7 +34608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34616,7 +34652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34634,7 +34670,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34661,7 +34697,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34705,7 +34741,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34818,7 +34854,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34865,7 +34901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34904,7 +34940,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -34978,7 +35014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35067,7 +35103,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35138,7 +35174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35208,7 +35244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35257,7 +35293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35298,7 +35334,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35339,7 +35375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35363,7 +35399,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35464,7 +35500,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35485,7 +35521,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -35510,7 +35546,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36136,7 +36172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36213,7 +36249,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36240,7 +36276,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36357,7 +36393,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36452,7 +36488,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36538,7 +36574,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36653,7 +36689,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36746,7 +36782,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -36922,7 +36958,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37026,7 +37062,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37321,7 +37357,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37424,7 +37460,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37492,7 +37528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37554,7 +37590,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37734,7 +37770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37775,7 +37811,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37805,7 +37841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -37831,7 +37867,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -38349,7 +38385,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -38886,7 +38922,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -39074,7 +39110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 + HOL88 Version 2.02 (GCL), built on 6/10/26 =============================================================================== #false : bool @@ -39092,10 +39128,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Wed Sep 3 06:41:55 2025 +Tue Oct 6 13:22:03 2026 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Sep 3 06:41:55 2025 +Tue Oct 6 13:22:03 2026 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39113,22 +39149,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -BASIC-HOL version 2.02 (GCL) created 3/9/25 +BASIC-HOL version 2.02 (GCL) created 6/10/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 3/9/25 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 6/10/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 3/9/25 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 6/10/26 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39632,7 +39668,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' @@ -39851,7 +39887,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' @@ -41490,7 +41526,7 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 1000256 bytes). +Output written on description.dvi (346 pages, 1000248 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -42058,7 +42094,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, 1083516 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' @@ -44270,7 +44306,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, 1150920 bytes). +Output written on reference.dvi (669 pages, 1150912 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' @@ -52531,7 +52567,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' @@ -52602,7 +52638,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 2025.09.03:0644' -> endpages.ps +' TeX output 2026.10.06:1324' -> endpages.ps @@ -52674,7 +52710,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 2025.09.03:0644' -> titlepages.ps +' TeX output 2026.10.06:1324' -> titlepages.ps @@ -52735,13 +52771,13 @@ dh_gencontrol dh_md5sums dh_builddeb -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-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-source' in '../hol88-library-source_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-contrib-source' in '../hol88-contrib-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-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-8_all.deb'. +dpkg-deb: building package 'hol88-doc' in '../hol88-doc_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_amd64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-8_amd64.changes @@ -52750,12 +52786,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/2997414/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/2997414/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/1080000 and its subdirectories -I: Current time: Tue Sep 2 18:45:25 -12 2025 -I: pbuilder-time-stamp: 1756881925 +I: removing directory /srv/workspace/pbuilder/2997414 and its subdirectories +I: Current time: Wed Oct 7 03:24:37 +14 2026 +I: pbuilder-time-stamp: 1791293077