Diff of the two buildlogs: -- --- b1/build.log 2025-03-12 17:35:08.930411671 +0000 +++ b2/build.log 2025-03-12 18:27:59.335537341 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Apr 14 11:34:14 -12 2026 -I: pbuilder-time-stamp: 1776209654 +I: Current time: Thu Mar 13 07:35:12 +14 2025 +I: pbuilder-time-stamp: 1741800912 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -25,52 +25,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/3988796/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/329909/tmp/hooks/D01_modify_environment starting +debug: Running on ionos1-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Mar 12 17:35 /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/329909/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/329909/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="37" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.37(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=20 ' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='f08f7862a4ed4509a1732411a89e0882' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='3988796' - PS1='# ' - PS2='> ' + INVOCATION_ID=55ca1c337eb94a1cb1a5eefdf2c6005e + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=329909 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.aoOuHpxI/pbuilderrc_GRwh --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.aoOuHpxI/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='111' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://213.165.73.152:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.aoOuHpxI/pbuilderrc_7yqd --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.aoOuHpxI/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=110 + SUDO_UID=105 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://46.16.76.132:3128 I: uname -a - Linux ionos15-amd64 6.12.12+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.12-1~bpo12+1 (2025-02-23) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-31-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.128-1 (2025-02-07) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Mar 4 2025 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/3988796/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Mar 4 11:20 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/329909/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -309,7 +341,7 @@ Get: 197 http://deb.debian.org/debian unstable/main amd64 xdg-utils all 1.2.1-2 [75.8 kB] Get: 198 http://deb.debian.org/debian unstable/main amd64 texlive-base all 2024.20250114-1 [22.8 MB] Get: 199 http://deb.debian.org/debian unstable/main amd64 texlive-latex-base all 2024.20250114-1 [1282 kB] -Fetched 190 MB in 8s (24.1 MB/s) +Fetched 190 MB in 11s (18.1 MB/s) Preconfiguring packages ... Selecting previously unselected package libsystemd-shared:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19783 files and directories currently installed.) @@ -975,8 +1007,8 @@ Setting up tzdata (2025a-2) ... Current default time zone: 'Etc/UTC' -Local time is now: Tue Apr 14 23:36:39 UTC 2026. -Universal Time is now: Tue Apr 14 23:36:39 UTC 2026. +Local time is now: Wed Mar 12 17:39:44 UTC 2025. +Universal Time is now: Wed Mar 12 17:39:44 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.13-1) ... @@ -1181,7 +1213,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/329909/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/329909/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 @@ -1435,21 +1471,6 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1457,6 +1478,12 @@ 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/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/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/abs_theory/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1464,49 +1491,43 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +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/res_quan/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/res_quan/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/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/pair/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +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/res_quan/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/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/latex-hol/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' -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/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1514,6 +1535,15 @@ 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/trs/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1521,12 +1551,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/window/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ -printf '\\begin{theindex}' >index.tex; \ -printf '\\mbox{}' >>index.tex; \ -printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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' 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 \ @@ -1574,7 +1610,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Apr 14 11:38:52 -12 2026 +Thu Mar 13 07:44:24 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2812,7 +2848,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 # mem = - : (* -> * list -> bool) @@ -2950,7 +2986,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #.............start address -T 0xa8ab70 () : void @@ -3109,7 +3145,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #.............start address -T 0xa8ab70 () : void @@ -3301,7 +3337,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 # concat = - : (string -> string -> string) @@ -3411,7 +3447,7 @@ start address -T 0xa80c40 ;; Finished loading "lisp/f-ol-net" start address -T 0x856fd0 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 14/4/26 + version 2.02 (GCL) created 13/3/25 #...start address -T 0xa8cd90 () : void @@ -3740,7 +3776,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 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 ###########################() : void @@ -3753,7 +3789,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 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 ################################################################################################() : void @@ -3898,7 +3934,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 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 ############################() : void @@ -3941,7 +3977,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 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 ############################Theory ind loaded () : void @@ -3978,7 +4014,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4019,7 +4055,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4421,7 +4457,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4489,7 +4525,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4694,7 +4730,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4818,7 +4854,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4904,7 +4940,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -4997,7 +5033,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5066,7 +5102,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5171,7 +5207,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5406,7 +5442,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5432,7 +5468,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5560,7 +5596,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5608,7 +5644,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5675,7 +5711,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5734,7 +5770,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5790,7 +5826,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 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #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) @@ -5803,7 +5839,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #() : void @@ -5855,7 +5891,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ##########################() : void @@ -5886,7 +5922,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ##############################() : void @@ -5973,7 +6009,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #######################################################################() : void @@ -6126,7 +6162,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ###########################() : void @@ -6161,7 +6197,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #############################() : void @@ -6222,7 +6258,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ###########################Theory arithmetic loaded () : void @@ -6717,7 +6753,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ##################################() : void @@ -6864,7 +6900,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #################################Theory list loaded () : void @@ -7203,7 +7239,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ###############################Theory list loaded () : void @@ -8700,7 +8736,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #############################() : void @@ -9084,7 +9120,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ############################() : void @@ -9382,7 +9418,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ############################() : void @@ -9522,7 +9558,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ############################################() : void @@ -9619,7 +9655,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 ##################################() : void @@ -9649,7 +9685,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -9666,7 +9702,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #Theory num loaded () : void @@ -9685,7 +9721,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -9842,7 +9878,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 # @@ -9880,7 +9916,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 # @@ -9914,7 +9950,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -9999,7 +10035,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -10040,7 +10076,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -10224,7 +10260,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10300,7 +10336,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 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #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) @@ -10313,7 +10349,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #() : void @@ -10377,11 +10413,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Apr 14 11:43:40 -12 2026 +Thu Mar 13 07:54:06 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Apr 14 11:43:40 -12 2026 +Thu Mar 13 07:54:07 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10404,7 +10440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -10488,7 +10524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -10594,7 +10630,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11344,7 +11380,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11367,7 +11403,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11410,7 +11446,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11446,7 +11482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11498,7 +11534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11530,7 +11566,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11568,7 +11604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11596,7 +11632,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11673,7 +11709,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11695,7 +11731,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11749,7 +11785,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11798,7 +11834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11949,7 +11985,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -11993,7 +12029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12068,7 +12104,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12118,7 +12154,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12181,7 +12217,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12234,7 +12270,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12280,7 +12316,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12368,7 +12404,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12406,7 +12442,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12467,7 +12503,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12531,7 +12567,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12557,7 +12593,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12582,7 +12618,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12621,7 +12657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -12697,7 +12733,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13434,7 +13470,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13457,7 +13493,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13500,7 +13536,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13535,7 +13571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13576,7 +13612,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13639,7 +13675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13662,7 +13698,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13687,7 +13723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13714,7 +13750,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -13750,7 +13786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14282,7 +14318,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14305,7 +14341,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14339,7 +14375,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14394,7 +14430,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14485,7 +14521,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14654,7 +14690,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -14818,7 +14854,7 @@ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. P z ==> l(y,z)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1294 PAIRED_EXT = |- !l m. (!x y. l(x,y) = m(x,y)) = (l = m) @@ -14887,7 +14923,7 @@ l(ms z,m) /\ l(ms z,n) ==> (f z = g z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1165 WO_RECURSE_LOCAL = @@ -14897,7 +14933,7 @@ (!f f' x. (!y. less l(ms y,ms x) ==> (f y = f' y)) ==> (h f x = h f' x)) ==> (!n. ?f. !x. l(ms x,n) ==> (f x = h f x)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1556 WO_RECURSE_EXISTS = @@ -14957,7 +14993,7 @@ |- !h ms. (!f g x. (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) @@ -14973,7 +15009,7 @@ Intermediate theorems generated: 68 INSEG_SUBSET_FL = |- !l m. m inseg l ==> (!x. fl m x ==> fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 187 INSEG_WOSET = |- !l m. m inseg l /\ woset l ==> woset m @@ -15016,7 +15052,7 @@ EXTEND_INSEG = |- !l a. woset l /\ fl l a ==> (\(x,y). l(x,y) /\ l(y,a)) inseg l -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 57 EXTEND_LINSEG = @@ -15024,7 +15060,7 @@ woset l /\ fl l a ==> (\(x,y). linseg l a(x,y) \/ (y = a) /\ (fl(linseg l a)x \/ (x = a))) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 489 ORDINAL_CHAINED = @@ -15045,11 +15081,11 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = @@ -15070,7 +15106,7 @@ WO_FL_RESTRICT = |- !l. woset l ==> (!P. fl(\(x,y). P x /\ P y /\ l(x,y))x = P x /\ fl l x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) @@ -15081,7 +15117,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 = @@ -15111,13 +15147,13 @@ Intermediate theorems generated: 1083 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File mk_wellorder loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15126,7 +15162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -15257,7 +15293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -15349,7 +15385,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -15441,12 +15477,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Tue Apr 14 11:46:38 -12 2026 +===> abs_theory rebuilt on Thu Mar 13 07:58:47 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -15619,7 +15655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -15803,7 +15839,7 @@ Intermediate theorems generated: 152 TRAT_EQ_AP = |- !p q. (p = q) ==> p trat_eq q -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 8 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -15912,7 +15948,7 @@ Theorem LESS_LESS_CASES autoloading from theory `arithmetic` ... LESS_LESS_CASES = |- !m n. (m = n) \/ m < n \/ n < m -Run time: 0.0s +Run time: 0.1s TRAT_ADD_TOTAL = |- !h i. @@ -16046,7 +16082,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 11032 #\ @@ -16056,7 +16092,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -16299,7 +16335,7 @@ Intermediate theorems generated: 85 HRAT_UP = |- !x. ?y. x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 HRAT_DOWN = |- !x. ?y. y hrat_lt x @@ -16444,7 +16480,7 @@ Intermediate theorems generated: 2 hreal_lt = |- !X Y. X hreal_lt Y = ~(X = Y) /\ (!x. cut X x ==> cut Y x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 HREAL_INV_ISACUT = @@ -16452,7 +16488,7 @@ isacut (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 502 HREAL_ADD_ISACUT = @@ -16499,7 +16535,7 @@ Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 155 hreal_sub = @@ -16519,7 +16555,7 @@ HREAL_SUB_ADD = |- !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X @@ -16550,7 +16586,7 @@ Intermediate theorems generated: 553 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 @@ -16566,7 +16602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -16816,7 +16852,7 @@ TREAL_EQ_TRANS = |- !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1147 TREAL_EQ_EQUIV = |- !p q. p treal_eq q = ($treal_eq p = $treal_eq q) @@ -16906,7 +16942,7 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1063 TREAL_LT_ADD = @@ -16922,7 +16958,7 @@ Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 hreal_of_treal = |- !x y. hreal_of_treal(x,y) = (@d. x = y hreal_add d) @@ -16991,7 +17027,7 @@ |- !x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==> (x1 treal_lt y1 = x2 treal_lt y2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 60 TREAL_INV_WELLDEF = @@ -17025,7 +17061,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.1s +Run time: 0.2s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -17075,7 +17111,7 @@ (?x. P x) /\ (?z. !x. P x ==> x real_lt z) ==> (?s. !y. (?x. P x /\ y real_lt x) = y real_lt s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 199 [|- ~(r1 = r0); @@ -17095,7 +17131,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.0s +Run time: 0.1s () : void Run time: 0.0s @@ -17104,7 +17140,7 @@ File realax.ml loaded () : void -Run time: 0.5s +Run time: 0.7s Intermediate theorems generated: 26795 #\ @@ -17114,7 +17150,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -17354,7 +17390,7 @@ Intermediate theorems generated: 18 REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 101 REAL_MUL_LZERO = |- !x. (& 0) * x = & 0 @@ -17370,7 +17406,7 @@ Intermediate theorems generated: 62 REAL_NEG_RMUL = |- !x y. --(x * y) = x * (-- y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 18 REAL_NEGNEG = |- !x. --(-- x) = x @@ -17478,7 +17514,7 @@ Intermediate theorems generated: 25 REAL_LT_NEGTOTAL = |- !x. (x = & 0) \/ (& 0) < x \/ (& 0) < (-- x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 REAL_LE_NEGTOTAL = |- !x. (& 0) <= x \/ (& 0) <= (-- x) @@ -17510,7 +17546,7 @@ Intermediate theorems generated: 20 REAL_LT_ADD2 = |- !w x y z. w < x /\ y < z ==> (w + y) < (x + z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 55 REAL_LE_ADD2 = |- !w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z) @@ -17574,7 +17610,7 @@ Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 32 REAL_SUB_LT = |- !x y. (& 0) < (x - y) = y < x @@ -17646,7 +17682,7 @@ Intermediate theorems generated: 22 REAL_LT_RMUL_IMP = |- !x y z. x < y /\ (& 0) < z ==> (x * z) < (y * z) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 29 REAL_LT_LMUL_IMP = |- !x y z. y < z /\ (& 0) < x ==> (x * y) < (x * z) @@ -17654,7 +17690,7 @@ Intermediate theorems generated: 29 REAL_LINV_UNIQ = |- !x y. (x * y = & 1) ==> (x = inv y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) @@ -17751,7 +17787,7 @@ Run time: 0.0s REAL_MUL = |- !m n. (& m) * (& n) = &(m num_mul n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 148 REAL_INV1 = |- inv(& 1) = & 1 @@ -17779,7 +17815,7 @@ Intermediate theorems generated: 28 REAL_LT_RDIV_0 = |- !y z. (& 0) < z ==> ((& 0) < (y / z) = (& 0) < y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 REAL_LT_RDIV = |- !x y z. (& 0) < z ==> ((x / z) < (y / z) = x < y) @@ -17840,7 +17876,7 @@ Intermediate theorems generated: 51 REAL_DOWN = |- !x. (& 0) < x ==> (?y. (& 0) < y /\ y < x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 24 REAL_DOWN2 = @@ -17873,7 +17909,7 @@ Intermediate theorems generated: 38 REAL_LT_NEG = |- !x y. (-- x) < (-- y) = y < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 79 REAL_LE_NEG = |- !x y. (-- x) <= (-- y) = y <= x @@ -17905,7 +17941,7 @@ Intermediate theorems generated: 33 REAL_LTE_ADD = |- !x y. (& 0) < x /\ (& 0) <= y ==> (& 0) < (x + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 33 REAL_LT_MUL2 = @@ -18012,7 +18048,7 @@ Intermediate theorems generated: 8 REAL_INV_LT1 = |- !x. (& 0) < x /\ x < (& 1) ==> (& 1) < (inv x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 290 REAL_POS_NZ = |- !x. (& 0) < x ==> ~(x = & 0) @@ -18061,7 +18097,7 @@ Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 87 abs = |- !x. abs x = ((& 0) <= x => x | -- x) @@ -18106,7 +18142,7 @@ Intermediate theorems generated: 31 ABS_NZ = |- !x. ~(x = & 0) = (& 0) < (abs x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) @@ -18135,7 +18171,7 @@ Intermediate theorems generated: 372 ABS_BOUND = |- !x y d. (abs(x - y)) < d ==> y < (x + d) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 54 ABS_STILLNZ = |- !x y. (abs(x - y)) < (abs y) ==> ~(x = & 0) @@ -18143,7 +18179,7 @@ Intermediate theorems generated: 56 ABS_CASES = |- !x. (x = & 0) \/ (& 0) < (abs x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z @@ -18181,7 +18217,7 @@ (abs(x - x0)) < ((y0 - x0) / (& 2)) /\ (abs(y - y0)) < ((y0 - x0) / (& 2)) ==> x < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 935 ABS_BOUNDS = |- !x k. (abs x) <= k = (-- k) <= x /\ x <= k @@ -18189,7 +18225,7 @@ Intermediate theorems generated: 250 pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 175 POW_0 = |- !n. (& 0) pow (SUC n) = & 0 @@ -18226,7 +18262,7 @@ Intermediate theorems generated: 152 POW_1 = |- !x. x pow 1 = x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 POW_2 = |- !x. x pow 2 = x * x @@ -18254,7 +18290,7 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 @@ -18270,7 +18306,7 @@ Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 73 Theorem LESS_EQ_SUC_REFL autoloading from theory `arithmetic` ... @@ -18313,14 +18349,14 @@ SUP_LEMMA3 = |- !d. (?z. !x. P x ==> x < z) ==> (?z. !x. (\x. P(x + d))x ==> x < z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 42 REAL_SUP_EXISTS = |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 45 sup = |- !P. sup P = (@s. !y. (?x. P x /\ y < x) = y < s) @@ -18395,7 +18431,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) @@ -18425,7 +18461,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)) @@ -18463,7 +18499,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 = @@ -18472,7 +18508,7 @@ Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) @@ -18530,13 +18566,13 @@ Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 81 SUM_OFFSET = |- !f n k. Sum(0,n)(\m. f(m num_add k)) = (Sum(0,n num_add k)f) - (Sum(0,k)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 141 SUM_REINDEX = @@ -18609,7 +18645,7 @@ File real.ml loaded () : void -Run time: 1.6s +Run time: 2.1s Intermediate theorems generated: 23746 #\ @@ -18619,7 +18655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -18783,7 +18819,7 @@ Intermediate theorems generated: 34 TOPOLOGY_UNION = |- !L P. P re_subset (open L) ==> open L(re_Union P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 45 neigh = @@ -18902,7 +18938,7 @@ METRIC_TRIANGLE = |- !m x y z. (dist m(x,z)) <= ((dist m(x,y)) + (dist m(y,z))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 52 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -19053,7 +19089,7 @@ Intermediate theorems generated: 34 MR1_SUB_LE = |- !x d. (& 0) <= d ==> (dist mr1(x,x - d) = d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 Theorem REAL_LT_IMP_LE autoloading from theory `REAL` ... @@ -19103,7 +19139,7 @@ File topology.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 4132 #\ @@ -19113,7 +19149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -19287,7 +19323,7 @@ Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... LESS_EQ_TRANS = |- !m n p. m num_le n /\ n num_le p ==> m num_le p -Run time: 0.0s +Run time: 0.1s Theorem LESS_EQ_CASES autoloading from theory `arithmetic` ... LESS_EQ_CASES = |- !m n. m num_le n \/ n num_le m @@ -19390,7 +19426,7 @@ dorder g ==> (x --> x0)(mtop d,g) /\ (x --> x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 313 SEQ_TENDS = @@ -19487,7 +19523,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` ... @@ -19594,7 +19630,7 @@ (!x y. (x --> (& 0))(mtop mr1,g) /\ (y --> (& 0))(mtop mr1,g) ==> ((\n. (x n) + (y n)) --> (& 0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 324 Theorem REAL_LT_MUL2 autoloading from theory `REAL` ... @@ -19705,7 +19741,7 @@ (!x x0 y y0. (x --> x0)(mtop mr1,g) /\ (y --> y0)(mtop mr1,g) ==> ((\n. (x n) - (y n)) --> (x0 - y0))(mtop mr1,g)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 95 Theorem REAL_ADD_LID autoloading from theory `REAL` ... @@ -19848,7 +19884,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -19996,7 +20032,7 @@ |- !d x x0. (x tends x0)(mtop d,$num_ge) = (!e. (& 0) < e ==> (?N. !n. n num_ge N ==> (dist d(x n,x0)) < e)) -Run time: 0.0s +Run time: 0.1s SEQ = |- !x x0. @@ -20117,7 +20153,7 @@ dorder g ==> (x tends x0)(mtop d,g) /\ (x tends x1)(mtop d,g) ==> (x0 = x1) -Run time: 0.1s +Run time: 0.0s SEQ_UNIQ = |- !x x1 x2. x --> x1 /\ x --> x2 ==> (x1 = x2) Run time: 0.0s @@ -20383,7 +20419,7 @@ Intermediate theorems generated: 39 SEQ_BCONV = |- !f. bounded(mr1,$num_ge)f /\ mono f ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... @@ -20573,7 +20609,7 @@ Theorem REAL_LT_ADDL autoloading from theory `REAL` ... REAL_LT_ADDL = |- !x y. y < (x + y) = (& 0) < x -Run time: 0.0s +Run time: 0.1s Theorem REAL_LE autoloading from theory `REAL` ... REAL_LE = |- !m n. (& m) <= (& n) = m num_le n @@ -20667,7 +20703,7 @@ (!n. (f n) <= (g n)) /\ (\n. (f n) - (g n)) --> (& 0) ==> (?l. ((!n. (f n) <= l) /\ f --> l) /\ (!n. l <= (g n)) /\ g --> l) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 295 Theorem ADD_SYM autoloading from theory `arithmetic` ... @@ -20909,7 +20945,7 @@ |- !f. summable f ==> (!k. (\n. f(n num_add k)) sums ((suminf f) - (Sum(0,k)f))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 299 Theorem REAL_EQ_IMP_LE autoloading from theory `REAL` ... @@ -20928,7 +20964,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.1s +Run time: 0.0s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -21065,7 +21101,7 @@ |- !x. ~(x = & 1) ==> (!n. Sum(0,n)(\n'. x pow n') = ((x pow n) - (& 1)) / (x - (& 1))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 411 Theorem REAL_NEG_INV autoloading from theory `REAL` ... @@ -21122,7 +21158,7 @@ c < (& 1) /\ (!n. n num_ge N ==> (abs(f(SUC n))) <= (c * (abs(f n)))) ==> summable f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 683 () : void @@ -21132,7 +21168,7 @@ File seq.ml loaded () : void -Run time: 0.6s +Run time: 0.9s Intermediate theorems generated: 18704 #\ @@ -21142,7 +21178,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -21356,7 +21392,7 @@ LIM_ADD = |- !f g l m. (f --> l)x /\ (g --> m)x ==> ((\x. (f x) + (g x)) --> (l + m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 40 Theorem NET_MUL autoloading from theory `NETS` ... @@ -21398,7 +21434,7 @@ LIM_INV = |- !f l. (f --> l)x /\ ~(l = & 0) ==> ((\x. inv(f x)) --> (inv l))x -Run time: 0.9s +Run time: 0.0s Intermediate theorems generated: 35 Theorem NET_SUB autoloading from theory `NETS` ... @@ -21672,7 +21708,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21721,7 +21757,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) + (g x)) diffl (l + m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 150 Theorem REAL_MUL_SYM autoloading from theory `REAL` ... @@ -21966,7 +22002,7 @@ |- !f l x. (f diffl l)x /\ ~(f x = & 0) ==> ((\x. inv(f x)) diffl (--(l / ((f x) pow 2))))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 106 Theorem REAL_MUL_RINV autoloading from theory `REAL` ... @@ -22049,7 +22085,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 412 Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... @@ -22133,7 +22169,7 @@ |- !f x l. (f diffl l)x /\ l < (& 0) ==> (?d. (& 0) < d /\ (!h. (& 0) < h /\ h < d ==> (f x) < (f(x - h)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 469 Theorem REAL_ADD_SUB2 autoloading from theory `REAL` ... @@ -22202,7 +22238,7 @@ Theorem REAL_NEG_ADD autoloading from theory `REAL` ... REAL_NEG_ADD = |- !x y. --(x + y) = (-- x) + (-- y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_EQ_RMUL autoloading from theory `REAL` ... REAL_EQ_RMUL = |- !x y z. (x * z = y * z) = (z = & 0) \/ (x = y) @@ -22212,7 +22248,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -22258,7 +22294,7 @@ File lim.ml loaded () : void -Run time: 1.6s +Run time: 0.9s Intermediate theorems generated: 21608 #\ @@ -22268,7 +22304,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -22377,7 +22413,7 @@ Intermediate theorems generated: 47 () : void -Run time: 0.0s +Run time: 0.1s Definition pow autoloading from theory `REAL` ... pow = |- (!x. x pow 0 = & 1) /\ (!x n. x pow (SUC n) = x * (x pow n)) @@ -22726,7 +22762,7 @@ |- !x x0 y y0. x tends_num_real x0 /\ y tends_num_real y0 ==> (\n. (x n) - (y n)) tends_num_real (x0 - y0) -Run time: 0.1s +Run time: 0.0s Definition sums autoloading from theory `SEQ` ... sums = |- !f s. f sums s = (\n. Sum(0,n)f) tends_num_real s @@ -22872,7 +22908,7 @@ Theorem POW_POS autoloading from theory `REAL` ... POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) -Run time: 0.0s +Run time: 0.1s Theorem POW_LE autoloading from theory `REAL` ... POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) @@ -22986,7 +23022,7 @@ (& 0) < k /\ (!h. (& 0) < (abs h) /\ (abs h) < k ==> (abs(f h)) <= (K * (abs h))) ==> (f tends_real_real (& 0))(& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 917 Theorem SER_LE autoloading from theory `SEQ` ... @@ -23018,7 +23054,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.0s +Run time: 0.1s Intermediate theorems generated: 502 Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... @@ -23120,7 +23156,7 @@ ((\x. suminf(\n. (c n) * (x pow n))) diffl (suminf(\n. (diffs c n) * (x pow n)))) x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2494 () : void @@ -23130,7 +23166,7 @@ File powser.ml loaded () : void -Run time: 0.3s +Run time: 0.5s Intermediate theorems generated: 8507 #\ @@ -23140,7 +23176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -23355,7 +23391,7 @@ |- !f g l m x. (f diffl l)x /\ (g diffl m)x ==> ((\x. (f x) + (g x)) diffl (l + m))x -Run time: 0.0s +Run time: 0.1s Theorem DIFF_DIV autoloading from theory `LIM` ... DIFF_DIV = @@ -23667,7 +23703,7 @@ & 0 | ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) = (\n. (EVEN n => ((--(& 1)) pow (n DIV 2)) / (&(FACT n)) | & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 361 Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... @@ -24037,7 +24073,7 @@ LN_MUL = |- !x y. (& 0) < x /\ (& 0) < y ==> (ln(x * y) = (ln x) + (ln y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 113 LN_INJ = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x = ln y) = (x = y)) @@ -24071,7 +24107,7 @@ LN_MONO_LE = |- !x y. (& 0) < x /\ (& 0) < y ==> ((ln x) <= (ln y) = x <= y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 53 LN_POW = |- !n x. (& 0) < x ==> (ln(x pow n) = (& n) * (ln x)) @@ -24200,7 +24236,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` ... @@ -24252,7 +24288,7 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -24285,7 +24321,7 @@ Intermediate theorems generated: 48 COS_NEG = |- !x. cos(-- x) = cos x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 47 Theorem REAL_DOUBLE autoloading from theory `REAL` ... @@ -24323,7 +24359,7 @@ (((--(& 1)) pow n) / (&(FACT((2 num_mul n) num_add 1)))) * (x pow ((2 num_mul n) num_add 1))) sums (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... @@ -24457,7 +24493,7 @@ Run time: 0.0s COS_ISZERO = |- ?! x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 775 pi = |- pi = (& 2) * (@x. (& 0) <= x /\ x <= (& 2) /\ (cos x = & 0)) @@ -24493,7 +24529,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` ... @@ -24608,7 +24644,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (?! x. (--(pi / (& 2))) <= x /\ x <= (pi / (& 2)) /\ (sin x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 431 Theorem REAL_DIV_RMUL autoloading from theory `REAL` ... @@ -24653,7 +24689,7 @@ |- !x. (& 0) <= x /\ (sin x = & 0) ==> (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 305 Theorem REAL_NEG_EQ autoloading from theory `REAL` ... @@ -24901,7 +24937,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 28 TAN_ATN = @@ -24916,7 +24952,7 @@ File transc.ml loaded () : void -Run time: 1.1s +Run time: 1.5s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24929,7 +24965,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -24951,7 +24987,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25017,7 +25053,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25049,7 +25085,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25158,7 +25194,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25311,7 +25347,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25384,7 +25420,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25464,7 +25500,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25621,7 +25657,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25776,7 +25812,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -25993,7 +26029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26015,7 +26051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26034,7 +26070,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26079,7 +26115,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26144,7 +26180,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26194,7 +26230,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26264,7 +26300,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26334,7 +26370,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26370,7 +26406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26423,7 +26459,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26495,7 +26531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26574,7 +26610,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26769,7 +26805,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -26806,7 +26842,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -27492,7 +27528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -27964,7 +28000,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -28228,7 +28264,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -28473,7 +28509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -28937,7 +28973,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29405,7 +29441,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29461,7 +29497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29551,7 +29587,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29750,7 +29786,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29782,7 +29818,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -29916,7 +29952,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30219,7 +30255,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30251,7 +30287,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30290,7 +30326,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30322,7 +30358,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30483,7 +30519,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30616,7 +30652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30805,7 +30841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30865,7 +30901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -30990,7 +31026,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -31101,7 +31137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -31126,7 +31162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -31154,7 +31190,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -31267,7 +31303,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -31770,7 +31806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32018,7 +32054,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32244,7 +32280,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32286,7 +32322,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32318,7 +32354,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32541,7 +32577,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -32934,7 +32970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -33047,7 +33083,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -33550,7 +33586,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -33798,7 +33834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34024,7 +34060,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34059,7 +34095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34098,7 +34134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34135,7 +34171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34156,7 +34192,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34253,7 +34289,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34275,7 +34311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34771,7 +34807,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34794,7 +34830,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34872,7 +34908,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34931,7 +34967,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34975,7 +35011,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -34993,7 +35029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35020,7 +35056,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35064,7 +35100,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35177,7 +35213,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35224,7 +35260,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35263,7 +35299,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35337,7 +35373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35426,7 +35462,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35497,7 +35533,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35567,7 +35603,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35616,7 +35652,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35657,7 +35693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35698,7 +35734,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35722,7 +35758,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35823,7 +35859,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35844,7 +35880,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -35869,7 +35905,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36495,7 +36531,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36572,7 +36608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36599,7 +36635,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36716,7 +36752,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36811,7 +36847,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -36897,7 +36933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37012,7 +37048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37105,7 +37141,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37281,7 +37317,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37385,7 +37421,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37680,7 +37716,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37783,7 +37819,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37851,7 +37887,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -37913,7 +37949,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -38093,7 +38129,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -38134,7 +38170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -38164,7 +38200,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -38190,7 +38226,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -38708,7 +38744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -39245,7 +39281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -39433,7 +39469,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #false : bool @@ -39451,10 +39487,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Tue Apr 14 11:53:28 -12 2026 +Thu Mar 13 08:14:08 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Apr 14 11:53:28 -12 2026 +Thu Mar 13 08:14:08 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39472,13 +39508,13 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -HOL-LCF version 2.02 (GCL) created 14/4/26 +HOL-LCF version 2.02 (GCL) created 13/3/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -BASIC-HOL version 2.02 (GCL) created 14/4/26 +BASIC-HOL version 2.02 (GCL) created 13/3/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39486,7 +39522,7 @@ # =============================================================================== - HOL88 Version 2.02 (GCL), built on 14/4/26 + HOL88 Version 2.02 (GCL), built on 13/3/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) @@ -39553,8 +39589,8 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. +dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' for i in Manual/Tutorial/ack.tex Manual/Reference/ack.tex Manual/Description/ack.tex; do\ ln -snf ../Latex/ack.tex $i ; done @@ -40227,7 +40263,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (114 pages, 338300 bytes). +Output written on tutorial.dvi (114 pages, 338304 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' @@ -41866,7 +41902,7 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 1000236 bytes). +Output written on description.dvi (346 pages, 1000240 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -42434,7 +42470,7 @@ (./drules.aux) (./conv.aux) (./tactics.aux) (./see.aux) (./references.aux) (./version2.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on description.dvi (353 pages, 1083496 bytes). +Output written on description.dvi (353 pages, 1083500 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -44646,7 +44682,7 @@ [663]) (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1150936 bytes). +Output written on reference.dvi (669 pages, 1150940 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -46836,7 +46872,7 @@ [663]) (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1155404 bytes). +Output written on reference.dvi (669 pages, 1155412 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -52978,7 +53014,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.04.14:1157' -> endpages.ps +' TeX output 2025.03.13:0825' -> endpages.ps @@ -53050,7 +53086,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2026.04.14:1157' -> titlepages.ps +' TeX output 2025.03.13:0825' -> titlepages.ps @@ -53146,10 +53182,10 @@ dpkg-deb: building package 'hol88-help' in '../hol88-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-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. 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_amd64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.changes @@ -53158,12 +53194,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/329909/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/329909/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/3988796 and its subdirectories -I: Current time: Tue Apr 14 11:58:08 -12 2026 -I: pbuilder-time-stamp: 1776211088 +I: removing directory /srv/workspace/pbuilder/329909 and its subdirectories +I: Current time: Thu Mar 13 08:27:56 +14 2025 +I: pbuilder-time-stamp: 1741804076