Diff of the two buildlogs: -- --- b1/build.log 2025-03-09 16:03:37.993067754 +0000 +++ b2/build.log 2025-03-09 16:14:22.491990153 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Apr 11 10:20:27 -12 2026 -I: pbuilder-time-stamp: 1775946027 +I: Current time: Mon Mar 10 06:03:40 +14 2025 +I: pbuilder-time-stamp: 1741536220 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-reproducible-base.tgz] I: copying local configuration @@ -25,52 +25,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3194928/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1807892/tmp/hooks/D01_modify_environment starting +debug: Running on ionos11-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 Mar 9 16:03 /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/1807892/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1807892/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=42 ' - DISTRIBUTION='trixie' - 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=20 ' + DIRSTACK=() + DISTRIBUTION=trixie + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='f3dcf9ed3265417fa2d43a62a4d7214f' - 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='3194928' - PS1='# ' - PS2='> ' + INVOCATION_ID=b53473b60fd145ecaa675f19a7d94886 + 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=1807892 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.iuSoHdQQ/pbuilderrc_iKO1 --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.iuSoHdQQ/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='111' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://213.165.73.152: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.iuSoHdQQ/pbuilderrc_2qgF --distribution trixie --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.iuSoHdQQ/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=111 + SUDO_UID=106 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://46.16.76.132:3128 I: uname -a - Linux ionos15-amd64 6.12.12+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.12-1~bpo12+1 (2025-02-23) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-31-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.128-1 (2025-02-07) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Mar 4 2025 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/3194928/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Nov 22 14:40 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1807892/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -309,7 +341,7 @@ Get: 197 http://deb.debian.org/debian trixie/main amd64 xdg-utils all 1.2.1-2 [75.8 kB] Get: 198 http://deb.debian.org/debian trixie/main amd64 texlive-base all 2024.20250114-1 [22.8 MB] Get: 199 http://deb.debian.org/debian trixie/main amd64 texlive-latex-base all 2024.20250114-1 [1282 kB] -Fetched 190 MB in 7s (28.2 MB/s) +Fetched 190 MB in 2s (80.5 MB/s) Preconfiguring packages ... Selecting previously unselected package libsystemd-shared: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 ... 19800 files and directories currently installed.) @@ -974,8 +1006,8 @@ Setting up tzdata (2025a-2) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Apr 11 22:21:12 UTC 2026. -Universal Time is now: Sat Apr 11 22:21:12 UTC 2026. +Local time is now: Sun Mar 9 16:04:40 UTC 2025. +Universal Time is now: Sun Mar 9 16:04:40 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.13-1) ... @@ -1180,7 +1212,11 @@ fakeroot is already the newest version (1.37-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/1807892/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for trixie +I: user script /srv/workspace/pbuilder/1807892/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1434,21 +1470,42 @@ 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' +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/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +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/parser/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' +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/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +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/unwind/Manual' +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/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; \ @@ -1463,49 +1520,9 @@ 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/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/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/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/word/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/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/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/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/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/reals/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ - 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/reals/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/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' +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/more_arithmetic/Manual' +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' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1513,6 +1530,12 @@ 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/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/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; \ @@ -1520,12 +1543,25 @@ 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/window/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ +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' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ + 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/reals/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/window/Manual' +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 \ @@ -1573,7 +1609,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Apr 11 10:21:55 -12 2026 +Mon Mar 10 06:06:10 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2811,7 +2847,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 # mem = - : (* -> * list -> bool) @@ -2949,7 +2985,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #.............start address -T 0xa8abd0 () : void @@ -3108,7 +3144,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #.............start address -T 0xa8abd0 () : void @@ -3300,7 +3336,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 # concat = - : (string -> string -> string) @@ -3410,7 +3446,7 @@ start address -T 0xa80ca0 ;; Finished loading "lisp/f-ol-net" start address -T 0x856fd0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 11/4/26 + version 2.02 (GCL) created 10/3/25 #...start address -T 0xa8cdf0 () : void @@ -3739,7 +3775,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 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 ###########################() : void @@ -3752,7 +3788,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 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 ################################################################################################() : void @@ -3897,7 +3933,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 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 ############################() : void @@ -3940,7 +3976,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 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 ############################Theory ind loaded () : void @@ -3977,7 +4013,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4018,7 +4054,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4420,7 +4456,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4488,7 +4524,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4693,7 +4729,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4817,7 +4853,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4903,7 +4939,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -4996,7 +5032,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5065,7 +5101,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5170,7 +5206,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5405,7 +5441,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5431,7 +5467,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5559,7 +5595,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5607,7 +5643,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5674,7 +5710,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5733,7 +5769,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5789,7 +5825,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 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre15 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5802,7 +5838,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 11/4/26 +HOL-LCF version 2.02 (GCL) created 10/3/25 #() : void @@ -5854,7 +5890,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ##########################() : void @@ -5885,7 +5921,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ##############################() : void @@ -5972,7 +6008,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #######################################################################() : void @@ -6125,7 +6161,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ###########################() : void @@ -6160,7 +6196,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #############################() : void @@ -6221,7 +6257,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ###########################Theory arithmetic loaded () : void @@ -6716,7 +6752,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ##################################() : void @@ -6863,7 +6899,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #################################Theory list loaded () : void @@ -7202,7 +7238,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ###############################Theory list loaded () : void @@ -8699,7 +8735,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #############################() : void @@ -9083,7 +9119,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ############################() : void @@ -9381,7 +9417,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ############################() : void @@ -9521,7 +9557,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ############################################() : void @@ -9618,7 +9654,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 ##################################() : void @@ -9648,7 +9684,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -9665,7 +9701,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #Theory num loaded () : void @@ -9684,7 +9720,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -9841,7 +9877,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 # @@ -9879,7 +9915,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 # @@ -9913,7 +9949,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -9998,7 +10034,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -10039,7 +10075,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -10223,7 +10259,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10299,7 +10335,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 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre15 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10312,7 +10348,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #() : void @@ -10376,11 +10412,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Apr 11 10:23:15 -12 2026 +Mon Mar 10 06:08:24 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Apr 11 10:23:15 -12 2026 +Mon Mar 10 06:08:24 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10403,7 +10439,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -10487,7 +10523,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -10593,7 +10629,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11343,7 +11379,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11366,7 +11402,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11409,7 +11445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11445,7 +11481,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11497,7 +11533,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11529,7 +11565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11567,7 +11603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11595,7 +11631,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11672,7 +11708,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11694,7 +11730,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11748,7 +11784,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11797,7 +11833,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11948,7 +11984,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -11992,7 +12028,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12067,7 +12103,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12117,7 +12153,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12180,7 +12216,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12233,7 +12269,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12279,7 +12315,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12367,7 +12403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12405,7 +12441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12466,7 +12502,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12530,7 +12566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12556,7 +12592,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12581,7 +12617,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12620,7 +12656,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -12696,7 +12732,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13433,7 +13469,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13456,7 +13492,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13499,7 +13535,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13534,7 +13570,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13575,7 +13611,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13638,7 +13674,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13661,7 +13697,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13686,7 +13722,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13713,7 +13749,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -13749,7 +13785,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14281,7 +14317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14304,7 +14340,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14338,7 +14374,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14393,7 +14429,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14484,7 +14520,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14653,7 +14689,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -14921,7 +14957,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 @@ -14960,7 +14996,7 @@ Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 170 UNION_INSEG = |- !P l. (!m. P m ==> m inseg l) ==> (Union P) inseg l @@ -15028,7 +15064,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 = @@ -15044,7 +15080,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) @@ -15095,7 +15131,7 @@ KL_POSET_LEMMA = |- poset(\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 386 KL = @@ -15116,7 +15152,7 @@ File mk_wellorder loaded () : void -Run time: 0.2s +Run time: 0.5s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15125,7 +15161,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -15256,7 +15292,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -15348,7 +15384,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -15417,7 +15453,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) @@ -15437,15 +15473,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Apr 11 10:23:47 -12 2026 +===> abs_theory rebuilt on Mon Mar 10 06:09:21 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -15618,7 +15654,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -15861,7 +15897,7 @@ TRAT_ADD_ASSOC = |- !h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -15985,7 +16021,7 @@ HRAT_SUCINT = |- (hrat_sucint 0 = hrat_1) /\ (!n. hrat_sucint(SUC n) = (hrat_sucint n) hrat_add hrat_1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 6487 HRAT_ADD_SYM = |- !h i. h hrat_add i = i hrat_add h @@ -16045,7 +16081,7 @@ File hrat.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 11032 #\ @@ -16055,7 +16091,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -16403,7 +16439,7 @@ Run time: 0.0s CUT_NEARTOP_ADD = |- !X e. ?x. cut X x /\ ~cut X(x hrat_add e) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 303 CUT_NEARTOP_MUL = @@ -16456,7 +16492,7 @@ HREAL_ADD_ISACUT = |- !X Y. isacut(\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 521 HREAL_MUL_ISACUT = @@ -16555,7 +16591,7 @@ File hreal.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 10456 #\ @@ -16565,7 +16601,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -16857,7 +16893,7 @@ |- !x y z. x treal_mul (y treal_add z) = (x treal_mul y) treal_add (x treal_mul z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 345 TREAL_ADD_LID = |- !x. (treal_0 treal_add x) treal_eq x @@ -16905,7 +16941,7 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16942,7 +16978,7 @@ TREAL_BIJ_WELLDEF = |- !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1446 TREAL_NEG_WELLDEF = @@ -17074,7 +17110,7 @@ (?x. P x) /\ (?z. !x. P x ==> x real_lt z) ==> (?s. !y. (?x. P x /\ y real_lt x) = y real_lt s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 199 [|- ~(r1 = r0); @@ -17103,7 +17139,7 @@ File realax.ml loaded () : void -Run time: 0.2s +Run time: 0.4s Intermediate theorems generated: 26795 #\ @@ -17113,7 +17149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -17405,7 +17441,7 @@ Intermediate theorems generated: 26 REAL_NOT_LE = |- !x y. ~x <= y = y < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 19 REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x @@ -17485,7 +17521,7 @@ Intermediate theorems generated: 73 REAL_LE_MUL = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x * y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) @@ -17569,7 +17605,7 @@ Intermediate theorems generated: 45 REAL_NEG_0 = |- --(& 0) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x @@ -17689,7 +17725,7 @@ Intermediate theorems generated: 19 REAL_POS = |- !n. (& 0) <= (& n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 70 Theorem LESS_0 autoloading from theory `prim_rec` ... @@ -17754,7 +17790,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 @@ -17816,7 +17852,7 @@ Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... LESS_SUC_REFL = |- !n. n num_lt (SUC n) -Run time: 0.0s +Run time: 0.1s REAL_LT_HALF2 = |- !d. (d / (& 2)) < d = (& 0) < d Run time: 0.0s @@ -17915,7 +17951,7 @@ Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -17927,7 +17963,7 @@ Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c @@ -18007,7 +18043,7 @@ Intermediate theorems generated: 26 REAL_EQ_IMP_LE = |- !x y. (x = y) ==> x <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) @@ -18064,7 +18100,7 @@ Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ABS_ZERO = |- !x. (abs x = & 0) = (x = & 0) @@ -18080,7 +18116,7 @@ Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 178 ABS_TRIANGLE = |- !x y. (abs(x + y)) <= ((abs x) + (abs y)) @@ -18138,7 +18174,7 @@ Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) @@ -18171,7 +18207,7 @@ Intermediate theorems generated: 94 ABS_SUB_ABS = |- !x y. (abs((abs x) - (abs y))) <= (abs(x - y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 80 ABS_BETWEEN2 = @@ -18200,7 +18236,7 @@ Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) @@ -18277,7 +18313,7 @@ Run time: 0.0s POW_2_LE1 = |- !n. (& 1) <= ((& 2) pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 118 Theorem ADD1 autoloading from theory `arithmetic` ... @@ -18356,7 +18392,7 @@ REAL_SUP_UBOUND_LE = |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 15 REAL_ARCH = |- !x. (& 0) < x ==> (!y. ?n. y < ((& n) * x)) @@ -18424,7 +18460,7 @@ |- !f g m n. (!r. m num_le r /\ r num_lt (n num_add m) ==> (f r = g r)) ==> (Sum(m,n)f = Sum(m,n)g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 82 SUM_POS = |- !f. (!n. (& 0) <= (f n)) ==> (!m n. (& 0) <= (Sum(m,n)f)) @@ -18448,7 +18484,7 @@ 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 -Run time: 0.1s +Run time: 0.0s Theorem LESS_EQUAL_ADD autoloading from theory `arithmetic` ... LESS_EQUAL_ADD = |- !m n. m num_le n ==> (?p. n = m num_add p) @@ -18505,7 +18541,7 @@ SUM_NSUB = |- !n f c. (Sum(0,n)f) - ((& n) * c) = Sum(0,n)(\p. (f p) - c) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 239 Theorem LESS_SUC autoloading from theory `prim_rec` ... @@ -18608,7 +18644,7 @@ File real.ml loaded () : void -Run time: 0.8s +Run time: 1.4s Intermediate theorems generated: 23746 #\ @@ -18618,7 +18654,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -19102,7 +19138,7 @@ File topology.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 4132 #\ @@ -19112,7 +19148,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -19389,7 +19425,7 @@ dorder g ==> (x --> x0)(mtop d,g) /\ (x --> x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 313 SEQ_TENDS = @@ -19625,7 +19661,7 @@ (!x y. bounded(mr1,g)x /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) * (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 484 Theorem REAL_LT_LMUL autoloading from theory `REAL` ... @@ -19847,7 +19883,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -20172,7 +20208,7 @@ Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 182 mono = @@ -20361,7 +20397,7 @@ |- !f. bounded(mr1,$num_ge)f /\ (!m n. m num_ge n ==> (f m) >= (f n)) ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 910 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -20420,7 +20456,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20652,7 +20688,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` ... @@ -20997,14 +21033,14 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 SER_COMPARA = |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable(\k. abs(f k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 41 Theorem ZERO_LESS_EQ autoloading from theory `arithmetic` ... @@ -21131,7 +21167,7 @@ File seq.ml loaded () : void -Run time: 0.3s +Run time: 0.5s Intermediate theorems generated: 18704 #\ @@ -21141,7 +21177,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -21567,7 +21603,7 @@ Intermediate theorems generated: 29 CONT_NEG = |- !x. f contl x ==> (\x. --(f x)) contl x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 CONT_INV = |- !x. f contl x /\ ~(f x = & 0) ==> (\x. inv(f x)) contl x @@ -21693,7 +21729,7 @@ Theorem REAL_MUL_LZERO autoloading from theory `REAL` ... REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 -Run time: 0.0s +Run time: 0.1s Definition real_div autoloading from theory `REAL` ... real_div = |- !x y. x / y = x * (inv y) @@ -21871,7 +21907,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -21913,7 +21949,7 @@ DIFF_POW = |- !n x. ((\x'. x' pow n) diffl ((& n) * (x pow (n num_sub 1))))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 335 Theorem REAL_ADD_RID autoloading from theory `REAL` ... @@ -22028,7 +22064,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22148,7 +22184,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f y) <= (f x))) ==> (l = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 572 Theorem REAL_NEG_EQ0 autoloading from theory `REAL` ... @@ -22193,7 +22229,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> f differentiable x) ==> (?z. a < z /\ z < b /\ (f diffl (& 0))z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3178 gfn = "\x. (f x) - ((((f b) - (f a)) / (b - a)) * x)" : term @@ -22257,7 +22293,7 @@ File lim.ml loaded () : void -Run time: 0.3s +Run time: 0.6s Intermediate theorems generated: 21608 #\ @@ -22267,7 +22303,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -22662,7 +22698,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (abs(f n)) * (z pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22838,7 +22874,7 @@ (\q. ((z + h) pow q) * (z pow (((n num_sub 2) num_sub p) num_sub q))))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 Theorem INV_SUC_EQ autoloading from theory `prim_rec` ... @@ -23129,7 +23165,7 @@ File powser.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 8507 #\ @@ -23139,7 +23175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -23960,7 +23996,7 @@ Intermediate theorems generated: 85 EXP_MONO_LE = |- !x y. (exp x) <= (exp y) = x <= y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 37 Theorem REAL_LE_ANTISYM autoloading from theory `REAL` ... @@ -24065,7 +24101,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 = @@ -24251,14 +24287,14 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1747 SIN_COS_NEG = |- !x. (((sin(-- x)) + (sin x)) pow 2) + (((cos(-- x)) - (cos x)) pow 2) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1099 Theorem REAL_SUMSQ autoloading from theory `REAL` ... @@ -24368,7 +24404,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24456,7 +24492,7 @@ Run time: 0.0s COS_ISZERO = |- ?! x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24489,7 +24525,7 @@ Theorem REAL_DIFFSQ autoloading from theory `REAL` ... REAL_DIFFSQ = |- !x y. (x + y) * (x - y) = (x * x) - (y * y) -Run time: 0.1s +Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 Run time: 0.0s @@ -24569,7 +24605,7 @@ Run time: 0.0s SIN_POS_PI = |- !x. (& 0) < x /\ x < pi ==> (& 0) < (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 96 COS_TOTAL = @@ -24838,7 +24874,7 @@ |- !y. atn y = (@x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 ASN = @@ -24915,7 +24951,7 @@ File transc.ml loaded () : void -Run time: 0.5s +Run time: 0.9s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24928,7 +24964,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -24950,7 +24986,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25016,7 +25052,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25048,7 +25084,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25157,7 +25193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25310,7 +25346,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25383,7 +25419,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25463,7 +25499,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25620,7 +25656,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25775,7 +25811,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -25992,7 +26028,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26014,7 +26050,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26033,7 +26069,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26078,7 +26114,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26143,7 +26179,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26193,7 +26229,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26263,7 +26299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26333,7 +26369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26369,7 +26405,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26422,7 +26458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26494,7 +26530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26573,7 +26609,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26768,7 +26804,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -26805,7 +26841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -27491,7 +27527,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -27963,7 +27999,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -28227,7 +28263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -28472,7 +28508,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -28936,7 +28972,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29404,7 +29440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29460,7 +29496,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29550,7 +29586,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29749,7 +29785,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29781,7 +29817,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -29915,7 +29951,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30218,7 +30254,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30250,7 +30286,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30289,7 +30325,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30321,7 +30357,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30482,7 +30518,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30615,7 +30651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30804,7 +30840,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30864,7 +30900,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -30989,7 +31025,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -31100,7 +31136,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -31125,7 +31161,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -31153,7 +31189,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -31266,7 +31302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -31769,7 +31805,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32017,7 +32053,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32243,7 +32279,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32285,7 +32321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32317,7 +32353,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32540,7 +32576,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -32933,7 +32969,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -33046,7 +33082,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -33549,7 +33585,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -33797,7 +33833,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34023,7 +34059,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34058,7 +34094,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34097,7 +34133,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34134,7 +34170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34155,7 +34191,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34252,7 +34288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34274,7 +34310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34770,7 +34806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34793,7 +34829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34871,7 +34907,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34930,7 +34966,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34974,7 +35010,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -34992,7 +35028,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35019,7 +35055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35063,7 +35099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35176,7 +35212,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35223,7 +35259,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35262,7 +35298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35336,7 +35372,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35425,7 +35461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35496,7 +35532,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35566,7 +35602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35615,7 +35651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35656,7 +35692,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35697,7 +35733,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35721,7 +35757,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35822,7 +35858,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35843,7 +35879,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -35868,7 +35904,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36494,7 +36530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36571,7 +36607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36598,7 +36634,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36715,7 +36751,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36810,7 +36846,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -36896,7 +36932,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37011,7 +37047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37104,7 +37140,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37280,7 +37316,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37384,7 +37420,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37679,7 +37715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37782,7 +37818,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37850,7 +37886,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -37912,7 +37948,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -38092,7 +38128,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -38133,7 +38169,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -38163,7 +38199,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -38189,7 +38225,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -38707,7 +38743,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -39244,7 +39280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -39432,7 +39468,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 + HOL88 Version 2.02 (GCL), built on 10/3/25 =============================================================================== #false : bool @@ -39450,10 +39486,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sat Apr 11 10:25:35 -12 2026 +Mon Mar 10 06:12:40 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Apr 11 10:25:35 -12 2026 +Mon Mar 10 06:12:40 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39471,22 +39507,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -HOL-LCF version 2.02 (GCL) created 11/4/26 +BASIC-HOL version 2.02 (GCL) created 10/3/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 11/4/26 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 10/3/25 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 11/4/26 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 10/3/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39552,8 +39588,8 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. +dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' for i in Manual/Tutorial/ack.tex Manual/Reference/ack.tex Manual/Description/ack.tex; do\ ln -snf ../Latex/ack.tex $i ; done @@ -40226,7 +40262,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, 338300 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' @@ -41865,7 +41901,7 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 1000236 bytes). +Output written on description.dvi (346 pages, 1000240 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' @@ -42433,7 +42469,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, 1083496 bytes). +Output written on description.dvi (353 pages, 1083500 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' @@ -44645,7 +44681,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, 1150936 bytes). +Output written on reference.dvi (669 pages, 1150940 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' @@ -46835,7 +46871,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, 1155404 bytes). +Output written on reference.dvi (669 pages, 1155412 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -52977,7 +53013,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.04.11:1026' -> endpages.ps +' TeX output 2025.03.10:0614' -> endpages.ps @@ -53049,7 +53085,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.04.11:1026' -> titlepages.ps +' TeX output 2025.03.10:0614' -> titlepages.ps @@ -53147,8 +53183,8 @@ dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.changes @@ -53157,12 +53193,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/1807892/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1807892/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/3194928 and its subdirectories -I: Current time: Sat Apr 11 10:26:35 -12 2026 -I: pbuilder-time-stamp: 1775946395 +I: removing directory /srv/workspace/pbuilder/1807892 and its subdirectories +I: Current time: Mon Mar 10 06:14:21 +14 2025 +I: pbuilder-time-stamp: 1741536861