Diff of the two buildlogs: -- --- b1/build.log 2024-06-05 03:09:46.946356727 +0000 +++ b2/build.log 2024-06-05 03:17:09.567554437 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Jun 4 15:03:10 -12 2024 -I: pbuilder-time-stamp: 1717556590 +I: Current time: Tue Jul 8 23:32:49 +14 2025 +I: pbuilder-time-stamp: 1751967169 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -28,51 +28,83 @@ dpkg-source: info: applying FTBFS_detection_fix I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/2563216/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/1481339/tmp/hooks/D01_modify_environment starting +debug: Running on infom02-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 Jul 8 09:33 /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/1481339/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/1481339/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' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="21" [3]="1" [4]="release" [5]="x86_64-pc-linux-gnu") + BASH_VERSION='5.2.21(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=amd64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='amd64' + 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='6dce8412fcb04cf59a6398218d3d0727' - 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='2563216' - PS1='# ' - PS2='> ' + INVOCATION_ID=440e2a5012cd4f9ea399c16b19afa05f + 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=1481339 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.qtiDHIYa/pbuilderrc_whpf --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.qtiDHIYa/b1 --logfile b1/build.log hol88_2.02.19940316dfsg-5.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' + 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.qtiDHIYa/pbuilderrc_XkLt --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.qtiDHIYa/b2 --logfile b2/build.log hol88_2.02.19940316dfsg-5.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' I: uname -a - Linux infom01-amd64 6.1.0-21-cloud-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.1.90-1 (2024-05-03) x86_64 GNU/Linux + Linux i-capture-the-hostname 6.7.12+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.7.12-1~bpo12+1 (2024-05-06) x86_64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Jun 4 07:42 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/2563216/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 Jul 7 14:05 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/1481339/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -308,7 +340,7 @@ Get: 194 http://deb.debian.org/debian unstable/main amd64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 195 http://deb.debian.org/debian unstable/main amd64 texlive-base all 2024.20240401-2 [22.7 MB] Get: 196 http://deb.debian.org/debian unstable/main amd64 texlive-latex-base all 2024.20240401-2 [1258 kB] -Fetched 195 MB in 2s (119 MB/s) +Fetched 195 MB in 3s (66.3 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libapparmor1:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19705 files and directories currently installed.) @@ -963,8 +995,8 @@ Setting up tzdata (2024a-4) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Jun 5 03:04:27 UTC 2024. -Universal Time is now: Wed Jun 5 03:04:27 UTC 2024. +Local time is now: Tue Jul 8 09:34:20 UTC 2025. +Universal Time is now: Tue Jul 8 09:34:20 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libasound2-data (1.2.11-1) ... @@ -1165,7 +1197,11 @@ fakeroot is already the newest version (1.34-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes +I: user script /srv/workspace/pbuilder/1481339/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/1481339/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/hol88-2.02.19940316dfsg/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../hol88_2.02.19940316dfsg-5_source.changes dpkg-buildpackage: info: source package hol88 dpkg-buildpackage: info: source version 2.02.19940316dfsg-5 dpkg-buildpackage: info: source distribution unstable @@ -1419,15 +1455,32 @@ 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/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/sets/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/Manual' +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/string/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' +\ + rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ + printf '\\begin{theindex}' >index.tex; \ + printf '\\mbox{}' >>index.tex; \ + printf '\\end{theindex}' >>index.tex +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' +make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/word/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]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/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/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; \ @@ -1435,28 +1488,52 @@ 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/string/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/string/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' +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/sets/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]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/sets/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/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' -make[1]: Entering 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/wellorder/Manual' +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/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/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/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/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/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/prettyp/Manual' +rm -f *.dvi *.aux *.toc *.log *.idx *.ilg +make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/prettyp/Manual' make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' \ rm -f *.dvi *.aux *.toc *.log *.idx *.ilg entries.tex; \ @@ -1464,53 +1541,12 @@ printf '\\mbox{}' >>index.tex; \ printf '\\end{theindex}' >>index.tex make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/numeral/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/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/word/Manual' -rm -f *.dvi *.aux *.toc *.log *.idx *.ilg -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/word/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/reals/Manual' -\ - rm -f *.dvi *.aux *.toc *.log *.idx *.ilg; \ - printf '\\begin{theindex}' >index.tex; \ - printf '\\mbox{}' >>index.tex; \ - printf '\\end{theindex}' >>index.tex -make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/Manual' -make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/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/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/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/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/res_quan/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/res_quan/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]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/latex-hol/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 \ @@ -1558,7 +1594,7 @@ >PATH=$(pwd):$PATH /usr/bin/make all make[1]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Jun 4 15:05:12 -12 2024 +Tue Jul 8 23:35:22 +14 2025 /usr/bin/make hol make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' if [ cl = cl ]; then\ @@ -2796,7 +2832,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 # mem = - : (* -> * list -> bool) @@ -2934,7 +2970,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #.............start address -T 0xa86180 () : void @@ -3093,7 +3129,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #.............start address -T 0xa86180 () : void @@ -3285,7 +3321,7 @@ NIL > -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 # concat = - : (string -> string -> string) @@ -3395,7 +3431,7 @@ start address -T 0xa7c260 ;; Finished loading "lisp/f-ol-net" start address -T 0xa35c50 ;; Finished loading "lisp/mk-hol-lcf" - version 2.02 (GCL) created 4/6/24 + version 2.02 (GCL) created 8/7/25 #...start address -T 0xa88320 () : void @@ -3724,7 +3760,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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 ###########################() : void @@ -3737,7 +3773,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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 ################################################################################################() : void @@ -3882,7 +3918,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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 ############################() : void @@ -3925,7 +3961,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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 ############################Theory ind loaded () : void @@ -3962,7 +3998,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 # map2 = - : (((* # **) -> ***) -> (* list # ** list) -> *** list) @@ -4003,7 +4039,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4405,7 +4441,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4473,7 +4509,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4678,7 +4714,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4802,7 +4838,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4888,7 +4924,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -4981,7 +5017,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5050,7 +5086,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5155,7 +5191,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5390,7 +5426,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5416,7 +5452,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5544,7 +5580,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5592,7 +5628,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5659,7 +5695,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5718,7 +5754,7 @@ 'quit();;'\ | hol-lcf -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5774,7 +5810,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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -5787,7 +5823,7 @@ /tmp/ > -HOL-LCF version 2.02 (GCL) created 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #() : void @@ -5839,7 +5875,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ##########################() : void @@ -5870,7 +5906,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ##############################() : void @@ -5957,7 +5993,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #######################################################################() : void @@ -6110,7 +6146,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ###########################() : void @@ -6145,7 +6181,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #############################() : void @@ -6206,7 +6242,7 @@ #################() : void ## -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ###########################Theory arithmetic loaded () : void @@ -6701,7 +6737,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ##################################() : void @@ -6848,7 +6884,7 @@ |- !x f. ?! fn. (fn[] = x) /\ (!h t. fn(CONS h t) = f(fn t)h t) ## -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #################################Theory list loaded () : void @@ -7187,7 +7223,7 @@ ##() : void ## -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ###############################Theory list loaded () : void @@ -8684,7 +8720,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #############################() : void @@ -9068,7 +9104,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ############################() : void @@ -9366,7 +9402,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ############################() : void @@ -9506,7 +9542,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ############################################() : void @@ -9603,7 +9639,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 ##################################() : void @@ -9633,7 +9669,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -9650,7 +9686,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #Theory num loaded () : void @@ -9669,7 +9705,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -9826,7 +9862,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 # @@ -9864,7 +9900,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 # @@ -9898,7 +9934,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -9983,7 +10019,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -10024,7 +10060,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -10208,7 +10244,7 @@ 'quit();;'\ | basic-hol -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 # define_load_lib_function = - : (string list -> void -> void) @@ -10284,7 +10320,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 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #GCL (GNU Common Lisp) 2.6.14 Fri Jan 13 10:47:56 AM EST 2023 CLtL1 git: Version_2_6_15pre8 Source License: LGPL(gcl,gmp), GPL(unexec,bfd,xgcl) @@ -10297,7 +10333,7 @@ /tmp/ > -BASIC-HOL version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #() : void @@ -10361,11 +10397,11 @@ =======> hol88 version 2.02 (GCL) made make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Jun 4 15:06:26 -12 2024 +Tue Jul 8 23:36:43 +14 2025 /usr/bin/make library make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Jun 4 15:06:26 -12 2024 +Tue Jul 8 23:36:43 +14 2025 (cd /build/reproducible-path/hol88-2.02.19940316dfsg/Library; /usr/bin/make LispType=cl\ Obj=o\ Lisp=gcl\ @@ -10388,7 +10424,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -10472,7 +10508,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -10578,7 +10614,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11328,7 +11364,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11351,7 +11387,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11394,7 +11430,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11430,7 +11466,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11482,7 +11518,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11514,7 +11550,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11552,7 +11588,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11580,7 +11616,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11657,7 +11693,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11679,7 +11715,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11733,7 +11769,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11782,7 +11818,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11933,7 +11969,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -11977,7 +12013,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12052,7 +12088,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12102,7 +12138,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12165,7 +12201,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12218,7 +12254,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12264,7 +12300,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12352,7 +12388,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12390,7 +12426,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12451,7 +12487,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12515,7 +12551,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12541,7 +12577,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12566,7 +12602,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12605,7 +12641,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -12681,7 +12717,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13418,7 +13454,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13441,7 +13477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13484,7 +13520,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13519,7 +13555,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13560,7 +13596,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13623,7 +13659,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13646,7 +13682,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13671,7 +13707,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13698,7 +13734,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -13734,7 +13770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14266,7 +14302,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14289,7 +14325,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14323,7 +14359,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14378,7 +14414,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14469,7 +14505,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14638,7 +14674,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -14906,7 +14942,7 @@ Theorem LESS_EQ_REFL autoloading from theory `arithmetic` ... LESS_EQ_REFL = |- !m. m <= m -Run time: 0.0s +Run time: 0.1s FL_NUM = |- !n. fl(\(m,n). m <= n)n Run time: 0.0s @@ -14941,7 +14977,7 @@ |- !h ms. (!f g x. (!y. (ms y) < (ms x) ==> (f y = g y)) ==> (h f x = h g x)) ==> (?! f. !x. f x = h f x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 259 UNION_FL = |- !P l. fl(Union P)x = (?l. P l /\ fl l x) @@ -15020,7 +15056,7 @@ |- !l a. fl(\(x,y). l(x,y) \/ (y = a) /\ (fl l x \/ (x = a)))x = fl l x \/ (x = a) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 659 ORDINAL_SUC = @@ -15033,7 +15069,7 @@ Intermediate theorems generated: 2338 ORDINAL_UNION = |- !P. (!l. P l ==> ordinal l) ==> ordinal(Union P) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2015 ORDINAL_UNION_LEMMA = @@ -15091,7 +15127,7 @@ (?P. (chain l P /\ C subset P) /\ (!R. chain l R /\ P subset R ==> (R = P)))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1083 () : void @@ -15101,7 +15137,7 @@ File mk_wellorder loaded () : void -Run time: 0.2s +Run time: 0.3s Intermediate theorems generated: 22538 #make[4]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/wellorder' @@ -15110,7 +15146,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -15241,7 +15277,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -15333,7 +15369,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -15412,7 +15448,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 @@ -15422,15 +15458,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 Tue Jun 4 15:06:58 -12 2024 +===> abs_theory rebuilt on Tue Jul 8 23:37:16 +14 2025 Making abs_theory.ml =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -15603,7 +15639,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -16040,7 +16076,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -16436,7 +16472,7 @@ isacut (\w. ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 502 HREAL_ADD_ISACUT = @@ -16550,7 +16586,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -16877,7 +16913,7 @@ TREAL_MUL_LINV = |- !x. ~x treal_eq treal_0 ==> ((treal_inv x) treal_mul x) treal_eq treal_1 -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 3953 TREAL_LT_TOTAL = |- !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x @@ -16902,7 +16938,7 @@ |- !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> treal_0 treal_lt (x treal_mul y) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 866 treal_of_hreal = |- !x. treal_of_hreal x = x hreal_add hreal_1,hreal_1 @@ -17098,7 +17134,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -17458,7 +17494,7 @@ Intermediate theorems generated: 25 REAL_NEG_GE0 = |- !x. (& 0) <= (-- x) = x <= (& 0) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 25 REAL_LT_NEGTOTAL = |- !x. (x = & 0) \/ (& 0) < x \/ (& 0) < (-- x) @@ -17646,7 +17682,7 @@ Intermediate theorems generated: 18 REAL_NEG_INV = |- !x. ~(x = & 0) ==> (--(inv x) = inv(-- x)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 71 REAL_INV_1OVER = |- !x. inv x = (& 1) / x @@ -17710,7 +17746,7 @@ Run time: 0.0s REAL_INJ = |- !m n. (& m = & n) = (m = n) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 57 Definition ADD autoloading from theory `arithmetic` ... @@ -17845,7 +17881,7 @@ Intermediate theorems generated: 25 REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 57 REAL_LE_SUB_LADD = |- !x y z. x <= (y - z) = (x + z) <= y @@ -17912,7 +17948,7 @@ Intermediate theorems generated: 22 REAL_SUB_NEG2 = |- !x y. (-- x) - (-- y) = y - x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 40 REAL_SUB_TRIANGLE = |- !a b c. (a - b) + (b - c) = a - c @@ -17974,7 +18010,7 @@ Intermediate theorems generated: 102 REAL_LE_RDIV = |- !x y z. (& 0) < x /\ (y * x) <= z ==> y <= (z / x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 101 REAL_LT_1 = |- !x y. (& 0) <= x /\ x < y ==> (x / y) < (& 1) @@ -18024,7 +18060,7 @@ Intermediate theorems generated: 165 REAL_POSSQ = |- !x. (& 0) < (x * x) = ~(x = & 0) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 68 REAL_SUMSQ = |- !x y. ((x * x) + (y * y) = & 0) = (x = & 0) /\ (y = & 0) @@ -18090,7 +18126,7 @@ Intermediate theorems generated: 31 ABS_NZ = |- !x. ~(x = & 0) = (& 0) < (abs x) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 139 ABS_INV = |- !x. ~(x = & 0) ==> (abs(inv x) = inv(abs x)) @@ -18131,7 +18167,7 @@ Intermediate theorems generated: 29 ABS_BETWEEN1 = |- !x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 102 ABS_SIGN = |- !x y. (abs(x - y)) < y ==> (& 0) < x @@ -18185,7 +18221,7 @@ Intermediate theorems generated: 108 POW_INV = |- !c. ~(c = & 0) ==> (!n. inv(c pow n) = (inv c) pow n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 126 POW_ABS = |- !c n. (abs c) pow n = abs(c pow n) @@ -18250,7 +18286,7 @@ Intermediate theorems generated: 54 REAL_LT1_POW2 = |- !x. (& 1) < x ==> (& 1) < (x pow 2) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 54 POW_POS_LT = |- !x n. (& 0) < x ==> (& 0) < (x pow (SUC n)) @@ -18321,7 +18357,7 @@ REAL_SUP_UBOUND = |- !P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> (!y. P y ==> y <= (sup P)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 87 SETOK_LE_LT = @@ -18387,7 +18423,7 @@ Intermediate theorems generated: 30 ABS_SUM = |- !f m n. (abs(Sum(m,n)f)) <= (Sum(m,n)(\n'. abs(f n'))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 103 Theorem LESS_EQ_ADD autoloading from theory `arithmetic` ... @@ -18447,7 +18483,7 @@ |- !f N. (!n. n num_ge N ==> (f n = & 0)) ==> (!m n. m num_ge N ==> (Sum(m,n)f = & 0)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 145 SUM_ADD = @@ -18520,7 +18556,7 @@ SUM_OFFSET = |- !f n k. Sum(0,n)(\m. f(m num_add k)) = (Sum(0,n num_add k)f) - (Sum(0,k)f) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 141 SUM_REINDEX = @@ -18583,7 +18619,7 @@ SUM_CANCEL = |- !f n d. Sum(n,d)(\n'. (f(SUC n')) - (f n')) = (f(n num_add d)) - (f n) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 206 () : void @@ -18593,7 +18629,7 @@ File real.ml loaded () : void -Run time: 0.9s +Run time: 0.8s Intermediate theorems generated: 23746 #\ @@ -18603,7 +18639,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -18921,7 +18957,7 @@ |- !m. istopology (\S. !x. S x ==> (?e. (& 0) < e /\ (!y. (dist m(x,y)) < e ==> S y))) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 544 MTOP_OPEN = @@ -18963,7 +18999,7 @@ |- !m x S. limpt(mtop m)x S = (!e. (& 0) < e ==> (?y. ~(x = y) /\ S y /\ (dist m(x,y)) < e)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 298 Theorem REAL_ADD_LINV autoloading from theory `REAL` ... @@ -19097,7 +19133,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -19471,7 +19507,7 @@ MR1_BOUNDED = |- !g f. bounded(mr1,g)f = (?k N. g N N /\ (!n. g n N ==> (abs(f n)) < k)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 331 Theorem REAL_NEG_SUB autoloading from theory `REAL` ... @@ -19481,7 +19517,7 @@ NET_NULL = |- !g x x0. (x --> x0)(mtop mr1,g) = ((\n. (x n) - x0) --> (& 0))(mtop mr1,g) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 151 Theorem LESS_0 autoloading from theory `prim_rec` ... @@ -19832,7 +19868,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -20367,7 +20403,7 @@ Intermediate theorems generated: 39 SEQ_BCONV = |- !f. bounded(mr1,$num_ge)f /\ mono f ==> convergent f -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 209 Theorem LESS_EQ_TRANS autoloading from theory `arithmetic` ... @@ -20768,7 +20804,7 @@ ?d. (& 0) < d /\ (!a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))) ==> (!a b. a <= b ==> P(a,b)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 3396 sums = |- !f s. f sums s = (\n. Sum(0,n)f) --> s @@ -20788,7 +20824,7 @@ Intermediate theorems generated: 16 SUMMABLE_SUM = |- !f. summable f ==> f sums (suminf f) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 30 SUM_UNIQ = |- !f x. f sums x ==> (x = suminf f) @@ -21110,7 +21146,7 @@ Intermediate theorems generated: 683 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 @@ -21126,7 +21162,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -21508,7 +21544,7 @@ Intermediate theorems generated: 2 differentiable = |- !f x. f differentiable x = (?l. (f diffl l)x) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2 DIFF_UNIQ = |- !f l m x. (f diffl l)x /\ (f diffl m)x ==> (l = m) @@ -21656,7 +21692,7 @@ ((f a) <= y /\ y <= (f b)) /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?x. a <= x /\ x <= b /\ (f x = y)) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 2647 Theorem REAL_NEGNEG autoloading from theory `REAL` ... @@ -21856,7 +21892,7 @@ DIFF_CHAIN = |- !f g x. (f diffl l)(g x) /\ (g diffl m)x ==> ((\x. f(g x)) diffl (l * m))x -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 2058 Theorem REAL_DIV_REFL autoloading from theory `REAL` ... @@ -22013,7 +22049,7 @@ |- !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==> (?M. !x. a <= x /\ x <= b ==> (f x) <= M) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1866 Theorem REAL_LE_LT autoloading from theory `REAL` ... @@ -22160,7 +22196,7 @@ |- !a b x. a < x /\ x < b ==> (?d. (& 0) < d /\ (!y. (abs(x - y)) < d ==> a <= y /\ y <= b)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 466 Theorem REAL_MEAN autoloading from theory `REAL` ... @@ -22252,7 +22288,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -22647,7 +22683,7 @@ |- !f x z. summable(\n. (f n) * (x pow n)) /\ (abs z) < (abs x) ==> summable(\n. (abs(f n)) * (z pow n)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 753 Theorem SER_ACONV autoloading from theory `SEQ` ... @@ -22730,7 +22766,7 @@ summable(\n. (diffs c n) * (x pow n)) ==> (\n. (& n) * ((c n) * (x pow (n num_sub 1)))) sums (suminf(\n. (diffs c n) * (x pow n))) -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 180 Theorem SUB_ADD autoloading from theory `arithmetic` ... @@ -23108,13 +23144,13 @@ Intermediate theorems generated: 2494 () : void -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1 File powser.ml loaded () : void -Run time: 0.1s +Run time: 0.2s Intermediate theorems generated: 8507 #\ @@ -23124,7 +23160,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -23651,7 +23687,7 @@ & 0 | ((--(& 1)) pow ((n num_sub 1) DIV 2)) / (&(FACT n)))) = (\n. (EVEN n => ((--(& 1)) pow (n DIV 2)) / (&(FACT n)) | & 0)) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 361 Theorem REAL_NEG_MINUS1 autoloading from theory `REAL` ... @@ -24521,7 +24557,7 @@ Intermediate theorems generated: 134 SIN_NPI = |- !n. sin((& n) * pi) = & 0 -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 137 SIN_POS_PI2 = |- !x. (& 0) < x /\ x < (pi / (& 2)) ==> (& 0) < (sin x) @@ -24543,7 +24579,7 @@ Theorem REAL_LT_SUB_RADD autoloading from theory `REAL` ... REAL_LT_SUB_RADD = |- !x y z. (x - y) < z = x < (z + y) -Run time: 0.0s +Run time: 0.1s Theorem REAL_LT_SUB_LADD autoloading from theory `REAL` ... REAL_LT_SUB_LADD = |- !x y z. x < (y - z) = (x + z) < y @@ -24805,7 +24841,7 @@ TAN_TOTAL = |- !y. ?! x. (--(pi / (& 2))) < x /\ x < (pi / (& 2)) /\ (tan x = y) -Run time: 0.0s +Run time: 0.1s Intermediate theorems generated: 1301 asn = @@ -24894,13 +24930,13 @@ Intermediate theorems generated: 103 () : void -Run time: 0.1s +Run time: 0.0s Intermediate theorems generated: 1 File transc.ml loaded () : void -Run time: 0.6s +Run time: 0.5s Intermediate theorems generated: 30503 #make[5]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library/reals/theories' @@ -24913,7 +24949,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -24935,7 +24971,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25001,7 +25037,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25033,7 +25069,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25142,7 +25178,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25295,7 +25331,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25368,7 +25404,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25448,7 +25484,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25605,7 +25641,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25760,7 +25796,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25977,7 +26013,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -25999,7 +26035,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26018,7 +26054,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26063,7 +26099,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26128,7 +26164,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26178,7 +26214,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26248,7 +26284,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26318,7 +26354,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26354,7 +26390,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26407,7 +26443,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26479,7 +26515,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26558,7 +26594,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26753,7 +26789,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -26790,7 +26826,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -27476,7 +27512,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -27948,7 +27984,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -28212,7 +28248,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -28457,7 +28493,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -28921,7 +28957,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29389,7 +29425,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29445,7 +29481,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29535,7 +29571,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29734,7 +29770,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29766,7 +29802,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -29900,7 +29936,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30203,7 +30239,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30235,7 +30271,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30274,7 +30310,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30306,7 +30342,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30467,7 +30503,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30600,7 +30636,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30789,7 +30825,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30849,7 +30885,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -30974,7 +31010,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -31085,7 +31121,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -31110,7 +31146,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -31138,7 +31174,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -31251,7 +31287,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -31754,7 +31790,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -32002,7 +32038,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -32022,99 +32058,98 @@ PP_to_ML_rules = -[((`name`, (Var_name(`n`, [])), -), [], PF(H_box[(0, PO_leaf(`n`, -))])); +[((`name`, (Var_name(`n`, [])), -), [], PF(H_box[(, PO_leaf(`n`, -))])); ((``, (Const_name(`INTCONST`, [Patt_child(Var_name(`n`, []))])), -), [], - PF(H_box[(0, PO_leaf(`n`, -))])); + PF(H_box[(, PO_leaf(`n`, -))])); ((``, (Const_name(`TOKCONST`, [Patt_child(Var_name(`n`, []))])), -), [], - PF(H_box[(0, PO_constant ```); - (0, PO_leaf(`n`, -)); - (0, PO_constant ```)])); + PF(H_box[(, PO_constant ```); + (, PO_leaf(`n`, -)); + (, PO_constant ```)])); ((``, (Const_name(`VAR`, [Patt_child(Var_name(`n`, []))])), -), [], - PF(H_box[(0, PO_leaf(`n`, -))])); + PF(H_box[(, PO_leaf(`n`, -))])); ((``, (Const_name(`CON`, [Patt_child(Var_name(`n`, []))])), -), [], - PF(H_box[(0, PO_leaf(`n`, -))])); + PF(H_box[(, PO_leaf(`n`, -))])); ((``, (Const_name(`CON0`, [Patt_child(Var_name(`n`, []))])), -), [], - PF(H_box[(0, PO_leaf(`n`, -))])); + PF(H_box[(, 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), + PF(H_box[(, PO_constant `(`); + (, + PO_format(PF(HV_box[((, (Abs 0), ), PO_leaf(`n`, -)); + ((, (Abs 0), ), PO_subcall((`c`, -), []))]))); - (0, PO_constant `)`)])); + (, 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), + PF(H_box[(, PO_constant `(`); + (, + PO_format(PF(HV_box[((, (Abs 1), ), PO_subcall((`c1`, -), [])); - ((1, (Abs 1), 0), + ((, (Abs 1), ), PO_subcall((`c2`, -), []))]))); - (0, PO_constant `)`)])); + (, 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, + PF(H_box[(, PO_constant `(\`); + (, + PO_format(PF(HV_box[((, (Abs 1), ), + PO_format(PF(H_box[(, PO_subcall((`c1`, -), [])); - (0, PO_constant `.`)]))); - ((1, (Abs 1), 0), + (, PO_constant `.`)]))); + ((, (Abs 1), ), PO_subcall((`c2`, -), []))]))); - (0, PO_constant `)`)])); + (, 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, + PF(H_box[(, PO_constant `[`); + (, + PO_format(PF(HoV_box[((, (Abs 0), ), + PO_expand(H_box[(, PO_subcall((`cl`, -), [])); - (0, PO_constant `;`)])); - ((0, (Abs 0), 0), + (, PO_constant `;`)])); + ((, (Abs 0), ), PO_subcall((`c`, -), []))]))); - (0, PO_constant `]`)])); + (, PO_constant `]`)])); ((``, (Const_name(`LIST`, [])), -), [], - PF(H_box[(0, PO_constant `[]`)])); + PF(H_box[(, PO_constant `[]`)])); ((``, (Print_loop((Const_name(`DUPL`, [Patt_child(Var_child `cl`); - Patt_child(Link_child(((Val 1), Default), - []))])), + Patt_child(Link_child(((Val), 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, + PF(H_box[(, PO_constant `(`); + (, + PO_format(PF(HV_box[((, (Abs 0), ), + PO_expand(H_box[(, PO_subcall((`cl`, -), [])); - (0, PO_constant `,`)])); - ((0, (Abs 0), 0), + (, PO_constant `,`)])); + ((, (Abs 0), ), PO_subcall((`c`, -), []))]))); - (0, PO_constant `)`)])); + (, PO_constant `)`)])); ((``, (Const_name(`LETREC`, [Patt_child(Const_name(`DUPL`, @@ -32135,44 +32170,44 @@ 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, + PF(V_box[(((Abs 0), ), + PO_format(PF(HV_box[((, (Inc 1), ), PO_constant `letrec`); + ((, (Inc 1), ), + PO_format(PF(H_box[(, PO_subcall((`var1`, -), [])); - (1, PO_constant `=`)]))); - ((1, (Inc 1), 0), + (, PO_constant `=`)]))); + ((, (Inc 1), ), 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, + (((Abs 0), ), + PO_expand(HV_box[((, (Inc 1), ), PO_constant `and`); + ((, (Inc 1), ), + PO_expand(H_box[(, PO_subcall((`varl`, -), [])); - (1, PO_constant `=`)])); - ((1, (Inc 1), 0), + (, PO_constant `=`)])); + ((, (Inc 1), ), 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`, -), []))])); + PF(HV_box[((, (Inc 1), ), PO_constant `letrec`); + ((, (Inc 1), ), + PO_format(PF(H_box[(, PO_subcall((`c1`, -), [])); + (, PO_constant `=`)]))); + ((, (Inc 1), ), 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), + PF(H_box[(, PO_constant `(`); + (, + PO_format(PF(V_box[(((Abs 0), ), PO_context_subcall(`name`, (`cl`, -), []))]))); - (0, PO_constant `)`)]))] + (, PO_constant `)`)]))] : print_rule list PP_to_ML_rules_fun = - : print_rule_function @@ -32228,7 +32263,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -32270,7 +32305,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -32291,2666 +32326,50 @@ .() : void -() : void - -() : void - -echo 'set_flag(`abort_when_fail`,true);;'\ - 'loadf `PP_printer/PP_printer`;;'\ - 'compilet `PP_parser/pp_lang1_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 +Error: TYPE-ERROR :DATUM (FUN%5726%493 (14 14 20 ...)) :EXPECTED-TYPE NUMBER +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. +TYPE-ERROR :DATUM (FUN%5726%493 (14 14 20 ...)) :EXPECTED-TYPE NUMBER + +Broken at FUN%5202%466. Type :H for Help. + 1 Return to top level. +>> +Error: UNBOUND-VARIABLE :NAME PP_TO_ML +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +UNBOUND-VARIABLE :NAME PP_TO_ML + +Broken at FUN%5202%466. + 1 (abort) Return to debug level 1. + 2 Return to top level. +>>> +Error: UNBOUND-VARIABLE :NAME FALSE +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +UNBOUND-VARIABLE :NAME FALSE + +Broken at FUN%5202%466. + 1 (abort) Return to debug level 2. + 2 Return to debug level 1. + 3 Return to top level. +>>>> +PP_PARSER/PP_LANG2 +>>>> +Error: ERROR "Caught fatal error [memory may be damaged]" +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +ERROR "Caught fatal error [memory may be damaged]" + +Broken at FUN%5202%466. + 1 (abort) Return to debug level 3. + 2 Return to debug level 2. + 3 Return to debug level 1. + 4 Return to top level. +>>>>>make[4]: *** [Makefile:151: PP_parser/pp_lang1_pp.ml] Error 255 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);;'\ @@ -34959,7 +32378,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -34977,7 +32396,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35004,7 +32423,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35048,7 +32467,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35161,7 +32580,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35208,7 +32627,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35247,7 +32666,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35321,7 +32740,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35410,7 +32829,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35481,7 +32900,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35551,7 +32970,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35600,7 +33019,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35641,7 +33060,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35682,7 +33101,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -35693,1099 +33112,39 @@ #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`;;'\ - 'compilet `latex_type_pp`;;'\ - 'quit();;' | /build/reproducible-path/hol88-2.02.19940316dfsg/hol - - -=============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 -=============================================================================== - -#false : bool - -Updating help search path -....................................................................................................................() : void - -#Updating help search path -...................................................................................................................................................() : void - -#......() : void - -....() : void - -.......() : 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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 4/6/24 -=============================================================================== - -#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 +# +Error: TYPE-ERROR :DATUM (FUN%5726%493 (14 21 22 ...)) :EXPECTED-TYPE NUMBER +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +TYPE-ERROR :DATUM (FUN%5726%493 (14 21 22 ...)) :EXPECTED-TYPE NUMBER + +Broken at FUN%5202%466. Type :H for Help. + 1 Return to top level. +>> +Error: UNBOUND-VARIABLE :NAME QUIT +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +UNBOUND-VARIABLE :NAME QUIT + +Broken at FUN%5202%466. + 1 (abort) Return to debug level 1. + 2 Return to top level. +>>> +NIL +>>> +Error: ERROR "Caught fatal error [memory may be damaged]" +Fast links are on: do (si::use-fast-links nil) for debugging +Signalled by FUN%5202%466. + +ERROR "Caught fatal error [memory may be damaged]" + +Broken at FUN%5202%466. + 1 (abort) Return to debug level 2. + 2 Return to debug level 1. + 3 Return to top level. +>>>>make[4]: *** [Makefile:36: latex_type_pp.ml] Error 255 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 @@ -36795,7 +33154,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -36881,7 +33240,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -36996,7 +33355,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37089,7 +33448,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37265,7 +33624,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37369,7 +33728,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37664,7 +34023,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37767,7 +34126,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37835,7 +34194,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -37897,7 +34256,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -38077,7 +34436,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -38118,7 +34477,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -38148,7 +34507,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -38174,7 +34533,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -38692,7 +35051,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -39229,7 +35588,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -39417,7 +35776,7 @@ =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #false : bool @@ -39435,10 +35794,10 @@ =======> library rebuilt make[3]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg/Library' date -Tue Jun 4 15:08:42 -12 2024 +Tue Jul 8 23:38:46 +14 2025 make[2]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' date -Tue Jun 4 15:08:42 -12 2024 +Tue Jul 8 23:38:46 +14 2025 make permissions make[2]: Entering directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find $(ls -1 | grep -v debian) \ @@ -39456,13 +35815,13 @@ 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 4/6/24 +HOL-LCF version 2.02 (GCL) created 8/7/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void # -HOL-LCF version 2.02 (GCL) created 4/6/24 +BASIC-HOL version 2.02 (GCL) created 8/7/25 #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) () : void @@ -39470,7 +35829,7 @@ # =============================================================================== - HOL88 Version 2.02 (GCL), built on 4/6/24 + HOL88 Version 2.02 (GCL), built on 8/7/25 =============================================================================== #HOL installed (`/usr/share/hol88-2.02.19940316dfsg`) @@ -48856,7 +45215,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 2024.06.04:1509' -> endpages.ps +' TeX output 2025.07.08:2339' -> endpages.ps @@ -48920,7 +45279,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 2024.06.04:1509' -> titlepages.ps +' TeX output 2025.07.08:2339' -> titlepages.ps @@ -48999,8 +45358,8 @@ dh_gencontrol: warning: Compatibility levels before 10 are deprecated (level 9 in use) dh_md5sums dh_builddeb -dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. dpkg-deb: building package 'hol88-library' in '../hol88-library_2.02.19940316dfsg-5_amd64.deb'. +dpkg-deb: building package 'hol88' in '../hol88_2.02.19940316dfsg-5_amd64.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' find lisp -name "*.l" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install find ml -type f -name "*ml" | awk '{a=$1;sub("/[^/]*$","",a);printf("%s usr/share/hol88-2.02.19940316dfsg/%s\n",$1,a);}' >>debian/hol88-source.install @@ -49076,12 +45435,12 @@ dh_md5sums dh_builddeb dpkg-deb: building package 'hol88-source' in '../hol88-source_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-help' in '../hol88-help_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. -dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-contrib-source' in '../hol88-contrib-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-help' in '../hol88-library-help_2.02.19940316dfsg-5_all.deb'. dpkg-deb: building package 'hol88-doc' in '../hol88-doc_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-library-source' in '../hol88-library-source_2.02.19940316dfsg-5_all.deb'. +dpkg-deb: building package 'hol88-contrib-help' in '../hol88-contrib-help_2.02.19940316dfsg-5_all.deb'. make[1]: Leaving directory '/build/reproducible-path/hol88-2.02.19940316dfsg' dpkg-genbuildinfo --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.buildinfo dpkg-genchanges --build=binary -O../hol88_2.02.19940316dfsg-5_amd64.changes @@ -49090,12 +45449,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/1481339/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/1481339/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/2563216 and its subdirectories -I: Current time: Tue Jun 4 15:09:46 -12 2024 -I: pbuilder-time-stamp: 1717556986 +I: removing directory /srv/workspace/pbuilder/1481339 and its subdirectories +I: Current time: Tue Jul 8 23:40:08 +14 2025 +I: pbuilder-time-stamp: 1751967608