Diff of the two buildlogs: -- --- b1/build.log 2025-07-16 14:33:20.996053317 +0000 +++ b2/build.log 2025-07-16 14:48:09.309028846 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Jul 16 02:22:42 -12 2025 -I: pbuilder-time-stamp: 1752675762 +I: Current time: Wed Aug 19 10:56:26 +14 2026 +I: pbuilder-time-stamp: 1787086586 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -26,52 +26,84 @@ dpkg-source: info: applying function_representation I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/1386708/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/803318/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 Aug 18 20:56 /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/803318/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/803318/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=40 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="37" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.37(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=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='54cc93fe58c743ab8e83cb584d71b773' - 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='1386708' - PS1='# ' - PS2='> ' + INVOCATION_ID=7d143f109b3a4e349a3e684078587d41 + 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=803318 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.wY2U15cv/pbuilderrc_QN9r --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.wY2U15cv/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-8.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.wY2U15cv/pbuilderrc_cAD1 --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.wY2U15cv/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-8.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-37-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.140-1 (2025-05-22) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.12.32+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.32-1~bpo12+1 (2025-06-21) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 May 12 19:25 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/1386708/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 12 2025 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/803318/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -205,7 +237,7 @@ Get: 92 http://deb.debian.org/debian unstable/main amd64 xdg-utils all 1.2.1-2 [75.8 kB] Get: 93 http://deb.debian.org/debian unstable/main amd64 texlive-base all 2024.20250309-1 [23.1 MB] Get: 94 http://deb.debian.org/debian unstable/main amd64 texlive-latex-base all 2024.20250309-1 [1294 kB] -Fetched 136 MB in 5s (28.6 MB/s) +Fetched 136 MB in 16s (8455 kB/s) Preconfiguring packages ... Selecting previously unselected package libproc2-0: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 ... 19849 files and directories currently installed.) @@ -621,7 +653,11 @@ fakeroot is already the newest version (1.37.1.2-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-8_source.changes +I: user script /srv/workspace/pbuilder/803318/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/803318/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-8_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-8 dpkg-buildpackage: info: source distribution unstable @@ -875,79 +911,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' @@ -958,15 +980,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 \ @@ -1030,7 +1066,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Jul 16 14:24:59 2025 +Tue Aug 18 21:03:13 2026 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2307,7 +2343,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 # mem = - : (* -> * list -> bool) @@ -2476,7 +2512,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x27254a0 .............() : void @@ -2667,7 +2703,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/ml-curry_ml.o 0x27254a0 .............() : void @@ -2892,7 +2928,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 # concat = - : (string -> string -> string) @@ -3033,7 +3069,7 @@ ;; Finished loading "lisp/f-ol-net" ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 16/7/25 + version 2.02 (GCL) created 18/8/26 #;; start address for /build/reproducible-path/hol88-2.02.19940316dfsg/ml/site_ml.o 0x27254a0 ...() : void @@ -3382,7 +3418,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 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 ###########################() : void @@ -3395,7 +3431,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 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 ################################################################################################() : void @@ -3540,7 +3576,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 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 ############################() : void @@ -3583,7 +3619,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 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 ############################Theory ind loaded () : void @@ -3620,7 +3656,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -3661,7 +3697,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4063,7 +4099,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4131,7 +4167,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4336,7 +4372,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4460,7 +4496,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4546,7 +4582,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4639,7 +4675,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4708,7 +4744,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -4813,7 +4849,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5048,7 +5084,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5074,7 +5110,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5202,7 +5238,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5250,7 +5286,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5317,7 +5353,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5376,7 +5412,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5432,7 +5468,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 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre6 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5444,7 +5480,7 @@ Temporary directory for compiler files set to /tmp/ > -HOL-LCF version 2.02 (GCL) created 16/7/25 +HOL-LCF version 2.02 (GCL) created 18/8/26 #() : void @@ -5496,7 +5532,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ##########################() : void @@ -5527,7 +5563,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ##############################() : void @@ -5614,7 +5650,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #######################################################################() : void @@ -5767,7 +5803,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ###########################() : void @@ -5802,7 +5838,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #############################() : void @@ -5863,7 +5899,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ###########################Theory arithmetic loaded () : void @@ -6358,7 +6394,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ##################################() : void @@ -6505,7 +6541,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #################################Theory list loaded () : void @@ -6844,7 +6880,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ###############################Theory list loaded () : void @@ -8341,7 +8377,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #############################() : void @@ -8725,7 +8761,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ############################() : void @@ -9023,7 +9059,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ############################() : void @@ -9163,7 +9199,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ############################################() : void @@ -9260,7 +9296,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 ##################################() : void @@ -9290,7 +9326,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -9307,7 +9343,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #Theory num loaded () : void @@ -9326,7 +9362,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -9483,7 +9519,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 # @@ -9521,7 +9557,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 # @@ -9555,7 +9591,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -9640,7 +9676,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -9681,7 +9717,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -9865,7 +9901,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 # define_load_lib_function = - : (string list -> void -> void) @@ -9941,7 +9977,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #GCL (GNU Common Lisp) 2.7.1 Thu Apr 10 09:38:27 PM EDT 2025 CLtL1 git: Version_2_7_2pre6 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -9953,7 +9989,7 @@ Temporary directory for compiler files set to /tmp/ > -BASIC-HOL version 2.02 (GCL) created 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #() : void @@ -10017,11 +10053,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Jul 16 14:27:33 2025 +Tue Aug 18 21:06:30 2026 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Jul 16 14:27:33 2025 +Tue Aug 18 21:06:30 2026 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10044,7 +10080,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -10128,7 +10164,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -10234,7 +10270,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -10984,7 +11020,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11007,7 +11043,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11050,7 +11086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11086,7 +11122,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11138,7 +11174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11170,7 +11206,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11208,7 +11244,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11236,7 +11272,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11313,7 +11349,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11335,7 +11371,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11389,7 +11425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11438,7 +11474,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11589,7 +11625,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11633,7 +11669,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11708,7 +11744,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11758,7 +11794,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11821,7 +11857,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11874,7 +11910,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -11920,7 +11956,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12008,7 +12044,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12046,7 +12082,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12107,7 +12143,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12171,7 +12207,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12197,7 +12233,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12222,7 +12258,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12261,7 +12297,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -12337,7 +12373,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13074,7 +13110,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13097,7 +13133,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13140,7 +13176,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13175,7 +13211,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13216,7 +13252,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13279,7 +13315,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13302,7 +13338,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13327,7 +13363,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13354,7 +13390,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13390,7 +13426,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13922,7 +13958,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13945,7 +13981,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -13979,7 +14015,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14034,7 +14070,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14125,7 +14161,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14294,7 +14330,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14458,7 +14494,7 @@ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. P z ==> l(y,z)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1294 PAIRED_EXT = |- !l m. (!x y. l(x,y) = m(x,y)) = (l = m) @@ -14509,7 +14545,7 @@ |- !P l. woset l /\ (!x. fl l x /\ (!y. less l(y,x) ==> P y) ==> P x) ==> (!x. fl l x ==> P x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 469 WO_INDUCT_TAC = - : tactic @@ -14586,7 +14622,7 @@ Theorem LESS_NOT_EQ autoloading from theory `prim_rec` ... LESS_NOT_EQ = |- !m n. m < n ==> ~(m = n) -Run time: 0.0s +Run time: 0.1s Definition LESS_OR_EQ autoloading from theory `arithmetic` ... LESS_OR_EQ = |- !m n. m <= n = m < n \/ (m = n) @@ -14621,7 +14657,7 @@ Intermediate theorems generated: 401 LINSEG_INSEG = |- !l a. woset l ==> (linseg l a) inseg l -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 240 LINSEG_WOSET = |- !l a. woset l ==> woset(linseg l a) @@ -14685,7 +14721,7 @@ ordinal (\(x,y). l(x,y) \/ (y = (@y. ~fl l y)) /\ (fl l x \/ (x = (@y. ~fl l y)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) @@ -14747,7 +14783,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1083 () : void @@ -14757,7 +14793,7 @@ File mk_wellorder loaded () : void -Run time: 0.4s +Run time: 1.1s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -14766,7 +14802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14897,7 +14933,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -14989,7 +15025,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -15068,7 +15104,7 @@ |- !x y a. ((a = x) = (a = y)) ==> (x = y); |- !a. I(I a) = a] : thm list -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2546 () : void @@ -15078,15 +15114,15 @@ File ../../Library/abs_theory/example.ml loaded () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 6013 -===> abs_theory rebuilt on Wed Jul 16 14:28:30 2025 +===> abs_theory rebuilt on Tue Aug 18 21:07:18 2026 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -15259,7 +15295,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -15539,7 +15575,7 @@ Run time: 0.0s TRAT_NOZERO = |- !h i. ~(h trat_add i) trat_eq h -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 250 Theorem LESS_ADD_1 autoloading from theory `arithmetic` ... @@ -15563,7 +15599,7 @@ Intermediate theorems generated: 599 TRAT_SUCINT_0 = |- !n. (trat_sucint n) trat_eq (n,0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 233 Theorem LESS_ADD_NONZERO autoloading from theory `arithmetic` ... @@ -15686,7 +15722,7 @@ File hrat.ml loaded () : void -Run time: 0.2s +Run time: 0.1s Intermediate theorems generated: 11032 #\ @@ -15696,7 +15732,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -16018,7 +16054,7 @@ Intermediate theorems generated: 102 CUT_STRADDLE = |- !X x y. cut X x /\ ~cut X y ==> x hrat_lt y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 137 Theorem LESS_SUC_REFL autoloading from theory `prim_rec` ... @@ -16154,7 +16190,7 @@ HREAL_SUB_ISACUT = |- !X Y. X hreal_lt Y ==> isacut(\w. ?x. ~cut X x /\ cut Y(x hrat_add w)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 400 HREAL_SUB_ADD = @@ -16206,7 +16242,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -16481,7 +16517,7 @@ TREAL_ADD_ASSOC = |- !x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 63 Theorem HREAL_MUL_ASSOC autoloading from theory `HREAL` ... @@ -16636,7 +16672,7 @@ TREAL_INV_WELLDEF = |- !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2545 REAL_10 = |- ~(r1 = r0) @@ -16665,7 +16701,7 @@ (!r. r0 real_lt r = (real_of_hreal(hreal_of_real r) = r)) REAL_ISO = |- !h i. h hreal_lt i ==> (real_of_hreal h) real_lt (real_of_hreal i) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 7766 REAL_ISO_EQ = @@ -16715,7 +16751,7 @@ (?x. P x) /\ (?z. !x. P x ==> x real_lt z) ==> (?s. !y. (?x. P x /\ y real_lt x) = y real_lt s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 199 [|- ~(r1 = r0); @@ -16744,7 +16780,7 @@ File realax.ml loaded () : void -Run time: 0.3s +Run time: 0.2s Intermediate theorems generated: 26795 #\ @@ -16754,7 +16790,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -17058,7 +17094,7 @@ Intermediate theorems generated: 28 REAL_LTE_TOTAL = |- !x y. x < y \/ y <= x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 27 REAL_LE_REFL = |- !x. x <= x @@ -17210,7 +17246,7 @@ Intermediate theorems generated: 45 REAL_NEG_0 = |- --(& 0) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 9 REAL_NEG_SUB = |- !x y. --(x - y) = y - x @@ -17266,7 +17302,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) @@ -17399,7 +17435,7 @@ Intermediate theorems generated: 26 REAL_OVER1 = |- !x. x / (& 1) = x -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 22 REAL_DIV_REFL = |- !x. ~(x = & 0) ==> (x / x = & 1) @@ -17444,7 +17480,7 @@ Intermediate theorems generated: 268 REAL_LT_FRACTION = |- !n d. 1 num_lt n ==> ((d / (& n)) < d = (& 0) < d) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 184 Theorem NOT_SUC autoloading from theory `num` ... @@ -17580,7 +17616,7 @@ Intermediate theorems generated: 24 REAL_EQ_SUB_RADD = |- !x y z. (x - y = z) = (x = z + y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 17 REAL_INV_MUL = @@ -17697,7 +17733,7 @@ Intermediate theorems generated: 169 REAL_MIDDLE1 = |- !a b. a <= b ==> a <= ((a + b) / (& 2)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 89 REAL_MIDDLE2 = |- !a b. a <= b ==> ((a + b) / (& 2)) <= b @@ -17766,7 +17802,7 @@ Intermediate theorems generated: 156 ABS_N = |- !n. abs(& n) = & n -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 21 ABS_BETWEEN = @@ -17874,7 +17910,7 @@ Intermediate theorems generated: 32 POW_POS = |- !x. (& 0) <= x ==> (!n. (& 0) <= (x pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 POW_LE = |- !n x y. (& 0) <= x /\ x <= y ==> (x pow n) <= (y pow n) @@ -17944,7 +17980,7 @@ |- !d. (!y. (?x. (\x. P(x + d))x /\ y < x) = y < s) ==> (!y. (?x. P x /\ y < x) = y < (s + d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 119 SUP_LEMMA2 = |- (?x. P x) ==> (?d x. (\x. P(x + d))x /\ (& 0) < x) @@ -17984,7 +18020,7 @@ |- !P. (?x. P x) /\ (?z. !x. P x ==> x <= z) = (?x. P x) /\ (?z. !x. P x ==> x < z) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 53 REAL_SUP_LE = @@ -18080,7 +18116,7 @@ SUM_ABS = |- !f m n. abs(Sum(m,n)(\m. abs(f m))) = Sum(m,n)(\m. abs(f m)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 42 SUM_ABS_LE = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) @@ -18259,7 +18295,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -18513,7 +18549,7 @@ Intermediate theorems generated: 20 METRIC_ZERO = |- !m x y. (dist m(x,y) = & 0) = (x = y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 41 METRIC_SAME = |- !m x. dist m(x,x) = & 0 @@ -18529,7 +18565,7 @@ Run time: 0.0s METRIC_POS = |- !m x y. (& 0) <= (dist m(x,y)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 91 Theorem REAL_LE_ANTISYM autoloading from theory `REAL` ... @@ -18753,7 +18789,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -18997,7 +19033,7 @@ (x --> x0)(mtop d,g) = (!e. (& 0) < e ==> (?n. g n n /\ (!m. g m n ==> (dist d(x m,x0)) < e))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 373 Theorem METRIC_TRIANGLE autoloading from theory `TOPOLOGY` ... @@ -19336,7 +19372,7 @@ dorder g ==> (!x x0. (x --> x0)(mtop mr1,g) = ((\n. --(x n)) --> (-- x0))(mtop mr1,g)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 121 NET_SUB = @@ -19392,7 +19428,7 @@ Definition LESS_OR_EQ autoloading from theory `arithmetic` ... LESS_OR_EQ = |- !m n. m num_le n = m num_lt n \/ (m = n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 Theorem REAL_LE autoloading from theory `REAL` ... @@ -19488,7 +19524,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -19813,7 +19849,7 @@ Run time: 0.0s SUBSEQ_SUC = |- !f. subseq f = (!n. (f n) num_lt (f(SUC n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 182 mono = @@ -20149,7 +20185,7 @@ Run time: 0.0s SEQ_ABS = |- !f. (\n. abs(f n)) --> (& 0) = f --> (& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 70 Theorem NET_ABS autoloading from theory `NETS` ... @@ -20432,7 +20468,7 @@ Intermediate theorems generated: 2 summable = |- !f. summable f = (?s. f sums s) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2 suminf = |- !f. suminf f = (@s. f sums s) @@ -20484,7 +20520,7 @@ |- !f n. summable f /\ (!m. n num_le m ==> (& 0) <= (f m)) ==> (Sum(0,n)f) <= (suminf f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 220 Theorem Sum autoloading from theory `REAL` ... @@ -20705,7 +20741,7 @@ |- !x. ~(x = & 1) ==> (!n. Sum(0,n)(\n'. x pow n') = ((x pow n) - (& 1)) / (x - (& 1))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 411 Theorem REAL_NEG_INV autoloading from theory `REAL` ... @@ -20782,7 +20818,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -21104,7 +21140,7 @@ LIM_EQUAL = |- !f g l x0. (!x. ~(x = x0) ==> (f x = g x)) ==> ((f --> l)x0 = (g --> l)x0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 171 Theorem REAL_LT_TRANS autoloading from theory `REAL` ... @@ -21160,7 +21196,7 @@ Intermediate theorems generated: 2 contl = |- !f x. f contl x = ((\h. f(x + h)) --> (f x))(& 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 differentiable = |- !f x. f differentiable x = (?l. (f diffl l)x) @@ -21458,7 +21494,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` ... @@ -21726,7 +21762,7 @@ (?M. (!x. a <= x /\ x <= b ==> (f x) <= M) /\ (?x. a <= x /\ x <= b /\ (f x = M))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1646 CONT_ATTAINS2 = @@ -21801,7 +21837,7 @@ (f diffl l)x /\ (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> (f x) <= (f y))) ==> (l = & 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 88 DIFF_LCONST = @@ -21875,7 +21911,7 @@ (!x. a <= x /\ x <= b ==> f contl x) /\ (!x. a < x /\ x < b ==> (f diffl (& 0))x) ==> (f b = f a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 253 DIFF_ISCONST = @@ -21908,7 +21944,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -22120,7 +22156,7 @@ Theorem SUB_0 autoloading from theory `arithmetic` ... SUB_0 = |- !m. (0 num_sub m = 0) /\ (m num_sub 0 = m) -Run time: 0.1s +Run time: 0.0s Theorem REAL_ADD_LID autoloading from theory `REAL` ... REAL_ADD_LID = |- !x. (& 0) + x = x @@ -22551,7 +22587,7 @@ (((((z + h) pow n) - (z pow n)) / h) - ((& n) * (z pow (n num_sub 1))))) <= ((& n) * ((&(n num_sub 1)) * ((K pow (n num_sub 2)) * (abs h)))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1294 Theorem REAL_MUL_LINV autoloading from theory `REAL` ... @@ -22780,7 +22816,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -23288,7 +23324,7 @@ Intermediate theorems generated: 1 EXP_FDIFF = |- diffs(\n. inv(&(FACT n))) = (\n. inv(&(FACT n))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 193 Theorem REAL_MUL_RZERO autoloading from theory `REAL` ... @@ -23738,7 +23774,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` ... @@ -23921,7 +23957,7 @@ Run time: 0.0s SIN_NEG = |- !x. sin(-- x) = --(sin x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 48 COS_NEG = |- !x. cos(-- x) = cos x @@ -23963,7 +23999,7 @@ (((--(& 1)) pow n) / (&(FACT((2 num_mul n) num_add 1)))) * (x pow ((2 num_mul n) num_add 1))) sums (sin x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 183 Theorem LESS_EQ_MONO autoloading from theory `arithmetic` ... @@ -24325,7 +24361,7 @@ (sin x = & 0) = (?n. EVEN n /\ (x = (& n) * (pi / (& 2)))) \/ (?n. EVEN n /\ (x = --((& n) * (pi / (& 2))))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 319 tan = |- !x. tan x = (sin x) / (cos x) @@ -24569,7 +24605,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -24591,7 +24627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -24657,7 +24693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -24689,7 +24725,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -24798,7 +24834,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -24951,7 +24987,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25024,7 +25060,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25104,7 +25140,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25261,7 +25297,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25416,7 +25452,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25633,7 +25669,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25655,7 +25691,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25674,7 +25710,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25719,7 +25755,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25784,7 +25820,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25834,7 +25870,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25904,7 +25940,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -25974,7 +26010,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26010,7 +26046,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26063,7 +26099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26135,7 +26171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26214,7 +26250,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26409,7 +26445,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -26446,7 +26482,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -27132,7 +27168,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -27604,7 +27640,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -27868,7 +27904,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -28113,7 +28149,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -28577,7 +28613,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29045,7 +29081,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29101,7 +29137,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29191,7 +29227,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29390,7 +29426,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29422,7 +29458,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29556,7 +29592,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29859,7 +29895,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29891,7 +29927,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29930,7 +29966,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -29962,7 +29998,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30123,7 +30159,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30256,7 +30292,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30445,7 +30481,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30505,7 +30541,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30630,7 +30666,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30741,7 +30777,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30766,7 +30802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30794,7 +30830,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -30907,7 +30943,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -31410,7 +31446,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -31658,7 +31694,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -31884,7 +31920,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -31926,7 +31962,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -31958,2655 +31994,18 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -# -pp_lang1_rules = -[((``, (Const_name(`NUM`, [Patt_child(Var_name(`num`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`num`, -))])); - ((``, (Const_name(`NEG`, [Patt_child(Var_child `num`)])), -), - [], - PF(H_box[(0, PO_constant `-`); (0, PO_subcall((`num`, -), []))])); - ((``, (Const_name(`STRING`, [Patt_child(Var_name(`string`, []))])), -), - [], - PF(H_box[(0, PO_constant `'`); - (0, PO_leaf(`string`, -)); - (0, PO_constant `'`)])); - ((``, - (Const_name(`TERMINAL`, [Patt_child(Var_name(`string`, []))])), - -), - [], - PF(H_box[(0, PO_constant `"`); - (0, PO_leaf(`string`, -)); - (0, PO_constant `"`)])); - ((``, (Const_name(`ML_FUN`, [Var_children `strings`])), -), - [], - PF(H_box[(0, PO_constant `{`); - (0, - PO_format(PF(V_box[(((Abs 0), 0), - PO_subcall((`strings`, -), []))]))); - (0, PO_constant `}`)])); - ((``, (Const_name(`ID`, [Patt_child(Var_name(`id`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`id`, -))])); - ((``, (Const_name(`NAME_META`, [Var_children `id`])), -), - [], - PF(H_box[(0, PO_constant `***`); (0, PO_subcall((`id`, -), []))])); - ((``, (Const_name(`CHILD_META`, [Var_children `id`])), -), - [], - PF(H_box[(0, PO_constant `*`); (0, PO_subcall((`id`, -), []))])); - ((``, (Const_name(`CHILDREN_META`, [Var_children `id`])), -), - [], - PF(H_box[(0, PO_constant `**`); (0, PO_subcall((`id`, -), []))])); - ((``, - (Print_loop((Const_name(`METAVAR_LIST`, - [Patt_child(Var_child `metavars`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`METAVAR_LIST`, - [Patt_child(Var_child `metavar`)]))), - -), - [], - PF(HV_box[((0, (Abs 3), 0), - PO_expand(H_box[(0, PO_subcall((`metavars`, -), [])); - (0, PO_constant `;`)])); - ((0, (Abs 3), 0), PO_subcall((`metavar`, -), []))])); - ((``, (Const_name(`MIN`, [Patt_child(Var_child `num`)])), -), - [], - PF(H_box[(0, PO_subcall((`num`, -), []))])); - ((``, (Const_name(`MAX`, [Patt_child(Var_child `num`)])), -), - [], - PF(H_box[(0, PO_subcall((`num`, -), []))])); - ((``, - (Const_name(`LOOP_RANGE`, - [Patt_child(Const_name(`MIN`, - [Patt_child(Var_child `num`)]))])), - -), - [], - PF(H_box[(0, PO_subcall((`num`, -), [])); (0, PO_constant `..`)])); - ((``, - (Const_name(`LOOP_RANGE`, - [Patt_child(Const_name(`MAX`, - [Patt_child(Var_child `num`)]))])), - -), - [], - PF(H_box[(0, PO_constant `..`); (0, PO_subcall((`num`, -), []))])); - ((``, - (Const_name(`LOOP_RANGE`, - [Patt_child(Var_child `min`); - Patt_child(Var_child `max`)])), - -), - [], - PF(H_box[(0, PO_subcall((`min`, -), [])); - (0, PO_constant `..`); - (0, PO_subcall((`max`, -), []))])); - ((``, - (Const_name(`LOOP_LINK`, - [Patt_child(Var_child `loop_range`); - Patt_child(Var_child `metavar_list`)])), - -), - [], - PF(H_box[(0, PO_constant `<`); - (0, PO_subcall((`loop_range`, -), [])); - (0, PO_constant `:`); - (1, PO_subcall((`metavar_list`, -), [])); - (0, PO_constant `>`)])); - ((``, (Const_name(`LOOP_LINK`, [Var_children `metavar_list`])), -), - [], - PF(H_box[(0, PO_constant `<`); - (0, PO_subcall((`metavar_list`, -), [])); - (0, PO_constant `>`)])); - ((``, (Const_name(`LABEL`, [Patt_child(Var_child `child_meta`)])), -), - [], - PF(H_box[(0, PO_constant `|`); - (0, PO_subcall((`child_meta`, -), [])); - (0, PO_constant `|`)])); - ((``, - (Const_name(`NODE_NAME`, [Patt_child(Var_child `node_name`)])), - -), - [], - PF(H_box[(0, PO_subcall((`node_name`, -), []))])); - ((``, (Const_name(`CHILD`, [Patt_child(Var_child `child`)])), -), - [], - PF(H_box[(0, PO_subcall((`child`, -), []))])); - ((``, - (Print_loop((Const_name(`CHILD_LIST`, - [Patt_child(Var_child `children`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`CHILD_LIST`, [Patt_child(Var_child `child`)]))), - -), - [], - PF(HV_box[((0, (Abs 3), 0), - PO_expand(H_box[(0, PO_subcall((`children`, -), [])); - (0, PO_constant `,`)])); - ((0, (Abs 3), 0), PO_subcall((`child`, -), []))])); - ((``, - (Const_name(`PATT_TREE`, - [Patt_child(Const_name(`NODE_NAME`, - [Patt_child(Var_child `node_name`)])); - Patt_child(Var_child `child_list`)])), - -), - [], - PF(HV_box[((0, (Abs 3), 0), PO_subcall((`node_name`, -), [])); - ((0, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_constant `(`); - (0, PO_subcall((`child_list`, -), [])); - (0, PO_constant `)`)])))])); - ((``, - (Const_name(`PATT_TREE`, - [Patt_child(Const_name(`NODE_NAME`, - [Patt_child(Var_child `node_name`)]))])), - -), - [], - PF(H_box[(0, PO_subcall((`node_name`, -), [])); (0, PO_constant `()`)])); - ((``, (Const_name(`PATT_TREE`, [Var_children `x`])), -), - [], - PF(HV_box[((0, (Abs 3), 0), PO_subcall((`x`, -), []))])); - ((``, (Const_name(`LOOP`, [Patt_child(Var_child `patt_tree`)])), -), - [], - PF(H_box[(0, PO_constant `[`); - (0, PO_subcall((`patt_tree`, -), [])); - (0, PO_constant `]`)])); - ((``, (Const_name(`TEST`, [Patt_child(Var_child `test`)])), -), - [], - PF(H_box[(0, PO_subcall((`test`, -), []))])); - ((``, - (Const_name(`PATTERN`, - [Patt_child(Var_child `string`); - Patt_child(Var_child `patt_tree`); - Var_children `test`])), - -), - [], - PF(H_box[(0, PO_subcall((`string`, -), [])); - (0, PO_constant `::`); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_subcall((`patt_tree`, -), [])); - ((1, (Abs 3), 0), - PO_expand(HV_box[((1, (Abs 3), 0), - PO_constant `where`); - ((1, (Abs 3), 0), - PO_subcall((`test`, - -), - []))]))])))])); - ((``, - (Const_name(`TRANSFORM`, [Patt_child(Var_child `transform`)])), - -), - [], - PF(H_box[(0, PO_subcall((`transform`, -), []))])); - ((``, - (Const_name(`P_SPECIAL`, - [Patt_child(Var_child `metavar`); - Patt_child(Var_child `transform`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, PO_subcall((`metavar`, -), [])); - (1, PO_constant `=`)]))); - ((1, (Abs 3), 0), PO_subcall((`transform`, -), []))])); - ((``, - (Print_loop((Const_name(`P_SPECIAL_LIST`, - [Patt_child(Var_child `p_specials`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`P_SPECIAL_LIST`, - [Patt_child(Var_child `p_special`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), - PO_expand(H_box[(0, PO_subcall((`p_specials`, -), [])); - (0, PO_constant `;`)])); - ((1, (Abs 0), 0), PO_subcall((`p_special`, -), []))]))] -: print_rule list - -pp_lang1_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File PP_parser/pp_lang1_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'compilet `PP_parser/pp_lang2_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - - -pp_lang2_rules = -[((``, (Const_name(`INT_EXP`, [Patt_child(Var_child `int_exp`)])), -), - [], - PF(H_box[(0, PO_subcall((`int_exp`, -), []))])); - ((``, - (Const_name(`ASSIGN`, - [Patt_child(Var_child `id`); Patt_child(Var_child `exp`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, PO_subcall((`id`, -), [])); - (1, PO_constant `:=`)]))); - ((1, (Abs 3), 0), PO_subcall((`exp`, -), []))])); - ((``, - (Print_loop((Const_name(`ASSIGNMENTS`, - [Patt_child(Var_child `assigns`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`ASSIGNMENTS`, - [Patt_child(Var_child `assign`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), - PO_expand(H_box[(0, PO_subcall((`assigns`, -), [])); - (0, PO_constant `;`)])); - ((1, (Abs 0), 0), PO_subcall((`assign`, -), []))])); - ((``, (Const_name(`F_SUBCALL`, [Patt_child(Var_child `child`)])), -), - [], - PF(H_box[(0, PO_subcall((`child`, -), []))])); - ((``, - (Const_name(`F_SUBCALL`, - [Patt_child(Var_child `transform`); - Patt_child(Var_child `metavar`)])), - -), - [], - PF(HV_box[((0, (Abs 3), 0), PO_subcall((`transform`, -), [])); - ((0, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_constant `(`); - (0, PO_subcall((`metavar`, -), [])); - (0, PO_constant `)`)])))])); - ((``, - (Const_name(`C_SUBCALL`, [Patt_child(Var_child `f_subcall`)])), - -), - [], - PF(H_box[(0, PO_subcall((`f_subcall`, -), []))])); - ((``, - (Const_name(`C_SUBCALL`, - [Patt_child(Var_child `string`); - Patt_child(Var_child `f_subcall`)])), - -), - [], - PF(HV_box[((0, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_subcall((`string`, -), [])); - (0, PO_constant `::`)]))); - ((0, (Abs 3), 0), PO_subcall((`f_subcall`, -), []))])); - ((``, - (Const_name(`LEAF_OR_SUBCALL`, - [Patt_child(Var_child `c_subcall`); - Var_children `assigns`])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), PO_subcall((`c_subcall`, -), [])); - ((1, (Abs 3), 0), - PO_expand(V_box[(((Abs 0), 0), PO_constant `with`); - (((Abs 3), 0), - PO_subcall((`assigns`, -), [])); - (((Abs 0), 0), PO_constant `end with`)]))])); - ((``, (Const_name(`INC`, [Patt_child(Var_child `num`)])), -), - [], - PF(H_box[(0, PO_constant `+`); (0, PO_subcall((`num`, -), []))])); - ((``, (Const_name(`H_PARAMS`, [Patt_child(Var_child `num`)])), -), - [], - PF(H_box[(0, PO_subcall((`num`, -), []))])); - ((``, - (Const_name(`V_PARAMS`, - [Patt_child(Var_child `indent`); - Patt_child(Var_child `num`)])), - -), - [], - PF(H_box[(0, PO_subcall((`indent`, -), [])); - (0, PO_constant `,`); - (0, PO_subcall((`num`, -), []))])); - ((``, - (Const_name(`HV_PARAMS`, - [Patt_child(Var_child `num1`); - Patt_child(Var_child `indent`); - Patt_child(Var_child `num2`)])), - -), - [], - PF(H_box[(0, PO_subcall((`num1`, -), [])); - (0, PO_constant `,`); - (0, PO_subcall((`indent`, -), [])); - (0, PO_constant `,`); - (0, PO_subcall((`num2`, -), []))])); - ((``, - (Const_name(`HOV_PARAMS`, - [Patt_child(Var_child `num1`); - Patt_child(Var_child `indent`); - Patt_child(Var_child `num2`)])), - -), - [], - PF(H_box[(0, PO_subcall((`num1`, -), [])); - (0, PO_constant `,`); - (0, PO_subcall((`indent`, -), [])); - (0, PO_constant `,`); - (0, PO_subcall((`num2`, -), []))])); - ((``, (Const_name(`H_BOX`, [Patt_child(Var_child `h_params`)])), -), - [], - PF(H_box[(1, PO_constant `h`); (1, PO_subcall((`h_params`, -), []))])); - ((``, (Const_name(`V_BOX`, [Patt_child(Var_child `v_params`)])), -), - [], - PF(H_box[(1, PO_constant `v`); (1, PO_subcall((`v_params`, -), []))])); - ((``, (Const_name(`HV_BOX`, [Patt_child(Var_child `hv_params`)])), -), - [], - PF(H_box[(1, PO_constant `hv`); (1, PO_subcall((`hv_params`, -), []))])); - ((``, (Const_name(`HOV_BOX`, [Patt_child(Var_child `hov_params`)])), -), - [], - PF(H_box[(1, PO_constant `hov`); - (1, PO_subcall((`hov_params`, -), []))])); - ((``, (Const_name(`OBJECT`, [Patt_child(Var_child `object`)])), -), - [], - PF(H_box[(0, PO_subcall((`object`, -), []))])); - ((``, - (Const_name(`H_OBJECT`, - [Var_children `h_params`; Patt_child(Var_child `object`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_expand(H_box[(0, PO_constant `<`); - (0, PO_subcall((`h_params`, -), [])); - (0, PO_constant `>`)])); - ((1, (Abs 3), 0), PO_subcall((`object`, -), []))])); - ((``, - (Const_name(`V_OBJECT`, - [Var_children `v_params`; Patt_child(Var_child `object`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_expand(H_box[(0, PO_constant `<`); - (0, PO_subcall((`v_params`, -), [])); - (0, PO_constant `>`)])); - ((1, (Abs 3), 0), PO_subcall((`object`, -), []))])); - ((``, - (Const_name(`HV_OBJECT`, - [Var_children `hv_params`; - Patt_child(Var_child `object`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_expand(H_box[(0, PO_constant `<`); - (0, PO_subcall((`hv_params`, -), [])); - (0, PO_constant `>`)])); - ((1, (Abs 3), 0), PO_subcall((`object`, -), []))])); - ((``, - (Const_name(`HOV_OBJECT`, - [Var_children `hov_params`; - Patt_child(Var_child `object`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_expand(H_box[(0, PO_constant `<`); - (0, PO_subcall((`hov_params`, -), [])); - (0, PO_constant `>`)])); - ((1, (Abs 3), 0), PO_subcall((`object`, -), []))])); - ((``, - (Print_loop((Const_name(`H_OBJECT_LIST`, - [Patt_child(Var_child `h_objects`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`H_OBJECT_LIST`, - [Patt_child(Var_child `h_object`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), PO_subcall((`h_objects`, -), [])); - ((1, (Abs 0), 0), PO_subcall((`h_object`, -), []))])); - ((``, - (Print_loop((Const_name(`V_OBJECT_LIST`, - [Patt_child(Var_child `v_objects`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`V_OBJECT_LIST`, - [Patt_child(Var_child `v_object`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), PO_subcall((`v_objects`, -), [])); - ((1, (Abs 0), 0), PO_subcall((`v_object`, -), []))])); - ((``, - (Print_loop((Const_name(`HV_OBJECT_LIST`, - [Patt_child(Var_child `hv_objects`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`HV_OBJECT_LIST`, - [Patt_child(Var_child `hv_object`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), PO_subcall((`hv_objects`, -), [])); - ((1, (Abs 0), 0), PO_subcall((`hv_object`, -), []))])); - ((``, - (Print_loop((Const_name(`HOV_OBJECT_LIST`, - [Patt_child(Var_child `hov_objects`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`HOV_OBJECT_LIST`, - [Patt_child(Var_child `hov_object`)]))), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), PO_subcall((`hov_objects`, -), [])); - ((1, (Abs 0), 0), PO_subcall((`hov_object`, -), []))])); - ((``, - (Const_name(`BOX_SPEC`, - [Patt_child(Var_child `box`); - Patt_child(Var_child `object_list`)])), - -), - [], - PF(H_box[(0, PO_constant `<`); - (0, PO_subcall((`box`, -), [])); - (0, PO_constant `>`); - (1, PO_subcall((`object_list`, -), []))])); - ((``, (Const_name(`EXPAND`, [Patt_child(Var_child `box_spec`)])), -), - [], - PF(H_box[(0, PO_constant `**[`); - (0, PO_subcall((`box_spec`, -), [])); - (0, PO_constant `]`)])); - ((``, (Const_name(`FORMAT`, [])), -), - [], - PF(H_box[(0, PO_constant `[]`)])); - ((``, (Const_name(`FORMAT`, [Patt_child(Var_child `box_spec`)])), -), - [], - PF(H_box[(0, PO_constant `[`); - (0, PO_subcall((`box_spec`, -), [])); - (0, PO_constant `]`)])); - ((``, - (Const_name(`FORMAT`, - [Patt_child(Var_child `test`); - Patt_child(Var_child `format1`); - Patt_child(Var_child `format2`)])), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(H_box[(1, PO_constant `if`); - (1, PO_subcall((`test`, -), []))]))); - ((1, (Abs 0), 0), - PO_format(PF(H_box[(1, PO_constant `then`); - (1, PO_subcall((`format1`, -), []))]))); - ((1, (Abs 0), 0), - PO_format(PF(H_box[(1, PO_constant `else`); - (1, PO_subcall((`format2`, -), []))])))])); - ((``, - (Const_name(`RULE`, - [Patt_child(Const_name(`PATTERN`, - [Patt_child(Var_child `string`); - Patt_child(Var_child `patt_tree`); - Var_children `test`])); - Var_children `p_specials`; - Patt_child(Var_child `format`)])), - -), - [], - PF(H_box[(0, PO_subcall((`string`, -), [])); - (0, PO_constant `::`); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(H_box[(1, - PO_format(PF(HV_box[((1, - (Abs 3), - 0), - PO_subcall((`patt_tree`, - -), - [])); - ((1, - (Abs 3), - 0), - PO_expand(HV_box[((1, - (Abs 3), - 0), - PO_constant `where`); - ((1, - (Abs 3), - 0), - PO_subcall((`test`, - -), - []))]))]))); - (1, - PO_constant `->`)]))); - ((1, (Abs 0), 0), - PO_expand(H_box[(1, PO_constant `<<`); - (1, - PO_subcall((`p_specials`, - -), - [])); - (1, PO_constant `>>`)])); - ((1, (Abs 0), 0), - PO_subcall((`format`, -), []))])))])); - ((``, - (Print_loop((Const_name(`RULE_LIST`, - [Patt_child(Var_child `rules`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`RULE_LIST`, [Patt_child(Var_child `rule`)]))), - -), - [], - PF(V_box[(((Abs 0), 1), - PO_expand(H_box[(0, PO_subcall((`rules`, -), [])); - (0, PO_constant `;`)])); - (((Abs 0), 1), - PO_format(PF(H_box[(0, PO_subcall((`rule`, -), [])); - (0, PO_constant `;`)])))])); - ((``, (Const_name(`RULES`, [Patt_child(Var_child `rule_list`)])), -), - [], - PF(V_box[(((Abs 3), 0), PO_constant `rules`); - (((Abs 3), 0), PO_subcall((`rule_list`, -), [])); - (((Abs 0), 1), PO_constant `end rules`)])); - ((``, - (Const_name(`BINDING`, - [Patt_child(Var_child `id`); - Patt_child(Var_child `ml_fun`)])), - -), - [], - PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, PO_subcall((`id`, -), [])); - (1, PO_constant `=`)]))); - ((1, (Abs 3), 0), PO_subcall((`ml_fun`, -), []))])); - ((``, - (Print_loop((Const_name(`BINDING_LIST`, - [Patt_child(Var_child `bindings`); - Patt_child(Link_child(((Default), Default), - []))])), - Const_name(`BINDING_LIST`, - [Patt_child(Var_child `binding`)]))), - -), - [], - PF(V_box[(((Abs 0), 1), - PO_expand(H_box[(0, PO_subcall((`bindings`, -), [])); - (0, PO_constant `;`)])); - (((Abs 0), 1), - PO_format(PF(H_box[(0, PO_subcall((`binding`, -), [])); - (0, PO_constant `;`)])))])); - ((``, - (Const_name(`DECLARS`, [Patt_child(Var_child `binding_list`)])), - -), - [], - PF(V_box[(((Abs 3), 0), PO_constant `declarations`); - (((Abs 3), 0), PO_subcall((`binding_list`, -), [])); - (((Abs 0), 1), PO_constant `end declarations`)])); - ((``, - (Const_name(`ABBREVS`, [Patt_child(Var_child `binding_list`)])), - -), - [], - PF(V_box[(((Abs 3), 0), PO_constant `abbreviations`); - (((Abs 3), 0), PO_subcall((`binding_list`, -), [])); - (((Abs 0), 1), PO_constant `end abbreviations`)])); - ((``, (Const_name(`BODY`, [Var_children `x`])), -), - [], - PF(V_box[(((Abs 0), 2), PO_subcall((`x`, -), []))])); - ((``, - (Const_name(`PP`, - [Patt_child(Var_child `id`); - Patt_child(Var_child `body`)])), - -), - [], - PF(V_box[(((Abs 0), 1), - PO_format(PF(H_box[(1, PO_constant `prettyprinter`); - (1, PO_subcall((`id`, -), [])); - (1, PO_constant `=`)]))); - (((Abs 0), 1), PO_subcall((`body`, -), [])); - (((Abs 0), 2), PO_constant `end prettyprinter`)]))] -: print_rule list - -pp_lang2_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File PP_parser/pp_lang2_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'loadf `PP_parser/pp_lang2_pp`;;'\ - 'compilet `PP_parser/lex`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - -..() : void - - -copy_chars = -- -: (int -> (string -> string) -> string -> (string -> void) -> void) - - -New constructors declared: -Lex_spec : (string -> lex_symb) -Lex_num : (string -> lex_symb) -Lex_id : (string -> lex_symb) -Lex_block : (((string # string) # string list) -> lex_symb) - - -is_lex_char = - : ((string # string # string) -> bool) - -is_lex_ucase = - : (string -> bool) - -is_lex_lcase = - : (string -> bool) - -is_lex_letter = - : (string -> bool) - -is_lex_digit = - : (string -> bool) - -is_lex_underscore = - : (string -> bool) - -is_lex_eof = - : (string -> bool) - -is_lex_eol = - : (string -> bool) - -is_lex_space = - : (string -> bool) - -lex_error = - : ((string -> string) -> string -> string -> string -> *) - -read_char = - : ((* -> string) -> * -> string) - -read_number = - : ((* -> string) -> * -> string -> (lex_symb # string)) - -read_identifier = -- -: ((string -> string) -> string -> string -> (lex_symb # string)) - -read_block = -- -: ((string -> string) -> - string -> - (string # string) -> - string -> - (lex_symb # string)) - -read_special = -- -: ((string -> string) -> - string -> - string list -> - string -> - (lex_symb # string)) - -read_symb = -- -: ((string -> string) -> - string -> - (string # string) list -> - string list -> - string list -> - string -> - (lex_symb # string)) - -- -: ((string -> string) -> - string -> - (string # string) list -> - string list -> - string list -> - string -> - (lex_symb # string)) - - -read_symb = -- -: ((string -> string) -> - string -> - (string # string) list -> - string list -> - string list -> - string -> - (lex_symb # string)) - -Calling Lisp compiler - -File PP_parser/lex compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'loadf `PP_parser/pp_lang2_pp`;;'\ - 'loadf `PP_parser/lex`;;'\ - 'compilet `PP_parser/syntax`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - -..() : void - -....................() : void - - - -PP_quotes = -[(`'`, `'`); (`"`, `"`); (`{`, `}`); (`#`, `#`); (`%`, `%`)] -: (string # string) list - -PP_keywords = -[`prettyprinter`; - `rules`; - `declarations`; - `abbreviations`; - `with`; - `end`; - `where`; - `if`; - `then`; - `else`; - `h`; - `v`; - `hv`; - `hov`] -: string list - -PP_specials = -[`+`; - `-`; - `*`; - `**`; - `***`; - `,`; - `;`; - `:`; - `::`; - `=`; - `:=`; - `->`; - `..`; - `(`; - `)`; - `**[`; - `[`; - `]`; - `<`; - `>`; - `<<`; - `>>`; - `|`] -: string list - -syntax_error = -- -: ((string -> string) -> string -> string -> string -> lex_symb -> *) - -general_error = -- -: ((string -> string) -> string -> string -> string -> string -> *) - -read_PP_symb = -- -: ((string -> string) -> string -> string -> (lex_symb # string)) - -read_PP_number = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_integer = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_string = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_terminal = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_ML_function = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_identifier = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_name_metavar = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_child_metavar = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_children_metavar = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_metavar_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_min = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_max = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_loop_range = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_loop_link = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_label = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_node_name = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_child = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_child_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_pattern_tree = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_loop = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_test = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_pattern = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_transformation = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_p_special = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_p_special_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_int_expression = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_assignment = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_assignments = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_fun_subcall = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_context_subcall = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_leaf_or_subcall = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_indent = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_h_params = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_v_params = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_hv_params = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_hov_params = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_h_box = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_v_box = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_hv_box = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_hov_box = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_object = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_h_object = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_v_object = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_hv_object = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_hov_object = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_h_object_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_v_object_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_hv_object_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_hov_object_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_box_spec = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_expand = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) -read_PP_format = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_rule = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_rule_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_rules = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_binding = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_binding_list = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_declarations = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_abbreviations = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP_body = -- -: ((string -> string) -> - string -> - (lex_symb # string) -> - (print_tree # lex_symb # string)) - -read_PP = - : ((string -> string) -> string -> print_tree) - -- : ((string -> string) -> string -> print_tree) - - -read_PP = - : ((string -> string) -> string -> print_tree) - -Calling Lisp compiler - -File PP_parser/syntax compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'loadf `PP_parser/pp_lang2_pp`;;'\ - 'loadf `PP_parser/lex`;;'\ - 'loadf `PP_parser/syntax`;;'\ - 'compilet `PP_parser/convert`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - -..() : void - -....................() : void - -.......................................................() : void - - - -construction_error = - : (print_tree -> string -> *) - -indirect_string = - : (string -> string) - -convert_NUM = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_NEG = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_ML_FUN = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_ID_to_VAR = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_ID_to_TOKCONST = -- -: ((print_tree # *) -> (print_tree # ** list)) - -convert_METAVAR = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_METAVAR_to_TOKCONST = -- -: ((print_tree # *) -> (print_tree # ** list)) - -convert_METAVAR_LIST = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_MIN = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_MAX = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_LOOP_RANGE = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_LOOP_LINK = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_LABEL = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_NODE_NAME = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_CHILD = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) -convert_CHILD_LIST = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) -convert_PATT_TREE = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) -convert_LOOP = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_STRING = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_TEST = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_PATTERN = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_TRANSFORM = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_P_SPECIAL = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_P_SPECIAL_LIST = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_INT_EXP = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_ASSIGN = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_ASSIGNMENTS = -- -: ((print_tree # (string # print_tree) list) -> (print_tree # * list)) - -convert_F_SUBCALL = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_C_SUBCALL = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_LEAF_OR_SUBCALL = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_TERMINAL = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_INC = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_H_PARAMS = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_V_PARAMS = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_HV_PARAMS = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_HOV_PARAMS = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_BOX = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_OBJECT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_H_OBJECT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_V_OBJECT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_HV_OBJECT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_HOV_OBJECT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_H_OBJECT_LIST = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_V_OBJECT_LIST = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_HV_OBJECT_LIST = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_HOV_OBJECT_LIST = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_BOX_SPEC = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_EXPAND = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) -convert_FORMAT = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_RULE = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_RULE_LIST = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_RULES = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_BINDING = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_BINDING_LIST_to_LIST = -- -: ((print_tree # *) -> (print_tree # ** list)) - -convert_BINDING_LIST_to_LETREC = -- -: ((print_tree # *) -> (print_tree # ** list)) - -convert_DECLARS = - : ((print_tree # *) -> (print_tree # ** list)) - -convert_ABBREVS = -- -: ((print_tree # *) -> (print_tree # (string # print_tree) list)) - -convert_BODY = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -convert_PP = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - - -convert_PP = -- -: ((print_tree # (string # print_tree) list) -> - (print_tree # (string # print_tree) list)) - -Calling Lisp compiler - -File PP_parser/convert compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'loadf `PP_parser/pp_lang2_pp`;;'\ - 'loadf `PP_parser/lex`;;'\ - 'loadf `PP_parser/syntax`;;'\ - 'loadf `PP_parser/convert`;;'\ - 'compilet `PP_parser/generate`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - -..() : void - -....................() : void - -.......................................................() : void - -.................................................() : void - - - -PP_to_ML_rules = -[((`name`, (Var_name(`n`, [])), -), [], PF(H_box[(0, PO_leaf(`n`, -))])); - ((``, (Const_name(`INTCONST`, [Patt_child(Var_name(`n`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`n`, -))])); - ((``, (Const_name(`TOKCONST`, [Patt_child(Var_name(`n`, []))])), -), - [], - PF(H_box[(0, PO_constant ```); - (0, PO_leaf(`n`, -)); - (0, PO_constant ```)])); - ((``, (Const_name(`VAR`, [Patt_child(Var_name(`n`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`n`, -))])); - ((``, (Const_name(`CON`, [Patt_child(Var_name(`n`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`n`, -))])); - ((``, (Const_name(`CON0`, [Patt_child(Var_name(`n`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`n`, -))])); - ((``, - (Const_name(`UNOP`, - [Patt_child(Var_name(`n`, [])); - Patt_child(Var_child `c`)])), - -), - [], - PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), PO_leaf(`n`, -)); - ((0, (Abs 0), 0), - PO_subcall((`c`, -), []))]))); - (0, PO_constant `)`)])); - ((``, - (Const_name(`APPN`, - [Patt_child(Var_child `c1`); Patt_child(Var_child `c2`)])), - -), - [], - PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HV_box[((1, (Abs 1), 0), - PO_subcall((`c1`, -), [])); - ((1, (Abs 1), 0), - PO_subcall((`c2`, -), []))]))); - (0, PO_constant `)`)])); - ((``, - (Const_name(`ABSTR`, - [Patt_child(Var_child `c1`); Patt_child(Var_child `c2`)])), - -), - [], - PF(H_box[(0, PO_constant `(\`); - (0, - PO_format(PF(HV_box[((1, (Abs 1), 0), - PO_format(PF(H_box[(0, - PO_subcall((`c1`, - -), - [])); - (0, PO_constant `.`)]))); - ((1, (Abs 1), 0), - PO_subcall((`c2`, -), []))]))); - (0, PO_constant `)`)])); - ((``, - (Const_name(`LIST`, [Var_children `cl`; Patt_child(Var_child `c`)])), - -), - [], - PF(H_box[(0, PO_constant `[`); - (0, - PO_format(PF(HoV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`cl`, -), - [])); - (0, PO_constant `;`)])); - ((0, (Abs 0), 0), - PO_subcall((`c`, -), []))]))); - (0, PO_constant `]`)])); - ((``, (Const_name(`LIST`, [])), -), - [], - PF(H_box[(0, PO_constant `[]`)])); - ((``, - (Print_loop((Const_name(`DUPL`, - [Patt_child(Var_child `cl`); - Patt_child(Link_child(((Val 1), Default), - []))])), - Var_child `c`)), - -), - [], - PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`cl`, -), - [])); - (0, PO_constant `,`)])); - ((0, (Abs 0), 0), - PO_subcall((`c`, -), []))]))); - (0, PO_constant `)`)])); - ((``, - (Const_name(`LETREC`, - [Patt_child(Const_name(`DUPL`, - [Patt_child(Var_child `var1`); - Patt_child(Print_loop((Const_name(`DUPL`, - [Patt_child(Var_child `varl`); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `varl`))])); - Patt_child(Const_name(`DUPL`, - [Patt_child(Var_child `body1`); - Patt_child(Print_loop((Const_name(`DUPL`, - [Patt_child(Var_child `bodyl`); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `bodyl`))]))])), - -), - [], - PF(V_box[(((Abs 0), 0), - PO_format(PF(HV_box[((1, (Inc 1), 0), PO_constant `letrec`); - ((1, (Inc 1), 0), - PO_format(PF(H_box[(1, - PO_subcall((`var1`, - -), - [])); - (1, PO_constant `=`)]))); - ((1, (Inc 1), 0), - PO_subcall((`body1`, -), []))]))); - (((Abs 0), 0), - PO_expand(HV_box[((1, (Inc 1), 0), PO_constant `and`); - ((1, (Inc 1), 0), - PO_expand(H_box[(1, - PO_subcall((`varl`, -), - [])); - (1, PO_constant `=`)])); - ((1, (Inc 1), 0), - PO_subcall((`bodyl`, -), []))]))])); - ((``, - (Const_name(`LETREC`, - [Patt_child(Var_child `c1`); Patt_child(Var_child `c2`)])), - -), - [], - PF(HV_box[((1, (Inc 1), 0), PO_constant `letrec`); - ((1, (Inc 1), 0), - PO_format(PF(H_box[(1, PO_subcall((`c1`, -), [])); - (1, PO_constant `=`)]))); - ((1, (Inc 1), 0), PO_subcall((`c2`, -), []))])); - ((``, (Const_name(`ML_FUN`, [Var_children `cl`])), -), - [], - PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(V_box[(((Abs 0), 0), - PO_context_subcall(`name`, - (`cl`, -), - []))]))); - (0, PO_constant `)`)]))] -: print_rule list - -PP_to_ML_rules_fun = - : print_rule_function - -write_strings = - : (((* # string) -> **) -> * -> string list -> void) - -generate_rule = - : (print_tree -> string list) - -write_rule = - : (((* # string) -> **) -> * -> print_tree -> void) - -write_rules = - : (((* # string) -> **) -> * -> print_tree list -> void) - -generate_declarations = - : (print_tree -> string list) - -write_declarations = -- -: (((* # string) -> **) -> * -> print_tree -> void) - -generate_head = - : (string -> string list) - -write_head = - : (((* # string) -> **) -> * -> string -> void) - -generate_tail = - : (string -> string list) - -write_tail = - : (((* # string) -> **) -> * -> string -> void) - -generate_ML = -- -: (((string # string) -> void) -> string -> print_tree -> void) - -- : (((string # string) -> void) -> string -> print_tree -> void) - - -generate_ML = -- -: (((string # string) -> void) -> string -> print_tree -> void) - -Calling Lisp compiler - -File PP_parser/generate compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/pp_lang1_pp`;;'\ - 'loadf `PP_parser/pp_lang2_pp`;;'\ - 'loadf `PP_parser/lex`;;'\ - 'loadf `PP_parser/syntax`;;'\ - 'loadf `PP_parser/convert`;;'\ - 'loadf `PP_parser/generate`;;'\ - 'compilet `PP_parser/PP_to_ML`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#..() : void - -..() : void - -....................() : void - -.......................................................() : void - -.................................................() : void - -...............() : void - - -PP_to_ML = - : (bool -> string -> string -> void) - -Calling Lisp compiler - -File PP_parser/PP_to_ML compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'compilet `PP_hol/hol_trees`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool ..................................................................................................................() : void -#.................................................................................................................................................() : void - # - -New constructors declared: -No_types : type_selection -Hidden_types : type_selection -Useful_types : type_selection -All_types : type_selection - -type_to_print_tree = - : (type -> print_tree) - -term_to_print_tree = - : (bool -> type_selection -> term -> print_tree) - -thm_to_print_tree = -- -: (bool -> bool -> type_selection -> thm -> print_tree) - -Calling Lisp compiler - -File PP_hol/hol_trees compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'compilet `PP_hol/precedence`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - - -type_prec = - : (string -> int) - -min_type_prec = 0 : int - -max_type_prec = 400 : int - -term_prec = - : (string -> int) - -min_term_prec = 0 : int - -max_term_prec = 1700 : int - -Calling Lisp compiler - -File PP_hol/precedence compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'PP_to_ML false `PP_hol/hol_type` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'loadf `PP_hol/precedence`;;'\ - 'compilet `PP_hol/hol_type_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - -......() : void - - -hol_type_rules = -[((`type`, (Const_name(`VAR`, [Patt_child(Var_name(`op`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`op`, -))])); - ((`type`, (Const_name(`OP`, [Patt_child(Var_name(`op`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`op`, -))])); - ((`type`, - (Const_name(`OP`, - [Patt_child(Var_name(`op`, [])); - Patt_child(Var_child `type1`); - Patt_child(Var_child `type2`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_subcall((`type1`, - -), - [(`prec`, - -)])); - (1, - PO_leaf(`op`, -))]))); - ((1, (Abs 3), 0), - PO_subcall((`type2`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`type`, - (Const_name(`OP`, - [Patt_child(Var_name(`op`, [])); - Var_children `types`; - Patt_child(Var_child `type`)])), - -), - [], - PF(HV_box[((0, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HV_box[((0, (Inc 3), 0), - PO_expand(H_box[(0, - PO_subcall((`types`, - -), - [(`prec`, - -)])); - (0, - PO_constant `,`)])); - ((0, (Inc 3), 0), - PO_subcall((`type`, - -), - [(`prec`, - -)]))]))); - (0, PO_constant `)`)]))); - ((0, (Abs 3), 0), PO_leaf(`op`, -))])); - ((`type`, (Const_name(`type`, [Patt_child(Var_child `type`)])), -), - [], - PF(H_box[(0, PO_constant `":`); - (0, PO_subcall((`type`, -), [(`prec`, -)])); - (0, PO_constant `"`)])); - ((`term`, (Var_child `type`), -), - [], - PF(H_box[(0, PO_context_subcall(`type`, (`type`, -), [(`prec`, -)]))]))] -: print_rule list - -hol_type_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File PP_hol/hol_type_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'PP_to_ML false `PP_hol/hol_term` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'loadf `PP_hol/precedence`;;'\ - 'loadf `PP_hol/hol_type_pp`;;'\ - 'compilet `PP_hol/hol_term_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - -......() : void - -..() : void - - -hol_term_rules = -[((`term`, - (Const_name(`CONST`, - [Patt_child(Const_name(`NIL`, [])); Wild_children])), - -), - [], - PF(H_box[(0, PO_constant `[]`)])); - ((`term`, (Const_name(`VAR`, [Patt_child(Var_name(`var`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`var`, -))])); - ((`term`, - (Const_name(`VAR`, - [Patt_child(Var_name(`var`, [])); - Patt_child(Const_name(`type`, - [Patt_child(Var_child `type`)]))])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), PO_leaf(`var`, -)); - ((0, (Abs 0), 0), - PO_format(PF(H_box[(0, PO_constant `:`); - (0, - PO_subcall((`type`, - -), - []))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`CONST`, [Patt_child(Var_name(`const`, []))])), - -), - [], - PF(H_box[(0, PO_leaf(`const`, -))])); - ((`term`, - (Const_name(`CONST`, - [Patt_child(Var_name(`const`, [])); - Patt_child(Const_name(`type`, - [Patt_child(Var_child `type`)]))])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), PO_leaf(`const`, -)); - ((0, (Abs 0), 0), - PO_format(PF(H_box[(0, PO_constant `:`); - (0, - PO_subcall((`type`, - -), - []))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `comps`)])); - Patt_child(Link_child(((Val 1), Default), - [`op`]))])), - Var_child `comp`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`comps`, - -), - [(`prec`, - -)])); - (0, PO_leaf(`op`, -))])); - ((0, (Abs 0), 0), - PO_subcall((`comp`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `args`)])); - Patt_child(Link_child(((Val 1), Default), - [`op`]))])), - Var_child `arg`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_expand(HV_box[((1, (Abs 0), 0), - PO_subcall((`args`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_leaf(`op`, -))])); - ((1, (Abs 0), 0), - PO_subcall((`arg`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `arg1`)])); - Patt_child(Var_child `arg2`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_subcall((`arg1`, - -), - [(`prec`, - -)])); - (1, - PO_leaf(`op`, -))]))); - ((1, (Abs 3), 0), - PO_subcall((`arg2`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, [])); - Wild_children])); - Patt_child(Var_child `arg`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, PO_leaf(`op`, -)); - (0, PO_subcall((`arg`, -), [(`prec`, -)])); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `bvs`); - Patt_child(Link_child(((Val 1), - Default), - [`op`]))]))])), - Var_child `body`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(0, - PO_leaf(`op`, -)); - (0, - PO_format(PF(HV_box[((1, - (Abs 0), - 0), - PO_subcall((`bvs`, - -), - [(`prec`, - -)]))]))); - (0, PO_constant `.`)]))); - ((1, (Abs 3), 0), - PO_subcall((`body`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `bvs`); - Patt_child(Link_child(((Val 1), Default), - []))])), - Var_child `body`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_constant `\`); - (0, - PO_format(PF(HV_box[((1, - (Abs 0), - 0), - PO_subcall((`bvs`, - -), - [(`prec`, - -)]))]))); - (0, PO_constant `.`)]))); - ((1, (Abs 3), 0), - PO_subcall((`body`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`COND`, - [])); - Wild_children])); - Patt_child(Var_child `cond`)])); - Patt_child(Var_child `x`)])); - Patt_child(Var_child `y`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 0), 0), - PO_subcall((`cond`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_constant `=>`)]))); - ((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 0), 0), - PO_subcall((`x`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_constant `|`)]))); - ((1, (Abs 0), 0), - PO_subcall((`y`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term_let`, - (Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `args`); - Patt_child(Link_child(((Default), Default), - []))])), - Wild_child)), - -), - [], - PF(H_box[(1, PO_context_subcall(`term`, (`args`, -), []))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child(Print_link((((Default), - Default), - []), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child (Wild_child)])); - Patt_child (Wild_child)])))])); - Patt_child(Print_label(`argsl`, - Print_loop((Const_name(`ABS`, - [Patt_child (Wild_child); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `letbodyl`)))])), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `bv`); - Patt_child(Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `bvl`); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `body`))]))])); - Patt_child(Print_label(`args`, - Print_loop((Const_name(`ABS`, - [Patt_child (Wild_child); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `letbody`)))]))), - -), - [(`argsl`, -); (`letbodyl`, -)], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_constant `let`); - (1, - PO_subcall((`bv`, - -), - [(`prec`, - -)])); - (1, - PO_context_subcall(`term_let`, - (`args`, - -), - [(`prec`, - -)])); - (1, - PO_constant `=`)]))); - ((1, (Abs 3), 0), - PO_subcall((`letbody`, - -), - [(`prec`, - -)]))]))); - ((1, (Abs 0), 0), - PO_expand(HV_box[((1, (Abs 3), 0), - PO_expand(H_box[(1, - PO_constant `and`); - (1, - PO_subcall((`bvl`, - -), - [(`prec`, - -)])); - (1, - PO_context_subcall(`term_let`, - (`argsl`, - -), - [(`prec`, - -)])); - (1, - PO_constant `=`)])); - ((1, (Abs 3), 0), - PO_subcall((`letbodyl`, - -), - [(`prec`, - -)]))])); - ((1, (Abs 0), 0), - PO_format(PF(H_box[(1, - PO_constant `in`); - (1, - PO_subcall((`body`, - -), - [(`prec`, - -)]))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`CONS`, - [])); - Wild_children])); - Patt_child(Var_child `elems`)])); - Patt_child(Print_link((((Default), Default), - []), - Const_name(`COMB`, - [Wild_children])))])), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`CONS`, - [])); - Wild_children])); - Patt_child(Var_child `elem`)])); - Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`NIL`, - [])); - Wild_children]))]))), - -), - [], - PF(H_box[(0, PO_constant `[`); - (0, - PO_format(PF(HoV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`elems`, - -), - [(`prec`, - -)])); - (0, PO_constant `;`)])); - ((0, (Abs 0), 0), - PO_subcall((`elem`, -), [(`prec`, -)]))]))); - (0, PO_constant `]`)])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Link_child(((Val 1), Default), - [])); - Patt_child(Var_child `rands`)])), - Var_child `rator`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_subcall((`rator`, -), [(`prec`, -)])); - ((1, (Abs 3), 0), - PO_subcall((`rands`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, (Const_name(`term`, [Patt_child(Var_child `term`)])), -), - [], - PF(H_box[(0, PO_constant `"`); - (0, PO_subcall((`term`, -), [(`prec`, -)])); - (0, PO_constant `"`)])); - ((`thm`, (Var_child `term`), -), - [], - PF(H_box[(0, PO_context_subcall(`term`, (`term`, -), [(`prec`, -)]))]))] -: print_rule list - -hol_term_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File PP_hol/hol_term_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'PP_to_ML false `PP_hol/hol_thm` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'loadf `PP_hol/precedence`;;'\ - 'loadf `PP_hol/hol_type_pp`;;'\ - 'loadf `PP_hol/hol_term_pp`;;'\ - 'compilet `PP_hol/hol_thm_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - -......() : void - -..() : void - -..() : void - - -hol_thm_rules = -[((`thm`, (Const_name(`dot`, [])), -), - [], - PF(H_box[(0, PO_constant `.`)])); - ((`thm`, (Const_name(`term`, [Patt_child(Var_child `term`)])), -), - [], - PF(H_box[(0, PO_subcall((`term`, -), []))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`dots`, [Var_children `dots`]))])), - -), - [], - PF(H_box[(1, PO_format(PF(H_box[(0, PO_subcall((`dots`, -), []))]))); - (1, PO_constant `|-`); - (1, PO_subcall((`concl`, -), []))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`hyp`, - [Var_children `hyps`; - Patt_child(Var_child `hyp`)]))])), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), - PO_expand(H_box[(0, PO_subcall((`hyps`, -), [])); - (0, PO_constant `,`)])); - ((1, (Abs 0), 0), PO_subcall((`hyp`, -), [])); - ((1, (Abs 0), 0), - PO_format(PF(H_box[(1, PO_constant `|-`); - (1, PO_subcall((`concl`, -), []))])))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`hyp`, []))])), - -), - [], - PF(H_box[(1, PO_constant `|-`); (1, PO_subcall((`concl`, -), []))]))] -: print_rule list - -hol_thm_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File PP_hol/hol_thm_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'loadf `PP_hol/precedence`;;'\ - 'loadf `PP_hol/hol_type_pp`;;'\ - 'loadf `PP_hol/hol_term_pp`;;'\ - 'loadf `PP_hol/hol_thm_pp`;;'\ - 'compilet `PP_hol/new_printers`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - -......() : void - -..() : void - -..() : void - -..() : void - - -hol_rules_fun = - : print_rule_function - -pp_convert_type = - : (type -> print_tree) - -pp_convert_term = - : (term -> print_tree) - -pp_convert_thm = - : (thm -> print_tree) - -pp_convert_all_thm = - : (thm -> print_tree) - -pp_print_type = - : (type -> void) - -pp_print_term = - : (term -> void) - -pp_print_thm = - : (thm -> void) - -pp_print_all_thm = - : (thm -> void) - -pp_print_theory = - : (string -> void) - -Calling Lisp compiler - -File PP_hol/new_printers compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'loadf `PP_parser/PP_parser`;;'\ - 'loadf `PP_hol/hol_trees`;;'\ - 'loadf `PP_hol/precedence`;;'\ - 'loadf `PP_hol/hol_type_pp`;;'\ - 'loadf `PP_hol/hol_term_pp`;;'\ - 'loadf `PP_hol/hol_thm_pp`;;'\ - 'loadf `PP_hol/new_printers`;;'\ - 'compilet `PP_hol/link_to_hol`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -..................................................................................................................() : void - -#.................................................................................................................................................() : void - -#....() : void - -......() : void - -..() : void - -..() : void - -..() : void - -..........() : void - - -- : (type -> void) - -- : (term -> void) - -- : (thm -> void) - -- : (term -> void) - -Calling Lisp compiler - -File PP_hol/link_to_hol compiled -() : void - -#===> library prettyp rebuilt +* cannot be a var +skipping: * error * in [ * error * ; * error * ; * error * ; * error * ; * error * ; * error * ; * error * . . .parse failed +evaluation failed compile -- PP_parser/pp_lang1_pp +make[4]: *** [Makefile:209: PP_parser/pp_lang1_pp_ml.o] Error 1 make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/trs' echo 'set_flag(`abort_when_fail`,true);;'\ @@ -34615,7 +32014,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34633,7 +32032,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34660,7 +32059,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34704,7 +32103,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34817,7 +32216,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34864,7 +32263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34903,7 +32302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -34977,7 +32376,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35066,7 +32465,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35137,7 +32536,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35207,7 +32606,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35256,7 +32655,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35297,7 +32696,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35338,7 +32737,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35362,7 +32761,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -35380,1068 +32779,10 @@ .......() : void -latex_type_rules = -[((`type`, (Const_name(`VAR`, [Patt_child(Var_name(`op`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`op`, -))])); - ((`type`, (Const_name(`OP`, [Patt_child(Var_name(`op`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`op`, -))])); - ((`type`, - (Const_name(`OP`, - [Patt_child(Var_name(`op`, [])); - Patt_child(Var_child `type1`); - Patt_child(Var_child `type2`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_subcall((`type1`, - -), - [(`prec`, - -)])); - (1, - PO_leaf(`op`, -))]))); - ((1, (Abs 3), 0), - PO_subcall((`type2`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`type`, - (Const_name(`OP`, - [Patt_child(Var_name(`op`, [])); - Var_children `types`; - Patt_child(Var_child `type`)])), - -), - [], - PF(HV_box[((0, (Abs 3), 0), - PO_format(PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HV_box[((0, (Inc 3), 0), - PO_expand(H_box[(0, - PO_subcall((`types`, - -), - [(`prec`, - -)])); - (0, - PO_constant `,`)])); - ((0, (Inc 3), 0), - PO_subcall((`type`, - -), - [(`prec`, - -)]))]))); - (0, PO_constant `)`)]))); - ((0, (Abs 3), 0), PO_leaf(`op`, -))])); - ((`type`, (Const_name(`type`, [Patt_child(Var_child `type`)])), -), - [], - PF(H_box[(0, PO_constant `":`); - (0, PO_subcall((`type`, -), [(`prec`, -)])); - (0, PO_constant `"`)])); - ((`term`, (Var_child `type`), -), - [], - PF(H_box[(0, PO_context_subcall(`type`, (`type`, -), [(`prec`, -)]))]))] -: print_rule list - -latex_type_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File latex_type_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'PP_to_ML false `latex_thm` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'PP_to_ML false `latex_term` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'loadf `filters`;;'\ - 'loadf `hol_trees`;;'\ - 'loadf `precedence`;;'\ - 'loadf `latex_type_pp`;;'\ - 'compilet `latex_term_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#......() : void - -....() : void - -.......() : void - -..() : void - - -latex_term_rules = -[((`term`, - (Const_name(`CONST`, - [Patt_child(Const_name(`NIL`, [])); Wild_children])), - -), - [], - PF(H_box[(0, PO_constant `\NIL `)])); - ((`term`, (Const_name(`VAR`, [Patt_child(Var_name(`var`, []))])), -), - [], - PF(H_box[(0, PO_leaf(`var`, -))])); - ((`term`, - (Const_name(`VAR`, - [Patt_child(Var_name(`var`, [])); - Patt_child(Const_name(`type`, - [Patt_child(Var_child `type`)]))])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), PO_leaf(`var`, -)); - ((0, (Abs 0), 0), - PO_format(PF(H_box[(0, PO_constant `:`); - (0, - PO_subcall((`type`, - -), - []))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`CONST`, [Patt_child(Var_name(`const`, []))])), - -), - [], - PF(H_box[(0, PO_leaf(`const`, -))])); - ((`term`, - (Const_name(`CONST`, - [Patt_child(Var_name(`const`, [])); - Patt_child(Const_name(`type`, - [Patt_child(Var_child `type`)]))])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), PO_leaf(`const`, -)); - ((0, (Abs 0), 0), - PO_format(PF(H_box[(0, PO_constant `:`); - (0, - PO_subcall((`type`, - -), - []))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `comps`)])); - Patt_child(Link_child(((Val 1), Default), - [`op`]))])), - Var_child `comp`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`comps`, - -), - [(`prec`, - -)])); - (0, PO_leaf(`op`, -))])); - ((0, (Abs 0), 0), - PO_subcall((`comp`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `args`)])); - Patt_child(Link_child(((Val 1), Default), - [`op`]))])), - Var_child `arg`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), PO_constant `(`); - ((1, (Abs 0), 0), - PO_expand(HV_box[((1, (Abs 0), 0), - PO_subcall((`args`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_constant `)\:\CONST{EXP}\:(`)])); - ((1, (Abs 0), 0), - PO_subcall((`arg`, -), [(`prec`, -)])); - ((1, (Abs 0), 0), PO_constant `)`)]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `args`)])); - Patt_child(Link_child(((Val 1), Default), - [`op`]))])), - Var_child `arg`)), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_expand(HV_box[((1, (Abs 0), 0), - PO_subcall((`args`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_leaf(`op`, -))])); - ((1, (Abs 0), 0), - PO_subcall((`arg`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `arg1`)])); - Patt_child(Var_child `arg2`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_subcall((`arg1`, - -), - [(`prec`, - -)])); - (1, - PO_leaf(`op`, -))]))); - ((1, (Abs 3), 0), - PO_subcall((`arg2`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, [])); - Wild_children])); - Patt_child(Var_child `arg`)])), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, PO_leaf(`op`, -)); - (0, PO_subcall((`arg`, -), [(`prec`, -)])); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Var_child `pred`)])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `bvs`); - Patt_child(Link_child(((Val 1), - Default), - [`op`; - `pred`]))]))])), - Var_child `body`)), - -), - [(`bv`, -); (`bvs`, -)], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF(H_box[(0, PO_constant `(`)])), - PF_empty))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(0, - PO_leaf(`op`, -)); - (0, - PO_format(PF(H_box[(1, - PO_subcall((`bv`, - -), - [])); - (1, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(1, - PO_expand(H_box[(0, - PO_constant `\,`); - (0, - PO_subcall((`bvs`, - -), - [(`prec`, - -)]))]))]))))]))); - (0, - PO_constant `\RESDOT `); - (0, - PO_format(PF(H_box[(1, - PO_subcall((`pred`, - -), - [(`prec`, - -)]))]))); - (0, - PO_constant `\DOT`)]))); - ((1, (Abs 3), 0), - PO_subcall((`body`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF(H_box[(0, PO_constant `)`)])), - PF_empty)))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Var_name(`op`, - [])); - Wild_children])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `bvs`); - Patt_child(Link_child(((Val 1), - Default), - [`op`]))]))])), - Var_child `body`)), - -), - [(`bv`, -); (`bvs`, -)], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF(H_box[(0, PO_constant `(`)])), - PF_empty))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(0, - PO_leaf(`op`, -)); - (0, - PO_format(PF(H_box[(1, - PO_subcall((`bv`, - -), - [])); - (1, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(1, - PO_expand(H_box[(0, - PO_constant `\,`); - (0, - PO_subcall((`bvs`, - -), - [(`prec`, - -)]))]))]))))]))); - (0, - PO_constant `\DOT`)]))); - ((1, (Abs 3), 0), - PO_subcall((`body`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF(H_box[(0, PO_constant `)`)])), - PF_empty)))])); - ((`term`, - (Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `bvs`); - Patt_child(Print_link((((Default), Default), - []), - Const_name(`ABS`, - [Wild_children])))])), - Const_name(`ABS`, - [Patt_child(Var_child `bv`); - Patt_child(Var_child `body`)]))), - -), - [], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_format(PF(H_box[(1, - PO_constant `\LAMBDA`); - (1, - PO_format(PF(H_box[(1, - PO_expand(H_box[(1, - PO_subcall((`bvs`, - -), - [(`prec`, - -)])); - (1, - PO_constant `\,`)]))]))); - (1, - PO_subcall((`bv`, - -), - [])); - (1, - PO_constant `\DOT`)]))); - ((1, (Abs 3), 0), - PO_subcall((`body`, -), [(`prec`, -)]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`COND`, - [])); - Wild_children])); - Patt_child(Var_child `cond`)])); - Patt_child(Var_child `x`)])); - Patt_child(Var_child `y`)])), - -), - [], - PF(H_box[(0, PO_constant `(`); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 0), 0), - PO_subcall((`cond`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_constant `\Rightarrow `)]))); - ((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 0), 0), - PO_subcall((`x`, - -), - [(`prec`, - -)])); - ((1, (Abs 0), 0), - PO_constant `\mid `)]))); - ((1, (Abs 0), 0), - PO_subcall((`y`, -), [(`prec`, -)]))]))); - (0, PO_constant `)`)])); - ((`term_let`, - (Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `args`); - Patt_child(Link_child(((Default), Default), - []))])), - Wild_child)), - -), - [], - PF(H_box[(1, PO_context_subcall(`term`, (`args`, -), []))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child(Print_link((((Default), - Default), - []), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child (Wild_child)])); - Patt_child (Wild_child)])))])); - Patt_child(Print_label(`argsl`, - Print_loop((Const_name(`ABS`, - [Patt_child (Wild_child); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `letbodyl`)))])), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`LET`, - [])); - Wild_children])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `bv`); - Patt_child(Print_loop((Const_name(`ABS`, - [Patt_child(Var_child `bvl`); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `body`))]))])); - Patt_child(Print_label(`args`, - Print_loop((Const_name(`ABS`, - [Patt_child (Wild_child); - Patt_child(Link_child(((Default), - Default), - []))])), - Var_child `letbody`)))]))), - -), - [(`argsl`, -); (`letbodyl`, -)], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HoV_box[((1, (Abs 0), 0), - PO_format(PF(HV_box[((1, (Abs 1), 0), - PO_format(PF(H_box[(1, - PO_constant `\KEYWD{let}\;`); - (1, - PO_subcall((`bv`, - -), - [(`prec`, - -)])); - (1, - PO_context_subcall(`term_let`, - (`args`, - -), - [(`prec`, - -)])); - (1, - PO_constant `=`)]))); - ((1, (Abs 1), 0), - PO_subcall((`letbody`, - -), - [(`prec`, - -)]))]))); - ((1, (Abs 0), 0), - PO_expand(HV_box[((1, (Abs 1), 0), - PO_expand(HV_box[((1, - (Abs 0), - 0), - PO_constant `\;\KEYWD{and}`); - ((1, - (Abs 0), - 0), - PO_subcall((`bvl`, - -), - [(`prec`, - -)])); - ((1, - (Abs 0), - 0), - PO_context_subcall(`term_let`, - (`argsl`, - -), - [(`prec`, - -)])); - ((1, - (Abs 0), - 0), - PO_constant `=`)])); - ((1, (Abs 1), 0), - PO_subcall((`letbodyl`, - -), - [(`prec`, - -)]))])); - ((1, (Abs 0), 0), - PO_format(PF(V_box[(((Abs 0), 0), - PO_constant `\;\KEYWD{in}`); - (((Abs 0), 0), - PO_format(PF(HV_box[((1, - (Abs 0), - 0), - PO_subcall((`body`, - -), - [(`prec`, - -)]))])))])))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`CONS`, - [])); - Wild_children])); - Patt_child(Var_child `elems`)])); - Patt_child(Print_link((((Default), Default), - []), - Const_name(`COMB`, - [Wild_children])))])), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`CONS`, - [])); - Wild_children])); - Patt_child(Var_child `elem`)])); - Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`NIL`, - [])); - Wild_children]))]))), - -), - [], - PF(H_box[(0, PO_constant `[`); - (0, - PO_format(PF(HoV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`elems`, - -), - [(`prec`, - -)])); - (0, PO_constant `;`)])); - ((0, (Abs 0), 0), - PO_subcall((`elem`, -), [(`prec`, -)]))]))); - (0, PO_constant `]`)])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Link_child(((Val 1), Default), - [])); - Patt_child(Var_child `rands`)])), - Var_child `rator`)), - -), - [(`rands`, -)], - PF(H_box[(0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `(`)])))); - (0, - PO_format(PF(HV_box[((1, (Abs 3), 0), - PO_subcall((`rator`, -), [(`prec`, -)])); - ((1, (Abs 3), 0), - PO_expand(H_box[(0, PO_constant `\,`); - (0, - PO_subcall((`rands`, - -), - [(`prec`, - -)]))]))]))); - (0, - PO_format(PF_branch((-), - (PF_empty), - PF(H_box[(0, PO_constant `)`)]))))])); - ((`term`, (Const_name(`term`, [Patt_child(Var_child `term`)])), -), - [], - PF(H_box[(0, PO_constant `"`); - (0, PO_subcall((`term`, -), [(`prec`, -)])); - (0, PO_constant `"`)])); - ((`thm`, (Var_child `term`), -), - [], - PF(H_box[(0, PO_context_subcall(`term`, (`term`, -), [(`prec`, -)]))]))] -: print_rule list - -latex_term_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File latex_term_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'loadf `filters`;;'\ - 'loadf `hol_trees`;;'\ - 'loadf `precedence`;;'\ - 'loadf `latex_type_pp`;;'\ - 'loadf `latex_term_pp`;;'\ - 'compilet `latex_thm_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#......() : void - -....() : void - -.......() : void - -..() : void - -..() : void - - -latex_thm_rules = -[((`thm`, (Const_name(`dot`, [])), -), - [], - PF(H_box[(0, PO_constant `.`)])); - ((`thm`, (Const_name(`term`, [Patt_child(Var_child `term`)])), -), - [], - PF(H_box[(0, PO_subcall((`term`, -), []))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`dots`, [Var_children `dots`]))])), - -), - [], - PF(H_box[(1, PO_format(PF(H_box[(0, PO_subcall((`dots`, -), []))]))); - (1, PO_constant `\THM`); - (1, PO_subcall((`concl`, -), []))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`hyp`, - [Var_children `hyps`; - Patt_child(Var_child `hyp`)]))])), - -), - [], - PF(HoV_box[((1, (Abs 0), 0), - PO_expand(H_box[(0, PO_subcall((`hyps`, -), [])); - (0, PO_constant `,`)])); - ((1, (Abs 0), 0), PO_subcall((`hyp`, -), [])); - ((1, (Abs 0), 0), - PO_format(PF(H_box[(1, PO_constant `\THM`); - (1, PO_subcall((`concl`, -), []))])))])); - ((`thm`, - (Const_name(`thm`, - [Patt_child(Var_child `concl`); - Patt_child(Const_name(`hyp`, []))])), - -), - [], - PF(H_box[(1, PO_constant `\THM`); (1, PO_subcall((`concl`, -), []))]))] -: print_rule list - -latex_thm_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File latex_thm_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'PP_to_ML false `latex_sets` ``;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'loadf `filters`;;'\ - 'loadf `hol_trees`;;'\ - 'loadf `precedence`;;'\ - 'loadf `latex_type_pp`;;'\ - 'loadf `latex_term_pp`;;'\ - 'loadf `latex_thm_pp`;;'\ - 'compilet `latex_sets_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#......() : void - -....() : void - -.......() : void - -..() : void - -..() : void - -..() : void - - -latex_sets_rules = -[((`term`, - (Const_name(`CONST`, - [Patt_child(Const_name(`EMPTY`, [])); Wild_children])), - -), - [], - PF(H_box[(0, PO_constant `\EMPTYSET `)])); - ((`term`, - (Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`GSPEC`, - [])); - Wild_children])); - Patt_child(Const_name(`ABS`, - [Patt_child(Var_child `var`); - Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child (Wild_child)])); - Patt_child(Var_child `elem`)])); - Patt_child(Var_child `spec`)]))]))])), - -), - [], - PF(H_box[(0, PO_constant `\BEGINSET `); - (0, - PO_format(PF(HV_box[((1, (Abs 1), 0), - PO_subcall((`elem`, -), [(`prec`, -)])); - ((1, (Abs 1), 0), - PO_constant `\SUCHTHAT `); - ((1, (Abs 1), 0), - PO_subcall((`spec`, -), [(`prec`, -)]))]))); - (0, PO_constant `\ENDSET `)])); - ((`term`, - (Print_loop((Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`INSERT`, - [])); - Wild_children])); - Patt_child(Var_child `elems`)])); - Patt_child(Print_link((((Default), Default), - []), - Const_name(`COMB`, - [Wild_children])))])), - Const_name(`COMB`, - [Patt_child(Const_name(`COMB`, - [Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`INSERT`, - [])); - Wild_children])); - Patt_child(Var_child `elem`)])); - Patt_child(Const_name(`CONST`, - [Patt_child(Const_name(`EMPTY`, - [])); - Wild_children]))]))), - -), - [], - PF(H_box[(0, PO_constant `\BEGINSET `); - (0, - PO_format(PF(HV_box[((0, (Abs 0), 0), - PO_expand(H_box[(0, - PO_subcall((`elems`, - -), - [(`prec`, - -)])); - (0, PO_constant `,`)])); - ((0, (Abs 0), 0), - PO_subcall((`elem`, -), [(`prec`, -)]))]))); - (0, PO_constant `\ENDSET `)]))] -: print_rule list - -latex_sets_rules_fun = - : print_rule_function - -Calling Lisp compiler - -File latex_sets_pp compiled -() : void - -#echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_printer`);;'\ - 'loadf(library_pathname() ^ `/prettyp/PP_parser`);;'\ - 'loadf `filters`;;'\ - 'loadf `hol_trees`;;'\ - 'loadf `precedence`;;'\ - 'loadf `latex_sets_pp`;;'\ - 'loadf `latex_thm_pp`;;'\ - 'loadf `latex_term_pp`;;'\ - 'loadf `latex_type_pp`;;'\ - 'compilet `formaters`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#......() : void - -....() : void - -.......() : void - -..() : void - -..() : void - -..() : void - -..() : void - - -output_strings = - : (string -> string list -> void) - -latex_hol_rules_fun = - : print_rule_function - -pp_convert_type = - : (type -> print_tree) - -pp_convert_term = - : (term -> print_tree) - -pp_convert_thm = - : (thm -> print_tree) - -pp_convert_all_thm = - : (thm -> print_tree) - -latex_type = - : (type -> void) - -latex_term = - : (term -> void) - -latex_thm = - : (thm -> void) - -latex_all_thm = - : (thm -> void) - -latex_type_to = - : (string -> type -> void) - -latex_type_add_to = - : (string -> type -> void) - -latex_term_to = - : (string -> term -> void) - -latex_term_add_to = - : (string -> term -> void) - -latex_thm_to = - : (string -> thm -> void) - -latex_thm_add_to = - : (string -> thm -> void) - -latex_all_thm_to = - : (string -> thm -> void) - -latex_all_thm_add_to = - : (string -> thm -> void) - -latex_theory_to = - : (string -> bool -> string -> void) - -latex_thm_tag = `@t ` : string - -latex_thm_end = `` : string - -latex_theorems_to = -- -: (string -> (string -> thm) -> string list -> void) - -latex_all_theorems_to = -- -: (string -> (string -> thm) -> string list -> void) - -latex_theorems_add_to = -- -: (string -> (string -> thm) -> string list -> void) - -Calling Lisp compiler - -File formaters compiled -() : void - -#===>Library latex-hol rebuilt +* cannot be a var +skipping: * error * in [ * error * ; * error * ; * error * ; * error * ; * error * ; * error * ] : print_rule list . . .parse failed +evaluation failed compile -- latex_type_pp +make[4]: *** [Makefile:43: latex_type_pp_ml.o] Error 1 make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/more_arithmetic' rm -f ineq.th @@ -36451,7 +32792,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -36537,7 +32878,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -36652,7 +32993,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -36745,7 +33086,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -36921,7 +33262,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37025,7 +33366,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37320,7 +33661,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37423,7 +33764,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37491,7 +33832,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37553,7 +33894,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37733,7 +34074,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37774,7 +34115,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37804,7 +34145,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -37830,7 +34171,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -38348,7 +34689,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -38885,7 +35226,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -39073,7 +35414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 + HOL88 Version 2.02 (GCL), built on 18/8/26 =============================================================================== #false : bool @@ -39091,10 +35432,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Wed Jul 16 14:31:22 2025 +Tue Aug 18 21:09:48 2026 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Wed Jul 16 14:31:22 2025 +Tue Aug 18 21:09:48 2026 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39112,22 +35453,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 16/7/25 +BASIC-HOL version 2.02 (GCL) created 18/8/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 16/7/25 -=============================================================================== +HOL-LCF version 2.02 (GCL) created 18/8/26 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 16/7/25 + +=============================================================================== + HOL88 Version 2.02 (GCL), built on 18/8/26 +=============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39631,7 +35972,7 @@ ### simple group (level 1) entered at line 168 ({) ### bottom level (see the transcript file for additional information) -Output written on tutorial.dvi (112 pages, 316552 bytes). +Output written on tutorial.dvi (112 pages, 316556 bytes). Transcript written on tutorial.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' make[4]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Tutorial' @@ -41489,7 +37830,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' @@ -46459,7 +42800,7 @@ [663]) (./reference.aux (./title.aux) (./preface.aux) (./ack.aux) (./contents.aux) (./entries.aux) (./theorems.aux) (./index.aux)) ) (see the transcript file for additional information) -Output written on reference.dvi (669 pages, 1155404 bytes). +Output written on reference.dvi (669 pages, 1155408 bytes). Transcript written on reference.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Reference' @@ -52530,7 +48871,7 @@ [1] [2]) (./preface.tex) [3] (./libraries.aux (./title.aux) (./preface.aux)) ) -Output written on libraries.dvi (3 pages, 2284 bytes). +Output written on libraries.dvi (3 pages, 2288 bytes). Transcript written on libraries.log. make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Libraries' make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Manual/Libraries' @@ -52601,7 +48942,7 @@ ===> endpages.dvi created dvips endpages > endpages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.07.16:1433' -> endpages.ps +' TeX output 2026.08.18:2110' -> endpages.ps @@ -52673,7 +49014,7 @@ ===> titlepages.dvi created dvips titlepages > titlepages.ps This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) -' TeX output 2025.07.16:1433' -> titlepages.ps +' TeX output 2026.08.18:2110' -> titlepages.ps @@ -52749,12 +49090,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/803318/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/803318/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/1386708 and its subdirectories -I: Current time: Wed Jul 16 02:33:20 -12 2025 -I: pbuilder-time-stamp: 1752676400 +I: removing directory /srv/workspace/pbuilder/803318 and its subdirectories +I: Current time: Wed Aug 19 11:11:08 +14 2026 +I: pbuilder-time-stamp: 1787087468