Diff of the two buildlogs: -- --- b1/build.log 2024-01-10 14:09:26.307448519 +0000 +++ b2/build.log 2024-01-10 14:16:48.362199803 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Jan 10 02:01:24 -12 2024 -I: pbuilder-time-stamp: 1704895284 +I: Current time: Wed Feb 12 10:32:24 +14 2025 +I: pbuilder-time-stamp: 1739305944 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bullseye-reproducible-base.tgz] I: copying local configuration @@ -18,7 +18,7 @@ I: copying [./hol88_2.02.19940316-35.1.debian.tar.xz] I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' -gpgv: keyblock resource '/tmp/dpkg-verify-sig.E1l6Gnye/trustedkeys.kbx': General error +gpgv: keyblock resource '/tmp/dpkg-verify-sig.r7qRG8nq/trustedkeys.kbx': General error gpgv: Signature made Tue Jan 5 11:49:56 2021 gpgv: using RSA key B8BF54137B09D35CF026FE9D091AB856069AAA1C gpgv: Can't check signature: No public key @@ -31,51 +31,82 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/4883/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/44301/tmp/hooks/D01_modify_environment starting +debug: Running on ionos16-i386. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Feb 11 20:32 /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/44301/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/44301/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='i386' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all,-fixfilepath parallel=8 ' - DISTRIBUTION='bullseye' - HOME='/root' - HOST_ARCH='i386' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="1" [2]="4" [3]="1" [4]="release" [5]="i686-pc-linux-gnu") + BASH_VERSION='5.1.4(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=i386 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all,-fixfilepath parallel=15 ' + DIRSTACK=() + DISTRIBUTION=bullseye + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=i686 + HOST_ARCH=i386 IFS=' ' - INVOCATION_ID='46a35de8eff340289e56a1af66126e95' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - LD_LIBRARY_PATH='/usr/lib/libeatmydata' - LD_PRELOAD='libeatmydata.so' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='4883' - PS1='# ' - PS2='> ' + INVOCATION_ID=b523733fd889421fa7e22ffc18c3368f + LANG=C + LANGUAGE=de_CH:de + LC_ALL=C + LD_LIBRARY_PATH=/usr/lib/libeatmydata + LD_PRELOAD=libeatmydata.so + MACHTYPE=i686-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=44301 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.5CP2Zml8/pbuilderrc_qXeG --distribution bullseye --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.5CP2Zml8/b1 --logfile b1/build.log hol88_2.02.19940316-35.1.dsc' - SUDO_GID='112' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://78.137.99.97: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.5CP2Zml8/pbuilderrc_Y7TA --distribution bullseye --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bullseye-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.5CP2Zml8/b2 --logfile b2/build.log hol88_2.02.19940316-35.1.dsc' + SUDO_GID=112 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://85.184.249.68:3128 I: uname -a - Linux ionos12-i386 6.1.0-17-686-pae #1 SMP PREEMPT_DYNAMIC Debian 6.1.69-1 (2023-12-30) i686 GNU/Linux + Linux i-capture-the-hostname 6.1.0-17-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.69-1 (2023-12-30) x86_64 GNU/Linux I: ls -l /bin total 5776 -rwxr-xr-x 1 root root 1367848 Mar 27 2022 bash @@ -135,7 +166,7 @@ -rwxr-xr-x 1 root root 46984 Sep 22 2020 rmdir -rwxr-xr-x 1 root root 22292 Sep 27 2020 run-parts -rwxr-xr-x 1 root root 125036 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Jan 7 09:27 sh -> dash + lrwxrwxrwx 1 root root 9 Feb 11 20:32 sh -> /bin/bash -rwxr-xr-x 1 root root 34696 Sep 22 2020 sleep -rwxr-xr-x 1 root root 83880 Sep 22 2020 stty -rwsr-xr-x 1 root root 79396 Jan 20 2022 su @@ -161,7 +192,7 @@ -rwxr-xr-x 1 root root 2206 Apr 10 2022 zless -rwxr-xr-x 1 root root 1842 Apr 10 2022 zmore -rwxr-xr-x 1 root root 4577 Apr 10 2022 znew -I: user script /srv/workspace/pbuilder/4883/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/44301/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -337,7 +368,7 @@ Get: 126 http://deb.debian.org/debian bullseye/main i386 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 127 http://deb.debian.org/debian bullseye/main i386 texlive-base all 2020.20210202-3 [20.8 MB] Get: 128 http://deb.debian.org/debian bullseye/main i386 texlive-latex-base all 2020.20210202-3 [1120 kB] -Fetched 128 MB in 8s (15.4 MB/s) +Fetched 128 MB in 1s (97.4 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package bsdextrautils. (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 ... 17763 files and directories currently installed.) @@ -759,8 +790,8 @@ Setting up tzdata (2021a-1+deb11u10) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Jan 10 14:02:05 UTC 2024. -Universal Time is now: Wed Jan 10 14:02:05 UTC 2024. +Local time is now: Tue Feb 11 20:33:00 UTC 2025. +Universal Time is now: Tue Feb 11 20:33:00 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up xtrans-dev (1.4.0-1) ... @@ -939,7 +970,11 @@ fakeroot is already the newest version (1.25.3-1.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.19940316/ && 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.19940316-35.1_source.changes +I: user script /srv/workspace/pbuilder/44301/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for bullseye +I: user script /srv/workspace/pbuilder/44301/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316/ && 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.19940316-35.1_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316-35.1 dpkg-buildpackage: info: source distribution unstable @@ -1193,24 +1228,39 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/taut/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/pair/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/window/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1218,30 +1268,6 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/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.19940316/Library/pair/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ @@ -1249,9 +1275,9 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1259,12 +1285,15 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' @@ -1275,9 +1304,15 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/latex-hol/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1332,7 +1367,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Wed Jan 10 02:02:33 -12 2024 +Wed Feb 12 10:33:29 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' if [ cl = cl ]; then\ @@ -2506,7 +2541,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 # mem = - : (* -> * list -> bool) @@ -2644,7 +2679,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #.............start address -T 0x8ad7c8 () : void @@ -2803,7 +2838,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #.............start address -T 0x8ad7c8 () : void @@ -2995,7 +3030,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 # concat = - : (string -> string -> string) @@ -3105,7 +3140,7 @@ start address -T 0x8a7ae0 ;; Finished loading "lisp/f-ol-net" start address -T 0x8633b8 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 10/1/24 + version 2.02 (GCL) created 12/2/25 #...start address -T 0x988008 () : void @@ -3418,7 +3453,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 ###########################() : void @@ -3431,7 +3466,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 ################################################################################################() : void @@ -3576,7 +3611,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 ############################() : void @@ -3619,7 +3654,7 @@ /build/reproducible-path/hol88-2.02.19940316/hol-lcf < /build/reproducible-path/hol88-2.02.19940316/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 ############################Theory ind loaded () : void @@ -3656,7 +3691,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3697,7 +3732,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4099,7 +4134,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4167,7 +4202,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4372,7 +4407,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4496,7 +4531,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4582,7 +4617,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4675,7 +4710,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4744,7 +4779,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -4849,7 +4884,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5084,7 +5119,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5110,7 +5145,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5238,7 +5273,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5286,7 +5321,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5353,7 +5388,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5412,7 +5447,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5468,7 +5503,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 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5481,7 +5516,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 10/1/24 +HOL-LCF version 2.02 (GCL) created 12/2/25 #() : void @@ -5533,7 +5568,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ##########################() : void @@ -5564,7 +5599,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ##############################() : void @@ -5651,7 +5686,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #######################################################################() : void @@ -5804,7 +5839,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ###########################() : void @@ -5839,7 +5874,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #############################() : void @@ -5900,7 +5935,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ###########################Theory arithmetic loaded () : void @@ -6395,7 +6430,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ##################################() : void @@ -6542,7 +6577,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #################################Theory list loaded () : void @@ -6881,7 +6916,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ###############################Theory list loaded () : void @@ -8378,7 +8413,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #############################() : void @@ -8762,7 +8797,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ############################() : void @@ -9060,7 +9095,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ############################() : void @@ -9200,7 +9235,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ############################################() : void @@ -9297,7 +9332,7 @@ /build/reproducible-path/hol88-2.02.19940316/basic-hol < /build/reproducible-path/hol88-2.02.19940316/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 ##################################() : void @@ -9327,7 +9362,7 @@ | /build/reproducible-path/hol88-2.02.19940316/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316 -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -9344,7 +9379,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #Theory num loaded () : void @@ -9363,7 +9398,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -9520,7 +9555,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 # @@ -9558,7 +9593,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 # @@ -9592,7 +9627,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -9677,7 +9712,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -9718,7 +9753,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -9902,7 +9937,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 # define_load_lib_function = - : (string list -> void -> void) @@ -9976,7 +10011,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 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #GCL (GNU Common Lisp) 2.6.12 CLtL1 Fri Apr 22 15:51:11 UTC 2016 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -9989,7 +10024,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #() : void @@ -10053,11 +10088,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Wed Jan 10 02:04:18 -12 2024 +Wed Feb 12 10:35:03 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' date -Wed Jan 10 02:04:18 -12 2024 +Wed Feb 12 10:35:03 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10080,7 +10115,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -10164,7 +10199,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -10270,7 +10305,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11020,7 +11055,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11043,7 +11078,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11086,7 +11121,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11122,7 +11157,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11174,7 +11209,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11206,7 +11241,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11244,7 +11279,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11272,7 +11307,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11349,7 +11384,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11371,7 +11406,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11425,7 +11460,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11474,7 +11509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11625,7 +11660,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11669,7 +11704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11744,7 +11779,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11794,7 +11829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11857,7 +11892,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11910,7 +11945,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -11956,7 +11991,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12044,7 +12079,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12082,7 +12117,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12143,7 +12178,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12207,7 +12242,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12233,7 +12268,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12258,7 +12293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12297,7 +12332,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -12373,7 +12408,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13110,7 +13145,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13133,7 +13168,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13176,7 +13211,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13211,7 +13246,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13252,7 +13287,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13315,7 +13350,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13338,7 +13373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13363,7 +13398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13390,7 +13425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13426,7 +13461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13958,7 +13993,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -13981,7 +14016,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14015,7 +14050,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14070,7 +14105,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14161,7 +14196,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14330,7 +14365,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14563,7 +14598,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 = @@ -14661,7 +14696,7 @@ Intermediate theorems generated: 240 LINSEG_WOSET = |- !l a. woset l ==> woset(linseg l a) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 39 LINSEG_FL = |- !l a x. woset l ==> (fl(linseg l a)x = less l(x,a)) @@ -14721,7 +14756,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -14730,7 +14765,7 @@ ORDINAL_UNION_LEMMA = |- !l x. ordinal l ==> fl l x ==> fl(Union ordinal)x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 ORDINAL_UP = @@ -14764,7 +14799,7 @@ |- !l. poset l /\ (!P. chain l P ==> (?y. fl l y /\ (!x. P x ==> l(x,y)))) ==> (?y. fl l y /\ (!x. l(y,x) ==> (y = x))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 795 kl_tm = "\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2" : term @@ -14783,7 +14818,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1083 () : void @@ -14802,7 +14837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -14933,7 +14968,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -15025,7 +15060,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -15104,7 +15139,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2546 () : void @@ -15114,15 +15149,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Wed Jan 10 02:05:04 -12 2024 +===> abs_theory rebuilt on Wed Feb 12 10:35:50 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -15295,7 +15330,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -15595,7 +15630,7 @@ h trat_eq i \/ (?d. h trat_eq (i trat_add d)) \/ (?d. i trat_eq (h trat_add d)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) @@ -15722,7 +15757,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 11032 #\ @@ -15732,7 +15767,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -16073,7 +16108,7 @@ Theorem num_CASES autoloading from theory `arithmetic` ... num_CASES = |- !m. (m = 0) \/ (?n. m = SUC n) -Run time: 0.1s +Run time: 0.0s Theorem HRAT_ARCH autoloading from theory `HRAT` ... HRAT_ARCH = |- !h. ?n d. hrat_sucint n = h hrat_add d @@ -16103,7 +16138,7 @@ |- !X Y. X hreal_mul Y = hreal(\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 hreal_inv = @@ -16199,7 +16234,7 @@ Intermediate theorems generated: 837 HREAL_LT_TOTAL = |- !X Y. (X = Y) \/ X hreal_lt Y \/ Y hreal_lt X -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 492 HREAL_LT = |- !X Y. X hreal_lt Y = (?D. Y = X hreal_add D) @@ -16242,7 +16277,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -16672,7 +16707,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -16771,7 +16806,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 @@ -16790,7 +16825,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -17166,7 +17201,7 @@ Intermediate theorems generated: 276 REAL_LE_SQUARE = |- !x. (& 0) <= (x * x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 REAL_LE_01 = |- (& 0) <= (& 1) @@ -17294,7 +17329,7 @@ Intermediate theorems generated: 35 REAL_INVINV = |- !x. ~(x = & 0) ==> (inv(inv x) = x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 114 REAL_LT_IMP_NE = |- !x y. x < y ==> ~(x = y) @@ -17330,7 +17365,7 @@ Intermediate theorems generated: 29 REAL_LINV_UNIQ = |- !x y. (x * y = & 1) ==> (x = inv y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 111 REAL_RINV_UNIQ = |- !x y. (x * y = & 1) ==> (y = inv x) @@ -17427,7 +17462,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 @@ -17537,7 +17572,7 @@ Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y @@ -17588,7 +17623,7 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 < x2 /\ y1 < y2 ==> (x1 * y1) < (x2 * y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) @@ -17651,7 +17686,7 @@ Intermediate theorems generated: 91 REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 REAL_LE_MUL2 = @@ -17688,7 +17723,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) @@ -17737,7 +17772,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) @@ -17769,7 +17804,7 @@ Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 385 ABS_LT_MUL2 = @@ -17798,7 +17833,7 @@ Intermediate theorems generated: 75 ABS_REFL = |- !x. (abs x = x) = (& 0) <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n @@ -17840,7 +17875,7 @@ ABS_CIRCLE = |- !x y h. (abs h) < ((abs y) - (abs x)) ==> (abs(x + h)) < (abs y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 61 REAL_SUB_ABS = |- !x y. ((abs x) - (abs y)) <= (abs(x - y)) @@ -17886,7 +17921,7 @@ POW_PLUS1 = |- !e. (& 0) < e ==> (!n. ((& 1) + ((& n) * e)) <= (((& 1) + e) pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 298 Theorem ADD_CLAUSES autoloading from theory `arithmetic` ... @@ -17910,7 +17945,7 @@ Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) @@ -17973,7 +18008,7 @@ |- !P. (?x. P x /\ (& 0) < x) /\ (?z. !x. P x ==> x < z) ==> (?s. !y. (?x. P x /\ y < x) = y < s) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 325 SUP_LEMMA1 = @@ -17984,7 +18019,7 @@ Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 SUP_LEMMA3 = @@ -18067,7 +18102,7 @@ Sum = |- (Sum(n,0)f = & 0) /\ (Sum(n,SUC m)f = (Sum(n,m)f) + (f(n num_add m))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 51 SUM_TWO = |- !f n p. (Sum(0,n)f) + (Sum(n,p)f) = Sum(0,n num_add p)f @@ -18094,7 +18129,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.1s +Run time: 0.0s Intermediate theorems generated: 272 SUM_EQ = @@ -18269,13 +18304,13 @@ |- !n p. (!y. y num_lt n ==> (?! x. x num_lt n /\ (p x = y))) ==> (!f. Sum(0,n)(\n'. f(p n')) = Sum(0,n)f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2469 SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 206 () : void @@ -18295,7 +18330,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -18536,7 +18571,7 @@ Run time: 0.0s metric_tydef = |- ?rep. TYPE_DEFINITION ismet rep -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 560 metric_tybij = @@ -18613,7 +18648,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18789,7 +18824,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -19372,7 +19407,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 NET_SUB = @@ -19414,7 +19449,7 @@ (!x y x0 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: 338 Theorem REAL_INV_NZ autoloading from theory `REAL` ... @@ -19524,7 +19559,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -20173,7 +20208,7 @@ Run time: 0.0s SEQ_SUC = |- !f l. f --> l = (\n. f(SUC n)) --> l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 236 Theorem ABS_ABS autoloading from theory `REAL` ... @@ -20460,7 +20495,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20480,7 +20515,7 @@ Intermediate theorems generated: 16 SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) @@ -20818,7 +20853,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -21169,7 +21204,7 @@ Theorem REAL_LTE_TRANS autoloading from theory `REAL` ... REAL_LTE_TRANS = |- !x y z. x < y /\ y <= z ==> x < z -Run time: 0.1s +Run time: 0.0s Theorem REAL_DOWN2 autoloading from theory `REAL` ... REAL_DOWN2 = @@ -21397,7 +21432,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` ... @@ -21494,7 +21529,7 @@ (?k d. (& 0) < d /\ (!x. (& 0) < (abs(x - x0)) /\ (abs(x - x0)) < d ==> (abs(f x)) < k)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 362 Theorem REAL_MUL_LID autoloading from theory `REAL` ... @@ -21771,7 +21806,7 @@ (?M. (!x. a <= x /\ x <= b ==> M <= (f x)) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 177 Theorem ABS_SIGN autoloading from theory `REAL` ... @@ -21902,7 +21937,7 @@ (!x. a < x /\ x < b ==> f differentiable x) ==> (?l z. a < z /\ z < b /\ (f diffl l)z /\ ((f b) - (f a) = (b - a) * l)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 612 DIFF_ISCONST_END = @@ -21944,7 +21979,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -22587,7 +22622,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22796,7 +22831,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 @@ -22806,7 +22841,7 @@ File powser.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 8507 #\ @@ -22816,7 +22851,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -23520,7 +23555,7 @@ Intermediate theorems generated: 420 EXP_LT_1 = |- !x. (& 0) < x ==> (& 1) < (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 56 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -23565,7 +23600,7 @@ Run time: 0.0s EXP_ADD = |- !x y. exp(x + y) = (exp x) * (exp y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 71 Theorem REAL_LE_SQUARE autoloading from theory `REAL` ... @@ -23836,7 +23871,7 @@ Run time: 0.0s COS_0 = |- cos(& 0) = & 1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 454 SIN_CIRCLE = |- !x. ((sin x) pow 2) + ((cos x) pow 2) = & 1 @@ -24149,7 +24184,7 @@ Intermediate theorems generated: 42 PI2_BOUNDS = |- (& 0) < (pi / (& 2)) /\ (pi / (& 2)) < (& 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 124 Theorem REAL_LT_ADD autoloading from theory `REAL` ... @@ -24470,13 +24505,13 @@ TAN_TOTAL_LEMMA = |- !y. (& 0) < y ==> (?x. (& 0) < x /\ x < (pi / (& 2)) /\ y < (tan x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1046 TAN_TOTAL_POS = |- !y. (& 0) <= y ==> (?x. (& 0) <= x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 372 Theorem POW_NZ autoloading from theory `REAL` ... @@ -24577,7 +24612,7 @@ Intermediate theorems generated: 28 ATN_BOUNDS = |- !y. (--(pi / (& 2))) < (atn y) /\ (atn y) < (pi / (& 2)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 28 TAN_ATN = @@ -24592,7 +24627,7 @@ File transc.ml loaded () : void -Run time: 0.8s +Run time: 0.7s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/theories' @@ -24605,7 +24640,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -24627,7 +24662,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -24693,7 +24728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -24725,7 +24760,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -24834,7 +24869,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -24987,7 +25022,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25060,7 +25095,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25140,7 +25175,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25297,7 +25332,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25452,7 +25487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25669,7 +25704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25691,7 +25726,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25710,7 +25745,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25755,7 +25790,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25820,7 +25855,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25870,7 +25905,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -25940,7 +25975,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26010,7 +26045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26046,7 +26081,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26099,7 +26134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26171,7 +26206,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26250,7 +26285,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26445,7 +26480,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -26482,7 +26517,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -27168,7 +27203,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -27640,7 +27675,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -27904,7 +27939,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -28149,7 +28184,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -28613,7 +28648,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29081,7 +29116,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29137,7 +29172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29227,7 +29262,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29426,7 +29461,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29458,7 +29493,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29592,7 +29627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29895,7 +29930,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29927,7 +29962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29966,7 +30001,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -29998,7 +30033,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30159,7 +30194,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30292,7 +30327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30481,7 +30516,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30541,7 +30576,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30666,7 +30701,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30777,7 +30812,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30802,7 +30837,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30830,7 +30865,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -30943,7 +30978,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -31446,7 +31481,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -31694,7 +31729,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -31920,7 +31955,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -31962,7 +31997,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -31994,7 +32029,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -32217,7 +32252,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -32610,7 +32645,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -32723,7 +32758,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33226,7 +33261,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33474,7 +33509,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33700,7 +33735,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33735,7 +33770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33774,7 +33809,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33811,7 +33846,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33832,7 +33867,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33929,7 +33964,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -33951,7 +33986,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34447,7 +34482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34470,7 +34505,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34548,7 +34583,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34607,7 +34642,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34651,7 +34686,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34669,7 +34704,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34696,7 +34731,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34740,7 +34775,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34853,7 +34888,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34900,7 +34935,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -34939,7 +34974,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35013,7 +35048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35102,7 +35137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35173,7 +35208,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35243,7 +35278,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35292,7 +35327,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35333,7 +35368,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35374,7 +35409,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35398,7 +35433,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35499,7 +35534,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35520,7 +35555,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -35545,7 +35580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36171,7 +36206,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36248,7 +36283,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36275,7 +36310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36392,7 +36427,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36487,7 +36522,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36573,7 +36608,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36688,7 +36723,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36781,7 +36816,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -36957,7 +36992,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37061,7 +37096,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37356,7 +37391,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37459,7 +37494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37527,7 +37562,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37589,7 +37624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37769,7 +37804,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37810,7 +37845,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37840,7 +37875,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -37866,7 +37901,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -38384,7 +38419,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -38921,7 +38956,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -39109,7 +39144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 + HOL88 Version 2.02 (GCL), built on 12/2/25 =============================================================================== #false : bool @@ -39127,10 +39162,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library' date -Wed Jan 10 02:07:46 -12 2024 +Wed Feb 12 10:38:24 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' date -Wed Jan 10 02:07:46 -12 2024 +Wed Feb 12 10:38:24 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316' find $(ls -1 | grep -v debian) \ @@ -39148,22 +39183,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -HOL-LCF version 2.02 (GCL) created 10/1/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 12/2/25 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 10/1/24 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 12/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void # -BASIC-HOL version 2.02 (GCL) created 10/1/24 +BASIC-HOL version 2.02 (GCL) created 12/2/25 #HOL installed (`/usr/share/hol88-2.02.19940316`) () : void @@ -39621,7 +39656,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, 335504 bytes). +Output written on tutorial.dvi (114 pages, 335508 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Tutorial' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Tutorial' @@ -40895,12 +40930,12 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 996428 bytes). +Output written on description.dvi (346 pages, 996432 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' ../LaTeX/makeindex ../../ description.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -41107,7 +41142,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, 1079640 bytes). +Output written on description.dvi (353 pages, 1079644 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Description' @@ -42661,12 +42696,12 @@ (./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, 1143284 bytes). +Output written on reference.dvi (669 pages, 1143288 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' ../LaTeX/makeindex ../../ reference.idx index.tex -../LaTeX/makeindex: 1: /bin/arch: not found +../LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44194,7 +44229,7 @@ (./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, 1147752 bytes). +Output written on reference.dvi (669 pages, 1147756 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Reference' @@ -44410,7 +44445,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/abs_theory/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ abs_theory.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44665,7 +44700,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/arith/Manual' ../../../Manual/LaTeX/makeindex ../../../ arith.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -44902,7 +44937,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/finite_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ finite_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45080,7 +45115,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/more_arithmetic/Manual' ../../../Manual/LaTeX/makeindex ../../../ more_arithmetic.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45269,7 +45304,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/numeral/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ numeral.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45388,7 +45423,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pair/Manual' ../../../Manual/LaTeX/makeindex ../../../ index.tex pair -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45504,7 +45539,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/parser/Manual' ../../../Manual/LaTeX/makeindex ../../../ parser.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -45744,7 +45779,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/pred_sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ pred_sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46085,7 +46120,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/prettyp/Manual' ../../../Manual/LaTeX/makeindex ../../../ prettyp.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46292,7 +46327,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reals/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reals.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46635,7 +46670,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/reduce/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ reduce.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -46827,7 +46862,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/res_quan/Manual' ../../../Manual/LaTeX/makeindex ../../../ res_quan.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47095,7 +47130,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/sets/Manual' ../../../Manual/LaTeX/makeindex ../../../ sets.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47256,7 +47291,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/string/Manual' ../../../Manual/LaTeX/makeindex ../../../ string.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47401,7 +47436,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/taut/Manual' ../../../Manual/LaTeX/makeindex ../../../ taut.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47553,7 +47588,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/trs/Manual' ../../../Manual/LaTeX/makeindex ../../../ trs.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47709,7 +47744,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/unwind/Manual' ../../../Manual/LaTeX/makeindex ../../../ unwind.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -47887,7 +47922,7 @@ make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/wellorder/Manual' \ ../../../Manual/LaTeX/makeindex ../../../ wellorder.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48083,7 +48118,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/window/Manual' ../../../Manual/LaTeX/makeindex ../../../ window.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48308,7 +48343,7 @@ make[6]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' make[6]: Entering directory '/build/reproducible-path/hol88-2.02.19940316/Library/word/Manual' ../../../Manual/LaTeX/makeindex ../../../ word.idx index.tex -../../../Manual/LaTeX/makeindex: 1: /bin/arch: not found +../../../Manual/LaTeX/makeindex: line 5: /bin/arch: No such file or directory makeindex is not built for . @@ -48502,7 +48537,7 @@ ) (/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd) [1] [2]) (./preface.tex) [3] (./libraries.aux (./title.aux) (./preface.aux)) ) -Output written on libraries.dvi (3 pages, 2272 bytes). +Output written on libraries.dvi (3 pages, 2276 bytes). Transcript written on libraries.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Libraries' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316/Manual/Libraries' @@ -48569,7 +48604,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.10:0208' -> endpages.ps +' TeX output 2025.02.12:1039' -> endpages.ps @@ -48632,7 +48667,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2020.1 Copyright 2020 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.01.10:0208' -> titlepages.ps +' TeX output 2025.02.12:1039' -> titlepages.ps @@ -48705,8 +48740,8 @@ dh_gencontrol dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316-35.1_i386.deb'. dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316-35.1_i386.deb'. +dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316-35.1_i386.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316/%s\n",$1,a);}' >>debian/hol88-source.install find ml -type f -name "*ml" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316/%s\n",$1,a);}' >>debian/hol88-source.install @@ -48795,12 +48830,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/44301/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/44301/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/4883 and its subdirectories -I: Current time: Wed Jan 10 02:09:25 -12 2024 -I: pbuilder-time-stamp: 1704895765 +I: removing directory /srv/workspace/pbuilder/44301 and its subdirectories +I: Current time: Wed Feb 12 10:39:43 +14 2025 +I: pbuilder-time-stamp: 1739306383