Diff of the two buildlogs: -- --- b1/build.log 2024-04-27 06:01:53.791890992 +0000 +++ b2/build.log 2024-04-27 06:22:54.298168507 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Fri Apr 26 17:42:57 -12 2024 -I: pbuilder-time-stamp: 1714196577 +I: Current time: Sat May 31 02:24:56 +14 2025 +I: pbuilder-time-stamp: 1748607896 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -28,52 +28,84 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/4072297/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3368281/tmp/hooks/D01_modify_environment starting +debug: Running on ionos5-amd64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 May 30 12:25 /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/3368281/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3368281/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='amd64' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=20 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="21" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 ' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=x86_64 + HOST_ARCH=amd64 IFS=' ' - INVOCATION_ID='445bef75fe454b2c953fbe4a53ab8bde' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='4072297' - PS1='# ' - PS2='> ' + INVOCATION_ID=cc9c9d4adc3a47919ae6baa5fd83b057 + LANG=C + LANGUAGE=et_EE:et + LC_ALL=C + MACHTYPE=x86_64-pc-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=3368281 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.vf6A1lnb/pbuilderrc_JGoO --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.vf6A1lnb/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='111' - SUDO_UID='106' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://46.16.76.132:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.vf6A1lnb/pbuilderrc_mDNZ --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.vf6A1lnb/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=110 + SUDO_UID=105 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://213.165.73.152:3128 I: uname -a - Linux ionos11-amd64 6.1.0-20-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.85-1 (2024-04-11) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.6.13+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.6.13-1~bpo12+1 (2024-02-15) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Apr 25 07:43 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/4072297/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 28 14:06 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/3368281/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -311,7 +343,7 @@ Get: 196 http://deb.debian.org/debian unstable/main amd64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 197 http://deb.debian.org/debian unstable/main amd64 texlive-base all 2023.20240207-1 [22.0 MB] Get: 198 http://deb.debian.org/debian unstable/main amd64 texlive-latex-base all 2023.20240207-1 [1255 kB] -Fetched 194 MB in 11s (17.3 MB/s) +Fetched 194 MB in 4s (46.6 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libapparmor1:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19694 files and directories currently installed.) @@ -973,8 +1005,8 @@ Setting up tzdata (2024a-3) ... Current default time zone: 'Etc/UTC' -Local time is now: Sat Apr 27 05:46:18 UTC 2024. -Universal Time is now: Sat Apr 27 05:46:18 UTC 2024. +Local time is now: Fri May 30 12:27:29 UTC 2025. +Universal Time is now: Fri May 30 12:27:29 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.11-1) ... @@ -1175,7 +1207,11 @@ fakeroot is already the newest version (1.34-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/3368281/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/3368281/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1429,79 +1465,65 @@ make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Covers' make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual' [ ! -f Makefile ] || for i in $(find Library -name Manual); do /usr/bin/make -C $i clean ; done +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex *.bak; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/window/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ +printf '\\begin{theindex}' >index.tex; \ +printf '\\mbox{}' >>index.tex; \ +printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/finite_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/abs_theory/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/taut/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/arith/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ printf '\\begin{theindex}' >index.tex; \ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/res_quan/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/unwind/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reduce/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/parser/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' @@ -1512,15 +1534,29 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/record_proof/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' rm -f *.dvi *.aux *.toc *.log *.idx *.ilg make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pred_sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex theorems.tex; \ -printf '\\begin{theindex}' >index.tex; \ -printf '\\mbox{}' >>index.tex; \ -printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/pair/Manual' find -name X.tex -exec rm -rf {} \; dh_clean -X./ml/site.ml.orig -X./contrib/tooltool/Makefile.orig \ -X./contrib/tooltool/events.c.orig -X./contrib/tooltool/func_fix.c.orig \ @@ -1568,7 +1604,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 26 17:49:24 -12 2024 +Sat May 31 02:29:32 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2806,7 +2842,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 # mem = - : (* -> * list -> bool) @@ -2944,7 +2980,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #.............start address -T 0xa86180 () : void @@ -3103,7 +3139,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #.............start address -T 0xa86180 () : void @@ -3295,7 +3331,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 # concat = - : (string -> string -> string) @@ -3405,7 +3441,7 @@ start address -T 0xa7c260 ;; Finished loading "lisp/f-ol-net" start address -T 0xa35c50 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 26/4/24 + version 2.02 (GCL) created 31/5/25 #...start address -T 0xa88320 () : void @@ -3734,7 +3770,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_PPLAMB.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 ###########################() : void @@ -3747,7 +3783,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_bool.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 ################################################################################################() : void @@ -3892,7 +3928,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ind.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 ############################() : void @@ -3935,7 +3971,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/hol-lcf < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_BASIC-HOL.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 ############################Theory ind loaded () : void @@ -3972,7 +4008,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4013,7 +4049,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4415,7 +4451,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4483,7 +4519,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4688,7 +4724,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4812,7 +4848,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4898,7 +4934,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -4991,7 +5027,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5060,7 +5096,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5165,7 +5201,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5400,7 +5436,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5426,7 +5462,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5554,7 +5590,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5602,7 +5638,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5669,7 +5705,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5728,7 +5764,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5784,7 +5820,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 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5797,7 +5833,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 26/4/24 +HOL-LCF version 2.02 (GCL) created 31/5/25 #() : void @@ -5849,7 +5885,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_combin.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ##########################() : void @@ -5880,7 +5916,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_num.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ##############################() : void @@ -5967,7 +6003,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_prim_rec.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #######################################################################() : void @@ -6120,7 +6156,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_fun.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ###########################() : void @@ -6155,7 +6191,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_arith_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #############################() : void @@ -6216,7 +6252,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ###########################Theory arithmetic loaded () : void @@ -6711,7 +6747,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_list_thms.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ##################################() : void @@ -6858,7 +6894,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #################################Theory list loaded () : void @@ -7197,7 +7233,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ###############################Theory list loaded () : void @@ -8694,7 +8730,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #############################() : void @@ -9078,7 +9114,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_ltree.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ############################() : void @@ -9376,7 +9412,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_tydefs.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ############################() : void @@ -9516,7 +9552,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_sum.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ############################################() : void @@ -9613,7 +9649,7 @@ /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol < /build/reproducible-path/hol88-2.02.19940316dfsg/theories/mk_one.ml;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 ##################################() : void @@ -9643,7 +9679,7 @@ | /build/reproducible-path/hol88-2.02.19940316dfsg/basic-hol;\ cd /build/reproducible-path/hol88-2.02.19940316dfsg -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -9660,7 +9696,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #Theory num loaded () : void @@ -9679,7 +9715,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -9836,7 +9872,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 # @@ -9874,7 +9910,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 # @@ -9908,7 +9944,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -9993,7 +10029,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -10034,7 +10070,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -10218,7 +10254,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10294,7 +10330,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 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10307,7 +10343,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #() : void @@ -10371,11 +10407,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 26 17:52:39 -12 2024 +Sat May 31 02:33:42 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 26 17:52:39 -12 2024 +Sat May 31 02:33:42 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10398,7 +10434,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -10482,7 +10518,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -10588,7 +10624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11338,7 +11374,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11361,7 +11397,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11404,7 +11440,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11440,7 +11476,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11492,7 +11528,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11524,7 +11560,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11562,7 +11598,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11590,7 +11626,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11667,7 +11703,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11689,7 +11725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11743,7 +11779,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11792,7 +11828,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11943,7 +11979,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -11987,7 +12023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12062,7 +12098,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12112,7 +12148,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12175,7 +12211,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12228,7 +12264,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12274,7 +12310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12362,7 +12398,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12400,7 +12436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12461,7 +12497,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12525,7 +12561,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12551,7 +12587,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12576,7 +12612,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12615,7 +12651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -12691,7 +12727,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13428,7 +13464,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13451,7 +13487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13494,7 +13530,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13529,7 +13565,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13570,7 +13606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13633,7 +13669,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13656,7 +13692,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13681,7 +13717,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13708,7 +13744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -13744,7 +13780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14276,7 +14312,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14299,7 +14335,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14333,7 +14369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14388,7 +14424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14479,7 +14515,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14648,7 +14684,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -14835,7 +14871,7 @@ WOSET_TRANS_LE = |- !l. woset l ==> (!x y z. l(x,y) /\ less l(y,z) ==> less l(x,z)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 143 WOSET_WELL_CONTRAPOS = @@ -14856,7 +14892,7 @@ |- !l. woset l ==> (!x y. fl l x /\ fl l y ==> (x = y) \/ less l(x,y) \/ less l(y,x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 172 WO_INDUCT = @@ -15068,14 +15104,14 @@ Intermediate theorems generated: 392 WO = |- !P. ?l. woset l /\ (fl l = P) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 403 HP = |- !l. poset l ==> (?P. chain l P /\ (!Q. chain l Q /\ P subset Q ==> (Q = P))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2506 ZL = @@ -15090,7 +15126,7 @@ KL_POSET_LEMMA = |- poset(\(c1,c2). C subset c1 /\ c1 subset c2 /\ chain l c2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 386 KL = @@ -15111,7 +15147,7 @@ File mk_wellorder loaded () : void -Run time: 0.6s +Run time: 0.5s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15120,7 +15156,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -15251,7 +15287,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -15343,7 +15379,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -15435,12 +15471,12 @@ Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Fri Apr 26 17:53:51 -12 2024 +===> abs_theory rebuilt on Sat May 31 02:35:21 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -15613,7 +15649,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -15851,12 +15887,12 @@ Theorem ADD_ASSOC autoloading from theory `arithmetic` ... ADD_ASSOC = |- !m n p. m + (n + p) = (m + n) + p -Run time: 0.1s +Run time: 0.0s TRAT_ADD_ASSOC = |- !h i j. (h trat_add (i trat_add j)) trat_eq ((h trat_add i) trat_add j) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 297 TRAT_MUL_SYM = |- !h i. (h trat_mul i) trat_eq (i trat_mul h) @@ -16050,7 +16086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -16403,7 +16439,7 @@ CUT_NEARTOP_MUL = |- !X u. hrat_1 hrat_lt u ==> (?x. cut X x /\ ~cut X(u hrat_mul x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 234 hreal_1 = |- hreal_1 = hreal(cut_of_hrat hrat_1) @@ -16474,7 +16510,7 @@ HREAL_MUL_ASSOC = |- !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 490 HREAL_LDISTRIB = @@ -16489,7 +16525,7 @@ Intermediate theorems generated: 278 HREAL_MUL_LINV = |- !X. (hreal_inv X) hreal_mul X = hreal_1 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 485 HREAL_NOZERO = |- !X Y. ~(X hreal_add Y = X) @@ -16550,7 +16586,7 @@ File hreal.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 10456 #\ @@ -16560,7 +16596,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -16900,12 +16936,12 @@ TREAL_LT_TRANS = |- !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1063 TREAL_LT_ADD = |- !x y z. y treal_lt z ==> (x treal_add y) treal_lt (x treal_add z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1045 TREAL_LT_MUL = @@ -16978,7 +17014,7 @@ TREAL_LT_WELLDEFL = |- !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 612 TREAL_LT_WELLDEF = @@ -16990,7 +17026,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -17048,7 +17084,7 @@ (?z. !x. P x ==> x real_lt z) ==> (?X. (\h. P(real_of_hreal h))X) /\ (?Y. !X. (\h. P(real_of_hreal h))X ==> X hreal_lt Y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 135 SUP_ALLPOS_LEMMA4 = @@ -17098,7 +17134,7 @@ File realax.ml loaded () : void -Run time: 0.4s +Run time: 0.5s Intermediate theorems generated: 26795 #\ @@ -17108,7 +17144,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -17376,7 +17412,7 @@ Intermediate theorems generated: 56 REAL_ENTIRE = |- !x y. (x * y = & 0) = (x = & 0) \/ (y = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 116 REAL_LT_LADD = |- !x y z. (x + y) < (x + z) = y < z @@ -17396,7 +17432,7 @@ Intermediate theorems generated: 24 REAL_LT_GT = |- !x y. x < y ==> ~y < x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 26 REAL_NOT_LE = |- !x y. ~x <= y = y < x @@ -17508,7 +17544,7 @@ Intermediate theorems generated: 55 REAL_LE_ADD2 = |- !w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 55 REAL_LE_ADD = |- !x y. (& 0) <= x /\ (& 0) <= y ==> (& 0) <= (x + y) @@ -17548,7 +17584,7 @@ Intermediate theorems generated: 33 REAL_LE_DOUBLE = |- !x. (& 0) <= (x + x) = (& 0) <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 72 REAL_LE_NEGL = |- !x. (-- x) <= x = (& 0) <= x @@ -17620,7 +17656,7 @@ Intermediate theorems generated: 43 REAL_INV_POS = |- !x. (& 0) < x ==> (& 0) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 133 REAL_LT_LMUL_0 = |- !x y. (& 0) < x ==> ((& 0) < (x * y) = (& 0) < y) @@ -17656,7 +17692,7 @@ Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 71 REAL_INV_1OVER = |- !x. inv x = (& 1) / x @@ -17742,7 +17778,7 @@ (m num_mul 1 = m) /\ ((SUC m) num_mul n = (m num_mul n) num_add n) /\ (m num_mul (SUC n) = m num_add (m num_mul n)) -Run time: 0.0s +Run time: 0.1s REAL_MUL = |- !m n. (& m) * (& n) = &(m num_mul n) Run time: 0.0s @@ -17787,7 +17823,7 @@ Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p -Run time: 0.1s +Run time: 0.0s Theorem NOT_LESS_0 autoloading from theory `prim_rec` ... NOT_LESS_0 = |- !n. ~n num_lt 0 @@ -17871,7 +17907,7 @@ Intermediate theorems generated: 79 REAL_LE_NEG = |- !x y. (-- x) <= (-- y) = y <= x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 37 REAL_ADD2_SUB2 = |- !a b c d. (a + b) - (c + d) = (a - c) + (b - d) @@ -17910,7 +17946,7 @@ Intermediate theorems generated: 344 REAL_LT_INV = |- !x y. (& 0) < x /\ x < y ==> (inv y) < (inv x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 282 REAL_SUB_LNEG = |- !x y. (-- x) - y = --(x + y) @@ -17947,7 +17983,7 @@ Intermediate theorems generated: 43 REAL_LE_RMUL = |- !x y z. (& 0) < z ==> ((x * z) <= (y * z) = x <= y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_SUB_INV2 = @@ -17976,7 +18012,7 @@ |- !x1 x2 y1 y2. (& 0) <= x1 /\ (& 0) <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> (x1 * y1) <= (x2 * y2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 345 REAL_LE_LDIV = |- !x y z. (& 0) < x /\ y <= (z * x) ==> (y / x) <= z @@ -18026,7 +18062,7 @@ Run time: 0.0s REAL_FACT_NZ = |- !n. ~(&(FACT n) = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_DIFFSQ = |- !x y. (x + y) * (x - y) = (x * x) - (y * y) @@ -18034,7 +18070,7 @@ Intermediate theorems generated: 165 REAL_POSSQ = |- !x. (& 0) < (x * x) = ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) @@ -18083,11 +18119,11 @@ Intermediate theorems generated: 604 ABS_POS = |- !x. (& 0) <= (abs x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 67 ABS_MUL = |- !x y. abs(x * y) = (abs x) * (abs y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 385 ABS_LT_MUL2 = @@ -18141,11 +18177,11 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 22 ABS_SIGN2 = |- !x y. (abs(x - y)) < (-- y) ==> x < (& 0) @@ -18191,7 +18227,7 @@ Intermediate theorems generated: 56 POW_NZ = |- !c n. ~(c = & 0) ==> ~(c pow n = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) @@ -18199,7 +18235,7 @@ Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 83 POW_PLUS1 = @@ -18248,7 +18284,7 @@ Intermediate theorems generated: 14 ABS_POW2 = |- !x. abs(x pow 2) = x pow 2 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 13 REAL_POW2_ABS = |- !x. (abs x) pow 2 = x pow 2 @@ -18260,7 +18296,7 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) @@ -18462,11 +18498,11 @@ SUM_ADD = |- !f g m n. Sum(m,n)(\n'. (f n') + (g n')) = (Sum(m,n)f) + (Sum(m,n)g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 133 SUM_CMUL = |- !f c m n. Sum(m,n)(\n'. c * (f n')) = c * (Sum(m,n)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 100 SUM_NEG = |- !f n d. Sum(n,d)(\n'. --(f n')) = --(Sum(n,d)f) @@ -18524,13 +18560,13 @@ Intermediate theorems generated: 56 SUM_2 = |- !f n. Sum(n,2)f = (f n) + (f(n num_add 1)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 81 SUM_OFFSET = |- !f n k. Sum(0,n)(\m. f(m num_add k)) = (Sum(0,n num_add k)f) - (Sum(0,k)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 141 SUM_REINDEX = @@ -18603,7 +18639,7 @@ File real.ml loaded () : void -Run time: 1.6s +Run time: 1.7s Intermediate theorems generated: 23746 #\ @@ -18613,7 +18649,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -18773,11 +18809,11 @@ open L re_universe /\ (!x y. open L x /\ open L y ==> open L(x re_intersect y)) /\ (!P. P re_subset (open L) ==> open L(re_Union P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 34 TOPOLOGY_UNION = |- !L P. P re_subset (open L) ==> open L(re_Union P) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 45 neigh = @@ -18931,7 +18967,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 = @@ -18973,7 +19009,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -19107,7 +19143,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -19656,7 +19692,7 @@ |- !g k x. (x --> (& 0))(mtop mr1,g) ==> ((\n. k * (x n)) --> (& 0))(mtop mr1,g) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 506 Theorem REAL_ADD_ASSOC autoloading from theory `REAL` ... @@ -19732,7 +19768,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` ... @@ -19832,7 +19868,7 @@ File nets.ml loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 7389 #\ @@ -19842,7 +19878,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -20102,7 +20138,7 @@ |- !x x0 y y0. x --> x0 /\ y --> y0 /\ ~(y0 = & 0) ==> (\n. (x n) / (y n)) --> (x0 / y0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 35 Theorem MTOP_TENDS_UNIQ autoloading from theory `NETS` ... @@ -20148,7 +20184,7 @@ (m num_add 0 = m) /\ ((SUC m) num_add n = SUC(m num_add n)) /\ (m num_add (SUC n) = SUC(m num_add n)) -Run time: 0.1s +Run time: 0.0s Theorem LESS_TRANS autoloading from theory `arithmetic` ... LESS_TRANS = |- !m n p. m num_lt n /\ n num_lt p ==> m num_lt p @@ -20415,7 +20451,7 @@ Run time: 0.0s SEQ_MONOSUB = |- !s. ?f. subseq f /\ mono(\n. s(f n)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1286 SEQ_SBOUNDED = @@ -20465,7 +20501,7 @@ Run time: 0.0s SEQ_CAUCHY = |- !f. cauchy f = convergent f -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 665 Theorem NET_LE autoloading from theory `NETS` ... @@ -20647,7 +20683,7 @@ ((!n. (f n) <= l) /\ f --> l) /\ (!n. m <= (g n)) /\ g --> m) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2190 Theorem REAL_SUB_0 autoloading from theory `REAL` ... @@ -20778,7 +20814,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.0s +Run time: 0.1s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20850,7 +20886,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) < (f m)) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem LESS_REFL autoloading from theory `prim_rec` ... @@ -20922,7 +20958,7 @@ ((f(n num_add (2 num_mul d))) + (f(n num_add ((2 num_mul d) num_add 1))))) ==> (Sum(0,n)f) < (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1204 Theorem SUM_ADD autoloading from theory `REAL` ... @@ -20992,7 +21028,7 @@ |- !f g. (?N. !n. n num_ge N ==> (abs(f n)) <= (g n)) /\ summable g ==> summable f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 395 SER_COMPARA = @@ -21017,7 +21053,7 @@ |- !f g. (!n. (abs(f n)) <= (g n)) /\ summable g ==> summable f /\ (suminf f) <= (suminf g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 136 Theorem SUM_ABS autoloading from theory `REAL` ... @@ -21126,7 +21162,7 @@ File seq.ml loaded () : void -Run time: 0.5s +Run time: 0.7s Intermediate theorems generated: 18704 #\ @@ -21136,7 +21172,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -21388,7 +21424,7 @@ (!x x0. (x tends x0)(mtop mr1,g) /\ ~(x0 = & 0) ==> ((\n. inv(x n)) tends (inv x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s LIM_INV = |- !f l. (f --> l)x /\ ~(l = & 0) ==> ((\x. inv(f x)) --> (inv l))x @@ -21666,7 +21702,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21812,7 +21848,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` ... @@ -21866,7 +21902,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -22023,7 +22059,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22206,7 +22242,7 @@ |- !f a b. (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))a = (\x. (f x) - ((((f b) - (f a)) / (b - a)) * x))b -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 443 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -22252,7 +22288,7 @@ File lim.ml loaded () : void -Run time: 0.6s +Run time: 0.7s Intermediate theorems generated: 21608 #\ @@ -22262,7 +22298,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -22514,7 +22550,7 @@ Theorem POW_ADD autoloading from theory `REAL` ... POW_ADD = |- !c m n. c pow (m num_add n) = (c pow m) * (c pow n) -Run time: 0.0s +Run time: 0.1s Theorem REAL_EQ_LMUL2 autoloading from theory `REAL` ... REAL_EQ_LMUL2 = |- !x y z. ~(x = & 0) ==> ((y = z) = (x * y = x * z)) @@ -22708,7 +22744,7 @@ Sum(0,n)(\n. (& n) * ((c n) * (x pow (n num_sub 1)))) = (Sum(0,n)(\n. (diffs c n) * (x pow n))) - ((& n) * ((c n) * (x pow (n num_sub 1)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 34 Theorem REAL_SUB_RZERO autoloading from theory `REAL` ... @@ -22905,7 +22941,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.0s +Run time: 0.1s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22955,7 +22991,7 @@ Definition abs autoloading from theory `REAL` ... abs = |- !x. abs x = ((& 0) <= x => x | -- x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 Theorem REAL_LT_HALF1 autoloading from theory `REAL` ... @@ -23114,7 +23150,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 @@ -23124,7 +23160,7 @@ File powser.ml loaded () : void -Run time: 0.3s +Run time: 0.6s Intermediate theorems generated: 8507 #\ @@ -23134,7 +23170,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -23478,7 +23514,7 @@ Theorem REAL_INV_MUL autoloading from theory `REAL` ... REAL_INV_MUL = |- !x y. ~(x = & 0) /\ ~(y = & 0) ==> (inv(x * y) = (inv x) * (inv y)) -Run time: 0.1s +Run time: 0.0s Theorem REAL_MUL autoloading from theory `REAL` ... REAL_MUL = |- !m n. (& m) * (& n) = &(m num_mul n) @@ -23560,7 +23596,7 @@ EXP_CONVERGES = |- !x. (\n. ((\n. inv(&(FACT n)))n) * (x pow n)) sums (exp x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 628 Theorem REAL_INV_POS autoloading from theory `REAL` ... @@ -23718,7 +23754,7 @@ Theorem REAL_LT_ADDR autoloading from theory `REAL` ... REAL_LT_ADDR = |- !x y. x < (x + y) = (& 0) < y -Run time: 0.1s +Run time: 0.0s Theorem ABS_LE autoloading from theory `REAL` ... ABS_LE = |- !x. x <= (abs x) @@ -23859,7 +23895,7 @@ Run time: 0.0s EXP_ADD_MUL = |- !x y. (exp(x + y)) * (exp(-- x)) = exp y -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 660 EXP_NEG_MUL = |- !x. (exp x) * (exp(-- x)) = & 1 @@ -24092,7 +24128,7 @@ ROOT_LN = |- !n x. (& 0) < x ==> (!n. root(SUC n)x = exp((ln x) / (&(SUC n)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 282 Theorem REAL_ENTIRE autoloading from theory `REAL` ... @@ -24246,7 +24282,7 @@ (((sin(x + y)) - (((sin x) * (cos y)) + ((cos x) * (sin y)))) pow 2) + (((cos(x + y)) - (((cos x) * (cos y)) - ((sin x) * (sin y)))) pow 2) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1747 SIN_COS_NEG = @@ -24363,7 +24399,7 @@ Run time: 0.0s SIN_POS = |- !x. (& 0) < x /\ x < (& 2) ==> (& 0) < (sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2052 COS_PAIRED = @@ -24487,7 +24523,7 @@ Run time: 0.0s SIN_PI2 = |- sin(pi / (& 2)) = & 1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 212 Theorem REAL_DIV_LMUL autoloading from theory `REAL` ... @@ -24611,7 +24647,7 @@ Theorem REAL_EQ_SUB_RADD autoloading from theory `REAL` ... REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_HALF2 autoloading from theory `REAL` ... REAL_LT_HALF2 = |- !d. (d / (& 2)) < d = (& 0) < d @@ -24636,7 +24672,7 @@ |- !x. (& 0) <= x /\ (cos x = & 0) ==> (?n. ~EVEN n /\ (x = (& n) * (pi / (& 2)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 675 Theorem REAL_LE_ADDR autoloading from theory `REAL` ... @@ -24734,7 +24770,7 @@ Intermediate theorems generated: 68 TAN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (tan x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 78 Theorem REAL_INV_1OVER autoloading from theory `REAL` ... @@ -24742,7 +24778,7 @@ Run time: 0.0s DIFF_TAN = |- !x. ~(cos x = & 0) ==> (tan diffl (inv((cos x) pow 2)))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 532 Theorem REAL_LT_INV autoloading from theory `REAL` ... @@ -24833,7 +24869,7 @@ |- !y. atn y = (@x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 ASN = @@ -24865,7 +24901,7 @@ |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (& 0) <= (acs y) /\ (acs y) <= pi /\ (cos(acs y) = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 79 ACS_COS = |- !y. (--(& 1)) <= y /\ y <= (& 1) ==> (cos(acs y) = y) @@ -24910,7 +24946,7 @@ File transc.ml loaded () : void -Run time: 1.2s +Run time: 1.0s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24923,7 +24959,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -24945,7 +24981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25011,7 +25047,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25043,7 +25079,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25152,7 +25188,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25305,7 +25341,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25378,7 +25414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25458,7 +25494,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25615,7 +25651,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25770,7 +25806,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -25987,7 +26023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26009,7 +26045,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26028,7 +26064,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26073,7 +26109,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26138,7 +26174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26188,7 +26224,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26258,7 +26294,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26328,7 +26364,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26364,7 +26400,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26417,7 +26453,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26489,7 +26525,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26568,7 +26604,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26763,7 +26799,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -26800,7 +26836,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -27486,7 +27522,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -27958,7 +27994,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -28222,7 +28258,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -28467,7 +28503,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -28931,7 +28967,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29399,7 +29435,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29455,7 +29491,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29545,7 +29581,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29744,7 +29780,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29776,7 +29812,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -29910,7 +29946,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30213,7 +30249,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30245,7 +30281,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30284,7 +30320,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30316,7 +30352,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30477,7 +30513,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30610,7 +30646,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30799,7 +30835,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30859,7 +30895,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -30984,7 +31020,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -31095,7 +31131,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -31120,7 +31156,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -31148,7 +31184,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -31261,7 +31297,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -31764,7 +31800,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32012,7 +32048,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32238,7 +32274,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32280,7 +32316,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32312,7 +32348,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32535,7 +32571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -32928,7 +32964,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -33041,7 +33077,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -33544,7 +33580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -33792,7 +33828,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34018,7 +34054,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34053,7 +34089,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34092,7 +34128,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34129,7 +34165,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34150,7 +34186,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34247,7 +34283,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34269,7 +34305,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34765,7 +34801,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34788,7 +34824,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34866,7 +34902,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34925,7 +34961,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34969,7 +35005,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -34987,7 +35023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35014,7 +35050,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35058,7 +35094,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35171,7 +35207,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35218,7 +35254,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35257,7 +35293,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35331,7 +35367,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35420,7 +35456,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35491,7 +35527,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35561,7 +35597,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35610,7 +35646,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35651,7 +35687,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35692,7 +35728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35716,7 +35752,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35817,7 +35853,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35838,7 +35874,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -35863,7 +35899,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36489,7 +36525,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36566,7 +36602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36593,7 +36629,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36710,7 +36746,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36805,7 +36841,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -36891,7 +36927,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37006,7 +37042,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37099,7 +37135,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37275,7 +37311,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37379,7 +37415,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37674,7 +37710,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37777,7 +37813,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37845,7 +37881,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -37907,7 +37943,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -38087,7 +38123,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -38128,7 +38164,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -38158,7 +38194,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -38184,7 +38220,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -38702,7 +38738,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -39239,7 +39275,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -39427,7 +39463,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 + HOL88 Version 2.02 (GCL), built on 31/5/25 =============================================================================== #false : bool @@ -39445,10 +39481,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Fri Apr 26 17:59:05 -12 2024 +Sat May 31 02:40:50 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Fri Apr 26 17:59:05 -12 2024 +Sat May 31 02:40:50 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39466,22 +39502,22 @@ printf 'install `'/usr/share/hol88-2.02.19940316dfsg'`;;\nlisp `(ml-save "foo")`;;\n' | ./$i &&\ mv foo $i; done -BASIC-HOL version 2.02 (GCL) created 26/4/24 +BASIC-HOL version 2.02 (GCL) created 31/5/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 26/4/24 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 31/5/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 26/4/24 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 31/5/25 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -41213,7 +41249,7 @@ ) (see the transcript file for additional information) -Output written on description.dvi (346 pages, 1000236 bytes). +Output written on description.dvi (346 pages, 1000240 bytes). Transcript written on description.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Description' @@ -42978,7 +43014,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, 1150936 bytes). +Output written on reference.dvi (669 pages, 1150940 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -48866,7 +48902,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.04.26:1800' -> endpages.ps +' TeX output 2025.05.31:0243' -> endpages.ps @@ -48930,7 +48966,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 Radical Eye Software (www.radicaleye.com) -' TeX output 2024.04.26:1800' -> titlepages.ps +' TeX output 2025.05.31:0243' -> titlepages.ps @@ -49085,12 +49121,12 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.buildinfo @@ -49100,12 +49136,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/3368281/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3368281/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/4072297 and its subdirectories -I: Current time: Fri Apr 26 18:01:53 -12 2024 -I: pbuilder-time-stamp: 1714197713 +I: removing directory /srv/workspace/pbuilder/3368281 and its subdirectories +I: Current time: Sat May 31 02:45:51 +14 2025 +I: pbuilder-time-stamp: 1748609151