Diff of the two buildlogs: -- --- b1/build.log 2025-03-09 08:38:29.424709394 +0000 +++ b2/build.log 2025-03-09 08:45:10.526662002 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Sat Mar 8 20:24:41 -12 2025 -I: pbuilder-time-stamp: 1741508681 +I: Current time: Sun Apr 12 05:01:30 +14 2026 +I: pbuilder-time-stamp: 1775919690 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,54 +26,86 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/8381/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/27174/tmp/hooks/D01_modify_environment starting +debug: Running on ionos6-i386. +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 Apr 11 15:01 /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/27174/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/27174/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='i386' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=11 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='i386' + 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]="i686-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=i386 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=21 ' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=i686 + HOST_ARCH=i386 IFS=' ' - INVOCATION_ID='6106952cee1c4836a16051c4ef9bc0b6' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - LD_LIBRARY_PATH='/usr/lib/libeatmydata' - LD_PRELOAD='libeatmydata.so' - 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='8381' - PS1='# ' - PS2='> ' + INVOCATION_ID=bbe9fd173a194547bdf29461c6cf29e3 + LANG=C + LANGUAGE=de_CH:de + LC_ALL=C + LD_LIBRARY_PATH=/usr/lib/libeatmydata + LD_PRELOAD=libeatmydata.so + MACHTYPE=i686-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=27174 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.27yZkJIS/pbuilderrc_DEt7 --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.27yZkJIS/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='112' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://46.16.76.132:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.27yZkJIS/pbuilderrc_ifaX --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.27yZkJIS/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=112 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://213.165.73.152:3128 I: uname -a - Linux ionos2-i386 6.1.0-31-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.128-1 (2025-02-07) 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 11:20 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/8381/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Mar 4 2025 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/27174/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -312,7 +344,7 @@ Get: 197 http://deb.debian.org/debian unstable/main i386 xdg-utils all 1.2.1-2 [75.8 kB] Get: 198 http://deb.debian.org/debian unstable/main i386 texlive-base all 2024.20250114-1 [22.8 MB] Get: 199 http://deb.debian.org/debian unstable/main i386 texlive-latex-base all 2024.20250114-1 [1282 kB] -Fetched 188 MB in 3s (75.1 MB/s) +Fetched 188 MB in 2s (95.3 MB/s) Preconfiguring packages ... Selecting previously unselected package libsystemd-shared:i386. (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 ... 19769 files and directories currently installed.) @@ -977,8 +1009,8 @@ Setting up tzdata (2025a-2) ... Current default time zone: 'Etc/UTC' -Local time is now: Sun Mar 9 08:25:41 UTC 2025. -Universal Time is now: Sun Mar 9 08:25:41 UTC 2025. +Local time is now: Sat Apr 11 15:02:03 UTC 2026. +Universal Time is now: Sat Apr 11 15:02:03 UTC 2026. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.13-1) ... @@ -1184,7 +1216,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/27174/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/27174/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 @@ -1438,12 +1474,49 @@ 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/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/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/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/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/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/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/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/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/taut/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/window/Manual' +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/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/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1451,21 +1524,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/trs/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/trs/Manual' +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/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/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/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/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1473,18 +1537,6 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/taut/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1492,19 +1544,18 @@ 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/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' +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/pred_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/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/string/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]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/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/abs_theory/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1512,24 +1563,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/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/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/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/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/arith/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/arith/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/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 \ @@ -1577,7 +1613,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Mar 8 20:27:37 -12 2025 +Sun Apr 12 05:03:01 +14 2026 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2815,7 +2851,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 # mem = - : (* -> * list -> bool) @@ -2953,7 +2989,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #.............start address -T 0x8ad990 () : void @@ -3112,7 +3148,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #.............start address -T 0x8ad990 () : void @@ -3304,7 +3340,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 # concat = - : (string -> string -> string) @@ -3414,7 +3450,7 @@ start address -T 0x8a2440 ;; Finished loading "lisp/f-ol-net" start address -T 0x7092f8 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 8/3/25 + version 2.02 (GCL) created 12/4/26 #...start address -T 0x6e6600 () : void @@ -3743,7 +3779,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 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 ###########################() : void @@ -3756,7 +3792,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 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 ################################################################################################() : void @@ -3901,7 +3937,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 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 ############################() : void @@ -3944,7 +3980,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 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 ############################Theory ind loaded () : void @@ -3981,7 +4017,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4022,7 +4058,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -4424,7 +4460,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -4492,7 +4528,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -4697,7 +4733,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -4821,7 +4857,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -4907,7 +4943,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5000,7 +5036,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5069,7 +5105,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5174,7 +5210,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5409,7 +5445,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5435,7 +5471,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5563,7 +5599,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5611,7 +5647,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5678,7 +5714,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5737,7 +5773,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5793,7 +5829,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 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre17 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5806,7 +5842,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #() : void @@ -5858,7 +5894,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ##########################() : void @@ -5889,7 +5925,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ##############################() : void @@ -5976,7 +6012,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #######################################################################() : void @@ -6129,7 +6165,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ###########################() : void @@ -6164,7 +6200,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #############################() : void @@ -6225,7 +6261,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ###########################Theory arithmetic loaded () : void @@ -6720,7 +6756,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ##################################() : void @@ -6867,7 +6903,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #################################Theory list loaded () : void @@ -7206,7 +7242,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ###############################Theory list loaded () : void @@ -8703,7 +8739,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #############################() : void @@ -9087,7 +9123,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ############################() : void @@ -9385,7 +9421,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ############################() : void @@ -9525,7 +9561,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ############################################() : void @@ -9622,7 +9658,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 ##################################() : void @@ -9652,7 +9688,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -9669,7 +9705,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #Theory num loaded () : void @@ -9688,7 +9724,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -9845,7 +9881,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 # @@ -9883,7 +9919,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 # @@ -9917,7 +9953,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -10002,7 +10038,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -10043,7 +10079,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -10227,7 +10263,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 # define_load_lib_function = - : (string list -> void -> void) @@ -10303,7 +10339,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 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre17 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10316,7 +10352,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #() : void @@ -10380,11 +10416,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Mar 8 20:30:23 -12 2025 +Sun Apr 12 05:04:24 +14 2026 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Mar 8 20:30:23 -12 2025 +Sun Apr 12 05:04:24 +14 2026 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10407,7 +10443,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -10491,7 +10527,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -10597,7 +10633,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11347,7 +11383,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11370,7 +11406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11413,7 +11449,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11449,7 +11485,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11501,7 +11537,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11533,7 +11569,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11571,7 +11607,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11599,7 +11635,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11676,7 +11712,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11698,7 +11734,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11752,7 +11788,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11801,7 +11837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11952,7 +11988,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -11996,7 +12032,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12071,7 +12107,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12121,7 +12157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12184,7 +12220,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12237,7 +12273,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12283,7 +12319,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12371,7 +12407,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12409,7 +12445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12470,7 +12506,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12534,7 +12570,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12560,7 +12596,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12585,7 +12621,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12624,7 +12660,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -12700,7 +12736,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13437,7 +13473,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13460,7 +13496,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13503,7 +13539,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13538,7 +13574,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13579,7 +13615,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13642,7 +13678,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13665,7 +13701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13690,7 +13726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13717,7 +13753,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -13753,7 +13789,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14285,7 +14321,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14308,7 +14344,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14342,7 +14378,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14397,7 +14433,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14488,7 +14524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14657,7 +14693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -14872,7 +14908,7 @@ |- !P l. woset l /\ (!x. fl l x /\ (!y. less l(y,x) ==> P y) ==> P x) ==> (!x. fl l x ==> P x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 469 WO_INDUCT_TAC = - : tactic @@ -14953,7 +14989,7 @@ Definition LESS_OR_EQ autoloading from theory `arithmetic` ... LESS_OR_EQ = |- !m n. m <= n = m < n \/ (m = n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 WO_RECURSE_NUM = @@ -14980,7 +15016,7 @@ Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l @@ -15009,7 +15045,7 @@ |- !l m. woset l ==> (m inseg l = (m = l) \/ (?a. fl l a /\ (m = linseg l a))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1172 EXTEND_FL = @@ -15057,7 +15093,7 @@ ORDINAL_UNION_LEMMA = |- !l x. ordinal l ==> fl l x ==> fl(Union ordinal)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 ORDINAL_UP = @@ -15084,7 +15120,7 @@ |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2506 ZL = @@ -15120,7 +15156,7 @@ File mk_wellorder loaded () : void -Run time: 0.5s +Run time: 0.2s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15129,7 +15165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -15260,7 +15296,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -15352,7 +15388,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -15431,7 +15467,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2546 () : void @@ -15441,15 +15477,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Sat Mar 8 20:31:46 -12 2025 +===> abs_theory rebuilt on Sun Apr 12 05:05:00 +14 2026 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -15622,7 +15658,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -15875,7 +15911,7 @@ TRAT_MUL_ASSOC = |- !h i j. (h trat_mul (i trat_mul j)) trat_eq ((h trat_mul i) trat_mul j) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 189 Theorem LEFT_ADD_DISTRIB autoloading from theory `arithmetic` ... @@ -16049,7 +16085,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 11032 #\ @@ -16059,7 +16095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -16361,7 +16397,7 @@ Intermediate theorems generated: 3 CUT_NONEMPTY = |- !X. ?x. cut X x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 37 CUT_BOUNDED = |- !X. ?x. ~cut X x @@ -16455,7 +16491,7 @@ isacut (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 502 HREAL_ADD_ISACUT = @@ -16469,7 +16505,7 @@ Intermediate theorems generated: 537 HREAL_ADD_SYM = |- !X Y. X hreal_add Y = Y hreal_add X -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 124 HREAL_MUL_SYM = |- !X Y. X hreal_mul Y = Y hreal_mul X @@ -16522,7 +16558,7 @@ HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16559,7 +16595,7 @@ File hreal.ml loaded () : void -Run time: 0.3s +Run time: 0.1s Intermediate theorems generated: 10456 #\ @@ -16569,7 +16605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -16844,7 +16880,7 @@ TREAL_ADD_ASSOC = |- !x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 63 Theorem HREAL_MUL_ASSOC autoloading from theory `HREAL` ... @@ -16921,7 +16957,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -16936,7 +16972,7 @@ |- (!h. hreal_of_treal(treal_of_hreal h) = h) /\ (!r. treal_0 treal_lt r = (treal_of_hreal(hreal_of_treal r)) treal_eq r) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 986 TREAL_ISO = @@ -17028,7 +17064,7 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -17098,7 +17134,7 @@ |- !x y z. y real_lt z ==> (x real_add y) real_lt (x real_add z); |- !x y. r0 real_lt x /\ r0 real_lt y ==> r0 real_lt (x real_mul y)] : thm list -Run time: 0.1s +Run time: 0.0s () : void Run time: 0.0s @@ -17107,7 +17143,7 @@ File realax.ml loaded () : void -Run time: 0.5s +Run time: 0.2s Intermediate theorems generated: 26795 #\ @@ -17117,7 +17153,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -17409,7 +17445,7 @@ Intermediate theorems generated: 26 REAL_NOT_LE = |- !x y. ~x <= y = y < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 19 REAL_LE_TOTAL = |- !x y. x <= y \/ y <= x @@ -17509,7 +17545,7 @@ Intermediate theorems generated: 20 REAL_LE_RADD = |- !x y z. (x + z) <= (y + z) = x <= y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 20 REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) @@ -17525,7 +17561,7 @@ Intermediate theorems generated: 22 REAL_LT_ADD = |- !x y. (& 0) < x /\ (& 0) < y ==> (& 0) < (x + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_LT_ADDNEG = |- !x y z. y < (x + (-- z)) = (y + z) < x @@ -17625,7 +17661,7 @@ Intermediate theorems generated: 114 REAL_LT_IMP_NE = |- !x y. x < y ==> ~(x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 43 REAL_INV_POS = |- !x. (& 0) < x ==> (& 0) < (inv x) @@ -17717,7 +17753,7 @@ Intermediate theorems generated: 321 REAL_LT = |- !m n. (& m) < (& n) = m num_lt n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 Theorem LESS_EQUAL_ANTISYM autoloading from theory `arithmetic` ... @@ -17774,7 +17810,7 @@ Intermediate theorems generated: 20 REAL_LT_NZ = |- !n. ~(& n = & 0) = (& 0) < (& n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 90 REAL_NZ_IMP_LT = |- !n. ~(n = 0) ==> (& 0) < (& n) @@ -17904,7 +17940,7 @@ Intermediate theorems generated: 33 REAL_LET_ADD = |- !x y. (& 0) <= x /\ (& 0) < y ==> (& 0) < (x + y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 33 REAL_LTE_ADD = |- !x y. (& 0) < x /\ (& 0) <= y ==> (& 0) < (x + y) @@ -17931,7 +17967,7 @@ Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c @@ -18027,7 +18063,7 @@ Intermediate theorems generated: 36 REAL_EQ_LMUL_IMP = |- !x y z. ~(x = & 0) /\ (x * y = x * z) ==> (y = z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 Theorem FACT_LESS autoloading from theory `arithmetic` ... @@ -18080,7 +18116,7 @@ Intermediate theorems generated: 9 ABS_1 = |- abs(& 1) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 31 ABS_NEG = |- !x. abs(-- x) = abs x @@ -18134,7 +18170,7 @@ ABS_BETWEEN = |- !x y d. (& 0) < d /\ (x - d) < y /\ y < (x + d) = (abs(y - x)) < d -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) @@ -18233,7 +18269,7 @@ Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) @@ -18293,14 +18329,14 @@ Intermediate theorems generated: 103 POW_MINUS1 = |- !n. (--(& 1)) pow (2 num_mul n) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 231 REAL_SUP_SOMEPOS = |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -18340,7 +18376,7 @@ REAL_SUP_UBOUND = |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 87 SETOK_LE_LT = @@ -18398,7 +18434,7 @@ Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 109 SUM_DIFF = |- !f m n. Sum(m,n)f = (Sum(0,m num_add n)f) - (Sum(0,m)f) @@ -18428,7 +18464,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)) @@ -18466,7 +18502,7 @@ |- !f N. (!n. n num_ge N ==> (f n = & 0)) ==> (!m n. m num_ge N ==> (Sum(m,n)f = & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 145 SUM_ADD = @@ -18525,7 +18561,7 @@ SUM_GROUP = |- !n k f. Sum(0,n)(\m. Sum(m num_mul k,k)f) = Sum(0,n num_mul k)f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 169 SUM_1 = |- !f n. Sum(n,1)f = f n @@ -18596,7 +18632,7 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2469 SUM_CANCEL = @@ -18612,7 +18648,7 @@ File real.ml loaded () : void -Run time: 1.8s +Run time: 0.8s Intermediate theorems generated: 23746 #\ @@ -18622,7 +18658,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -18827,7 +18863,7 @@ Intermediate theorems generated: 2 CLOSED_LIMPT = |- !top S. closed top S = (!x. limpt top x S ==> S x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 433 ismet = @@ -18982,7 +19018,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -19032,7 +19068,7 @@ Theorem REAL_ADD_SUB autoloading from theory `REAL` ... REAL_ADD_SUB = |- !x y. (x + y) - x = y -Run time: 0.1s +Run time: 0.0s MR1_ADD = |- !x d. dist mr1(x,x + d) = abs d Run time: 0.0s @@ -19106,7 +19142,7 @@ File topology.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 4132 #\ @@ -19116,7 +19152,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -19321,7 +19357,7 @@ Run time: 0.0s DORDER_TENDSTO = |- !m x. dorder(tendsto(m,x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 257 Definition re_subset autoloading from theory `TOPOLOGY` ... @@ -19490,7 +19526,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19509,7 +19545,7 @@ Theorem REAL_LT autoloading from theory `REAL` ... REAL_LT = |- !m n. (& m) < (& n) = m num_lt n -Run time: 0.1s +Run time: 0.0s NET_CONV_BOUNDED = |- !g x x0. (x --> x0)(mtop mr1,g) ==> bounded(mr1,g)x @@ -19841,7 +19877,7 @@ File nets.ml loaded () : void -Run time: 0.3s +Run time: 0.1s Intermediate theorems generated: 7389 #\ @@ -19851,7 +19887,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -20157,7 +20193,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.1s +Run time: 0.0s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -20424,7 +20460,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20787,7 +20823,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20931,7 +20967,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -21135,7 +21171,7 @@ File seq.ml loaded () : void -Run time: 0.6s +Run time: 0.3s Intermediate theorems generated: 18704 #\ @@ -21145,7 +21181,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -21675,7 +21711,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21896,7 +21932,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.0s +Run time: 0.1s Theorem ADD_SUB autoloading from theory `arithmetic` ... ADD_SUB = |- !a c. (a num_add c) num_sub c = a @@ -21974,7 +22010,7 @@ Theorem REAL_MUL_RINV autoloading from theory `REAL` ... REAL_MUL_RINV = |- !x. ~(x = & 0) ==> (x * (inv x) = & 1) -Run time: 0.1s +Run time: 0.0s Theorem REAL_INV_MUL autoloading from theory `REAL` ... REAL_INV_MUL = @@ -22172,7 +22208,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: 96 INTERVAL_LEMMA = @@ -22197,7 +22233,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 @@ -22261,7 +22297,7 @@ File lim.ml loaded () : void -Run time: 0.6s +Run time: 0.3s Intermediate theorems generated: 21608 #\ @@ -22271,7 +22307,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -22391,7 +22427,7 @@ SUB = |- (!m. 0 num_sub m = 0) /\ (!m n. (SUC m) num_sub n = (m num_lt n => 0 | SUC(m num_sub n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem LESS_IMP_LESS_OR_EQ autoloading from theory `arithmetic` ... @@ -22842,7 +22878,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` ... @@ -23021,7 +23057,7 @@ (& 0) < (abs h) /\ (abs h) < k ==> (!n. (abs(g h n)) <= ((f n) * (abs h)))) ==> ((\h. suminf(g h)) tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 502 Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... @@ -23133,7 +23169,7 @@ File powser.ml loaded () : void -Run time: 0.3s +Run time: 0.1s Intermediate theorems generated: 8507 #\ @@ -23143,7 +23179,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -23805,7 +23841,7 @@ Run time: 0.0s EXP_0 = |- exp(& 0) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 274 Theorem REAL_LE_REFL autoloading from theory `REAL` ... @@ -24167,7 +24203,7 @@ Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 690 Theorem REAL_ADD_RINV autoloading from theory `REAL` ... @@ -24203,7 +24239,7 @@ Run time: 0.0s SIN_BOUND = |- !x. (abs(sin x)) <= (& 1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem ABS_BOUNDS autoloading from theory `REAL` ... @@ -24284,7 +24320,7 @@ Run time: 0.0s SIN_NEG = |- !x. sin(-- x) = --(sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 COS_NEG = |- !x. cos(-- x) = cos x @@ -24496,7 +24532,7 @@ Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 212 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -24712,7 +24748,7 @@ Intermediate theorems generated: 46 TAN_PERIODIC = |- !x. tan(x + ((& 2) * pi)) = tan x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 24 Theorem REAL_LDISTRIB autoloading from theory `REAL` ... @@ -24824,7 +24860,7 @@ TAN_TOTAL = |- !y. ?! x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1301 asn = @@ -24904,7 +24940,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 TAN_ATN = @@ -24919,7 +24955,7 @@ File transc.ml loaded () : void -Run time: 1.2s +Run time: 0.5s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24932,7 +24968,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -24954,7 +24990,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25020,7 +25056,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25052,7 +25088,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25161,7 +25197,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25314,7 +25350,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25387,7 +25423,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25467,7 +25503,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25624,7 +25660,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25779,7 +25815,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -25996,7 +26032,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26018,7 +26054,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26037,7 +26073,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26082,7 +26118,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26147,7 +26183,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26197,7 +26233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26267,7 +26303,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26337,7 +26373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26373,7 +26409,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26426,7 +26462,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26498,7 +26534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26577,7 +26613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26772,7 +26808,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -26809,7 +26845,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -27495,7 +27531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -27967,7 +28003,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -28231,7 +28267,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -28476,7 +28512,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -28940,7 +28976,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29408,7 +29444,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29464,7 +29500,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29554,7 +29590,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29753,7 +29789,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29785,7 +29821,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -29919,7 +29955,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30222,7 +30258,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30254,7 +30290,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30293,7 +30329,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30325,7 +30361,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30486,7 +30522,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30619,7 +30655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30808,7 +30844,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30868,7 +30904,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -30993,7 +31029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -31104,7 +31140,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -31129,7 +31165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -31157,7 +31193,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -31270,7 +31306,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -31773,7 +31809,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32021,7 +32057,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32247,7 +32283,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32289,7 +32325,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32321,7 +32357,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32544,7 +32580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -32937,7 +32973,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -33050,7 +33086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -33553,7 +33589,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -33801,7 +33837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34027,7 +34063,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34062,7 +34098,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34101,7 +34137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34138,7 +34174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34159,7 +34195,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34256,7 +34292,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34278,7 +34314,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34774,7 +34810,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34797,7 +34833,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34875,7 +34911,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34934,7 +34970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34978,7 +35014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -34996,7 +35032,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35023,7 +35059,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35067,7 +35103,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35180,7 +35216,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35227,7 +35263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35266,7 +35302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35340,7 +35376,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35429,7 +35465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35500,7 +35536,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35570,7 +35606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35619,7 +35655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35660,7 +35696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35701,7 +35737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35725,7 +35761,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35826,7 +35862,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35847,7 +35883,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -35872,7 +35908,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36498,7 +36534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36575,7 +36611,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36602,7 +36638,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36719,7 +36755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36814,7 +36850,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -36900,7 +36936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37015,7 +37051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37108,7 +37144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37284,7 +37320,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37388,7 +37424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37683,7 +37719,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37786,7 +37822,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37854,7 +37890,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -37916,7 +37952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -38096,7 +38132,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -38137,7 +38173,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -38167,7 +38203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -38193,7 +38229,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -38711,7 +38747,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -39248,7 +39284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -39436,7 +39472,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #false : bool @@ -39454,10 +39490,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Sat Mar 8 20:36:07 -12 2025 +Sun Apr 12 05:07:05 +14 2026 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Sat Mar 8 20:36:07 -12 2025 +Sun Apr 12 05:07:05 +14 2026 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39475,7 +39511,7 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -BASIC-HOL version 2.02 (GCL) created 8/3/25 +HOL-LCF version 2.02 (GCL) created 12/4/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39483,14 +39519,14 @@ # =============================================================================== - HOL88 Version 2.02 (GCL), built on 8/3/25 + HOL88 Version 2.02 (GCL), built on 12/4/26 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 8/3/25 +BASIC-HOL version 2.02 (GCL) created 12/4/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41869,7 +41905,7 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 1000240 bytes). +Output written on description.dvi (346 pages, 1000236 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' @@ -42437,7 +42473,7 @@ (./drules.aux) (./conv.aux) (./tactics.aux) (./see.aux) (./references.aux) (./version2.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on description.dvi (353 pages, 1083500 bytes). +Output written on description.dvi (353 pages, 1083496 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' @@ -44649,7 +44685,7 @@ [663]) (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1150940 bytes). +Output written on reference.dvi (669 pages, 1150936 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' @@ -46839,7 +46875,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, 1155412 bytes). +Output written on reference.dvi (669 pages, 1155404 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' @@ -52981,7 +53017,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.03.08:2038' -> endpages.ps +' TeX output 2026.04.12:0507' -> endpages.ps @@ -53053,7 +53089,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.03.08:2038' -> titlepages.ps +' TeX output 2026.04.12:0507' -> titlepages.ps @@ -53146,13 +53182,13 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_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-library-help' in '../hol88-library-help_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'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_i386.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_i386.changes @@ -53161,12 +53197,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/27174/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/27174/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/8381 and its subdirectories -I: Current time: Sat Mar 8 20:38:28 -12 2025 -I: pbuilder-time-stamp: 1741509508 +I: removing directory /srv/workspace/pbuilder/27174 and its subdirectories +I: Current time: Sun Apr 12 05:08:07 +14 2026 +I: pbuilder-time-stamp: 1775920087