I: pbuilder: network access will be disabled during build I: Current time: Thu Dec 25 15:51:43 +14 2025 I: pbuilder-time-stamp: 1766627503 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration W: --override-config is not set; not updating apt.conf Read the manpage for details. I: mounting /proc filesystem I: mounting /sys filesystem I: creating /{dev,run}/shm I: mounting /dev/pts filesystem I: redirecting /dev/ptmx to /dev/pts/ptmx I: policy-rc.d already exists I: Copying source file I: copying [ott_0.33+ds-4.dsc] I: copying [./ott_0.33+ds.orig.tar.xz] I: copying [./ott_0.33+ds-4.debian.tar.xz] I: Extracting source gpgv: Signature made Sat Aug 3 12:40:31 2024 gpgv: using RSA key 6DE24E97ECA886CC56E6250E21B8EEF1B1893081 gpgv: issuer "glondu@debian.org" gpgv: Can't check signature: No public key dpkg-source: warning: cannot verify inline signature for ./ott_0.33+ds-4.dsc: no acceptable signature found dpkg-source: info: extracting ott in ott-0.33+ds dpkg-source: info: unpacking ott_0.33+ds.orig.tar.xz dpkg-source: info: unpacking ott_0.33+ds-4.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying typos.patch dpkg-source: info: applying coq_8.19.patch I: Not using root during the build. I: Installing the build-deps I: user script /srv/workspace/pbuilder/288991/tmp/hooks/D01_modify_environment starting debug: Running on codethink03-arm64. 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 Dec 25 01:51 /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/288991/tmp/hooks/D01_modify_environment finished I: user script /srv/workspace/pbuilder/288991/tmp/hooks/D02_print_environment starting I: set 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]="32" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") BASH_VERSION='5.2.32(1)-release' BUILDDIR=/build/reproducible-path BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' BUILDUSERNAME=pbuilder2 BUILD_ARCH=arm64 DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' DIRSTACK=() DISTRIBUTION=unstable EUID=0 FUNCNAME=([0]="Echo" [1]="main") GROUPS=() HOME=/root HOSTNAME=i-capture-the-hostname HOSTTYPE=aarch64 HOST_ARCH=arm64 IFS=' ' INVOCATION_ID=2c3c4d604c9d4ab59bd655632f8a3a34 LANG=C LANGUAGE=nl_BE:nl LC_ALL=C MACHTYPE=aarch64-unknown-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=288991 PS4='+ ' 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.Ah3GwisQ/pbuilderrc_MVeE --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.Ah3GwisQ/b2 --logfile b2/build.log ott_0.33+ds-4.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' http_proxy=http://192.168.101.4:3128 I: uname -a Linux i-capture-the-hostname 6.1.0-27-cloud-arm64 #1 SMP Debian 6.1.115-1 (2024-11-01) aarch64 GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Aug 4 2024 /bin -> usr/bin I: user script /srv/workspace/pbuilder/288991/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy Version: 0.invalid.0 Architecture: arm64 Maintainer: Debian Pbuilder Team Description: Dummy package to satisfy dependencies with aptitude - created by pbuilder This package was created automatically by pbuilder to satisfy the build-dependencies of the package being currently built. Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, help2man, hevea, libcoq-core-ocaml-dev, libcoq-stdlib, libocamlgraph-ocaml-dev, pandoc dpkg-deb: building package 'pbuilder-satisfydepends-dummy' in '/tmp/satisfydepends-aptitude/pbuilder-satisfydepends-dummy.deb'. Selecting previously unselected package pbuilder-satisfydepends-dummy. (Reading database ... 20084 files and directories currently installed.) Preparing to unpack .../pbuilder-satisfydepends-dummy.deb ... Unpacking pbuilder-satisfydepends-dummy (0.invalid.0) ... dpkg: pbuilder-satisfydepends-dummy: dependency problems, but configuring anyway as you requested: pbuilder-satisfydepends-dummy depends on coq; however: Package coq is not installed. pbuilder-satisfydepends-dummy depends on debhelper-compat (= 13); however: Package debhelper-compat is not installed. pbuilder-satisfydepends-dummy depends on dh-coq; however: Package dh-coq is not installed. pbuilder-satisfydepends-dummy depends on dh-ocaml; however: Package dh-ocaml is not installed. pbuilder-satisfydepends-dummy depends on help2man; however: Package help2man is not installed. pbuilder-satisfydepends-dummy depends on hevea; however: Package hevea is not installed. pbuilder-satisfydepends-dummy depends on libcoq-core-ocaml-dev; however: Package libcoq-core-ocaml-dev is not installed. pbuilder-satisfydepends-dummy depends on libcoq-stdlib; however: Package libcoq-stdlib is not installed. pbuilder-satisfydepends-dummy depends on libocamlgraph-ocaml-dev; however: Package libocamlgraph-ocaml-dev is not installed. pbuilder-satisfydepends-dummy depends on pandoc; however: Package pandoc is not installed. Setting up pbuilder-satisfydepends-dummy (0.invalid.0) ... Reading package lists... Building dependency tree... Reading state information... Initializing package states... Writing extended state information... Building tag database... pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0) pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0) The following NEW packages will be installed: autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} coq{a} debhelper{a} dh-autoreconf{a} dh-coq{a} dh-ocaml{a} dh-strip-nondeterminism{a} dwz{a} file{a} fontconfig-config{a} fonts-urw-base35{a} gettext{a} gettext-base{a} ghostscript{a} groff-base{a} help2man{a} hevea{a} hicolor-icon-theme{a} imagemagick{a} imagemagick-7-common{a} imagemagick-7.q16{a} intltool-debian{a} libarchive-zip-perl{a} libavahi-client3{a} libavahi-common-data{a} libavahi-common3{a} libbrotli1{a} libcairo2{a} libcom-err2{a} libcompiler-libs-ocaml-dev{a} libconfig-tiny-perl{a} libcoq-core-ocaml{a} libcoq-core-ocaml-dev{a} libcoq-stdlib{a} libcups2t64{a} libdav1d7{a} libdbus-1-3{a} libde265-0{a} libdebhelper-perl{a} libdeflate0{a} libelf1t64{a} libexpat1{a} libfftw3-double3{a} libfile-stripnondeterminism-perl{a} libfindlib-ocaml{a} libfindlib-ocaml-dev{a} libfontconfig1{a} libfontenc1{a} libfreetype6{a} libglib2.0-0t64{a} libgmp-dev{a} libgmp3-dev{a} libgmpxx4ldbl{a} libgraphite2-3{a} libgs-common{a} libgs10{a} libgs10-common{a} libgssapi-krb5-2{a} libharfbuzz0b{a} libheif-plugin-dav1d{a} libheif-plugin-libde265{a} libheif1{a} libice6{a} libicu72{a} libidn12{a} libijs-0.35{a} libjbig0{a} libjbig2dec0{a} libjpeg62-turbo{a} libk5crypto3{a} libkeyutils1{a} libkpathsea6{a} libkrb5-3{a} libkrb5support0{a} liblcms2-2{a} liblerc4{a} liblocale-gettext-perl{a} liblqr-1-0{a} libltdl7{a} liblua5.4-0{a} libmagic-mgc{a} libmagic1t64{a} libmagickcore-7.q16-10{a} libmagickwand-7.q16-10{a} libmpfi0{a} libncurses-dev{a} libncurses6{a} libnetpbm11t64{a} libnsl2{a} libnuma1{a} libocamlgraph-ocaml-dev{a} libopenjp2-7{a} libpaper-utils{a} libpaper1{a} libpipeline1{a} libpixman-1-0{a} libpng16-16t64{a} libpotrace0{a} libptexenc1{a} libpython3-stdlib{a} libpython3.12-minimal{a} libpython3.12-stdlib{a} libraw23t64{a} libreadline8t64{a} libsharpyuv0{a} libsm6{a} libstdlib-ocaml{a} libstdlib-ocaml-dev{a} libsynctex2{a} libteckit0{a} libtexlua53-5{a} libtiff6{a} libtirpc-common{a} libtirpc3t64{a} libtool{a} libuchardet0{a} libwebp7{a} libwebpdemux2{a} libwebpmux3{a} libx11-6{a} libx11-data{a} libxau6{a} libxaw7{a} libxcb-render0{a} libxcb-shm0{a} libxcb1{a} libxdmcp6{a} libxext6{a} libxi6{a} libxml2{a} libxmu6{a} libxpm4{a} libxrender1{a} libxt6t64{a} libyaml-0-2{a} libzarith-ocaml{a} libzarith-ocaml-dev{a} libzstd-dev{a} libzzip-0-13t64{a} m4{a} man-db{a} media-types{a} netbase{a} netpbm{a} ocaml{a} ocaml-base{a} ocaml-findlib{a} ocaml-interp{a} pandoc{a} pandoc-data{a} po-debconf{a} poppler-data{a} python3{a} python3-minimal{a} python3.12{a} python3.12-minimal{a} readline-common{a} sensible-utils{a} t1utils{a} tex-common{a} texlive-base{a} texlive-binaries{a} tzdata{a} ucf{a} x11-common{a} xdg-utils{a} xfonts-encodings{a} xfonts-utils{a} The following packages are RECOMMENDED but will NOT be installed: ca-certificates curl dbus dvisvgm fonts-droid-fallback krb5-locales ledit libarchive-cpio-perl libfile-mimeinfo-perl libglib2.0-data libgpm2 libheif-plugin-aomenc libheif-plugin-x265 libltdl-dev libmagickcore-7.q16-10-extra libmail-sendmail-perl libnet-dbus-perl libx11-protocol-perl lmodern lynx ocaml-man rlfe rlwrap shared-mime-info wget x11-utils x11-xserver-utils xdg-user-dirs 0 packages upgraded, 172 newly installed, 0 to remove and 0 not upgraded. Need to get 415 MB of archives. After unpacking 1506 MB will be used. Writing extended state information... Get: 1 http://deb.debian.org/debian unstable/main arm64 liblocale-gettext-perl arm64 1.07-7+b1 [15.2 kB] Get: 2 http://deb.debian.org/debian unstable/main arm64 libfftw3-double3 arm64 3.3.10-2 [337 kB] Get: 3 http://deb.debian.org/debian unstable/main arm64 libexpat1 arm64 2.6.4-1 [90.7 kB] Get: 4 http://deb.debian.org/debian unstable/main arm64 libbrotli1 arm64 1.1.0-2+b6 [297 kB] Get: 5 http://deb.debian.org/debian unstable/main arm64 libpng16-16t64 arm64 1.6.44-2 [273 kB] Get: 6 http://deb.debian.org/debian unstable/main arm64 libfreetype6 arm64 2.13.3+dfsg-1 [422 kB] Get: 7 http://deb.debian.org/debian unstable/main arm64 libfontenc1 arm64 1:1.1.8-1+b1 [22.5 kB] Get: 8 http://deb.debian.org/debian unstable/main arm64 x11-common all 1:7.7+23.1 [216 kB] Get: 9 http://deb.debian.org/debian unstable/main arm64 xfonts-encodings all 1:1.0.4-2.2 [577 kB] Get: 10 http://deb.debian.org/debian unstable/main arm64 xfonts-utils arm64 1:7.7+7 [89.3 kB] Get: 11 http://deb.debian.org/debian unstable/main arm64 fonts-urw-base35 all 20200910-8 [10.8 MB] Get: 12 http://deb.debian.org/debian unstable/main arm64 fontconfig-config arm64 2.15.0-1.1+b1 [318 kB] Get: 13 http://deb.debian.org/debian unstable/main arm64 libfontconfig1 arm64 2.15.0-1.1+b1 [387 kB] Get: 14 http://deb.debian.org/debian unstable/main arm64 libsharpyuv0 arm64 1.4.0-0.1+b1 [112 kB] Get: 15 http://deb.debian.org/debian unstable/main arm64 libdav1d7 arm64 1.5.0-1+b1 [248 kB] Get: 16 http://deb.debian.org/debian unstable/main arm64 libheif-plugin-dav1d arm64 1.19.3-1 [11.2 kB] Get: 17 http://deb.debian.org/debian unstable/main arm64 libde265-0 arm64 1.0.15-1+b2 [153 kB] Get: 18 http://deb.debian.org/debian unstable/main arm64 libheif-plugin-libde265 arm64 1.19.3-1 [14.9 kB] Get: 19 http://deb.debian.org/debian unstable/main arm64 libheif1 arm64 1.19.3-1 [419 kB] Get: 20 http://deb.debian.org/debian unstable/main arm64 libjbig0 arm64 2.1-6.1+b2 [30.4 kB] Get: 21 http://deb.debian.org/debian unstable/main arm64 libjpeg62-turbo arm64 1:2.1.5-3+b1 [173 kB] Get: 22 http://deb.debian.org/debian unstable/main arm64 liblcms2-2 arm64 2.16-2 [151 kB] Get: 23 http://deb.debian.org/debian unstable/main arm64 libglib2.0-0t64 arm64 2.82.2-3 [1411 kB] Get: 24 http://deb.debian.org/debian unstable/main arm64 liblqr-1-0 arm64 0.4.2-2.1+b2 [27.0 kB] Get: 25 http://deb.debian.org/debian unstable/main arm64 libltdl7 arm64 2.4.7-8 [392 kB] Get: 26 http://deb.debian.org/debian unstable/main arm64 libopenjp2-7 arm64 2.5.0-2+b4 [185 kB] Get: 27 http://deb.debian.org/debian unstable/main arm64 libraw23t64 arm64 0.21.3-1+b1 [370 kB] Get: 28 http://deb.debian.org/debian unstable/main arm64 libdeflate0 arm64 1.22-1 [42.2 kB] Get: 29 http://deb.debian.org/debian unstable/main arm64 liblerc4 arm64 4.0.0+ds-5 [146 kB] Get: 30 http://deb.debian.org/debian unstable/main arm64 libwebp7 arm64 1.4.0-0.1+b1 [268 kB] Get: 31 http://deb.debian.org/debian unstable/main arm64 libtiff6 arm64 4.5.1+git230720-5 [309 kB] Get: 32 http://deb.debian.org/debian unstable/main arm64 libwebpdemux2 arm64 1.4.0-0.1+b1 [110 kB] Get: 33 http://deb.debian.org/debian unstable/main arm64 libwebpmux3 arm64 1.4.0-0.1+b1 [122 kB] Get: 34 http://deb.debian.org/debian unstable/main arm64 libxau6 arm64 1:1.0.11-1 [20.6 kB] Get: 35 http://deb.debian.org/debian unstable/main arm64 libxdmcp6 arm64 1:1.1.5-1 [27.8 kB] Get: 36 http://deb.debian.org/debian unstable/main arm64 libxcb1 arm64 1.17.0-2+b1 [143 kB] Get: 37 http://deb.debian.org/debian unstable/main arm64 libx11-data all 2:1.8.10-2 [337 kB] Get: 38 http://deb.debian.org/debian unstable/main arm64 libx11-6 arm64 2:1.8.10-2 [789 kB] Get: 39 http://deb.debian.org/debian unstable/main arm64 libxext6 arm64 2:1.3.4-1+b2 [49.3 kB] Get: 40 http://deb.debian.org/debian unstable/main arm64 libicu72 arm64 72.1-5+b1 [9239 kB] Get: 41 http://deb.debian.org/debian unstable/main arm64 libxml2 arm64 2.12.7+dfsg+really2.9.14-0.2+b1 [630 kB] Get: 42 http://deb.debian.org/debian unstable/main arm64 imagemagick-7-common all 8:7.1.1.39+dfsg1-2 [66.7 kB] Get: 43 http://deb.debian.org/debian unstable/main arm64 libmagickcore-7.q16-10 arm64 8:7.1.1.39+dfsg1-2 [1648 kB] Get: 44 http://deb.debian.org/debian unstable/main arm64 libmagickwand-7.q16-10 arm64 8:7.1.1.39+dfsg1-2 [267 kB] Get: 45 http://deb.debian.org/debian unstable/main arm64 poppler-data all 0.4.12-1 [1601 kB] Get: 46 http://deb.debian.org/debian unstable/main arm64 libpython3.12-minimal arm64 3.12.7-3 [808 kB] Get: 47 http://deb.debian.org/debian unstable/main arm64 python3.12-minimal arm64 3.12.7-3 [1940 kB] Get: 48 http://deb.debian.org/debian unstable/main arm64 python3-minimal arm64 3.12.7-1 [26.8 kB] Get: 49 http://deb.debian.org/debian unstable/main arm64 media-types all 10.1.0 [26.9 kB] Get: 50 http://deb.debian.org/debian unstable/main arm64 netbase all 6.4 [12.8 kB] Get: 51 http://deb.debian.org/debian unstable/main arm64 tzdata all 2024b-3 [255 kB] Get: 52 http://deb.debian.org/debian unstable/main arm64 libkrb5support0 arm64 1.21.3-3 [32.1 kB] Get: 53 http://deb.debian.org/debian unstable/main arm64 libcom-err2 arm64 1.47.1-1+b1 [23.1 kB] Get: 54 http://deb.debian.org/debian unstable/main arm64 libk5crypto3 arm64 1.21.3-3 [80.8 kB] Get: 55 http://deb.debian.org/debian unstable/main arm64 libkeyutils1 arm64 1.6.3-4 [9352 B] Get: 56 http://deb.debian.org/debian unstable/main arm64 libkrb5-3 arm64 1.21.3-3 [310 kB] Get: 57 http://deb.debian.org/debian unstable/main arm64 libgssapi-krb5-2 arm64 1.21.3-3 [126 kB] Get: 58 http://deb.debian.org/debian unstable/main arm64 libtirpc-common all 1.3.4+ds-1.3 [10.9 kB] Get: 59 http://deb.debian.org/debian unstable/main arm64 libtirpc3t64 arm64 1.3.4+ds-1.3+b1 [78.7 kB] Get: 60 http://deb.debian.org/debian unstable/main arm64 libnsl2 arm64 1.3.0-3+b3 [37.9 kB] Get: 61 http://deb.debian.org/debian unstable/main arm64 readline-common all 8.2-5 [69.3 kB] Get: 62 http://deb.debian.org/debian unstable/main arm64 libreadline8t64 arm64 8.2-5 [159 kB] Get: 63 http://deb.debian.org/debian unstable/main arm64 libpython3.12-stdlib arm64 3.12.7-3 [1902 kB] Get: 64 http://deb.debian.org/debian unstable/main arm64 python3.12 arm64 3.12.7-3 [671 kB] Get: 65 http://deb.debian.org/debian unstable/main arm64 libpython3-stdlib arm64 3.12.7-1 [9708 B] Get: 66 http://deb.debian.org/debian unstable/main arm64 python3 arm64 3.12.7-1 [27.8 kB] Get: 67 http://deb.debian.org/debian unstable/main arm64 sensible-utils all 0.0.24 [24.8 kB] Get: 68 http://deb.debian.org/debian unstable/main arm64 libmagic-mgc arm64 1:5.45-3+b1 [314 kB] Get: 69 http://deb.debian.org/debian unstable/main arm64 libmagic1t64 arm64 1:5.45-3+b1 [102 kB] Get: 70 http://deb.debian.org/debian unstable/main arm64 file arm64 1:5.45-3+b1 [43.4 kB] Get: 71 http://deb.debian.org/debian unstable/main arm64 gettext-base arm64 0.22.5-2 [198 kB] Get: 72 http://deb.debian.org/debian unstable/main arm64 libuchardet0 arm64 0.0.8-1+b2 [69.2 kB] Get: 73 http://deb.debian.org/debian unstable/main arm64 groff-base arm64 1.23.0-5 [1129 kB] Get: 74 http://deb.debian.org/debian unstable/main arm64 bsdextrautils arm64 2.40.2-11 [91.2 kB] Get: 75 http://deb.debian.org/debian unstable/main arm64 libpipeline1 arm64 1.5.8-1 [40.2 kB] Get: 76 http://deb.debian.org/debian unstable/main arm64 man-db arm64 2.13.0-1 [1404 kB] Get: 77 http://deb.debian.org/debian unstable/main arm64 ucf all 3.0043+nmu1 [55.2 kB] Get: 78 http://deb.debian.org/debian unstable/main arm64 m4 arm64 1.4.19-4 [277 kB] Get: 79 http://deb.debian.org/debian unstable/main arm64 autoconf all 2.72-3 [493 kB] Get: 80 http://deb.debian.org/debian unstable/main arm64 autotools-dev all 20220109.1 [51.6 kB] Get: 81 http://deb.debian.org/debian unstable/main arm64 automake all 1:1.16.5-1.3 [823 kB] Get: 82 http://deb.debian.org/debian unstable/main arm64 autopoint all 0.22.5-2 [723 kB] Get: 83 http://deb.debian.org/debian unstable/main arm64 libcoq-stdlib arm64 8.20.0+dfsg-1 [23.5 MB] Get: 84 http://deb.debian.org/debian unstable/main arm64 libstdlib-ocaml arm64 5.2.0-3 [571 kB] Get: 85 http://deb.debian.org/debian unstable/main arm64 ocaml-base arm64 5.2.0-3 [443 kB] Get: 86 http://deb.debian.org/debian unstable/main arm64 libfindlib-ocaml arm64 1.9.6-3 [181 kB] Get: 87 http://deb.debian.org/debian unstable/main arm64 libzarith-ocaml arm64 1.14-1 [115 kB] Get: 88 http://deb.debian.org/debian unstable/main arm64 libcoq-core-ocaml arm64 8.20.0+dfsg-1 [26.3 MB] Get: 89 http://deb.debian.org/debian unstable/main arm64 libstdlib-ocaml-dev arm64 5.2.0-3 [11.0 MB] Get: 90 http://deb.debian.org/debian unstable/main arm64 libcompiler-libs-ocaml-dev arm64 5.2.0-3 [47.1 MB] Get: 91 http://deb.debian.org/debian unstable/main arm64 ocaml-interp arm64 5.2.0-3 [6851 kB] Get: 92 http://deb.debian.org/debian unstable/main arm64 libncurses6 arm64 6.5-2+b1 [96.1 kB] Get: 93 http://deb.debian.org/debian unstable/main arm64 libncurses-dev arm64 6.5-2+b1 [338 kB] Get: 94 http://deb.debian.org/debian unstable/main arm64 libzstd-dev arm64 1.5.6+dfsg-1+b1 [329 kB] Get: 95 http://deb.debian.org/debian unstable/main arm64 ocaml arm64 5.2.0-3 [20.1 MB] Get: 96 http://deb.debian.org/debian unstable/main arm64 ocaml-findlib arm64 1.9.6-3 [621 kB] Get: 97 http://deb.debian.org/debian unstable/main arm64 coq arm64 8.20.0+dfsg-1 [80.9 MB] Get: 98 http://deb.debian.org/debian unstable/main arm64 libdebhelper-perl all 13.20 [89.7 kB] Get: 99 http://deb.debian.org/debian unstable/main arm64 libtool all 2.4.7-8 [517 kB] Get: 100 http://deb.debian.org/debian unstable/main arm64 dh-autoreconf all 20 [17.1 kB] Get: 101 http://deb.debian.org/debian unstable/main arm64 libarchive-zip-perl all 1.68-1 [104 kB] Get: 102 http://deb.debian.org/debian unstable/main arm64 libfile-stripnondeterminism-perl all 1.14.0-1 [19.5 kB] Get: 103 http://deb.debian.org/debian unstable/main arm64 dh-strip-nondeterminism all 1.14.0-1 [8448 B] Get: 104 http://deb.debian.org/debian unstable/main arm64 libelf1t64 arm64 0.192-4 [189 kB] Get: 105 http://deb.debian.org/debian unstable/main arm64 dwz arm64 0.15-1+b1 [102 kB] Get: 106 http://deb.debian.org/debian unstable/main arm64 gettext arm64 0.22.5-2 [1532 kB] Get: 107 http://deb.debian.org/debian unstable/main arm64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get: 108 http://deb.debian.org/debian unstable/main arm64 po-debconf all 1.0.21+nmu1 [248 kB] Get: 109 http://deb.debian.org/debian unstable/main arm64 debhelper all 13.20 [915 kB] Get: 110 http://deb.debian.org/debian unstable/main arm64 dh-coq all 0.11 [6776 B] Get: 111 http://deb.debian.org/debian unstable/main arm64 libconfig-tiny-perl all 2.30-1 [18.9 kB] Get: 112 http://deb.debian.org/debian unstable/main arm64 dh-ocaml all 2.4 [62.9 kB] Get: 113 http://deb.debian.org/debian unstable/main arm64 libgs-common all 10.04.0~dfsg-1 [148 kB] Get: 114 http://deb.debian.org/debian unstable/main arm64 libgs10-common all 10.04.0~dfsg-1 [474 kB] Get: 115 http://deb.debian.org/debian unstable/main arm64 libavahi-common-data arm64 0.8-13+b3 [112 kB] Get: 116 http://deb.debian.org/debian unstable/main arm64 libavahi-common3 arm64 0.8-13+b3 [42.3 kB] Get: 117 http://deb.debian.org/debian unstable/main arm64 libdbus-1-3 arm64 1.14.10-6 [196 kB] Get: 118 http://deb.debian.org/debian unstable/main arm64 libavahi-client3 arm64 0.8-13+b3 [46.0 kB] Get: 119 http://deb.debian.org/debian unstable/main arm64 libcups2t64 arm64 2.4.10-2 [235 kB] Get: 120 http://deb.debian.org/debian unstable/main arm64 libidn12 arm64 1.42-2+b1 [80.2 kB] Get: 121 http://deb.debian.org/debian unstable/main arm64 libijs-0.35 arm64 0.35-15.1+b2 [14.9 kB] Get: 122 http://deb.debian.org/debian unstable/main arm64 libjbig2dec0 arm64 0.20-1+b3 [60.1 kB] Get: 123 http://deb.debian.org/debian unstable/main arm64 libpaper1 arm64 1.1.29+b2 [13.0 kB] Get: 124 http://deb.debian.org/debian unstable/main arm64 libice6 arm64 2:1.1.1-1 [62.1 kB] Get: 125 http://deb.debian.org/debian unstable/main arm64 libsm6 arm64 2:1.2.4-1 [34.2 kB] Get: 126 http://deb.debian.org/debian unstable/main arm64 libxt6t64 arm64 1:1.2.1-1.2+b1 [173 kB] Get: 127 http://deb.debian.org/debian unstable/main arm64 libgs10 arm64 10.04.0~dfsg-1 [2351 kB] Get: 128 http://deb.debian.org/debian unstable/main arm64 ghostscript arm64 10.04.0~dfsg-1 [50.5 kB] Get: 129 http://deb.debian.org/debian unstable/main arm64 help2man arm64 1.49.3+b1 [198 kB] Get: 130 http://deb.debian.org/debian unstable/main arm64 libnetpbm11t64 arm64 2:11.08.01-1+b1 [177 kB] Get: 131 http://deb.debian.org/debian unstable/main arm64 netpbm arm64 2:11.08.01-1+b1 [2047 kB] Get: 132 http://deb.debian.org/debian unstable/main arm64 tex-common all 6.18 [32.5 kB] Get: 133 http://deb.debian.org/debian unstable/main arm64 libpaper-utils arm64 1.1.29+b2 [9128 B] Get: 134 http://deb.debian.org/debian unstable/main arm64 libkpathsea6 arm64 2024.20240313.70630+ds-5 [153 kB] Get: 135 http://deb.debian.org/debian unstable/main arm64 libptexenc1 arm64 2024.20240313.70630+ds-5 [47.9 kB] Get: 136 http://deb.debian.org/debian unstable/main arm64 libsynctex2 arm64 2024.20240313.70630+ds-5 [60.3 kB] Get: 137 http://deb.debian.org/debian unstable/main arm64 libtexlua53-5 arm64 2024.20240313.70630+ds-5 [106 kB] Get: 138 http://deb.debian.org/debian unstable/main arm64 t1utils arm64 1.41-4+b1 [57.6 kB] Get: 139 http://deb.debian.org/debian unstable/main arm64 libpixman-1-0 arm64 0.44.0-3 [168 kB] Get: 140 http://deb.debian.org/debian unstable/main arm64 libxcb-render0 arm64 1.17.0-2+b1 [115 kB] Get: 141 http://deb.debian.org/debian unstable/main arm64 libxcb-shm0 arm64 1.17.0-2+b1 [105 kB] Get: 142 http://deb.debian.org/debian unstable/main arm64 libxrender1 arm64 1:0.9.10-1.1+b2 [27.2 kB] Get: 143 http://deb.debian.org/debian unstable/main arm64 libcairo2 arm64 1.18.2-2 [483 kB] Get: 144 http://deb.debian.org/debian unstable/main arm64 libgraphite2-3 arm64 1.3.14-2+b1 [70.4 kB] Get: 145 http://deb.debian.org/debian unstable/main arm64 libharfbuzz0b arm64 10.0.1-1 [441 kB] Get: 146 http://deb.debian.org/debian unstable/main arm64 libmpfi0 arm64 1.5.4+ds-4 [34.5 kB] Get: 147 http://deb.debian.org/debian unstable/main arm64 libpotrace0 arm64 1.16-2+b2 [23.4 kB] Get: 148 http://deb.debian.org/debian unstable/main arm64 libteckit0 arm64 2.5.12+ds1-1+b1 [303 kB] Get: 149 http://deb.debian.org/debian unstable/main arm64 libxmu6 arm64 2:1.1.3-3+b3 [55.6 kB] Get: 150 http://deb.debian.org/debian unstable/main arm64 libxpm4 arm64 1:3.5.17-1+b2 [53.2 kB] Get: 151 http://deb.debian.org/debian unstable/main arm64 libxaw7 arm64 2:1.0.16-1 [195 kB] Get: 152 http://deb.debian.org/debian unstable/main arm64 libxi6 arm64 2:1.8.2-1 [77.8 kB] Get: 153 http://deb.debian.org/debian unstable/main arm64 libzzip-0-13t64 arm64 0.13.72+dfsg.1-1.3 [56.6 kB] Get: 154 http://deb.debian.org/debian unstable/main arm64 texlive-binaries arm64 2024.20240313.70630+ds-5 [7358 kB] Get: 155 http://deb.debian.org/debian unstable/main arm64 xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 156 http://deb.debian.org/debian unstable/main arm64 texlive-base all 2024.20241115-1 [22.7 MB] Get: 157 http://deb.debian.org/debian unstable/main arm64 hicolor-icon-theme all 0.18-1 [12.0 kB] Get: 158 http://deb.debian.org/debian unstable/main arm64 imagemagick-7.q16 arm64 8:7.1.1.39+dfsg1-2 [726 kB] Get: 159 http://deb.debian.org/debian unstable/main arm64 imagemagick arm64 8:7.1.1.39+dfsg1-2 [19.8 kB] Get: 160 http://deb.debian.org/debian unstable/main arm64 hevea arm64 2.36-2+b2 [2316 kB] Get: 161 http://deb.debian.org/debian unstable/main arm64 libfindlib-ocaml-dev arm64 1.9.6-3 [155 kB] Get: 162 http://deb.debian.org/debian unstable/main arm64 libgmpxx4ldbl arm64 2:6.3.0+dfsg-2+b2 [329 kB] Get: 163 http://deb.debian.org/debian unstable/main arm64 libgmp-dev arm64 2:6.3.0+dfsg-2+b2 [621 kB] Get: 164 http://deb.debian.org/debian unstable/main arm64 libgmp3-dev arm64 2:6.3.0+dfsg-2+b2 [322 kB] Get: 165 http://deb.debian.org/debian unstable/main arm64 libzarith-ocaml-dev arm64 1.14-1 [141 kB] Get: 166 http://deb.debian.org/debian unstable/main arm64 libcoq-core-ocaml-dev arm64 8.20.0+dfsg-1 [69.2 MB] Get: 167 http://deb.debian.org/debian unstable/main arm64 liblua5.4-0 arm64 5.4.6-3+b2 [133 kB] Get: 168 http://deb.debian.org/debian unstable/main arm64 libnuma1 arm64 2.0.18-1+b1 [21.8 kB] Get: 169 http://deb.debian.org/debian unstable/main arm64 libocamlgraph-ocaml-dev arm64 2.1.0-3+b1 [6808 kB] Get: 170 http://deb.debian.org/debian unstable/main arm64 libyaml-0-2 arm64 0.2.5-1+b2 [49.3 kB] Get: 171 http://deb.debian.org/debian unstable/main arm64 pandoc-data all 3.1.11.1-3 [459 kB] Get: 172 http://deb.debian.org/debian unstable/main arm64 pandoc arm64 3.1.11.1+ds-2 [26.2 MB] Fetched 415 MB in 2s (236 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package liblocale-gettext-perl. (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 ... 20084 files and directories currently installed.) Preparing to unpack .../00-liblocale-gettext-perl_1.07-7+b1_arm64.deb ... Unpacking liblocale-gettext-perl (1.07-7+b1) ... Selecting previously unselected package libfftw3-double3:arm64. Preparing to unpack .../01-libfftw3-double3_3.3.10-2_arm64.deb ... Unpacking libfftw3-double3:arm64 (3.3.10-2) ... Selecting previously unselected package libexpat1:arm64. Preparing to unpack .../02-libexpat1_2.6.4-1_arm64.deb ... Unpacking libexpat1:arm64 (2.6.4-1) ... Selecting previously unselected package libbrotli1:arm64. Preparing to unpack .../03-libbrotli1_1.1.0-2+b6_arm64.deb ... Unpacking libbrotli1:arm64 (1.1.0-2+b6) ... Selecting previously unselected package libpng16-16t64:arm64. Preparing to unpack .../04-libpng16-16t64_1.6.44-2_arm64.deb ... Unpacking libpng16-16t64:arm64 (1.6.44-2) ... Selecting previously unselected package libfreetype6:arm64. Preparing to unpack .../05-libfreetype6_2.13.3+dfsg-1_arm64.deb ... Unpacking libfreetype6:arm64 (2.13.3+dfsg-1) ... Selecting previously unselected package libfontenc1:arm64. Preparing to unpack .../06-libfontenc1_1%3a1.1.8-1+b1_arm64.deb ... Unpacking libfontenc1:arm64 (1:1.1.8-1+b1) ... Selecting previously unselected package x11-common. Preparing to unpack .../07-x11-common_1%3a7.7+23.1_all.deb ... Unpacking x11-common (1:7.7+23.1) ... Selecting previously unselected package xfonts-encodings. Preparing to unpack .../08-xfonts-encodings_1%3a1.0.4-2.2_all.deb ... Unpacking xfonts-encodings (1:1.0.4-2.2) ... Selecting previously unselected package xfonts-utils. Preparing to unpack .../09-xfonts-utils_1%3a7.7+7_arm64.deb ... Unpacking xfonts-utils (1:7.7+7) ... Selecting previously unselected package fonts-urw-base35. Preparing to unpack .../10-fonts-urw-base35_20200910-8_all.deb ... Unpacking fonts-urw-base35 (20200910-8) ... Selecting previously unselected package fontconfig-config. Preparing to unpack .../11-fontconfig-config_2.15.0-1.1+b1_arm64.deb ... Unpacking fontconfig-config (2.15.0-1.1+b1) ... Selecting previously unselected package libfontconfig1:arm64. Preparing to unpack .../12-libfontconfig1_2.15.0-1.1+b1_arm64.deb ... Unpacking libfontconfig1:arm64 (2.15.0-1.1+b1) ... Selecting previously unselected package libsharpyuv0:arm64. Preparing to unpack .../13-libsharpyuv0_1.4.0-0.1+b1_arm64.deb ... Unpacking libsharpyuv0:arm64 (1.4.0-0.1+b1) ... Selecting previously unselected package libdav1d7:arm64. Preparing to unpack .../14-libdav1d7_1.5.0-1+b1_arm64.deb ... Unpacking libdav1d7:arm64 (1.5.0-1+b1) ... Selecting previously unselected package libheif-plugin-dav1d:arm64. Preparing to unpack .../15-libheif-plugin-dav1d_1.19.3-1_arm64.deb ... Unpacking libheif-plugin-dav1d:arm64 (1.19.3-1) ... Selecting previously unselected package libde265-0:arm64. Preparing to unpack .../16-libde265-0_1.0.15-1+b2_arm64.deb ... Unpacking libde265-0:arm64 (1.0.15-1+b2) ... Selecting previously unselected package libheif-plugin-libde265:arm64. Preparing to unpack .../17-libheif-plugin-libde265_1.19.3-1_arm64.deb ... Unpacking libheif-plugin-libde265:arm64 (1.19.3-1) ... Selecting previously unselected package libheif1:arm64. Preparing to unpack .../18-libheif1_1.19.3-1_arm64.deb ... Unpacking libheif1:arm64 (1.19.3-1) ... Selecting previously unselected package libjbig0:arm64. Preparing to unpack .../19-libjbig0_2.1-6.1+b2_arm64.deb ... Unpacking libjbig0:arm64 (2.1-6.1+b2) ... Selecting previously unselected package libjpeg62-turbo:arm64. Preparing to unpack .../20-libjpeg62-turbo_1%3a2.1.5-3+b1_arm64.deb ... Unpacking libjpeg62-turbo:arm64 (1:2.1.5-3+b1) ... Selecting previously unselected package liblcms2-2:arm64. Preparing to unpack .../21-liblcms2-2_2.16-2_arm64.deb ... Unpacking liblcms2-2:arm64 (2.16-2) ... Selecting previously unselected package libglib2.0-0t64:arm64. Preparing to unpack .../22-libglib2.0-0t64_2.82.2-3_arm64.deb ... Unpacking libglib2.0-0t64:arm64 (2.82.2-3) ... Selecting previously unselected package liblqr-1-0:arm64. Preparing to unpack .../23-liblqr-1-0_0.4.2-2.1+b2_arm64.deb ... Unpacking liblqr-1-0:arm64 (0.4.2-2.1+b2) ... Selecting previously unselected package libltdl7:arm64. Preparing to unpack .../24-libltdl7_2.4.7-8_arm64.deb ... Unpacking libltdl7:arm64 (2.4.7-8) ... Selecting previously unselected package libopenjp2-7:arm64. Preparing to unpack .../25-libopenjp2-7_2.5.0-2+b4_arm64.deb ... Unpacking libopenjp2-7:arm64 (2.5.0-2+b4) ... Selecting previously unselected package libraw23t64:arm64. Preparing to unpack .../26-libraw23t64_0.21.3-1+b1_arm64.deb ... Unpacking libraw23t64:arm64 (0.21.3-1+b1) ... Selecting previously unselected package libdeflate0:arm64. Preparing to unpack .../27-libdeflate0_1.22-1_arm64.deb ... Unpacking libdeflate0:arm64 (1.22-1) ... Selecting previously unselected package liblerc4:arm64. Preparing to unpack .../28-liblerc4_4.0.0+ds-5_arm64.deb ... Unpacking liblerc4:arm64 (4.0.0+ds-5) ... Selecting previously unselected package libwebp7:arm64. Preparing to unpack .../29-libwebp7_1.4.0-0.1+b1_arm64.deb ... Unpacking libwebp7:arm64 (1.4.0-0.1+b1) ... Selecting previously unselected package libtiff6:arm64. Preparing to unpack .../30-libtiff6_4.5.1+git230720-5_arm64.deb ... Unpacking libtiff6:arm64 (4.5.1+git230720-5) ... Selecting previously unselected package libwebpdemux2:arm64. Preparing to unpack .../31-libwebpdemux2_1.4.0-0.1+b1_arm64.deb ... Unpacking libwebpdemux2:arm64 (1.4.0-0.1+b1) ... Selecting previously unselected package libwebpmux3:arm64. Preparing to unpack .../32-libwebpmux3_1.4.0-0.1+b1_arm64.deb ... Unpacking libwebpmux3:arm64 (1.4.0-0.1+b1) ... Selecting previously unselected package libxau6:arm64. Preparing to unpack .../33-libxau6_1%3a1.0.11-1_arm64.deb ... Unpacking libxau6:arm64 (1:1.0.11-1) ... Selecting previously unselected package libxdmcp6:arm64. Preparing to unpack .../34-libxdmcp6_1%3a1.1.5-1_arm64.deb ... Unpacking libxdmcp6:arm64 (1:1.1.5-1) ... Selecting previously unselected package libxcb1:arm64. Preparing to unpack .../35-libxcb1_1.17.0-2+b1_arm64.deb ... Unpacking libxcb1:arm64 (1.17.0-2+b1) ... Selecting previously unselected package libx11-data. Preparing to unpack .../36-libx11-data_2%3a1.8.10-2_all.deb ... Unpacking libx11-data (2:1.8.10-2) ... Selecting previously unselected package libx11-6:arm64. Preparing to unpack .../37-libx11-6_2%3a1.8.10-2_arm64.deb ... Unpacking libx11-6:arm64 (2:1.8.10-2) ... Selecting previously unselected package libxext6:arm64. Preparing to unpack .../38-libxext6_2%3a1.3.4-1+b2_arm64.deb ... Unpacking libxext6:arm64 (2:1.3.4-1+b2) ... Selecting previously unselected package libicu72:arm64. Preparing to unpack .../39-libicu72_72.1-5+b1_arm64.deb ... Unpacking libicu72:arm64 (72.1-5+b1) ... Selecting previously unselected package libxml2:arm64. Preparing to unpack .../40-libxml2_2.12.7+dfsg+really2.9.14-0.2+b1_arm64.deb ... Unpacking libxml2:arm64 (2.12.7+dfsg+really2.9.14-0.2+b1) ... Selecting previously unselected package imagemagick-7-common. Preparing to unpack .../41-imagemagick-7-common_8%3a7.1.1.39+dfsg1-2_all.deb ... Unpacking imagemagick-7-common (8:7.1.1.39+dfsg1-2) ... Selecting previously unselected package libmagickcore-7.q16-10:arm64. Preparing to unpack .../42-libmagickcore-7.q16-10_8%3a7.1.1.39+dfsg1-2_arm64.deb ... Unpacking libmagickcore-7.q16-10:arm64 (8:7.1.1.39+dfsg1-2) ... Selecting previously unselected package libmagickwand-7.q16-10:arm64. Preparing to unpack .../43-libmagickwand-7.q16-10_8%3a7.1.1.39+dfsg1-2_arm64.deb ... Unpacking libmagickwand-7.q16-10:arm64 (8:7.1.1.39+dfsg1-2) ... Selecting previously unselected package poppler-data. Preparing to unpack .../44-poppler-data_0.4.12-1_all.deb ... Unpacking poppler-data (0.4.12-1) ... Selecting previously unselected package libpython3.12-minimal:arm64. Preparing to unpack .../45-libpython3.12-minimal_3.12.7-3_arm64.deb ... Unpacking libpython3.12-minimal:arm64 (3.12.7-3) ... Selecting previously unselected package python3.12-minimal. Preparing to unpack .../46-python3.12-minimal_3.12.7-3_arm64.deb ... Unpacking python3.12-minimal (3.12.7-3) ... Setting up libpython3.12-minimal:arm64 (3.12.7-3) ... Setting up libexpat1:arm64 (2.6.4-1) ... Setting up python3.12-minimal (3.12.7-3) ... Selecting previously unselected package python3-minimal. (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 ... 22178 files and directories currently installed.) Preparing to unpack .../00-python3-minimal_3.12.7-1_arm64.deb ... Unpacking python3-minimal (3.12.7-1) ... Selecting previously unselected package media-types. Preparing to unpack .../01-media-types_10.1.0_all.deb ... Unpacking media-types (10.1.0) ... Selecting previously unselected package netbase. Preparing to unpack .../02-netbase_6.4_all.deb ... Unpacking netbase (6.4) ... Selecting previously unselected package tzdata. Preparing to unpack .../03-tzdata_2024b-3_all.deb ... Unpacking tzdata (2024b-3) ... Selecting previously unselected package libkrb5support0:arm64. Preparing to unpack .../04-libkrb5support0_1.21.3-3_arm64.deb ... Unpacking libkrb5support0:arm64 (1.21.3-3) ... Selecting previously unselected package libcom-err2:arm64. Preparing to unpack .../05-libcom-err2_1.47.1-1+b1_arm64.deb ... Unpacking libcom-err2:arm64 (1.47.1-1+b1) ... Selecting previously unselected package libk5crypto3:arm64. Preparing to unpack .../06-libk5crypto3_1.21.3-3_arm64.deb ... Unpacking libk5crypto3:arm64 (1.21.3-3) ... Selecting previously unselected package libkeyutils1:arm64. Preparing to unpack .../07-libkeyutils1_1.6.3-4_arm64.deb ... Unpacking libkeyutils1:arm64 (1.6.3-4) ... Selecting previously unselected package libkrb5-3:arm64. Preparing to unpack .../08-libkrb5-3_1.21.3-3_arm64.deb ... Unpacking libkrb5-3:arm64 (1.21.3-3) ... Selecting previously unselected package libgssapi-krb5-2:arm64. Preparing to unpack .../09-libgssapi-krb5-2_1.21.3-3_arm64.deb ... Unpacking libgssapi-krb5-2:arm64 (1.21.3-3) ... Selecting previously unselected package libtirpc-common. Preparing to unpack .../10-libtirpc-common_1.3.4+ds-1.3_all.deb ... Unpacking libtirpc-common (1.3.4+ds-1.3) ... Selecting previously unselected package libtirpc3t64:arm64. Preparing to unpack .../11-libtirpc3t64_1.3.4+ds-1.3+b1_arm64.deb ... Adding 'diversion of /lib/aarch64-linux-gnu/libtirpc.so.3 to /lib/aarch64-linux-gnu/libtirpc.so.3.usr-is-merged by libtirpc3t64' Adding 'diversion of /lib/aarch64-linux-gnu/libtirpc.so.3.0.0 to /lib/aarch64-linux-gnu/libtirpc.so.3.0.0.usr-is-merged by libtirpc3t64' Unpacking libtirpc3t64:arm64 (1.3.4+ds-1.3+b1) ... Selecting previously unselected package libnsl2:arm64. Preparing to unpack .../12-libnsl2_1.3.0-3+b3_arm64.deb ... Unpacking libnsl2:arm64 (1.3.0-3+b3) ... Selecting previously unselected package readline-common. Preparing to unpack .../13-readline-common_8.2-5_all.deb ... Unpacking readline-common (8.2-5) ... Selecting previously unselected package libreadline8t64:arm64. Preparing to unpack .../14-libreadline8t64_8.2-5_arm64.deb ... Adding 'diversion of /lib/aarch64-linux-gnu/libhistory.so.8 to /lib/aarch64-linux-gnu/libhistory.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/aarch64-linux-gnu/libhistory.so.8.2 to /lib/aarch64-linux-gnu/libhistory.so.8.2.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/aarch64-linux-gnu/libreadline.so.8 to /lib/aarch64-linux-gnu/libreadline.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/aarch64-linux-gnu/libreadline.so.8.2 to /lib/aarch64-linux-gnu/libreadline.so.8.2.usr-is-merged by libreadline8t64' Unpacking libreadline8t64:arm64 (8.2-5) ... Selecting previously unselected package libpython3.12-stdlib:arm64. Preparing to unpack .../15-libpython3.12-stdlib_3.12.7-3_arm64.deb ... Unpacking libpython3.12-stdlib:arm64 (3.12.7-3) ... Selecting previously unselected package python3.12. Preparing to unpack .../16-python3.12_3.12.7-3_arm64.deb ... Unpacking python3.12 (3.12.7-3) ... Selecting previously unselected package libpython3-stdlib:arm64. Preparing to unpack .../17-libpython3-stdlib_3.12.7-1_arm64.deb ... Unpacking libpython3-stdlib:arm64 (3.12.7-1) ... Setting up python3-minimal (3.12.7-1) ... Selecting previously unselected package python3. (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 ... 23240 files and directories currently installed.) Preparing to unpack .../000-python3_3.12.7-1_arm64.deb ... Unpacking python3 (3.12.7-1) ... Selecting previously unselected package sensible-utils. Preparing to unpack .../001-sensible-utils_0.0.24_all.deb ... Unpacking sensible-utils (0.0.24) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../002-libmagic-mgc_1%3a5.45-3+b1_arm64.deb ... Unpacking libmagic-mgc (1:5.45-3+b1) ... Selecting previously unselected package libmagic1t64:arm64. Preparing to unpack .../003-libmagic1t64_1%3a5.45-3+b1_arm64.deb ... Unpacking libmagic1t64:arm64 (1:5.45-3+b1) ... Selecting previously unselected package file. Preparing to unpack .../004-file_1%3a5.45-3+b1_arm64.deb ... Unpacking file (1:5.45-3+b1) ... Selecting previously unselected package gettext-base. Preparing to unpack .../005-gettext-base_0.22.5-2_arm64.deb ... Unpacking gettext-base (0.22.5-2) ... Selecting previously unselected package libuchardet0:arm64. Preparing to unpack .../006-libuchardet0_0.0.8-1+b2_arm64.deb ... Unpacking libuchardet0:arm64 (0.0.8-1+b2) ... Selecting previously unselected package groff-base. Preparing to unpack .../007-groff-base_1.23.0-5_arm64.deb ... Unpacking groff-base (1.23.0-5) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../008-bsdextrautils_2.40.2-11_arm64.deb ... Unpacking bsdextrautils (2.40.2-11) ... Selecting previously unselected package libpipeline1:arm64. Preparing to unpack .../009-libpipeline1_1.5.8-1_arm64.deb ... Unpacking libpipeline1:arm64 (1.5.8-1) ... Selecting previously unselected package man-db. Preparing to unpack .../010-man-db_2.13.0-1_arm64.deb ... Unpacking man-db (2.13.0-1) ... Selecting previously unselected package ucf. Preparing to unpack .../011-ucf_3.0043+nmu1_all.deb ... Moving old data out of the way Unpacking ucf (3.0043+nmu1) ... Selecting previously unselected package m4. Preparing to unpack .../012-m4_1.4.19-4_arm64.deb ... Unpacking m4 (1.4.19-4) ... Selecting previously unselected package autoconf. Preparing to unpack .../013-autoconf_2.72-3_all.deb ... Unpacking autoconf (2.72-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../014-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../015-automake_1%3a1.16.5-1.3_all.deb ... Unpacking automake (1:1.16.5-1.3) ... Selecting previously unselected package autopoint. Preparing to unpack .../016-autopoint_0.22.5-2_all.deb ... Unpacking autopoint (0.22.5-2) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../017-libcoq-stdlib_8.20.0+dfsg-1_arm64.deb ... Unpacking libcoq-stdlib (8.20.0+dfsg-1) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../018-libstdlib-ocaml_5.2.0-3_arm64.deb ... Unpacking libstdlib-ocaml (5.2.0-3) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../019-ocaml-base_5.2.0-3_arm64.deb ... Unpacking ocaml-base (5.2.0-3) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../020-libfindlib-ocaml_1.9.6-3_arm64.deb ... Unpacking libfindlib-ocaml (1.9.6-3) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../021-libzarith-ocaml_1.14-1_arm64.deb ... Unpacking libzarith-ocaml (1.14-1) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../022-libcoq-core-ocaml_8.20.0+dfsg-1_arm64.deb ... Unpacking libcoq-core-ocaml (8.20.0+dfsg-1) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../023-libstdlib-ocaml-dev_5.2.0-3_arm64.deb ... Unpacking libstdlib-ocaml-dev (5.2.0-3) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../024-libcompiler-libs-ocaml-dev_5.2.0-3_arm64.deb ... Unpacking libcompiler-libs-ocaml-dev (5.2.0-3) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../025-ocaml-interp_5.2.0-3_arm64.deb ... Unpacking ocaml-interp (5.2.0-3) ... Selecting previously unselected package libncurses6:arm64. Preparing to unpack .../026-libncurses6_6.5-2+b1_arm64.deb ... Unpacking libncurses6:arm64 (6.5-2+b1) ... Selecting previously unselected package libncurses-dev:arm64. Preparing to unpack .../027-libncurses-dev_6.5-2+b1_arm64.deb ... Unpacking libncurses-dev:arm64 (6.5-2+b1) ... Selecting previously unselected package libzstd-dev:arm64. Preparing to unpack .../028-libzstd-dev_1.5.6+dfsg-1+b1_arm64.deb ... Unpacking libzstd-dev:arm64 (1.5.6+dfsg-1+b1) ... Selecting previously unselected package ocaml. Preparing to unpack .../029-ocaml_5.2.0-3_arm64.deb ... Unpacking ocaml (5.2.0-3) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../030-ocaml-findlib_1.9.6-3_arm64.deb ... Unpacking ocaml-findlib (1.9.6-3) ... Selecting previously unselected package coq. Preparing to unpack .../031-coq_8.20.0+dfsg-1_arm64.deb ... Unpacking coq (8.20.0+dfsg-1) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../032-libdebhelper-perl_13.20_all.deb ... Unpacking libdebhelper-perl (13.20) ... Selecting previously unselected package libtool. Preparing to unpack .../033-libtool_2.4.7-8_all.deb ... Unpacking libtool (2.4.7-8) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../034-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../035-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../036-libfile-stripnondeterminism-perl_1.14.0-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.14.0-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../037-dh-strip-nondeterminism_1.14.0-1_all.deb ... Unpacking dh-strip-nondeterminism (1.14.0-1) ... Selecting previously unselected package libelf1t64:arm64. Preparing to unpack .../038-libelf1t64_0.192-4_arm64.deb ... Unpacking libelf1t64:arm64 (0.192-4) ... Selecting previously unselected package dwz. Preparing to unpack .../039-dwz_0.15-1+b1_arm64.deb ... Unpacking dwz (0.15-1+b1) ... Selecting previously unselected package gettext. Preparing to unpack .../040-gettext_0.22.5-2_arm64.deb ... Unpacking gettext (0.22.5-2) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../041-intltool-debian_0.35.0+20060710.6_all.deb ... Unpacking intltool-debian (0.35.0+20060710.6) ... Selecting previously unselected package po-debconf. Preparing to unpack .../042-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../043-debhelper_13.20_all.deb ... Unpacking debhelper (13.20) ... Selecting previously unselected package dh-coq. Preparing to unpack .../044-dh-coq_0.11_all.deb ... Unpacking dh-coq (0.11) ... Selecting previously unselected package libconfig-tiny-perl. Preparing to unpack .../045-libconfig-tiny-perl_2.30-1_all.deb ... Unpacking libconfig-tiny-perl (2.30-1) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../046-dh-ocaml_2.4_all.deb ... Unpacking dh-ocaml (2.4) ... Selecting previously unselected package libgs-common. Preparing to unpack .../047-libgs-common_10.04.0~dfsg-1_all.deb ... Unpacking libgs-common (10.04.0~dfsg-1) ... Selecting previously unselected package libgs10-common. Preparing to unpack .../048-libgs10-common_10.04.0~dfsg-1_all.deb ... Unpacking libgs10-common (10.04.0~dfsg-1) ... Selecting previously unselected package libavahi-common-data:arm64. Preparing to unpack .../049-libavahi-common-data_0.8-13+b3_arm64.deb ... Unpacking libavahi-common-data:arm64 (0.8-13+b3) ... Selecting previously unselected package libavahi-common3:arm64. Preparing to unpack .../050-libavahi-common3_0.8-13+b3_arm64.deb ... Unpacking libavahi-common3:arm64 (0.8-13+b3) ... Selecting previously unselected package libdbus-1-3:arm64. Preparing to unpack .../051-libdbus-1-3_1.14.10-6_arm64.deb ... Unpacking libdbus-1-3:arm64 (1.14.10-6) ... Selecting previously unselected package libavahi-client3:arm64. Preparing to unpack .../052-libavahi-client3_0.8-13+b3_arm64.deb ... Unpacking libavahi-client3:arm64 (0.8-13+b3) ... Selecting previously unselected package libcups2t64:arm64. Preparing to unpack .../053-libcups2t64_2.4.10-2_arm64.deb ... Unpacking libcups2t64:arm64 (2.4.10-2) ... Selecting previously unselected package libidn12:arm64. Preparing to unpack .../054-libidn12_1.42-2+b1_arm64.deb ... Unpacking libidn12:arm64 (1.42-2+b1) ... Selecting previously unselected package libijs-0.35:arm64. Preparing to unpack .../055-libijs-0.35_0.35-15.1+b2_arm64.deb ... Unpacking libijs-0.35:arm64 (0.35-15.1+b2) ... Selecting previously unselected package libjbig2dec0:arm64. Preparing to unpack .../056-libjbig2dec0_0.20-1+b3_arm64.deb ... Unpacking libjbig2dec0:arm64 (0.20-1+b3) ... Selecting previously unselected package libpaper1:arm64. Preparing to unpack .../057-libpaper1_1.1.29+b2_arm64.deb ... Unpacking libpaper1:arm64 (1.1.29+b2) ... Selecting previously unselected package libice6:arm64. Preparing to unpack .../058-libice6_2%3a1.1.1-1_arm64.deb ... Unpacking libice6:arm64 (2:1.1.1-1) ... Selecting previously unselected package libsm6:arm64. Preparing to unpack .../059-libsm6_2%3a1.2.4-1_arm64.deb ... Unpacking libsm6:arm64 (2:1.2.4-1) ... Selecting previously unselected package libxt6t64:arm64. Preparing to unpack .../060-libxt6t64_1%3a1.2.1-1.2+b1_arm64.deb ... Unpacking libxt6t64:arm64 (1:1.2.1-1.2+b1) ... Selecting previously unselected package libgs10:arm64. Preparing to unpack .../061-libgs10_10.04.0~dfsg-1_arm64.deb ... Unpacking libgs10:arm64 (10.04.0~dfsg-1) ... Selecting previously unselected package ghostscript. Preparing to unpack .../062-ghostscript_10.04.0~dfsg-1_arm64.deb ... Unpacking ghostscript (10.04.0~dfsg-1) ... Selecting previously unselected package help2man. Preparing to unpack .../063-help2man_1.49.3+b1_arm64.deb ... Unpacking help2man (1.49.3+b1) ... Selecting previously unselected package libnetpbm11t64:arm64. Preparing to unpack .../064-libnetpbm11t64_2%3a11.08.01-1+b1_arm64.deb ... Unpacking libnetpbm11t64:arm64 (2:11.08.01-1+b1) ... Selecting previously unselected package netpbm. Preparing to unpack .../065-netpbm_2%3a11.08.01-1+b1_arm64.deb ... Unpacking netpbm (2:11.08.01-1+b1) ... Selecting previously unselected package tex-common. Preparing to unpack .../066-tex-common_6.18_all.deb ... Unpacking tex-common (6.18) ... Selecting previously unselected package libpaper-utils. Preparing to unpack .../067-libpaper-utils_1.1.29+b2_arm64.deb ... Unpacking libpaper-utils (1.1.29+b2) ... Selecting previously unselected package libkpathsea6:arm64. Preparing to unpack .../068-libkpathsea6_2024.20240313.70630+ds-5_arm64.deb ... Unpacking libkpathsea6:arm64 (2024.20240313.70630+ds-5) ... Selecting previously unselected package libptexenc1:arm64. Preparing to unpack .../069-libptexenc1_2024.20240313.70630+ds-5_arm64.deb ... Unpacking libptexenc1:arm64 (2024.20240313.70630+ds-5) ... Selecting previously unselected package libsynctex2:arm64. Preparing to unpack .../070-libsynctex2_2024.20240313.70630+ds-5_arm64.deb ... Unpacking libsynctex2:arm64 (2024.20240313.70630+ds-5) ... Selecting previously unselected package libtexlua53-5:arm64. Preparing to unpack .../071-libtexlua53-5_2024.20240313.70630+ds-5_arm64.deb ... Unpacking libtexlua53-5:arm64 (2024.20240313.70630+ds-5) ... Selecting previously unselected package t1utils. Preparing to unpack .../072-t1utils_1.41-4+b1_arm64.deb ... Unpacking t1utils (1.41-4+b1) ... Selecting previously unselected package libpixman-1-0:arm64. Preparing to unpack .../073-libpixman-1-0_0.44.0-3_arm64.deb ... Unpacking libpixman-1-0:arm64 (0.44.0-3) ... Selecting previously unselected package libxcb-render0:arm64. Preparing to unpack .../074-libxcb-render0_1.17.0-2+b1_arm64.deb ... Unpacking libxcb-render0:arm64 (1.17.0-2+b1) ... Selecting previously unselected package libxcb-shm0:arm64. Preparing to unpack .../075-libxcb-shm0_1.17.0-2+b1_arm64.deb ... Unpacking libxcb-shm0:arm64 (1.17.0-2+b1) ... Selecting previously unselected package libxrender1:arm64. Preparing to unpack .../076-libxrender1_1%3a0.9.10-1.1+b2_arm64.deb ... Unpacking libxrender1:arm64 (1:0.9.10-1.1+b2) ... Selecting previously unselected package libcairo2:arm64. Preparing to unpack .../077-libcairo2_1.18.2-2_arm64.deb ... Unpacking libcairo2:arm64 (1.18.2-2) ... Selecting previously unselected package libgraphite2-3:arm64. Preparing to unpack .../078-libgraphite2-3_1.3.14-2+b1_arm64.deb ... Unpacking libgraphite2-3:arm64 (1.3.14-2+b1) ... Selecting previously unselected package libharfbuzz0b:arm64. Preparing to unpack .../079-libharfbuzz0b_10.0.1-1_arm64.deb ... Unpacking libharfbuzz0b:arm64 (10.0.1-1) ... Selecting previously unselected package libmpfi0:arm64. Preparing to unpack .../080-libmpfi0_1.5.4+ds-4_arm64.deb ... Unpacking libmpfi0:arm64 (1.5.4+ds-4) ... Selecting previously unselected package libpotrace0:arm64. Preparing to unpack .../081-libpotrace0_1.16-2+b2_arm64.deb ... Unpacking libpotrace0:arm64 (1.16-2+b2) ... Selecting previously unselected package libteckit0:arm64. Preparing to unpack .../082-libteckit0_2.5.12+ds1-1+b1_arm64.deb ... Unpacking libteckit0:arm64 (2.5.12+ds1-1+b1) ... Selecting previously unselected package libxmu6:arm64. Preparing to unpack .../083-libxmu6_2%3a1.1.3-3+b3_arm64.deb ... Unpacking libxmu6:arm64 (2:1.1.3-3+b3) ... Selecting previously unselected package libxpm4:arm64. Preparing to unpack .../084-libxpm4_1%3a3.5.17-1+b2_arm64.deb ... Unpacking libxpm4:arm64 (1:3.5.17-1+b2) ... Selecting previously unselected package libxaw7:arm64. Preparing to unpack .../085-libxaw7_2%3a1.0.16-1_arm64.deb ... Unpacking libxaw7:arm64 (2:1.0.16-1) ... Selecting previously unselected package libxi6:arm64. Preparing to unpack .../086-libxi6_2%3a1.8.2-1_arm64.deb ... Unpacking libxi6:arm64 (2:1.8.2-1) ... Selecting previously unselected package libzzip-0-13t64:arm64. Preparing to unpack .../087-libzzip-0-13t64_0.13.72+dfsg.1-1.3_arm64.deb ... Unpacking libzzip-0-13t64:arm64 (0.13.72+dfsg.1-1.3) ... Selecting previously unselected package texlive-binaries. Preparing to unpack .../088-texlive-binaries_2024.20240313.70630+ds-5_arm64.deb ... Unpacking texlive-binaries (2024.20240313.70630+ds-5) ... Selecting previously unselected package xdg-utils. Preparing to unpack .../089-xdg-utils_1.1.3-4.1_all.deb ... Unpacking xdg-utils (1.1.3-4.1) ... Selecting previously unselected package texlive-base. Preparing to unpack .../090-texlive-base_2024.20241115-1_all.deb ... Unpacking texlive-base (2024.20241115-1) ... Selecting previously unselected package hicolor-icon-theme. Preparing to unpack .../091-hicolor-icon-theme_0.18-1_all.deb ... Unpacking hicolor-icon-theme (0.18-1) ... Selecting previously unselected package imagemagick-7.q16. Preparing to unpack .../092-imagemagick-7.q16_8%3a7.1.1.39+dfsg1-2_arm64.deb ... Unpacking imagemagick-7.q16 (8:7.1.1.39+dfsg1-2) ... Selecting previously unselected package imagemagick. Preparing to unpack .../093-imagemagick_8%3a7.1.1.39+dfsg1-2_arm64.deb ... Unpacking imagemagick (8:7.1.1.39+dfsg1-2) ... Selecting previously unselected package hevea. Preparing to unpack .../094-hevea_2.36-2+b2_arm64.deb ... Unpacking hevea (2.36-2+b2) ... Selecting previously unselected package libfindlib-ocaml-dev. Preparing to unpack .../095-libfindlib-ocaml-dev_1.9.6-3_arm64.deb ... Unpacking libfindlib-ocaml-dev (1.9.6-3) ... Selecting previously unselected package libgmpxx4ldbl:arm64. Preparing to unpack .../096-libgmpxx4ldbl_2%3a6.3.0+dfsg-2+b2_arm64.deb ... Unpacking libgmpxx4ldbl:arm64 (2:6.3.0+dfsg-2+b2) ... Selecting previously unselected package libgmp-dev:arm64. Preparing to unpack .../097-libgmp-dev_2%3a6.3.0+dfsg-2+b2_arm64.deb ... Unpacking libgmp-dev:arm64 (2:6.3.0+dfsg-2+b2) ... Selecting previously unselected package libgmp3-dev:arm64. Preparing to unpack .../098-libgmp3-dev_2%3a6.3.0+dfsg-2+b2_arm64.deb ... Unpacking libgmp3-dev:arm64 (2:6.3.0+dfsg-2+b2) ... Selecting previously unselected package libzarith-ocaml-dev. Preparing to unpack .../099-libzarith-ocaml-dev_1.14-1_arm64.deb ... Unpacking libzarith-ocaml-dev (1.14-1) ... Selecting previously unselected package libcoq-core-ocaml-dev. Preparing to unpack .../100-libcoq-core-ocaml-dev_8.20.0+dfsg-1_arm64.deb ... Unpacking libcoq-core-ocaml-dev (8.20.0+dfsg-1) ... Selecting previously unselected package liblua5.4-0:arm64. Preparing to unpack .../101-liblua5.4-0_5.4.6-3+b2_arm64.deb ... Unpacking liblua5.4-0:arm64 (5.4.6-3+b2) ... Selecting previously unselected package libnuma1:arm64. Preparing to unpack .../102-libnuma1_2.0.18-1+b1_arm64.deb ... Unpacking libnuma1:arm64 (2.0.18-1+b1) ... Selecting previously unselected package libocamlgraph-ocaml-dev. Preparing to unpack .../103-libocamlgraph-ocaml-dev_2.1.0-3+b1_arm64.deb ... Unpacking libocamlgraph-ocaml-dev (2.1.0-3+b1) ... Selecting previously unselected package libyaml-0-2:arm64. Preparing to unpack .../104-libyaml-0-2_0.2.5-1+b2_arm64.deb ... Unpacking libyaml-0-2:arm64 (0.2.5-1+b2) ... Selecting previously unselected package pandoc-data. Preparing to unpack .../105-pandoc-data_3.1.11.1-3_all.deb ... Unpacking pandoc-data (3.1.11.1-3) ... Selecting previously unselected package pandoc. Preparing to unpack .../106-pandoc_3.1.11.1+ds-2_arm64.deb ... Unpacking pandoc (3.1.11.1+ds-2) ... Setting up media-types (10.1.0) ... Setting up libpipeline1:arm64 (1.5.8-1) ... Setting up libgraphite2-3:arm64 (1.3.14-2+b1) ... Setting up liblcms2-2:arm64 (2.16-2) ... Setting up libpixman-1-0:arm64 (0.44.0-3) ... Setting up libsharpyuv0:arm64 (1.4.0-0.1+b1) ... Setting up libxau6:arm64 (1:1.0.11-1) ... Setting up libxdmcp6:arm64 (1:1.1.5-1) ... Setting up libkeyutils1:arm64 (1.6.3-4) ... Setting up libxcb1:arm64 (1.17.0-2+b1) ... Setting up libicu72:arm64 (72.1-5+b1) ... Setting up liblerc4:arm64 (4.0.0+ds-5) ... Setting up libzstd-dev:arm64 (1.5.6+dfsg-1+b1) ... Setting up bsdextrautils (2.40.2-11) ... Setting up hicolor-icon-theme (0.18-1) ... Setting up libmagic-mgc (1:5.45-3+b1) ... Setting up libxcb-render0:arm64 (1.17.0-2+b1) ... Setting up dh-coq (0.11) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libyaml-0-2:arm64 (0.2.5-1+b2) ... Setting up imagemagick-7-common (8:7.1.1.39+dfsg1-2) ... Setting up libtirpc-common (1.3.4+ds-1.3) ... Setting up libijs-0.35:arm64 (0.35-15.1+b2) ... Setting up libdebhelper-perl (13.20) ... Setting up libgs-common (10.04.0~dfsg-1) ... Setting up libbrotli1:arm64 (1.1.0-2+b6) ... Setting up libmagic1t64:arm64 (1:5.45-3+b1) ... Setting up x11-common (1:7.7+23.1) ... invoke-rc.d: could not determine current runlevel Setting up X socket directories... /tmp/.X11-unix /tmp/.ICE-unix. Setting up libdeflate0:arm64 (1.22-1) ... Setting up gettext-base (0.22.5-2) ... Setting up m4 (1.4.19-4) ... Setting up libxcb-shm0:arm64 (1.17.0-2+b1) ... Setting up libcom-err2:arm64 (1.47.1-1+b1) ... Setting up file (1:5.45-3+b1) ... Setting up libconfig-tiny-perl (2.30-1) ... Setting up libjbig0:arm64 (2.1-6.1+b2) ... Setting up libnetpbm11t64:arm64 (2:11.08.01-1+b1) ... Setting up libelf1t64:arm64 (0.192-4) ... Setting up poppler-data (0.4.12-1) ... Setting up libkrb5support0:arm64 (1.21.3-3) ... Setting up tzdata (2024b-3) ... Current default time zone: 'Etc/UTC' Local time is now: Thu Dec 25 01:52:20 UTC 2025. Universal Time is now: Thu Dec 25 01:52:20 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libfontenc1:arm64 (1:1.1.8-1+b1) ... Setting up autotools-dev (20220109.1) ... Setting up libglib2.0-0t64:arm64 (2.82.2-3) ... No schema files found: doing nothing. Setting up libcoq-stdlib (8.20.0+dfsg-1) ... Setting up libgmpxx4ldbl:arm64 (2:6.3.0+dfsg-2+b2) ... Setting up libjpeg62-turbo:arm64 (1:2.1.5-3+b1) ... Setting up libzzip-0-13t64:arm64 (0.13.72+dfsg.1-1.3) ... Setting up libx11-data (2:1.8.10-2) ... Setting up libjbig2dec0:arm64 (0.20-1+b3) ... Setting up libteckit0:arm64 (2.5.12+ds1-1+b1) ... Setting up libavahi-common-data:arm64 (0.8-13+b3) ... Setting up libncurses6:arm64 (6.5-2+b1) ... Setting up libdbus-1-3:arm64 (1.14.10-6) ... Setting up xfonts-encodings (1:1.0.4-2.2) ... Setting up t1utils (1.41-4+b1) ... Setting up libtexlua53-5:arm64 (2024.20240313.70630+ds-5) ... Setting up libstdlib-ocaml (5.2.0-3) ... Setting up libpng16-16t64:arm64 (1.6.44-2) ... Setting up libidn12:arm64 (1.42-2+b1) ... Setting up autopoint (0.22.5-2) ... Setting up libmpfi0:arm64 (1.5.4+ds-4) ... Setting up ocaml-base (5.2.0-3) ... Setting up libk5crypto3:arm64 (1.21.3-3) ... Setting up libltdl7:arm64 (2.4.7-8) ... Setting up libfftw3-double3:arm64 (3.3.10-2) ... Setting up libkpathsea6:arm64 (2024.20240313.70630+ds-5) ... Setting up libraw23t64:arm64 (0.21.3-1+b1) ... Setting up autoconf (2.72-3) ... Setting up libwebp7:arm64 (1.4.0-0.1+b1) ... Setting up libnuma1:arm64 (2.0.18-1+b1) ... Setting up dwz (0.15-1+b1) ... Setting up libdav1d7:arm64 (1.5.0-1+b1) ... Setting up liblqr-1-0:arm64 (0.4.2-2.1+b2) ... Setting up sensible-utils (0.0.24) ... Setting up libtiff6:arm64 (4.5.1+git230720-5) ... Setting up libuchardet0:arm64 (0.0.8-1+b2) ... Setting up liblua5.4-0:arm64 (5.4.6-3+b2) ... Setting up libopenjp2-7:arm64 (2.5.0-2+b4) ... Setting up libx11-6:arm64 (2:1.8.10-2) ... Setting up netbase (6.4) ... Setting up libkrb5-3:arm64 (1.21.3-3) ... Setting up pandoc-data (3.1.11.1-3) ... Setting up libde265-0:arm64 (1.0.15-1+b2) ... Setting up libwebpmux3:arm64 (1.4.0-0.1+b1) ... Setting up readline-common (8.2-5) ... Setting up libxml2:arm64 (2.12.7+dfsg+really2.9.14-0.2+b1) ... Setting up xdg-utils (1.1.3-4.1) ... update-alternatives: using /usr/bin/xdg-open to provide /usr/bin/open (open) in auto mode Setting up liblocale-gettext-perl (1.07-7+b1) ... Setting up libsynctex2:arm64 (2024.20240313.70630+ds-5) ... Setting up libpotrace0:arm64 (1.16-2+b2) ... Setting up automake (1:1.16.5-1.3) ... update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode Setting up libfile-stripnondeterminism-perl (1.14.0-1) ... Setting up libice6:arm64 (2:1.1.1-1) ... Setting up libncurses-dev:arm64 (6.5-2+b1) ... Setting up gettext (0.22.5-2) ... Setting up libgmp-dev:arm64 (2:6.3.0+dfsg-2+b2) ... Setting up libxpm4:arm64 (1:3.5.17-1+b2) ... Setting up libxrender1:arm64 (1:0.9.10-1.1+b2) ... Setting up libtool (2.4.7-8) ... Setting up libstdlib-ocaml-dev (5.2.0-3) ... Setting up libwebpdemux2:arm64 (1.4.0-0.1+b1) ... Setting up libavahi-common3:arm64 (0.8-13+b3) ... Setting up dh-ocaml (2.4) ... Setting up libfindlib-ocaml (1.9.6-3) ... Setting up libxext6:arm64 (2:1.3.4-1+b2) ... Setting up libzarith-ocaml (1.14-1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up help2man (1.49.3+b1) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (5.2.0-3) ... Setting up ocaml-interp (5.2.0-3) ... Setting up libptexenc1:arm64 (2024.20240313.70630+ds-5) ... Setting up pandoc (3.1.11.1+ds-2) ... Setting up libfreetype6:arm64 (2.13.3+dfsg-1) ... Setting up ocaml-findlib (1.9.6-3) ... Setting up libgssapi-krb5-2:arm64 (1.21.3-3) ... Setting up ucf (3.0043+nmu1) ... Setting up netpbm (2:11.08.01-1+b1) ... Setting up libreadline8t64:arm64 (8.2-5) ... Setting up dh-strip-nondeterminism (1.14.0-1) ... Setting up libcoq-core-ocaml (8.20.0+dfsg-1) ... Setting up groff-base (1.23.0-5) ... Setting up libgmp3-dev:arm64 (2:6.3.0+dfsg-2+b2) ... Setting up libharfbuzz0b:arm64 (10.0.1-1) ... Setting up libsm6:arm64 (2:1.2.4-1) ... Setting up libavahi-client3:arm64 (0.8-13+b3) ... Setting up libpaper1:arm64 (1.1.29+b2) ... Creating config file /etc/papersize with new version Setting up libxi6:arm64 (2:1.8.2-1) ... Setting up libtirpc3t64:arm64 (1.3.4+ds-1.3+b1) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up libpaper-utils (1.1.29+b2) ... Setting up ocaml (5.2.0-3) ... Setting up xfonts-utils (1:7.7+7) ... Setting up man-db (2.13.0-1) ... Not building database; man-db/auto-update is not 'true'. Setting up tex-common (6.18) ... update-language: texlive-base not installed and configured, doing nothing! Setting up libxt6t64:arm64 (1:1.2.1-1.2+b1) ... Setting up libfindlib-ocaml-dev (1.9.6-3) ... Setting up libnsl2:arm64 (1.3.0-3+b3) ... Setting up libzarith-ocaml-dev (1.14-1) ... Setting up libcups2t64:arm64 (2.4.10-2) ... Setting up libocamlgraph-ocaml-dev (2.1.0-3+b1) ... Setting up libxmu6:arm64 (2:1.1.3-3+b3) ... Setting up libpython3.12-stdlib:arm64 (3.12.7-3) ... Setting up python3.12 (3.12.7-3) ... Setting up debhelper (13.20) ... Setting up libxaw7:arm64 (2:1.0.16-1) ... Setting up fonts-urw-base35 (20200910-8) ... Setting up libpython3-stdlib:arm64 (3.12.7-1) ... Setting up libgs10-common (10.04.0~dfsg-1) ... Setting up fontconfig-config (2.15.0-1.1+b1) ... Setting up python3 (3.12.7-1) ... Setting up coq (8.20.0+dfsg-1) ... Setting up libcoq-core-ocaml-dev (8.20.0+dfsg-1) ... Setting up libfontconfig1:arm64 (2.15.0-1.1+b1) ... Setting up libgs10:arm64 (10.04.0~dfsg-1) ... Setting up ghostscript (10.04.0~dfsg-1) ... Setting up libcairo2:arm64 (1.18.2-2) ... Setting up texlive-binaries (2024.20240313.70630+ds-5) ... update-alternatives: using /usr/bin/xdvi-xaw to provide /usr/bin/xdvi.bin (xdvi.bin) in auto mode update-alternatives: using /usr/bin/bibtex.original to provide /usr/bin/bibtex (bibtex) in auto mode Setting up texlive-base (2024.20241115-1) ... tl-paper: setting paper size for dvips to a4: /var/lib/texmf/dvips/config/config-paper.ps tl-paper: setting paper size for dvipdfmx to a4: /var/lib/texmf/dvipdfmx/dvipdfmx-paper.cfg tl-paper: setting paper size for xdvi to a4: /var/lib/texmf/xdvi/XDvi-paper tl-paper: setting paper size for pdftex to a4: /var/lib/texmf/tex/generic/tex-ini-files/pdftexconfig.tex Setting up libheif-plugin-dav1d:arm64 (1.19.3-1) ... Setting up libheif-plugin-libde265:arm64 (1.19.3-1) ... Setting up libheif1:arm64 (1.19.3-1) ... Setting up libmagickcore-7.q16-10:arm64 (8:7.1.1.39+dfsg1-2) ... Setting up libmagickwand-7.q16-10:arm64 (8:7.1.1.39+dfsg1-2) ... Setting up imagemagick-7.q16 (8:7.1.1.39+dfsg1-2) ... update-alternatives: using /usr/bin/compare-im7.q16 to provide /usr/bin/compare (compare) in auto mode update-alternatives: using /usr/bin/compare-im7.q16 to provide /usr/bin/compare-im7 (compare-im7) in auto mode update-alternatives: using /usr/bin/animate-im7.q16 to provide /usr/bin/animate (animate) in auto mode update-alternatives: using /usr/bin/animate-im7.q16 to provide /usr/bin/animate-im7 (animate-im7) in auto mode update-alternatives: using /usr/bin/convert-im7.q16 to provide /usr/bin/convert (convert) in auto mode update-alternatives: using /usr/bin/convert-im7.q16 to provide /usr/bin/convert-im7 (convert-im7) in auto mode update-alternatives: using /usr/bin/composite-im7.q16 to provide /usr/bin/composite (composite) in auto mode update-alternatives: using /usr/bin/composite-im7.q16 to provide /usr/bin/composite-im7 (composite-im7) in auto mode update-alternatives: using /usr/bin/conjure-im7.q16 to provide /usr/bin/conjure (conjure) in auto mode update-alternatives: using /usr/bin/conjure-im7.q16 to provide /usr/bin/conjure-im7 (conjure-im7) in auto mode update-alternatives: using /usr/bin/import-im7.q16 to provide /usr/bin/import (import) in auto mode update-alternatives: using /usr/bin/import-im7.q16 to provide /usr/bin/import-im7 (import-im7) in auto mode update-alternatives: using /usr/bin/identify-im7.q16 to provide /usr/bin/identify (identify) in auto mode update-alternatives: using /usr/bin/identify-im7.q16 to provide /usr/bin/identify-im7 (identify-im7) in auto mode update-alternatives: using /usr/bin/stream-im7.q16 to provide /usr/bin/stream (stream) in auto mode update-alternatives: using /usr/bin/stream-im7.q16 to provide /usr/bin/stream-im7 (stream-im7) in auto mode update-alternatives: using /usr/bin/display-im7.q16 to provide /usr/bin/display (display) in auto mode update-alternatives: using /usr/bin/display-im7.q16 to provide /usr/bin/display-im7 (display-im7) in auto mode update-alternatives: using /usr/bin/montage-im7.q16 to provide /usr/bin/montage (montage) in auto mode update-alternatives: using /usr/bin/montage-im7.q16 to provide /usr/bin/montage-im7 (montage-im7) in auto mode update-alternatives: using /usr/bin/mogrify-im7.q16 to provide /usr/bin/mogrify (mogrify) in auto mode update-alternatives: using /usr/bin/mogrify-im7.q16 to provide /usr/bin/mogrify-im7 (mogrify-im7) in auto mode update-alternatives: using /usr/bin/magick-im7.q16 to provide /usr/bin/magick (magick) in auto mode update-alternatives: warning: skip creation of /usr/share/man/man1/magick.1.gz because associated file /usr/share/man/man1/magick-im7.q16.1.gz (of link group magick) doesn't exist update-alternatives: using /usr/bin/magick-im7.q16 to provide /usr/bin/magick-im7 (magick-im7) in auto mode update-alternatives: warning: skip creation of /usr/share/man/man1/magick-im7.1.gz because associated file /usr/share/man/man1/magick-im7.q16.1.gz (of link group magick-im7) doesn't exist update-alternatives: using /usr/bin/magick-script-im7.q16 to provide /usr/bin/magick-script (magick-script) in auto mode update-alternatives: warning: skip creation of /usr/share/man/man1/magick-script.1.gz because associated file /usr/share/man/man1/magick-script-im7.q16.1.gz (of link group magick-script) doesn't exist update-alternatives: using /usr/bin/magick-script-im7.q16 to provide /usr/bin/magick-script-im7 (magick-script-im7) in auto mode update-alternatives: warning: skip creation of /usr/share/man/man1/magick-script-im7.1.gz because associated file /usr/share/man/man1/magick-script-im7.q16.1.gz (of link group magick-script-im7) doesn't exist Setting up hevea (2.36-2+b2) ... Setting up imagemagick (8:7.1.1.39+dfsg1-2) ... Processing triggers for libc-bin (2.40-3) ... Processing triggers for tex-common (6.18) ... Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Building format(s) --all. This may take some time... done. Reading package lists... Building dependency tree... Reading state information... Reading extended state information... Initializing package states... Writing extended state information... Building tag database... -> Finished parsing the build-deps I: Building the package I: user script /srv/workspace/pbuilder/288991/tmp/hooks/A99_set_merged_usr starting Not re-configuring usrmerge for unstable I: user script /srv/workspace/pbuilder/288991/tmp/hooks/A99_set_merged_usr finished hostname: Name or service not known I: Running cd /build/reproducible-path/ott-0.33+ds/ && 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 > ../ott_0.33+ds-4_source.changes dpkg-buildpackage: info: source package ott dpkg-buildpackage: info: source version 0.33+ds-4 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Stéphane Glondu dpkg-source --before-build . dpkg-buildpackage: info: host architecture arm64 debian/rules clean dh clean --with coq,ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/reproducible-path/ott-0.33+ds' cp src/version.ml src/version.ml.bak make clean make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds' cd src; make clean make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' ocamllex grammar_lexer.mll 374 states, 16439 transitions, table size 68000 bytes 3397 additional bytes used for bindings ocamlyacc -v grammar_parser.mly 2 rules never reduced ocamldep location.ml types.ml auxl.ml merge.ml global_option.ml grammar_lexer.ml grammar_parser.mli grammar_parser.ml version.ml grammar_pp.ml parse_table.ml glr.ml new_term_parser.ml term_parser.ml dependency.ml bounds.ml context_pp.ml quotient_rules.ml grammar_typecheck.ml transform.ml substs_pp.ml subrules_pp.ml embed_pp.ml defns.ml ln_transform.ml coq_induct.ml system_pp.ml lex_menhir_pp.ml align.ml main.ml align.mli bounds.mli coq_induct.mli defns.mli dependency.mli embed_pp.mli grammar_typecheck.mli merge.mli subrules_pp.mli substs_pp.mli system_pp.mli lex_menhir_pp.mli transform.mli term_parser.mli > .depend rm -f *~ *.cmi *.cmo *.cmx *.o rm -f grammar_lexer.ml grammar_parser.ml \ grammar_parser.mli grammar_parser.output rm -f version.ml rm -rf ott ott.byt ott.opt ../bin/ott rm -f grammar_parser.tex *.mly-y2l rm -f *.aux *.log *.dvi *.ps *.pdf *.annot rm -f out.thy out.v outScript.sml outTheory.uo outTheory.ui outTheory.sig outTheory.sml out.tex out.sty rm -f tmp_*.dot tmp.dot rm -f tmp_*.ott rm -f testRegr* rm -f *Theory.* *.ui *.uo make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' rm -f *~ rm -f ott.install make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds' make -C doc clean make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/doc' rm -f *.aux *.log *.dvi *.annot top.doc top.tex top.ps top.pdf top2.ps top2.pdf top2.ggl top2.blg top2.html top2.image.tex top2.tex bind-doc.pdf bind-doc.ps bind-wmm-2.bbl bind-wmm-2.blg bind-wmm-2.pdf bind-wmm-2.ps paper.bbl paper.blg paper.tex s rm -f bind-doc-2.ps bind-doc-2.pdf bind-2.tex bind-2.thy rm -f binding.1.aux binding.1.tex binding.2.aux binding.2.tex binding.3.aux binding.3.tex binding.4.aux binding.4.tex binding.5.aux binding.5.tex binding.6.alltt.tex binding.6b.aux binding.6b.tex binding.6bScript.sml rm -f test10.0.alltt test10.2.aux test10.4.alltt test10.aux test10.meta.tex test10.tex test10.v test10_homs.alltt test10st.tex test10.2.alltt test10.2.tex test10.7.alltt test10.meta.aux test10.ml test10.thy test10Script.sml test10st.aux test21.1.alltt rm -f test11.alltt test12.thy test12.v test13.aux test13.tex test13d.aux test13d.tex test17.10.aux test17.10.tex test7tt.mng.alltt.tex rm -f slides-arg.dvi rm -f slides-sl.dvi rm -f slides-icfp.dvi rm -f slides-parsec.dvi rm -f grammar_parser.tex *.mly-y2l grammar_parser_hevea.tex rm -f top2*.gif top2.haux top2.htoc top2.lof rm -f squishtex.hand.alltt.tex rm -f options.txt test7.tex test7afilter.out.ps test7tt.tex test8.tex tmp.dot tmp_0.dot tmp_1.dot tmp_2.dot top.toc top2.bbl top2.toc version.tex x.tex rm -f bind.tex bind.thy rm -f test10_tuple.tex test10_tuple.thy test10_tuple.v test10_tupleScript.sml test10b.tex test10b.thy test10b.v test10bScript.sml test10st_narrow.tex test10st_narrow.thy test10st_narrow.v test10st_narrowScript.sml rm -f test10.alltt.tex test10_html.html rm -f README.tex rm -f *~ make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/doc' mv src/version.ml.bak src/version.ml rm -f src/.depend src/version.tex coq/.lia.cache coq/.Makefile.coq.d rm -f doc/README.* doc/test10.despaced.v doc/test10.lem find . -name "*.vo*" -delete find . -name "*.aux" -delete find . -name "Makefile.coq*" -delete find . -name "*.glob" -delete make[1]: Leaving directory '/build/reproducible-path/ott-0.33+ds' dh_ocamlclean dh_clean debian/rules binary dh binary --with coq,ocaml dh_update_autotools_config dh_autoreconf dh_ocamlinit dh_auto_configure debian/rules override_dh_auto_build make[1]: Entering directory '/build/reproducible-path/ott-0.33+ds' make -C coq make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/coq' coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/coq' COQDEP VFILES COQC ott_list_support.v COQC ott_list_base.v File "./ott_list_base.v", line 187, characters 13-20: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_base.v", line 188, characters 16-27: Warning: Notation app_nil_end is deprecated since 8.18. Use app_nil_r instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] COQC ott_list_eq_dec.v COQC ott_list_core.v COQC ott_list_nth.v COQC ott_list_takedrop.v File "./ott_list_takedrop.v", line 170, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 170, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 170, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 179, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 179, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 179, characters 10-17: Warning: Notation app_ass is deprecated since 8.18. Use app_assoc instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 196, characters 18-29: Warning: Notation app_nil_end is deprecated since 8.18. Use app_nil_r instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 196, characters 18-29: Warning: Notation app_nil_end is deprecated since 8.18. Use app_nil_r instead. [deprecated-syntactic-definition-since-8.18,deprecated-since-8.18,deprecated-syntactic-definition,deprecated,default] COQC ott_list_predicate.v COQC ott_list_mem.v COQC ott_list_flat_map.v COQC ott_list_repeat.v COQC ott_list_distinct.v COQC ott_list.v make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/coq' make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/coq' make -C src make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' ocamllex grammar_lexer.mll 374 states, 16439 transitions, table size 68000 bytes 3397 additional bytes used for bindings ocamlyacc -v grammar_parser.mly 2 rules never reduced ocamldep location.ml types.ml auxl.ml merge.ml global_option.ml grammar_lexer.ml grammar_parser.mli grammar_parser.ml version.ml grammar_pp.ml parse_table.ml glr.ml new_term_parser.ml term_parser.ml dependency.ml bounds.ml context_pp.ml quotient_rules.ml grammar_typecheck.ml transform.ml substs_pp.ml subrules_pp.ml embed_pp.ml defns.ml ln_transform.ml coq_induct.ml system_pp.ml lex_menhir_pp.ml align.ml main.ml align.mli bounds.mli coq_induct.mli defns.mli dependency.mli embed_pp.mli grammar_typecheck.mli merge.mli subrules_pp.mli substs_pp.mli system_pp.mli lex_menhir_pp.mli transform.mli term_parser.mli > .depend ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c location.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c types.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c auxl.ml File "auxl.ml", lines 405-412, characters 7-19: 405 | .......( match hse with 406 | | Hom_index _ | Hom_terminal _ -> [] 407 | | Hom_string s -> 408 | let strs = Str.split (Str.regexp "[ \t]+") s in 409 | let ntrs_hom = List.filter (fun st -> List.mem st defined_ntrs) strs in 410 | if promote 411 | then List.map (promote_ntr xd) ntrs_hom 412 | else ntrs_hom ). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) File "auxl.ml", lines 467-471, characters 7-59: 467 | .......( match hse with 468 | | Hom_index _ | Hom_terminal _ -> [] 469 | | Hom_string s -> 470 | let strs = Str.split (Str.regexp "[ \t]+") s in 471 | List.filter (fun st -> List.mem st defined_mvrs) strs ). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) File "auxl.ml", lines 1839-1854, characters 4-42: 1839 | ....( match stre with 1840 | | Struct_md mvr -> "metavar def: "^mvr 1841 | | Struct_rs ntrs -> "rule def: "^(String.concat " " ntrs) 1842 | | Struct_srs xs -> "subrule def: "^ 1843 | (String.concat " " ... 1851 | | Struct_axs xs -> "aux def: "^ 1852 | (String.concat " " xs) 1853 | | Struct_fun_or_defnclass s -> "fundefn_class def: "^s 1854 | | Struct_embed (_,h,_) -> "embed: "^h) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Struct_crs _ ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c merge.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c merge.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c global_option.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_parser.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_lexer.ml File "grammar_lexer.mll", line 471, characters 10-13: Warning 26 [unused-var]: unused variable loc. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_parser.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c version.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_pp.ml File "grammar_pp.ml", lines 1875-2131, characters 6-25: 1875 | ......( match m with 1876 | | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" 1877 | | Ascii ao -> 1878 | pp_auxfn m xd f ^ ""^pp_LPAREN ^ "" 1879 | ^ pp_ntlist ... 2128 | else 2129 | ( "(flat_map (fun "^pat_fun^" => "^pp_body^ pat_fun_end ^ ") " 2130 | ^ de1i.de1_compound_id 2131 | ^ ")", [], [] ) ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _) (However, some guarded clause may match this value.) File "grammar_pp.ml", lines 4022-4025, characters 16-45: 4022 | ................(match hse with 4023 | | Hom_string _ -> arity_of_homspec hs' 4024 | | Hom_index i -> max (1+i) (arity_of_homspec hs') 4025 | | Hom_terminal _ -> arity_of_homspec hs') Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) File "grammar_pp.ml", line 3624, characters 6-18: 3624 | let debug_string = "" (* ("(* pp_symterm_list_items entry:\nstlis= [" ^String.concat " ; " (List.map pp_plain_symterm_list_item stlis)^"]\nprod_es= ["^String.concat " ; "(List.map pp_plain_element prod_es)^"] *)\n\n")*) in ^^^^^^^^^^^^ Warning 26 [unused-var]: unused variable debug_string. File "grammar_pp.ml", line 3756, characters 6-18: 3756 | let debug_string = "" in (*("pp_symterm_list_body entry:\nstlb= ["^String.concat " ; " (pp_plain_symterm_list_body stlb)^"]\nprod_es= ["^String.concat " ; " (List.map pp_plain_element prod_es)^"]\n\n") in*) ^^^^^^^^^^^^ Warning 26 [unused-var]: unused variable debug_string. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c parse_table.ml File "parse_table.ml", line 914, characters 47-50: 914 | prod_action = (fun [r] -> r); ^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: r::_::_ ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c glr.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c new_term_parser.ml File "new_term_parser.ml", lines 150-177, characters 11-29: 150 | ...........function 151 | | "[" -> "lbrac" 152 | | "]" -> "rbrac" 153 | | "!" -> "excl" 154 | | "\"" -> "doublequote" ... 174 | | "}" -> "rcurly" 175 | | "|" -> "bar" 176 | | "~" -> "tilde" 177 | | "-" -> "minus". Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: "" File "new_term_parser.ml", line 289, characters 14-39: 289 | let res_charl [Res_char c; Res_charl l] = ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::Res_charl l::_::_ File "new_term_parser.ml", line 292, characters 20-45: 292 | let res_cons_string [Res_char c; Res_charl l] = ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::Res_charl l::_::_ File "new_term_parser.ml", line 295, characters 14-39: 295 | let res_stlil [Res_stli a; Res_stlil b] = Res_stlil (a::b);; ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli a::Res_stlil b::_::_ File "new_term_parser.ml", lines 342-346, characters 67-66: 342 | ...................................................................function 343 | [] -> [] 344 | | Res_ignore::rl -> process_prod_res rl 345 | | Res_ste ste::rl -> ste::process_prod_res rl 346 | | Res_st st::rl -> Ste_st (dummy_loc, st)::process_prod_res rl Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Res_none|Res_stli _|Res_stlil _|Res_char _|Res_charl _|Res_string _| Res_int _|Res_si _|Res_sil _)::_ File "new_term_parser.ml", line 382, characters 19-32: 382 | (fun [Res_stlil x] -> elc x); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stlil x::_::_ File "new_term_parser.ml", line 401, characters 13-25: 401 | (fun [Res_stli x]-> Res_stlil [x]); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli x::_::_ File "new_term_parser.ml", line 416, characters 21-30: 416 | (fun [x; _; y] -> res_stlil [x; y]) ^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::y::_::_ File "new_term_parser.ml", lines 463-466, characters 31-64: 463 | ...............................[Res_stli (Stli_single (_, es1)); 464 | _; 465 | Res_int n'; 466 | Res_stli (Stli_single (_, es2))]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli (Stli_single (_, es1))::_::Res_int n':: Res_stli (Stli_single (_, es2))::_::_ File "new_term_parser.ml", lines 476-481, characters 31-64: 476 | ...............................[Res_stli (Stli_single (_, es1)); 477 | _; 478 | _; 479 | Res_int n'; 480 | _; 481 | Res_stli (Stli_single (_, es2))]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli (Stli_single (_, es1))::_::_::Res_int n'::_:: Res_stli (Stli_single (_, es2))::_::_ File "new_term_parser.ml", lines 488-489, characters 23-26: 488 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 489 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_::_ File "new_term_parser.ml", lines 508-511, characters 23-26: 508 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 509 | _; 510 | _; Res_string ivr'; 511 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_:: Res_string ivr'::_::_::_ File "new_term_parser.ml", lines 536-544, characters 23-26: 536 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 537 | _; 538 | _; 539 | Res_string lower; 540 | _; 541 | Res_int dotlength; 542 | _; 543 | Res_si si'; 544 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_:: Res_string lower::_::Res_int dotlength::_::Res_si si'::_::_::_ File "new_term_parser.ml", line 560, characters 23-35: 560 | (fun [Res_stli x] -> Res_stlil [x])); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli x::_::_ File "new_term_parser.ml", line 574, characters 29-38: 574 | (fun [x; _; y] -> res_stlil [x; y])); ^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::y::_::_ File "new_term_parser.ml", line 603, characters 20-27: 603 | (fun (_::rl) -> build_res rl) in ^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "new_term_parser.ml", line 609, characters 20-27: 609 | (fun (_::rl) -> build_res rl) in ^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "new_term_parser.ml", line 628, characters 17-23: 628 | (fun [_; x] -> x) ^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::x::_::_ File "new_term_parser.ml", line 638, characters 18-32: 638 | (fun [_; Res_sil l] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil l::_::_ File "new_term_parser.ml", line 649, characters 23-37: 649 | (fun [_; Res_sil l] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil l::_::_ File "new_term_parser.ml", line 664, characters 11-25: 664 | (fun [_; Res_sil x] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil x::_::_ File "new_term_parser.ml", line 695, characters 19-39: 695 | (fun (_::Res_string s::_) -> Res_ste (Ste_metavar (dummy_loc, mvd.mvd_name, (s, [])))) ^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _:: (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _| Res_charl _|Res_int _|Res_si _|Res_sil _)::_ File "new_term_parser.ml", line 703, characters 21-38: 703 | (fun [_; Res_string s] -> ^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_string s::_::_ File "new_term_parser.ml", line 710, characters 21-38: 710 | (fun [_; Res_string s] -> ^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_string s::_::_ File "new_term_parser.ml", line 715, characters 21-59: 715 | (fun [((Res_ste (Ste_var (_, _, s))) as x)] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_ste (Ste_var (_, _, s))::_::_ File "new_term_parser.ml", line 742, characters 11-23: 742 | (fun [Res_char c] -> Res_charl [c]); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::_::_ File "new_term_parser.ml", line 748, characters 11-24: 748 | (fun [Res_charl s] -> Res_string (Auxl.string_of_char_list s)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl s::_::_ File "new_term_parser.ml", line 761, characters 11-33: 761 | (fun [Res_si s; Res_sil sl] -> Res_sil (s::sl)); ^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_si s::Res_sil sl::_::_ File "new_term_parser.ml", line 767, characters 11-24: 767 | (fun [Res_charl l] -> Res_si (Si_num (Auxl.string_of_char_list l))); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl l::_::_ File "new_term_parser.ml", line 771, characters 11-16: 771 | (fun [rsi] -> rsi); ^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: rsi::_::_ File "new_term_parser.ml", line 794, characters 11-24: 794 | (fun [Res_charl c] -> Res_charl ('_'::c)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl c::_::_ File "new_term_parser.ml", line 796, characters 11-24: 796 | (fun [Res_charl c] -> Res_charl ('\''::c)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl c::_::_ File "new_term_parser.ml", line 831, characters 11-25: 831 | (fun [Res_string s] -> Res_si (Si_var (s, 0))); ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_string s::_::_ File "new_term_parser.ml", line 835, characters 11-25: 835 | (fun [Res_string s] -> Res_si (Si_var (s, -1))); ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_string s::_::_ File "new_term_parser.ml", line 846, characters 18-32: 846 | (fun [_; Res_sil x] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil x::_::_ File "new_term_parser.ml", line 858, characters 18-21: 858 | (fun [x] -> x); ^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::_ File "new_term_parser.ml", line 338, characters 6-23: 338 | let add_greater_prior (i1 : int) (i2 : int) = ^^^^^^^^^^^^^^^^^ Warning 26 [unused-var]: unused variable add_greater_prior. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c term_parser.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c term_parser.ml File "term_parser.ml", lines 1139-1172, characters 2-11: 1139 | ..let Ascii oldopts = pp_ascii_opts_default in 1140 | let opts = Ascii {oldopts with ppa_colour = !Auxl.colour} in 1141 | let sts = parse_complete lookup ntr concrete s in 1142 | let sts = transform sts in 1143 | match sts with ... 1169 | begin 1170 | report_error (Some l) (sstart ^ concat "" intermed); 1171 | St_uninterpreted(l, "multiple parses") 1172 | end Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq {coq_quantified_vars_from_de={ _ }; coq_non_local_hyp_defn={ _ }; coq_non_local_hyp_defn_vars={ _ }; coq_list_types={ _ }; coq_list_aux_defns={defined={ _ }; newly_defined={ _ }}; coq_library={contents=(_, _)}; coq_locally_nameless={ _ }; _ }| Isa {isa_library={contents=(_, _)}; _ }|Hol {hol_library={contents=(_, _)}}| Lem {lem_library={contents=(_, _)}}| Twf {twf_current_defn={ _ }; twf_library={contents=(_, _)}}|Tex { _ }| Caml {caml_library={contents=(_, _)}; _ }| Lex {ppm_caml_opts={caml_library={contents=(_, _)}; _ }; _ }| Menhir {ppm_caml_opts={caml_library={contents=(_, _)}; _ }; _ }) File "term_parser.ml", line 1222, characters 30-48: 1222 | List.map (fun (Ntp.Gtp.Res_st s) -> s) res ^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Res_ignore|Res_none|Res_ste _|Res_stli _|Res_stlil _|Res_char _|Res_charl _| Res_string _|Res_int _|Res_si _|Res_sil _) ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c dependency.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c dependency.ml File "dependency.ml", lines 571-579, characters 2-74: 571 | ..match m with 572 | | Isa io when io.ppi_isa_primrec -> isa_primrec_collapse m xd funcs 573 | | Isa io when not io.ppi_isa_primrec -> isa_fun_collapse m xd funcs 574 | | Hol _ -> hol_collapse m xd funcs 575 | | Lem _ -> lem_collapse m xd funcs 576 | | Coq _ -> coq_collapse m xd funcs 577 | | Twf _ -> twf_collapse m xd funcs 578 | | Caml _ -> caml_collapse m xd funcs 579 | | Tex _ | Ascii _ -> Auxl.error None "internal: collapse of Tex-Ascii\n" Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Isa _|Lex _|Menhir _) (However, some guarded clause may match this value.) File "dependency.ml", lines 584-714, characters 2-53: 584 | ..match m with 585 | | Tex _ | Ascii _ -> Auxl.error None "internal: print of Tex-Ascii\n" 586 | | Isa io -> 587 | let print_lemma block = 588 | if ( List.exists ... 711 | (* (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ "FOO1" ^ h2 ^ "FOO2"^ h3 ^ "FOO3"^s) block))*) 712 | (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ h2 ^ h3 ^ s ^ " end\n") block)) 713 | ^ "\n") in 714 | String.concat "" (List.map print_block sorting) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Lex _|Menhir _) ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c bounds.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c bounds.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c context_pp.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c quotient_rules.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_typecheck.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c grammar_typecheck.ml File "grammar_typecheck.ml", lines 54-56, characters 4-82: 54 | ....match (xs,keys) with 55 | | ([],[]) -> None 56 | | (x::xs, key::keys) -> if (List.mem key keys) then Some x else helper xs keys. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ([], _::_) ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c transform.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c transform.ml File "transform.ml", line 107, characters 6-11: 107 | let id_nt = (id,[]) in ^^^^^ Warning 26 [unused-var]: unused variable id_nt. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c substs_pp.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c substs_pp.ml File "substs_pp.ml", lines 333-336, characters 10-11: 333 | ..........(match m with 334 | | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " list" 335 | | Lem _ -> "list " ^Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr 336 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) File "substs_pp.ml", lines 1400-1412, characters 3-4: 1400 | ...(match m with 1401 | | Caml _ -> 1402 | "(" 1403 | ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 1404 | ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ... 1409 | ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 1410 | ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this 1411 | ^ ")" 1412 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) File "substs_pp.ml", lines 1747-1876, characters 3-8: 1747 | ...( match m with 1748 | | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error (Some p.prod_loc) "pp_fv_symterm_list_body" 1749 | | Isa io when io.ppi_isa_primrec -> 1750 | let args = 1751 | String.concat "_" ... 1873 | ("(flat_map (fun (pat_:"^de1i.de1_coq_type_of_pattern^") => match pat_ with " ^ de1i.de1_pattern ^ " => "^pp_body^" end) " 1874 | ^ de1i.de1_compound_id 1875 | ^ ")"), funcs 1876 | ).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Twf _) (However, some guarded clause may match this value.) File "substs_pp.ml", lines 2030-2033, characters 5-6: 2030 | .....(match m with 2031 | | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that ^ " list" 2032 | | Lem _ -> " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that 2033 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c subrules_pp.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c subrules_pp.ml File "subrules_pp.ml", lines 167-368, characters 8-2: 167 | ........( match m with 168 | | Isa io when io.ppi_isa_primrec -> 169 | let typ = 170 | Auxl.the (Grammar_pp.pp_elements 171 | m xd ((Si_punct "_")::sie) elbu.elb_es true false true true) ^ " list" in ... 365 | [ " %{ TWELF NOT IMPLEMENTED }%"], deps, [] 366 | | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subelement" 367 | 368 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _) (However, some guarded clause may match this value.) File "subrules_pp.ml", line 333, characters 9-13: 333 | let args = ^^^^ Warning 26 [unused-var]: unused variable args. File "subrules_pp.ml", line 453, characters 10-14: 453 | let srln = Grammar_pp.pp_nontermroot_ty m xd srl in ^^^^ Warning 26 [unused-var]: unused variable srln. File "subrules_pp.ml", line 454, characters 10-14: 454 | let srlu = Grammar_pp.pp_nontermroot_ty m xd sru in ^^^^ Warning 26 [unused-var]: unused variable srlu. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c embed_pp.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c embed_pp.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c defns.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c defns.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c ln_transform.ml File "ln_transform.ml", lines 1057-1067, characters 4-7: 1057 | ....match mse with 1058 | | Empty -> 1059 | "0",[] 1060 | | MetaVarExp mv -> 1061 | "1",[] (* FZ is this correct in the general case? *) ... 1064 | | Aux (f1,nt1) -> 1065 | let name = arity_name f1 (Auxl.promote_ntr xd_transformed (Auxl.primary_ntr_of_ntr xd_transformed (fst nt1))) in 1066 | name ^ " " ^ Grammar_pp.pp_nonterm m xd_transformed nt1, 1067 | [name] Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (NonTermExp _|MetaVarListExp (_, _)|NonTermListExp (_, _)|AuxList (_, _, _)) ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c coq_induct.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c coq_induct.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c system_pp.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c system_pp.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c lex_menhir_pp.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c lex_menhir_pp.ml File "lex_menhir_pp.ml", lines 274-285, characters 10-11: 274 | ..........(match ocamllex_hom_opt, ocamllex_remove_hom with 275 | | Some ocamllex_hom, false -> 276 | Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, Some ocamllex_hom, ocamllex_of_string_hom_opt)) 277 | | None, false -> 278 | (* hack: default to ocamllex-remove *) ... 282 | Auxl.error (Some mvd.mvd_loc) ("ocamllex output: both ocamllex and ocamllex-remove hom for "^mvd.mvd_name^"\n") 283 | | None, true -> 284 | Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, None, ocamllex_of_string_hom_opt)) 285 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Some ocamllex_hom, true) File "lex_menhir_pp.ml", line 281, characters 12-36: 281 | | Some ocamllex_hom, false -> ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 11 [redundant-case]: this match case is unused. File "lex_menhir_pp.ml", lines 331-335, characters 13-42: 331 | .............(match ocaml_type with 332 | | "string" -> "" 333 | | "int" -> "int_of_string" 334 | | "float" -> "float_of_string" 335 | | "bool" -> "bool_of_string") Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: "" File "lex_menhir_pp.ml", line 271, characters 11-13: 271 | let hs = List.assoc "ocamllex-remove" mvd.mvd_rep in ^^ Warning 26 [unused-var]: unused variable hs. File "lex_menhir_pp.ml", line 430, characters 56-60: 430 | let menhir_semantic_value_id_of_ntmv ((ntmvr,suffix) as ntmv) = ^^^^ Warning 26 [unused-var]: unused variable ntmv. File "lex_menhir_pp.ml", line 788, characters 16-23: 788 | let m_ocaml = Caml { Types.ppo_include_terminals=false; Types.caml_library = ref ("",[]) } in ^^^^^^^ Warning 26 [unused-var]: unused variable m_ocaml. File "lex_menhir_pp.ml", line 789, characters 16-23: 789 | let m_ascii = Types.error_opts in ^^^^^^^ Warning 26 [unused-var]: unused variable m_ascii. ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c align.mli ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c align.ml ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -c main.ml File "main.ml", line 780, characters 14-27: 780 | let sd_quotiented = Auxl.caml_rename sd in ^^^^^^^^^^^^^ Warning 26 [unused-var]: unused variable sd_quotiented. File "main.ml", line 799, characters 11-24: 799 | let sd_quotiented = Auxl.caml_rename sd in ^^^^^^^^^^^^^ Warning 26 [unused-var]: unused variable sd_quotiented. sed -e 's/__VERSION__/0.33/' \ -e '/__DATE__/r tmp_date.txt' \ -e '/__DATE__/d' version.tex echo Makefile location.cmo types.cmo auxl.cmo merge.cmo global_option.cmo grammar_lexer.cmo grammar_parser.cmo version.cmo grammar_pp.cmo parse_table.cmo glr.cmo new_term_parser.cmo term_parser.cmo dependency.cmo bounds.cmo context_pp.cmo quotient_rules.cmo grammar_typecheck.cmo transform.cmo substs_pp.cmo subrules_pp.cmo embed_pp.cmo defns.cmo ln_transform.cmo coq_induct.cmo system_pp.cmo lex_menhir_pp.cmo align.cmo main.cmo align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex Makefile location.cmo types.cmo auxl.cmo merge.cmo global_option.cmo grammar_lexer.cmo grammar_parser.cmo version.cmo grammar_pp.cmo parse_table.cmo glr.cmo new_term_parser.cmo term_parser.cmo dependency.cmo bounds.cmo context_pp.cmo quotient_rules.cmo grammar_typecheck.cmo transform.cmo substs_pp.cmo subrules_pp.cmo embed_pp.cmo defns.cmo ln_transform.cmo coq_induct.cmo system_pp.cmo lex_menhir_pp.cmo align.cmo main.cmo align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -v The OCaml compiler, version 5.2.0 Standard library directory: /usr/lib/aarch64-linux-gnu/ocaml/5.2.0 ocamlfind ocamlc -package str -package ocamlgraph -linkpkg -g -dtypes -o ott.byt location.cmo types.cmo auxl.cmo merge.cmo global_option.cmo grammar_lexer.cmo grammar_parser.cmo version.cmo grammar_pp.cmo parse_table.cmo glr.cmo new_term_parser.cmo term_parser.cmo dependency.cmo bounds.cmo context_pp.cmo quotient_rules.cmo grammar_typecheck.cmo transform.cmo substs_pp.cmo subrules_pp.cmo embed_pp.cmo defns.cmo ln_transform.cmo coq_induct.cmo system_pp.cmo lex_menhir_pp.cmo align.cmo main.cmo ln -s -f ott.byt ott make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' make -C doc top2.html make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/doc' cp -f top2.mng top2.tex # placeholder for later use of ott as a filter chmod ugo-w top2.tex cd ../src; make tmp_test7_clean.ott make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' rm -f tmp_test7_clean.ott (grep -v ^a | sed -e 's/^r//g' | grep -v ^% ) < ../tests/test7.ott > tmp_test7_clean.ott chmod ugo-w tmp_test7_clean.ott make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' ../src/ott \ -o test7.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testSeven \ -tex_filter ../tests/test7tt.mng test7tt.tex \ ../tests/non_super_tabular.ott ../src/tmp_test7_clean.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 File ../src/tmp_test7_clean.ott on line 23, column 1 - 27: Warning: Free variables in hom element [[typevar]] File ../src/tmp_test7_clean.ott on line 29, column 78 - 104: Warning: Free variables in hom element [[typevar]] Definition rules: 48 good 0 bad Definition rule clauses: 99 good 0 bad ../src/ott -colour true -showraw true \ -o test8.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testEight \ ../tests/non_super_tabular.ott ../tests/test8.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar value_name , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} metavar ident ::= {{ isa string }} {{ coq nat }} {{ hol string }} {{ ocaml int }} {{ lex Alphanum }} metavar integer_literal ::= {{ isa int }} {{ coq nat }} {{ hol num }} {{ ocaml int }} {{ lex numeral }} metavar index , i , j , n , m ::= {{ isa nat }} {{ coq nat }} {{ hol num }} {{ ocaml int }} {{ lex numeral }} grammar typeconstr :: TC_ ::= | unit :: :: unit | bool :: :: bool | int :: :: int typvar , tv :: TV_ ::={{ coq-equality decide equality . apply eq_value_name . }} | ' ident :: :: ident typexpr , t :: TE_ ::= | typvar :: :: var | typexpr -> typexpr' :: :: arrow | typeconstr :: :: constr0 | ( typexpr ) :: S :: paren {{ ich [[typexpr]] }} {{ ocaml [[typexpr]] }} typscheme , ts :: TS_ ::= | ( typvar1 , .. , typvarn ) typexpr :: :: ts (+ bind typvar1..typvarn in typexpr +) | generalise ( G , t ) :: M :: ts3 {{ isa (TS_ts (List . remdups (list_minus (ftv_typexpr [[t]] ) (ftv_G [[G]] ))) [[t]] ) }} {{ coq (TS_ts (remove_duplicates (make_list_typvar (list_minus eq_typvar (ftv_typexpr [[t]] ) (ftv_G [[G]] )))) [[t]] ) }} {{ hol (TS_ts (remove_duplicates (list_minus (ftv_typexpr [[t]] ) (ftv_G [[G]] ))) [[t]] ) }} {{ ocaml TODO }} constant , c :: CONST_ ::= | integer_literal :: :: int | false :: :: false | true :: :: true | () :: :: unit | (&&) :: :: and | not :: :: not expr , e :: E_ ::= | value_name :: :: ident | constant :: :: constant | expr expr' :: :: apply | function value_name -> expr :: :: function (+ bind value_name in expr +) | let value_name = expr in expr' :: :: let (+ bind value_name in expr' +) | ( expr ) :: S :: paren {{ ich [[expr]] }} {{ ocaml [[expr]] }} | { v / x } e :: M :: subst {{ isa subst_expr [[v]] [[x]] [[e]] }} {{ ch (subst_expr [[v]] [[x]] [[e]] ) }} {{ ocaml (subst_expr [[v]] [[x]] [[e]] ) }} value , v :: V_ ::= | constant :: :: constant | function value_name -> expr :: :: function G{{ tex \Gamma }} :: G_ ::= | empty :: :: em | G , value_name : typscheme :: :: vn formula :: formula_ ::= | judgement :: :: judgement | not ( formula ) :: :: not {{ isa Not( [[formula]] ) }} {{ coq not( [[formula]] ) }} {{ hol ~( [[formula]] ) }} {{ ocaml TODO }} | typscheme > t :: :: gen {{ isa ? typvars . ? typexpr . ? s . [[typscheme]] = TS_ts typvars typexpr & typvars=List . map fst s & tsubst_typexpr s typexpr = [[t]] }} {{ coq (exists tvs, exists txp, exists s, [[typscheme]] = TS_ts tvs txp /\ tvs = make_list_typvar (List . map (fun (x:typvar*typexpr) => match x with (x1,x2) => x1 end) s) /\ tsubst_typexpr s txp = [[t]] ) }} {{ hol ? typvars typexpr s . ( [[typscheme]] = TS_ts typvars typexpr ) /\ (typvars=MAP FST s ) /\ (tsubst_typexpr s typexpr = [[t]] ) }} {{ ocaml TODO }} | typscheme = typscheme' :: :: eqt {{ ich [[typscheme]] = [[typscheme']] }} {{ ocaml TODO }} | value_name = value_name' :: :: eqv {{ ich [[value_name]] = [[value_name']] }} {{ ocaml TODO }} terminals :: terminals_ ::= | -> :: :: arrow {{ tex \rightarrow }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} subrules v <:: expr substitutions subst expr value_name tsubst typexpr typvarfreevars ftv typexpr typvarembed {{ coq Fixpoint remove_duplicates (l:list_typvar) : list_typvar := match l with | Nil_list_typvar => Nil_list_typvar | Cons_list_typvar h t => if (list_mem eq_typvar h (unmake_list_typvar t)) then remove_duplicates t else Cons_list_typvar h (remove_duplicates t) end. }} {{ hol val _ = Define ` (remove_duplicates [] = []) /\ (remove_duplicates (x::xs) = if (MEM x xs) then remove_duplicates xs else x::(remove_duplicates xs)) `; }} Defns Jtype :: ::= Defn value_name : typscheme in G :: :: VTSin :: VTSin_ by [[ --------------- :: vn1| value_name : typscheme in G, value_name:typscheme ]] [[ | value_name : typscheme in G | not(value_name = value_name') --------------- :: vn2| value_name : typscheme in G, value_name':typscheme' ]] Defn G |- constant : t :: :: G_constant :: constant_ by [[ --------------- :: int| G |- integer_literal : int ]] [[ --------------- :: false| G |- false : bool ]] [[ --------------- :: true| G |- true : bool ]] [[ --------------- :: unit| G |- () : unit ]] [[ --------------- :: and| G |- (&&) : bool -> ( bool -> bool ) ]] [[ --------------- :: not| G |- not : bool -> bool ]] Defn G |- e : t :: :: Get :: Get_ by [[ | x:typscheme in G | typscheme > t --------------- :: value_name| G |- x:t ]] [[ | :G_constant: G |- constant : t --------------- :: constant| G |- constant : t ]] [[ | G |- e : t1->t2 | G |- e' : t1 --------------- :: apply| G |- e e' : t2 ]] [[ | G,x1: ( ) t1 |- e : t --------------- I :: lambda| G |- function x1->e : t1->t ]] [[ | G |- e : t | G,x:typscheme |- e':t' | typscheme = generalise(G,t) --------------- :: let| G |- let x=e in e' : t' ]] Defns Jop :: JO_ ::= Defn e --> e' :: :: red :: red_ by [[ --------------- :: app| (function x->e) v --> {v/x} e ]] [[ --------------- :: let| let x = v in e --> {v/x} e ]] [[ | e --> e' --------------- :: context_app1| e e1 --> e' e1 ]] [[ | e --> e' --------------- :: context_app2| v e --> v e' ]] [[ | e --> e' --------------- :: context_let| let x=e in e1 --> let x=e' in e1 ]] [[ --------------- :: not_1| not true --> false ]] [[ --------------- :: not_2| not false --> true ]] [[ --------------- :: and_1| ((&&) true) e --> e ]] [[ --------------- :: and_2| ((&&) false) e --> false ]] Definition rules: 22 good 0 bad Definition rule clauses: 36 good 0 bad ../src/ott -colour true -showraw true \ -o test10.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testTen \ -o test10.thy \ -o test10.v \ -o test10Script.sml \ -o test10.lem \ -o test10.ml \ ../tests/non_super_tabular.ott ../tests/test10.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar var , x ::= {{ com term variable }} {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ coq-equality }} {{ ocaml int }} {{ lex alphanum }} {{ tex \mathit { [[var]] } }} grammar term , t :: t_ ::={{ com term }} | x :: :: var {{ com variable }} | \ x . t :: :: lam (+ bind x in t +) {{ com lambda }} | t t' :: :: app {{ com app }} | ( t ) :: S :: paren {{ icho [[t]] }} {{ lem [[t]] }} | { t / x } t' :: M :: sub {{ icho (tsubst_term [[t]] [[x]] [[t']] ) }} {{ lem (tsubst_term [[t]] [[x]] [[t']] ) }} val , v :: v_ ::={{ com value }} | \ x . t :: :: lam {{ com lambda }} terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} subrules val <:: term substitutions tsubst term varDefns Jop :: ::= Defn t1 --> t2 :: :: reduce :: {{ com $ [[t1]] $ reduces to $ [[t2]] $ }} {{ lemwcf witness type reduce_witness; check reduce_check; eval : input -> output }}by [[ --------------- :: ax_app| (\x.t1) v2 --> {v2/x}t1 ]] [[ | t1 --> t1' --------------- :: ctx_app_fun| t1 t --> t1' t ]] [[ | t1 --> t1' --------------- :: ctx_app_arg| v t1 --> v t1' ]] Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad cd ../src; make grammar_parser.tex make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' cat grammar_parser.mly | tr -d \' | grep -v '%start' | grep -v '%type' | sed -e 's/%prec [^ ]*//' > grammar_parser.mly-y2l ../aux/y2l/y2l grammar_parser.mly-y2l -O2 > grammar_parser.tex make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' cp -f ../src/grammar_parser.tex . ../src/ott -colour true -showraw true \ -o test10.meta.tex \ -tex_show_meta true \ -tex_wrap false \ -tex_name_prefix testTenMeta \ ../tests/non_super_tabular.ott ../tests/test10.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar var , x ::= {{ com term variable }} {{ isa string }} {{ coq nat }} {{ hol string }} {{ lem string }} {{ coq-equality }} {{ ocaml int }} {{ lex alphanum }} {{ tex \mathit { [[var]] } }} grammar term , t :: t_ ::={{ com term }} | x :: :: var {{ com variable }} | \ x . t :: :: lam (+ bind x in t +) {{ com lambda }} | t t' :: :: app {{ com app }} | ( t ) :: S :: paren {{ icho [[t]] }} {{ lem [[t]] }} | { t / x } t' :: M :: sub {{ icho (tsubst_term [[t]] [[x]] [[t']] ) }} {{ lem (tsubst_term [[t]] [[x]] [[t']] ) }} val , v :: v_ ::={{ com value }} | \ x . t :: :: lam {{ com lambda }} terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} subrules val <:: term substitutions tsubst term varDefns Jop :: ::= Defn t1 --> t2 :: :: reduce :: {{ com $ [[t1]] $ reduces to $ [[t2]] $ }} {{ lemwcf witness type reduce_witness; check reduce_check; eval : input -> output }}by [[ --------------- :: ax_app| (\x.t1) v2 --> {v2/x}t1 ]] [[ | t1 --> t1' --------------- :: ctx_app_fun| t1 t --> t1' t ]] [[ | t1 --> t1' --------------- :: ctx_app_arg| v t1 --> v t1' ]] Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad ../src/ott -colour true -showraw true \ -o test13.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testThirteen \ ../tests/non_super_tabular.ott ../tests/test13.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar terminal , t ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar metavarroot , mvr ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar nontermroot , ntr ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar suffix , suff ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar auxfn , f ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar prodname , pn ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar index , i , j , n , m ::= {{ isa string }} {{ coq nat }} {{ hol string }} grammar metavar :: mv_ ::= | metavarroot suffix :: :: 1 nonterm :: nt_ ::= | nontermroot suffix :: :: 1 element :: e_ ::= | terminal :: :: tm | metavar :: :: mv | nonterm :: :: nt mse :: mse_ ::= | metavar :: :: mv | nonterm :: :: nt | auxfn ( nonterm ) :: :: f | mse union mse' :: :: union | {} :: :: empty bindspec , bs :: bs_ ::= | bind mse in nonterm :: :: bind | auxfn = mse :: :: auxfn prod{{ hol production }} :: p_ ::= | | element1 .. elementm :: :: prodname (+ bindspec1 .. bindspecn +) :: :: 1 rule :: r_ ::= | nontermroot :: '' ::= prod1 .. prodm :: :: 1 grammar_rules :: g_ ::= | grammar rule1 .. rulem :: :: 1 formula :: formula_ ::= | judgement :: :: judgement terminals :: ::= | {} :: :: quote {{ tex \texttt { \ { \ } } }} | ( :: :: lparen {{ tex \texttt { ( } }} | ) :: :: rparen {{ tex \texttt { ) } }} | (+ :: :: lparenplus {{ tex \texttt { (+ } }} | +) :: :: rparenplus {{ tex \texttt { +) } }} | '' :: :: quotequote {{ tex \texttt { '' } }} | :: :: :: coloncolon {{ tex \texttt { :: } }} | ::= :: :: coloncoloneq {{ tex \texttt { ::= } }} | grammar :: :: tgrammar {{ tex \texttt { grammar } }} | bind :: :: bind {{ tex \texttt { bind } }} | in :: :: in {{ tex \texttt { in } }} | union :: :: union {{ tex \texttt { union } }} ../src/ott -help > options.txt ../src/ott -colour true -showraw true \ -o test10st.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testTenst \ ../tests/non_super_tabular.ott ../tests/test10st.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar termvar , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} {{ tex \mathit { [[termvar]] } }} {{ com term variable }} metavar typvar , X ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lem string }} {{ ocaml int }} {{ tex \mathit { [[typvar]] } }} {{ com type variable }} grammar t :: t_ ::={{ com term }} | x :: :: Var {{ com variable }} | \ x . t :: :: Lam (+ bind x in t +) {{ com abstraction }} | t t' :: :: App {{ com application }} | ( t ) :: S :: paren {{ ichl [[t]] }} {{ ocaml int }} | { t / x } t' :: M :: tsub {{ ichl ( tsubst_t [[t]] [[x]] [[t']] ) }} {{ ocaml int }} v :: v_ ::={{ com value }} | \ x . t :: :: Lam {{ com abstraction }} T :: T_ ::={{ com type }} | X :: :: var {{ com variable }} | T -> T' :: :: arrow {{ com function }} | ( T ) :: S :: paren {{ ichl [[T]] }} {{ ocaml int }} G{{ tex \Gamma }} :: G_ ::={{ isa (termvar*T) list }} {{ coq list (termvar*T) }} {{ ocaml (termvar*T) list }} {{ lem list (termvar*T) }} {{ hol (termvar#T) list }} {{ com type environment }} | empty :: :: em {{ isa Nil }} {{ coq G_nil }} {{ hol [ ] }} {{ lem [ ] }} | G , x : T :: :: vn {{ isa ( [[x]] , [[T]] )# [[G]] }} {{ coq (cons ( [[x]] , [[T]] ) [[G]] ) }} {{ hol (( [[x]] , [[T]] ):: [[G]] ) }} {{ lem (( [[x]] , [[T]] ):: [[G]] ) }} terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} | -> :: :: arrow {{ tex \rightarrow }} | |- :: :: turnstile {{ tex \vdash }} | in :: :: in {{ tex \in }} formula :: formula_ ::= | judgement :: :: judgement | not ( formula ) :: :: not {{ isa (Not [[formula]] )) }} {{ coq (not [[formula]] ) }} {{ hol (~ [[formula]] ) }} {{ lem (not [[formula]] ) }} | x = x' :: :: eqv {{ ichl [[x]] = [[x']] }} | x : T in G :: :: xTG {{ isa ? G1 G2 . [[G]] = G1 @ ( [[x]] , [[T]] )# [[G2]] & [[x]] ~:fst ` set G1 }} {{ coq (bound [[x]] [[T]] [[G]] ) }} {{ lem (bound [[x]] [[T]] [[G]] ) }} {{ hol ? G1 G2 . ( [[G]] = G1 ++ ( [[x]] , [[T]] ):: [[G2]] ) /\ ~(MEM [[x]] (MAP FST G1)) }} embed {{ coq Notation G_nil := (@nil (termvar*T)). Definition bound x T0 G := exists G1, exists G2, (G = List.app G1 (List.cons (x,T0) G2)) /\ ~In x (List.map (@fst termvar T) G1). }} {{ lem let rec bound x t0 g = match g with | (x',t')::g' -> if x=x' then t0=t' else bound x t0 g' | [] -> false end }} subrules v <:: t freevars fv t xsubstitutions tsubst t xDefns Jtype :: ::= Defn G |- t : T :: :: GtT :: GtT_ by [[ | x:T in G --------------- :: value_name| G |- x:T ]] [[ | G |- t : T1->T2 | G |- t' : T1 --------------- :: apply| G |- t t' : T2 ]] [[ | G,x1: T1 |- t : T --------------- :: lambda| G |- \x1.t : T1->T ]] Defns Jop :: ::= Defn t1 --> t2 :: :: reduce :: {{ com $ [[t1]] $ reduces to $ [[t2]] $ }}by [[ --------------- :: ax_app| (\x.t12) v2 --> {v2/x}t12 ]] [[ | t1 --> t1' --------------- :: ctx_app_fun| t1 t --> t1' t ]] [[ | t1 --> t1' --------------- :: ctx_app_arg| v t1 --> v t1' ]] embed {{ coq Hint Constructors reduce GtT : rules. }} File ../tests/test10st.ott on line 55, column 7 - 81: Warning: Free variables in hom element [[G2]] File ../tests/test10st.ott on line 58, column 7 - 92: Warning: Free variables in hom element [[G2]] Definition rules: 6 good 0 bad Definition rule clauses: 12 good 0 bad ../src/ott -colour true -showraw true \ -o test12.thy \ -o test12.v \ ../tests/test12.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 grammar e :: e_ ::= | F f :: :: f | C c :: :: c a :: a_ ::= | B b :: :: b | 0 :: :: 0 b :: b_ ::= | A a :: :: a c :: c_ ::= | A a :: :: a d :: d_ ::={{ isa string }} {{ coq nat }} {{ hol string }} | A a :: :: a f :: f_ ::= | EA e a :: :: ea ../src/ott -colour true -showraw true \ -o test17.10.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testSeventeenTen \ ../tests/non_super_tabular.ott \ ../tests/test17.10.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar typevar , X ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lex Alphanum }} {{ tex \mathit { [[typevar]] } }} {{ com type variable }} {{ isavar '' [[typevar]] '' }} {{ texvar \mathrm { [[typevar]] } }} metavar termvar , x ::= {{ isa string }} {{ coq nat }} {{ hol string }} {{ coq-equality }} {{ lex alphanum }} {{ tex \mathit { [[termvar]] } }} {{ com term variable }} {{ isavar '' [[termvar]] '' }} {{ texvar \mathrm { [[termvar]] } }} metavar label , l , k ::= {{ isa string }} {{ coq nat }} {{ hol string }} {{ lex alphanum }} {{ tex \mathit { [[label]] } }} {{ com field label }} metavar index , i , j , n , m ::= {{ isa nat }} {{ coq nat }} {{ hol num }} {{ lex numeral }} {{ com indices }} grammar T{{ hol Typ }} , S , U :: T_ ::={{ com type }} | X :: :: Var {{ com type variable }} | { l1 : T1 , .. , ln : Tn } :: :: Rec {{ com record }} t :: t_ ::={{ com term }} | x :: :: Var {{ com variable }} | { } :: :: Rec_comp_lu_some {{ com record --- complu with terminal }} | t . l :: :: Proj {{ com projection }} G{{ tex \Gamma }} , D{{ tex \Delta }} :: G_ ::={{ com type environment }} | empty :: :: empty | G , X <: T :: :: type | G , x : T :: :: term | G , G' :: M :: comma {{ ich TODO }} {{ ocaml TODO }} | G1 , .. , Gn :: M :: dots {{ ich TODO }} {{ ocaml TODO }} formula :: formula_ ::= | judgement :: :: judgement | formula1 .. formulan :: :: dots terminals :: terminals_ ::= | |- :: :: turnstile {{ tex \vdash }} | <: :: :: subtype {{ tex <: }} Defns Jtype :: ::= Defn G |- t : T :: :: Ty :: Ty_ {{ com term $ [[t]] $ has type $ [[T]] $ }}by [[ | G|-t1:T1 .. G|-tn:Tn --------------- :: Rcd_dotform| G|- {l1=t1,..,ln=tn}:{l1:T1,..,ln:Tn} ]] [[ | G|- t:{l1:T1,..,ln:Tn} --------------- :: Proj_dotform| G|- t.lj : Tj ]] [[ | --------------- :: Rcd_comp| G|- { }:{ } ]] [[ | G|- t: { } --------------- :: Proj_comp| G|- t.lj : Tj ]] [[ | --------------- :: Rcd_comp_u| G|- { }:{ } ]] [[ | G|- t: { } --------------- :: Proj_comp_u| G|- t.lj : Tj ]] [[ | --------------- :: Rcd_comp_lu| G|- { }:{ } ]] [[ | G|- t: { } --------------- :: Proj_comp_lu| G|- t.lj : Tj ]] [[ | G|- t:{l0:T0,..,ln-1:Tn-1} --------------- :: Proj_dotform_minus| G|- t.lj : Tj ]] [[ | G|- t: { } --------------- :: Proj_comp_lu_minus| G|- t.lj : Tj ]] Definition rules: 10 good 0 bad Definition rule clauses: 20 good 0 bad ../src/ott -alltt test10.0.alltt ../tests/test10.0.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 % minimal metavar termvar, x ::= grammar t :: 't_' ::= | x :: :: Var | \ x . t :: :: Lam | t t' :: :: App | ( t ) :: S:: Paren | { t / x } t' :: M:: Tsub v :: 'v_' ::= | \ x . t :: :: Lam subrules v <:: t defns Jop :: '' ::= defn t1 --> t2 :: ::reduce::'' by -------------------------- :: ax_app (\x.t12) v2 --> {v2/x}t12 t1 --> t1' -------------- :: ctx_app_fun t1 t --> t1' t t1 --> t1' -------------- :: ctx_app_arg v t1 --> v t1' Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad ../src/ott -alltt test10.2.alltt ../tests/test10.2.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 % minimal + latex + comments metavar termvar, x ::= {{ tex \mathit{[[termvar]]} }} grammar t :: 't_' ::= {{ com term }} | x :: :: Var {{ com variable}} | \ x . t :: :: Lam {{ com lambda }} | t t' :: :: App {{ com app }} | ( t ) :: S:: Paren | { t / x } t' :: M:: Tsub v :: 'v_' ::= {{ com value }} | \ x . t :: :: Lam {{ com lambda }} terminals :: 'terminals_' ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} subrules v <:: t defns Jop :: '' ::= defn t1 --> t2 :: ::reduce::'' {{ com $[[t1]]$ reduces to $[[t2]]$}} by -------------------------- :: ax_app (\x.t12) v2 --> {v2/x}t12 t1 --> t1' -------------- :: ctx_app_fun t1 t --> t1' t t1 --> t1' -------------- :: ctx_app_arg v t1 --> v t1' Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad ../src/ott -alltt test10.4.alltt ../tests/test10.4.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 % minimal + binding + subst + coq/hol/isa metavar termvar, x ::= {{ isa string}} {{ coq nat}} {{ hol string}} {{ coq-equality }} grammar t :: 't_' ::= | x :: :: Var | \ x . t :: :: Lam (+ bind x in t +) | t t' :: :: App | ( t ) :: S:: Paren {{ icho [[t]] }} | { t / x } t' :: M:: Tsub {{ icho (tsubst_t [[t]] [[x]] [[t']])}} v :: 'v_' ::= | \ x . t :: :: Lam subrules v <:: t substitutions single t x :: tsubst defns Jop :: '' ::= defn t1 --> t2 :: ::reduce::'' by -------------------------- :: ax_app (\x.t12) v2 --> {v2/x}t12 t1 --> t1' -------------- :: ctx_app_fun t1 t --> t1' t t1 --> t1' -------------- :: ctx_app_arg v t1 --> v t1' Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad ../src/ott -alltt test10.7.alltt ../tests/test10.7.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 % all metavar termvar, x ::= {{ com term variable }} {{ isa string}} {{ coq nat}} {{ hol string}} {{ coq-equality }} {{ ocaml int}} {{ lex alphanum}} {{ tex \mathit{[[termvar]]} }} grammar t :: 't_' ::= {{ com term }} | x :: :: Var {{ com variable}} | \ x . t :: :: Lam (+ bind x in t +) {{ com lambda }} | t t' :: :: App {{ com app }} | ( t ) :: S:: Paren {{ icho [[t]] }} | { t / x } t' :: M:: Tsub {{ icho (tsubst_t [[t]] [[x]] [[t']])}} v :: 'v_' ::= {{ com value }} | \ x . t :: :: Lam {{ com lambda }} terminals :: 'terminals_' ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} subrules v <:: t substitutions single t x :: tsubst defns Jop :: '' ::= defn t1 --> t2 :: ::reduce::'' {{ com $[[t1]]$ reduces to $[[t2]]$}} by -------------------------- :: ax_app (\x.t12) v2 --> {v2/x}t12 t1 --> t1' -------------- :: ctx_app_fun t1 t --> t1' t t1 --> t1' -------------- :: ctx_app_arg v t1 --> v t1' Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad rm -rf README.tex cat ../README.md | sed -e 's/|//g' > README.tmp.md pandoc README.tmp.md -o README.tmp.tex cat README.tmp.tex | sed -e 's/section{Ott}/section{Getting started with Ott (the README)}/g' | sed -e 's/href/ahref/g' | sed -e 's/\\noalign{\\medskip}//g' > README.tex chmod ugo-w README.tex ../src/ott -colour true -showraw true \ -o test10.2.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testTenTwo \ ../tests/non_super_tabular.ott ../tests/test10.2.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{tabular}{llcllllll}#1\end{tabular} } \renewcommand{\[[TEX_NAME_PREFIX]]metavartabular}[1]{\begin{tabular}{ll}#1\end{tabular} } }} metavar termvar , x ::= {{ tex \mathit { [[termvar]] } }} grammar t :: t_ ::={{ com term }} | x :: :: Var {{ com variable }} | \ x . t :: :: Lam {{ com lambda }} | t t' :: :: App {{ com app }} | ( t ) :: S :: Paren | { t / x } t' :: M :: Tsub v :: v_ ::={{ com value }} | \ x . t :: :: Lam {{ com lambda }} terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} subrules v <:: t Defns Jop :: ::= Defn t1 --> t2 :: :: reduce :: {{ com $ [[t1]] $ reduces to $ [[t2]] $ }}by [[ --------------- :: ax_app| (\x.t12) v2 --> {v2/x}t12 ]] [[ | t1 --> t1' --------------- :: ctx_app_fun| t1 t --> t1' t ]] [[ | t1 --> t1' --------------- :: ctx_app_arg| v t1 --> v t1' ]] Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad cat ../tests/test7tt.mng | sed -e 's/\\/BACKSLASH/g' | sed -e 's/{/LEFTBRACKET/g' | sed -e 's/}/\\myrb\{\}/g' | sed -e 's/LEFTBRACKET/\\mylb\{\}/g' | sed -e 's/BACKSLASH/\\mybackslash\{\}/g' | sed -e 's/\[\[/\\mysym{\[\[}/g' | sed -e 's/\]\]/\\mysym{\]\]}/g' | sed -e 's/:concrete:/\\mykw\{:concrete:\}/g' > test7tt.mng.alltt.tex ../src/ott -colour true -showraw true \ -o binding.1.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingOne \ ../tests/squishtex.ott \ ../tests/binding.1.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} metavar value_name , x , f ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} grammar t :: E_ ::= | let rec x = t in t' :: :: letrec (+ bind x in t bind x in t' +) terminals :: terminals_ ::= | -> :: :: arrow {{ tex \rightarrow }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} ../src/ott -colour true -showraw true \ -o binding.2.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingTwo \ ../tests/squishtex.ott \ ../tests/binding.2.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} metavar value_name , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} grammar t :: E_ ::= | x :: :: ident | ( t1 , t2 ) :: :: pair | let p = t in t' :: :: letrec (+ bind binders(p) in t' +) p :: P_ ::= | _ :: :: wildcard (+ binders={} +) | x :: :: ident (+ binders=x +) | ( p1 , p2 ) :: :: pair (+ binders=binders(p1) union binders(p2) +) terminals :: terminals_ ::= | -> :: :: arrow {{ tex \rightarrow }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} ../src/ott -colour true -showraw true \ -o binding.3.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingThree \ ../tests/squishtex.ott \ ../tests/binding.3.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} metavar value_name , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} metavar label , l , k ::= {{ isa string }} {{ coq nat }} {{ hol string }} {{ lex alphanum }} {{ tex \mathit { [[label]] } }} {{ com field label }} {{ isavar '' [[label]] '' }} {{ holvar " [[label]] " }} {{ ocamlvar " [[label]] " }} metavar index , i , j , n , m ::= {{ isa nat }} {{ coq nat }} {{ hol num }} {{ lex numeral }} {{ com indices }} grammar t :: E_ ::= | x :: :: ident | { l1 = t1 , .. , ln = tn } :: :: record | let p = t in t' :: :: let (+ bind b(p) in t' +) p :: P_ ::= | x :: :: ident (+ b=x +) | { l1 = p1 , .. , ln = pn } :: :: record (+ b=b(p1..pn) +) terminals :: terminals_ ::= | -> :: :: arrow {{ tex \rightarrow }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} ../src/ott -colour true -showraw true \ -o binding.4.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingFour \ ../tests/squishtex.ott \ ../tests/binding.4.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} embed {{ tex \newcommand{\[[TEX_NAME_PREFIX]]testterma}{ [[ p1 | p2 ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermb}{ [[ (p1,p2) ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermc}{ [[ let ((None,Some x)|(Some x,None)) = y in (x,x) ]] } }} metavar value_name , x , y ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} grammar t :: E_ ::= | x :: :: ident | ( t1 , t2 ) :: :: pair | None :: :: None | Some p :: :: Some | let p = t in t' :: :: let (+ bind b(p) in t' +) p :: P_ ::= | x :: :: Var (+ b=x +) | ( p1 , p2 ) :: :: pair (+ b=b(p1) union b(p2) +) | p1 | p2 :: :: or (+ b=b(p1) union b(p2) +) | None :: :: None (+ b={} +) | Some p :: :: Some (+ b=b(p) +) | ( p ) :: S :: Paren terminals :: terminals_ ::= | -> :: :: arrow {{ tex \rightarrow }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} ../src/ott -colour true -showraw true \ -o binding.5.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingFive \ ../tests/squishtex.ott \ ../tests/binding.5.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} embed {{ tex \newcommand{\[[TEX_NAME_PREFIX]]testterma}{ [[ :J_type: empty, X<:Top, Y<:X->X, x:X, y:Y |- y x : X ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermb}{ [[ :Jb_type: empty, X<:Top, Y<:X->X, x:X, y:Y |- y x : X ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermc}{ [[ :Gb_term: empty, X<:Top, Y<:X->X, x:X, y:Y ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermC}{ [[ :Gb_term: empty, W<:Top, Y<:W->W, x:W, y:Y ]] } \newcommand{\[[TEX_NAME_PREFIX]]testtermd}{ [[ :Jc_type: Gc |- t : T ]] } \newcommand{\[[TEX_NAME_PREFIX]]testterme}{ [[ Gc ]] } }} metavar typevar , X ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex Alphanum }} metavar termvar , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} {{ lex alphanum }} grammar T :: T_ ::= | X :: :: T_Var | Top :: :: T_Top | T -> T' :: :: T_Fun | Forall X <: T . T' :: :: T_Forall (+ bind X in T' +) t :: t_ ::= | x :: :: Var | \ x : T . t :: :: Lam (+ bind x in t +) | t t' :: :: App | \ X <: T . t :: :: TLam (+ bind X in t +) | t [ T ] :: :: TApp | let p = t in t' :: :: Let (+ bind bo(p) in t' +) p :: p_ ::= | x : T :: :: Var (+ bo=x +) G{{ tex \Gamma }} :: G_ ::= | empty :: :: empty (+ Tdom={} tdom={} +) | G , X <: T :: :: type (+ Tdom=Tdom(G) union X tdom=tdom(G) +) | G , x : T :: :: term (+ Tdom=Tdom(G) tdom=tdom(G) union x +) J :: J_ ::= | G |- T <: T' :: :: subtype | G |- t : T :: :: type | t --> t' :: :: red Gb{{ tex \Gamma^b }} :: Gb_ ::= | empty :: :: empty (+ Tdom={} tdom={} +) | Gb , X <: T :: :: type (+ Tdom=Tdom(Gb) union X tdom={} bind Tdom(Gb) in T +) {{ tex [[Gb]] ,\, [[X]] [[<:]] [[T]] }} | Gb , x : T :: :: term (+ Tdom=Tdom(Gb) tdom=tdom(Gb) union x bind Tdom(Gb) in T +) {{ tex [[Gb]] ,\, [[x]] [[:]] [[T]] }} Jb :: Jb_ ::= | Gb |- T <: T' :: :: subtype (+ bind Tdom(Gb) in T bind Tdom(Gb) in T' +) | Gb |- t : T :: :: type (+ bind Tdom(Gb) in t bind Tdom(Gb) in T bind tdom(Gb) in t +) | t --> t' :: :: red Gc{{ tex \Gamma }} :: Gc_ ::= | empty :: :: empty | Gc , X <: T :: :: type {{ tex [[Gc]] ,\, [[X]] [[<:]] [[T]] }} | Gc , x : T :: :: term {{ tex [[Gc]] ,\, [[x]] [[:]] [[T]] }} Jc :: Jc_ ::= | Gc |- t : T :: :: type terminals :: terminals_ ::= | -> :: :: arrow {{ tex \mathord { \rightarrow } }} | : :: :: colon {{ tex \mathord { : } }} | function :: :: function {{ tex \textbf { function } }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | { :: :: leftbrace {{ tex \ { }} | } :: :: rightbrace {{ tex \ } }} | \ :: :: lam {{ tex \lambda }} | Forall :: :: forall {{ tex \forall }} | empty :: :: empty {{ tex \varnothing }} ../src/ott -alltt binding.6.alltt.tex ../tests/binding.6.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 metavar label, l ::= {{ hol string }} {{ coq nat }} indexvar index, n ::= {{ hol num }} {{ coq nat }} grammar term, t :: 't_' ::= | { l1 = t1 , .. , ln = tn } :: :: record ../src/ott -colour true -showraw true \ -o binding.6b.tex \ -o binding.6bScript.sml \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix bindingSixb \ ../tests/squishtex.ott \ ../tests/binding.6.ott \ ../tests/binding.6b.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} metavar label , l ::= {{ hol string }} {{ coq nat }} metavar index , n ::= {{ hol num }} {{ coq nat }} grammar term , t :: t_ ::= | { l1 = t1 , .. , ln = tn } :: :: record grammar T{{ hol Typ }} , S , U :: T_ ::={{ com type }} | { l1 : T1 , .. , ln : Tn } :: :: Rec {{ com record }} G{{ tex \Gamma }} , D{{ tex \Delta }} :: G_ ::={{ com type environment }} | empty :: :: empty formula :: formula_ ::= | judgement :: :: judgement | formula1 .. formulan :: :: dots terminals :: terminals_ ::= | \ :: :: lambda {{ tex \lambda }} | -> :: :: arrow {{ tex \rightarrow }} | => :: :: Arrow {{ tex \Rightarrow }} | |- :: :: turnstile {{ tex \vdash }} | --> :: :: red {{ tex \longrightarrow }} | Forall :: :: forall {{ tex \forall }} | <: :: :: subtype {{ tex <: }} | |-> :: :: mapsto {{ tex \mapsto }} | = :: :: eq {{ tex \!\! = \!\! }} | : :: :: colon {{ tex \!\! : \!\! }} Defns Jtype :: ::= Defn G |- t : T :: :: Ty :: Ty_ {{ com term [[t]] has type [[T]] }}by [[ | G|-t0:T0 .. G|-tn-1:Tn-1 --------------- :: Rcd| G|- {l0=t0,..,ln-1=tn-1}:{l0:T0,..,ln-1:Tn-1} ]] Definition rules: 1 good 0 bad Definition rule clauses: 2 good 0 bad ../src/ott -alltt test11.alltt ../tests/test11.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 metavar termvar , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }} grammar t :: 't_' ::= | x :: :: Var | \ x . t :: :: Lam (+ bind x in t +) | t t' :: :: App | Foo v :: :: Foo v :: 'v_' ::= | \ x . t :: :: Lam subrules v <:: t defns Jb :: '' ::= defn Baz t , v :: :: Baz :: '' by --------- :: ax Baz t , v Definition rules: 1 good 0 bad Definition rule clauses: 1 good 0 bad ../src/ott -alltt test10_homs.alltt ../tests/test10_homs.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 metavar termvar , x ::= {{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ lex alphanum }} {{ tex \mathit{[[termvar]]} }} {{ com term variable }} grammar t :: 't_' ::= {{ com term }} | x :: :: Var | \ x . t :: :: Lam | t t' :: :: App | ( t ) :: S :: paren | { t / x } t' :: M :: tsub v :: 'v_' ::= {{ com value }} | \ x . t :: :: Lam terminals :: 'terminals_' ::= | \ :: :: lambda {{ tex \lambda }} | --> :: :: red {{ tex \longrightarrow }} homs 't_' :: Lam (+ bind x in t +) homs 't_' :: Var {{ com variable }} :: Lam {{ com abstraction }} :: App {{ com application }} :: paren {{ ich [[t]] }} :: tsub {{ ich ( tsubst_t [[t]] [[x]] [[t']] ) }} homs '' :: reduce {{ com $[[t1]]$ reduces to $[[t2]]$ }} subrules v <:: t substitutions single t x :: tsubst defns Jop :: '' ::= defn t1 --> t2 :: :: reduce :: '' by -------------------------- :: ax_app (\x.t12) v2 --> {v2/x}t12 t1 --> t1' -------------- :: ctx_app_fun t1 t --> t1' t t1 --> t1' -------------- :: ctx_app_arg v t1 --> v t1' Definition rules: 3 good 0 bad Definition rule clauses: 5 good 0 bad cat grammar_parser.tex | sed -e 's/longtable/tabular/g' > grammar_parser_hevea.tex ../src/ott -alltt squishtex.hand.alltt.tex squishtex.hand.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1] {\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3] {$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6] { \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule} {\\[2.0mm]} }} ../src/ott -colour true -showraw true \ -o test13d.tex \ -tex_show_meta false \ -tex_wrap false \ -tex_name_prefix testThirteend \ ../tests/squishtex.ott \ ../tests/test13d.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 embed {{ tex-preamble \renewcommand{\[[TEX_NAME_PREFIX]]grammartabular}[1]{\begin{minipage}{\columnwidth}\begin{tabular}{ll}#1\end{tabular}\end{minipage} } \renewcommand{\[[TEX_NAME_PREFIX]]rulehead}[3]{$#1$ $#2$ & $#3$} \renewcommand{\[[TEX_NAME_PREFIX]]prodline}[6]{ \quad $#1$ \ $#2$ & \quad $#3 #4$ $#5$ $#6$} \renewcommand{\[[TEX_NAME_PREFIX]]interrule}{\\[2.0mm]} }} metavar terminal , tm ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar metavarroot , mvr ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar nontermroot , ntr ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar suffix , suff ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar variable , var ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar auxfn , f ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar prodname , pn ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar index , i , j , k , l , m , n , o , q , jp{{ tex \mbox { $\scriptstyle j'$ } }} , qp{{ tex \mbox { $\scriptstyle q'$ } }} , np{{ tex \mbox { $\scriptstyle n'$ } }} , op{{ tex \mbox { $\scriptstyle o'$ } }} , mp{{ tex \mbox { $\scriptstyle m'$ } }} , ip{{ tex \mbox { $\scriptstyle i'$ } }} ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar defnclassname , dcn ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar defnname , dn ::= {{ isa string }} {{ coq nat }} {{ hol string }} metavar defnrulename , drn ::= {{ isa string }} {{ coq nat }} {{ hol string }} grammar metavar , mv :: mv_ ::= | metavarroot suffix :: :: 1 nonterm , nt :: nt_ ::= | nontermroot suffix :: :: 1 element , e :: e_ ::= | terminal :: :: tm | metavar :: :: mv | nonterm :: :: nt metavar_set_expression , mse :: mse_ ::= | metavar :: :: mv | auxfn ( nonterm ) :: :: f {{ tex [[auxfn]] \texttt { ( } [[nonterm]] \texttt { ) } }} | mse union mse' :: :: union | {} :: :: empty bindspec , bs :: bs_ ::= | bind mse in nonterm :: :: bind | auxfn = mse :: :: auxfn prod , p :: p_ ::= | | element1 .. elementm :: :: prodname (+ bs1 .. bsn +) :: :: 1 rule , r :: r_ ::= | nontermroot :: '' ::= prod1 .. prodm :: :: 1 grammar_rules , g :: g_ ::= | grammar rule1 .. rulem :: :: 1 auxfn_type , at :: at_ ::= | nontermroot1 .. nontermrootn -> metavarroot :: :: 1 auxfn_type_env , Phi{{ tex \Phi }} :: ate_ ::= | empty :: :: 1 | Phi , auxfn : auxfn_type :: :: 2 grammar_type , G{{ tex \Gamma }} :: gt_ ::= | nontermroot1 .. nontermrootn :: :: 1 concrete_abstract_syntax_term , cast :: cast_ ::= | var : mvr :: :: 1 | prodname ( cast1 , .. , castm ) :: :: 2 cast_type , ct :: cast_type_ ::= | ntr :: :: 1 | mvr :: :: 2 substitution , s :: subst_ ::={{ isa (concrete_abstract_syntax_term*variable*metavarroot) list }} | { cast1 / var1 : mvr1 , .. , castn / varn : mvrn } :: :: 1 {{ isa [[ ( cast1 , var1 , mvr1 ) .. ( castn , varn , mvrn ) ]] }} | filter var_set from s :: M :: 2 {{ isa filter (% x . not x: [[var_set]] ) [[s]] }} {{ coq TODO }} symterm , st :: st_ ::= | stnb :: :: 1 | nonterm :: :: 2 symterm_node_body , stnb :: stnb_ ::= | prodname ( ste1 , .. , stem ) :: :: 1 symterm_element , ste :: ste_ ::= | st :: :: symterm | metavar :: :: metavar | var : mvr :: :: variable ntmv :: ntmv_ ::= | nt :: :: 1 | mv :: :: 2 ntmv_list :: ntmv_list_ ::={{ isa ntmv list }} | ntmv1 , .. , ntmvn :: :: 1 {{ isa [[ntmv1 ..ntmvn ]] }} | remove_terminals ( e1 .. en ) :: M :: 2 {{ isa SOME l . ( [[e1..en]] , l ) \ remove_terminals2 }} {{ coq TODO }} | [] :: M :: 4 {{ isa Nil }} {{ coq TODO }} | ntmv , ntmv_list :: M :: 3 {{ isa ( [[ntmv]] ) # ( [[ntmv_list]] ) }} {{ coq TODO }} var_set :: var_set_ ::={{ isa (variable*metavarroot) set }} | {} :: M :: 1 {{ ich { } }} | { var : mvr } :: M :: 2 {{ ich { ( [[var]] , [[mvr]] ) } }} | union { var_set | formula } :: M :: 3 {{ ich Union { [[var_set]] | [[formula]] } }} | var_set union var_set' :: M :: 3_5 {{ ich ( [[var_set]] ) Un ( [[var_set']] ) }} | [| mse |] g ( cast ) :: M :: 4 {{ ich SOME var_set . ( [[mse]] , [[g]] , [[cast]] , var_set) \ interp_mse }} | var_set - var_set' :: M :: 5 {{ ich [[var_set]] - [[var_set']] }} | union { } :: M :: 6 {{ ich Union ( set [[ ]] ) }} formula :: formula_ ::= | judgement :: :: judgement | formula1 ... formulan :: :: dots | i = j :: :: ieq {{ ic [[i]] = [[j]] }} | f = f' :: :: feq {{ ic [[f]] = [[f']] }} | mvr = mvr' :: :: mvreq {{ ic [[mvr]] = [[mvr']] }} | ntr = ntr' :: :: ntreq {{ ic [[ntr]] = [[ntr']] }} | var = var' :: :: vareq {{ ic [[var]] = [[var']] }} | mv = mv' :: :: mveq {{ ic [[mv]] = [[mv']] }} | nt = nt' :: :: nteq {{ ic [[nt]] = [[nt']] }} | ntmv = ntmv' :: :: ntmveq {{ ic [[ntmv]] = [[ntmv']] }} | e = e' :: :: eeq {{ ic [[e]] = [[e']] }} | mse = mse' :: :: mseeq {{ ic [[mse]] = [[mse']] }} | bs = bs' :: :: bseq {{ ic [[bs]] = [[bs']] }} | p = p' :: :: peq {{ ic [[p]] = [[p']] }} | r = r' :: :: req {{ ic [[r]] = [[r']] }} | g = g' :: :: geq {{ ic [[g]] = [[g']] }} | var_set = var_set' :: :: var_seteq {{ ic [[var_set]] = [[var_set']] }} | cast = cast' :: :: casteq {{ ic [[cast]] = [[cast']] }} | s = s' :: :: seq {{ ic [[s]] = [[s']] }} | ( formula ) :: :: paren {{ ic ( [[formula]] ) }} | not formula :: :: not {{ isa Not( [[formula]] ) }} | forall i isin 1 -- m . formula :: :: forall {{ tex \forall [[i]] \in 1 .. [[m]] . [[formula]] }} {{ isa (! [[i]] . ((1::nat)<= [[i]] & [[i]] <= [[m]] ) --> [[formula]] ) }} | exists i isin 1 -- m . formula :: :: exists {{ tex \exists [[i]] \in 1 .. [[m]] . [[formula]] }} {{ isa (? [[i]] . ((1::nat)<= [[i]] & [[i]] <= [[m]] ) --> [[formula]] ) }} | existsuniq i isin 1 -- m . formula :: :: existsuni {{ tex \exists ! [[i]] \in 1 .. [[m]] . [[formula]] }} {{ isa (? [[i]] . ((1::nat)<= [[i]] & [[i]] <= [[m]] ) --> [[formula]] ) }} | exists nt . formula :: :: existsnt {{ tex \exists [[nt]] . [[formula]] }} {{ isa (? [[nt]] . [[formula]] ) }} | exists var:mvr . formula :: :: existsvar {{ tex \exists [[var:mvr]] . [[formula]] }} {{ isa (? [[var]] [[mvr]] . [[formula]] ) }} | formula /\ formula' :: :: and {{ isa ( [[formula]] & [[formula']] ) }} | formula => formula' :: :: implies {{ isa ( [[formula]] --> [[formula']] ) }} | true :: :: true {{ isa True }} | j INDEXES p1 .. pm :: :: Indexesp {{ coq (1 <= [[j]] /\ [[j]] <= length (unmake_list'p [[p1..pm]] )) }} {{ hol (1 <= [[j]] /\ [[j]] <= LENGTH [[p1..pm]] ) }} {{ isa (1 <= [[j]] & [[j]] <= length [[p1..pm]] ) }} terminals :: ::= | {} :: :: quote {{ tex \texttt { \ { \ } } }} | (+ :: :: lparenplus {{ tex \texttt { (+ } }} | +) :: :: rparenplus {{ tex \texttt { +) } }} | '' :: :: quotequote {{ tex \texttt { '' } }} | :: :: :: coloncolon {{ tex \texttt { :: } }} | ::= :: :: coloncoloneq {{ tex \texttt { ::= } }} | grammar :: :: tgrammar {{ tex \texttt { grammar } }} | bind :: :: bind {{ tex \texttt { bind } }} | in :: :: in {{ tex \texttt { in } }} | union :: :: union {{ tex \texttt { union } }} | -> :: :: arrow {{ tex \rightarrow }} | => :: :: AArrow {{ tex \Rightarrow }} | |- :: :: turnstile {{ tex \vdash }} | /\ :: :: wedge {{ tex { \scriptsize\wedge } }} | \/ :: :: vee {{ tex { \scriptsize\vee } }} | | :: :: bar {{ tex \texttt { | } }} | defns :: :: tdefns {{ tex \texttt { defns } }} | defn :: :: tdefn {{ tex \texttt { defn } }} | isin :: :: isin {{ tex \in }} Defns Jtype :: ::= Defn Phi |- f : at :: :: FF :: FF_ by [[ --------------- :: 1| Phi,f:at |- f : at ]] [[ | Phi |- f : at | not (f=f') --------------- :: 2| Phi,f':at' |- f:at ]] Defn Phi ; e1 .. en |- mse : metavarroot :: :: Mse :: Mse_ by [[ --------------- :: 1| Phi;e1..en |- {} : mvr ]] [[ | ej = mvr suff --------------- :: 2| Phi;e1..en |- mvr suff : mvr ]] [[ | Phi |- f : ntr1 .. ntrm -> mvr | ej = nt | :formula_nteq: nt = ntri suff --------------- :: 3| Phi;e1..en |- f(nt) : mvr ]] [[ | Phi;e1..en |- mse : mvr | Phi;e1..en |- mse' : mvr --------------- :: 4| Phi;e1..en |- mse union mse' : mvr ]] Defn Phi ; e1 .. en |- bs ok :: :: Bs :: Bs_ by [[ | Phi;e1..en |- mse : mvr | existsuniq j isin 1 -- n . ej=nt --------------- :: 1| Phi;e1..en |- bind mse in nt ok ]] [[ | Phi;e1..en |- mse : mvr | Phi |- f : ntr1..ntrn -> mvr --------------- :: 2| Phi;e1..en |- f=mse ok ]] Defn Phi |- prod ok :: :: Prod :: Prod_ by [[ | forall i isin 1--m. Phi;e1..en |- bsi ok | prod = | e1..en :: :: prodname (+ bs1..bsm +) --------------- :: 1| Phi |- prod ok ]] Defn Phi |- rule ok :: :: Rule :: Rule_ by [[ | forall i isin 1--m. Phi |- prodi ok | rule = ntr :: '' ::= prod1..prodm --------------- :: 1| Phi |- rule ok ]] Defn Phi |- grammar_rules ok :: :: Grammar :: Grammar_ by [[ | forall i isin 1--m. Phi |- rulei ok | grammar_rules = grammar rule1..rulem | forall i isin 1--m. forall j isin 1--n. ((rulei=ntr :: '' ::= prod1..prodm /\ rulej=ntr :: '' ::= prod1'..prodn') => i=j) --------------- :: 1| Phi |- grammar_rules ok ]] [[ ]] [[ ]] Defn remove_suffix ( ntmv ) = ct :: :: remove_suffix :: remove_suffix_ by [[ --------------- :: 1| remove_suffix(ntr suff) = ntr ]] [[ --------------- :: 2| remove_suffix(mvr suff) = mvr ]] [[ ]] Defn remove_terminals ( e1 .. en ) = ntmv_list :: :: remove_terminals2 :: remove_terminals2_ by [[ --------------- :: 1| remove_terminals() = [] ]] [[ | remove_terminals(e1..en) = ntmv_list --------------- :: 2| remove_terminals(tm e1..en) = ntmv_list ]] [[ | remove_terminals(e1..en) = ntmv_list --------------- :: 3| remove_terminals(nt e1..en) = nt,ntmv_list ]] [[ | remove_terminals(e1..en) = ntmv_list --------------- :: 4| remove_terminals(mv e1..en) = mv,ntmv_list ]] Defn p isin g ( ntr ) :: :: lookup_p :: lookup_p_ by [[ | g = grammar r1 .. rl | ri = ntr :: '' ::= p1 .. pm | j INDEXES p1 .. pm --------------- :: 2| pj isin g ( ntr ) ]] Defn g |- cast : cast_type :: :: cast_ty :: cast_ty_ by [[ --------------- :: 1| g |- var : mvr : mvr ]] [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr) | remove_terminals(e1..en) = ntmv1,..,ntmvq | remove_suffix(ntmv1)=ct1 .. remove_suffix(ntmvq)=ctq | g |- cast1 : ct1 .. g |- castq : ctq --------------- :: 2| g |- pn(cast1,..,castq) : ntr ]] Defn [| mse |] g ( cast ) => var_set :: :: interp_mse :: interp_mse_ by [[ --------------- :: 1| [| {} |]g (cast) => {} ]] [[ | [| mse |] g (cast) => var_set | [| mse' |] g (cast) => var_set' --------------- :: 2| [| mse union mse' |]g (cast) => var_set union var_set' ]] [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr) | remove_terminals(e1..en) = ntmv1,..,ntmvq | ntmvl = nt | :formula_nteq: nt = ntr' suff' | castl = pn' (cast'1, .. , cast'qp) | | e'1 .. e'np :: :: pn' (+ bs'1 .. bs'op +) isin g(ntr') | bs'k = f=mse' | [|mse'|]g(castl) => var_set --------------- :: 3| [| f(nt) |]g(pn(cast1,..,castq)) => var_set ]] [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr) | remove_terminals(e1..en) = ntmv1,..,ntmvq | ntmvl = mv | castl = var':mvr' --------------- :: 4| [| mv |]g(pn(cast1,..,castq)) => {var':mvr'} ]] Defn var : mvr in dom ( s ) :: :: indom :: indom_ by [[ --------------- :: 1| var:mvr in dom ({, cast/var:mvr, }) ]] Defns Jsubst_fv :: ::= Defn subst s in cast = cast'' :: :: subst :: subst_ by [[ --------------- :: 1| subst {, cast/var:mvr, } in pn(var:mvr) = cast ]] [[ | not(var:mvr in dom (s)) --------------- :: 2| subst s in pn(var:mvr) = pn(var:mvr) ]] [[ --------------- :: 0| subst s in var:mvr = var:mvr ]] [[ | cast = pn() | not(exists var:mvr. cast = pn (var:mvr) ) | | e1 .. en :: :: pn (+ bs1 .. bsm +) isin g(ntr) | remove_terminals(e1..en) = | | | cast' = pn() --------------- :: 3| subst s in cast = cast' ]] [[ ]] Defn fv ntr mvr of cast = var_set :: :: fv :: fv_ by [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr') | not (ntr = ntr') --------------- :: 1| fv ntr mvr of pn(var:mvr) = {} ]] [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr) | not (mvr = mvr') --------------- :: 1_5| fv ntr mvr of pn(var:mvr') = {} ]] [[ | | e1 .. en :: :: pn (+ bs1 .. bso +) isin g(ntr) --------------- :: 2| fv ntr mvr of pn(var:mvr) = { var:mvr } ]] [[ --------------- :: 0| fv ntr mvr of var:mvr = {} ]] [[ | cast = pn() | not(exists var:mvr. cast = pn (var:mvr) ) | | e1 .. en :: :: pn (+ bs1 .. bsm +) isin g(ntr) | remove_terminals(e1..en) = | | | var_set = union {} --------------- :: 3| fv ntr mvr of cast = var_set ]] File ../tests/test13d.ott on line 168, column 31 - 72: Warning: Free variables in hom element [[var]] File ../tests/test13d.ott on line 168, column 31 - 72: Warning: Free variables in hom element [[mvr]] Definition rules: 34 good 0 bad Definition rule clauses: 97 good 0 bad cat test10.v | sed -e 's/\n\n/\n/g' > test10.despaced.v ../src/ott -alltt test21.1.alltt ../tests/test21.1.ott Ott version 0.33 distribution of Mon 16 Jan 15:32:01 GMT 2023 metavar n ::= grammar e :: e_ ::= | n :: :: num | - e :: :: neg | e1 + e2 :: :: add | e1 - e2 :: :: sub | e1 e2 :: :: mul | e1 / e2 :: :: div | e1 , .. , e2 :: :: tup | ( e ) :: M :: par {{ icho [[e]] }} parsing e_add left e_add % #1 e_sub left e_sub e_add left e_sub % #3 e_sub left e_add e_mul left e_mul e_div left e_div e_mul left e_div e_div left e_mul e_neg <= e_add % #9 e_neg <= e_sub e_neg <= e_mul e_neg <= e_div e_neg <= e_tup e_add <= e_div e_add <= e_mul % #15 e_add <= e_tup e_sub <= e_div e_sub <= e_mul e_sub <= e_tup e_mul <= e_tup % #20 e_div <= e_tup hevea -fix top2 Exclude comment 'comment' ./top2.tex:28: Warning: Command not found: \geometry ./top2.tex:126: Warning: \today needs '-exec xxdate.exe' option ./top2.tex:159: Warning: Undefined citation: 'ott-jfp' ./top2.tex:164: Warning: Undefined citation: 'ott-sub' ./top2.tex:176: Warning: Undefined citation: 'Pierce:TypeSystems' ./top2.tex:177: Warning: Undefined citation: 'poplmark' ./top2.tex:178: Warning: Undefined citation: 'Leroy-generativity' ./top2.tex:180: Warning: Undefined citation: 'ljam-sub' ./README.tex:197: Warning: Command not found: \noalign ./README.tex:197: Warning: Command not found: \noalign ./README.tex:197: Warning: Command not found: \noalign ./README.tex:211: Warning: Command not found: \Shaded ./README.tex:212: Warning: Command not found: \Highlighting ./README.tex:213: Warning: Command not found: \NormalTok ./README.tex:214: Warning: Command not found: \NormalTok ./README.tex:214: Warning: Command not found: \textquotesingle ./README.tex:215: Warning: Command not found: \endHighlighting ./README.tex:216: Warning: Command not found: \endShaded ./README.tex:222: Warning: Command not found: \Shaded ./README.tex:223: Warning: Command not found: \Highlighting ./README.tex:224: Warning: Command not found: \NormalTok ./README.tex:225: Warning: Command not found: \NormalTok ./README.tex:225: Warning: Command not found: \textquotesingle ./README.tex:226: Warning: Command not found: \NormalTok ./README.tex:226: Warning: Command not found: \textquotesingle ./README.tex:227: Warning: Command not found: \endHighlighting ./README.tex:228: Warning: Command not found: \endShaded ./README.tex:287: Warning: Command not found: \noalign ./README.tex:287: Warning: Command not found: \noalign ./README.tex:287: Warning: Command not found: \noalign ./top2.tex:232: Warning: Undefined label: 'a45' ./top2.tex:240: Warning: minipage, output may be poor ./top2.tex:312: Warning: Undefined label: 'a61' ./top2.tex:364: Warning: Undefined label: 'a53' ./top2.tex:398: Warning: Undefined label: 'a45' ./top2.tex:437: Warning: Undefined label: 'a17' ./top2.tex:451: Warning: Undefined label: 'a46' ./top2.tex:451: Warning: Undefined label: 'a49' ./top2.tex:458: Warning: minipage, output may be poor ./top2.tex:515: Warning: Undefined label: 'a49' ./top2.tex:640: Warning: Undefined label: 'a60' ./top2.tex:655: Warning: Undefined label: 'a51' ./top2.tex:655: Warning: Undefined label: 'a45' ./top2.tex:656: Warning: Undefined label: 'a47' ./top2.tex:662: Warning: Undefined label: 'a6' ./top2.tex:662: Warning: Undefined label: 'a5' ./top2.tex:662: Warning: Undefined label: 'a40' ./top2.tex:668: Warning: minipage, output may be poor ./top2.tex:704: Warning: Undefined label: 'a62' ./top2.tex:747: Warning: minipage, output may be poor ./top2.tex:755: Warning: minipage, output may be poor ./top2.tex:762: Warning: minipage, output may be poor ./top2.tex:865: Warning: Undefined label: 'a19' ./top2.tex:883: Warning: Undefined label: 'a61' ./top2.tex:897: Warning: Undefined label: 'a5' ./top2.tex:928: Warning: Undefined label: 'a6' ./top2.tex:1155: Warning: Undefined label: 'a54' ./top2.tex:1166: Warning: Undefined label: 'a46' ./top2.tex:1167: Warning: Undefined label: 'a51' ./top2.tex:1167: Warning: Undefined label: 'a58' ./top2.tex:1184: Warning: Undefined label: 'a56' ./top2.tex:1197: Warning: Undefined label: 'a46' ./top2.tex:1204: Warning: Undefined label: 'a59' ./top2.tex:1208: Warning: Undefined label: 'a22' ./top2.tex:1214: Warning: minipage, output may be poor ./top2.tex:1221: Warning: minipage, output may be poor ./top2.tex:1359: Warning: Undefined label: 'a56' ./top2.tex:1359: Warning: Undefined label: 'a55' ./top2.tex:1423: Warning: Undefined label: 'a47' ./top2.tex:1524: Warning: Undefined label: 'a13' ./top2.tex:1606: Warning: Undefined label: 'a61' ./top2.tex:1627: Warning: Undefined citation: 'FGLMR96' ./top2.tex:1851: Warning: Undefined label: 'a63' ./top2.tex:2184: Warning: Undefined label: 'a64' ./top2.tex:2451: Warning: Undefined label: 'a66' ./top2.tex:2905: Warning: Undefined label: 'parsing_figure' ./top2.tex:2928: Warning: '_' occurring outside math mode ./top2.tex:2964: Warning: Undefined label: 'a12' ./top2.tex:2966: Warning: Undefined citation: 'Pierce:TypeSystems' ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2973: Warning: minipage, output may be poor ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2977: Warning: Undefined citation: 'LevinPierce99' ./top2.tex:3012: Warning: Undefined label: 'a38' ./top2.tex:3014: Warning: Undefined label: 'a68' ./top2.tex:3019: Warning: minipage, output may be poor ./top2.tex:3186: Warning: Undefined label: 'a51' ./top2.tex:3187: Warning: Undefined label: 'a61' ./top2.tex:3190: Warning: Undefined label: 'a19' ./top2.tex:3367: Warning: Undefined label: 'a56' ./top2.tex:3574: Warning: Undefined label: 'a43' ./grammar_parser_hevea.tex:12: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:17: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:22: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:27: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:32: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:37: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:42: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:47: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:52: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:57: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:62: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:67: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:72: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:77: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:82: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:87: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:92: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:97: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:102: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:107: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:112: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:117: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:122: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:127: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:132: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:137: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:142: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:147: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:152: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:157: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:162: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:167: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:172: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:177: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:182: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:187: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:192: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:197: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:202: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:207: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:212: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:217: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:222: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:227: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:232: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:237: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:242: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:247: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:252: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:257: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:262: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:267: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:272: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:277: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:282: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:287: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:292: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:297: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:302: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:307: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:312: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:317: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:322: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:327: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:332: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:337: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:342: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:347: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:352: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:357: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:362: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:367: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:372: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:377: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:382: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:387: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:392: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:397: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:402: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:407: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:412: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:417: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:422: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:427: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:432: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:437: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:442: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:447: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:452: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:457: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:462: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:467: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:472: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:477: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:482: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:487: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:492: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:497: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:502: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:507: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:512: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:517: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:522: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:527: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:532: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:537: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:542: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:547: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:552: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:557: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:562: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:567: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:572: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:577: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:582: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:587: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:592: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:597: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:602: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:607: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:612: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:617: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:622: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:627: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:632: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:637: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:642: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:647: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:652: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:657: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:662: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:667: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:672: Warning: minipage, output may be poor HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. HeVeA Warning: images may have changed, run 'imagen top2' Run, run, again... Exclude comment 'comment' ./top2.tex:28: Warning: Command not found: \geometry ./top2.tex:126: Warning: \today needs '-exec xxdate.exe' option ./top2.tex:159: Warning: Undefined citation: 'ott-jfp' ./top2.tex:164: Warning: Undefined citation: 'ott-sub' ./top2.tex:176: Warning: Undefined citation: 'Pierce:TypeSystems' ./top2.tex:177: Warning: Undefined citation: 'poplmark' ./top2.tex:178: Warning: Undefined citation: 'Leroy-generativity' ./top2.tex:180: Warning: Undefined citation: 'ljam-sub' ./README.tex:197: Warning: Command not found: \noalign ./README.tex:197: Warning: Command not found: \noalign ./README.tex:197: Warning: Command not found: \noalign ./README.tex:211: Warning: Command not found: \Shaded ./README.tex:212: Warning: Command not found: \Highlighting ./README.tex:213: Warning: Command not found: \NormalTok ./README.tex:214: Warning: Command not found: \NormalTok ./README.tex:214: Warning: Command not found: \textquotesingle ./README.tex:215: Warning: Command not found: \endHighlighting ./README.tex:216: Warning: Command not found: \endShaded ./README.tex:222: Warning: Command not found: \Shaded ./README.tex:223: Warning: Command not found: \Highlighting ./README.tex:224: Warning: Command not found: \NormalTok ./README.tex:225: Warning: Command not found: \NormalTok ./README.tex:225: Warning: Command not found: \textquotesingle ./README.tex:226: Warning: Command not found: \NormalTok ./README.tex:226: Warning: Command not found: \textquotesingle ./README.tex:227: Warning: Command not found: \endHighlighting ./README.tex:228: Warning: Command not found: \endShaded ./README.tex:287: Warning: Command not found: \noalign ./README.tex:287: Warning: Command not found: \noalign ./README.tex:287: Warning: Command not found: \noalign ./top2.tex:240: Warning: minipage, output may be poor ./top2.tex:458: Warning: minipage, output may be poor ./top2.tex:668: Warning: minipage, output may be poor ./top2.tex:747: Warning: minipage, output may be poor ./top2.tex:755: Warning: minipage, output may be poor ./top2.tex:762: Warning: minipage, output may be poor ./top2.tex:1214: Warning: minipage, output may be poor ./top2.tex:1221: Warning: minipage, output may be poor ./top2.tex:1627: Warning: Undefined citation: 'FGLMR96' ./top2.tex:2928: Warning: '_' occurring outside math mode ./top2.tex:2966: Warning: Undefined citation: 'Pierce:TypeSystems' ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2973: Warning: minipage, output may be poor ./top2.tex:2973: Warning: Command not found: \columnwidth ./top2.tex:2977: Warning: Undefined citation: 'LevinPierce99' ./top2.tex:3019: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:12: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:17: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:22: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:27: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:32: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:37: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:42: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:47: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:52: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:57: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:62: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:67: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:72: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:77: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:82: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:87: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:92: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:97: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:102: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:107: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:112: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:117: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:122: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:127: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:132: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:137: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:142: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:147: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:152: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:157: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:162: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:167: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:172: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:177: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:182: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:187: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:192: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:197: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:202: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:207: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:212: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:217: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:222: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:227: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:232: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:237: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:242: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:247: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:252: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:257: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:262: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:267: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:272: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:277: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:282: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:287: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:292: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:297: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:302: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:307: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:312: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:317: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:322: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:327: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:332: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:337: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:342: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:347: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:352: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:357: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:362: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:367: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:372: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:377: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:382: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:387: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:392: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:397: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:402: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:407: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:412: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:417: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:422: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:427: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:432: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:437: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:442: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:447: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:452: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:457: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:462: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:467: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:472: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:477: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:482: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:487: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:492: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:497: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:502: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:507: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:512: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:517: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:522: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:527: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:532: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:537: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:542: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:547: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:552: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:557: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:562: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:567: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:572: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:577: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:582: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:587: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:592: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:597: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:602: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:607: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:612: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:617: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:622: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:627: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:632: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:637: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:642: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:647: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:652: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:657: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:662: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:667: Warning: minipage, output may be poor ./grammar_parser_hevea.tex:672: Warning: minipage, output may be poor Fixpoint reached in 2 step(s) Now, I am running imagen for you RESOLUTION: 100 /usr/share/hevea/imagen: line 106: latex: command not found This is dvips(k) 2024.1 (TeX Live 2025/dev) Copyright 2024 Radical Eye Software (www.radicaleye.com) dvips: DVI file can't be opened: top2.image.dvi: No such file or directory sed 's/textboxed{border:1px/textboxed{border:0px/g' < top2.html > top2.tmp.html mv top2.tmp.html top2.html make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/doc' help2man -N src/ott > debian/ott.1 make[1]: Leaving directory '/build/reproducible-path/ott-0.33+ds' dh_auto_test create-stamp debian/debhelper-build-stamp dh_prep debian/rules override_dh_auto_install make[1]: Entering directory '/build/reproducible-path/ott-0.33+ds' DESTDIR=/build/reproducible-path/ott-0.33+ds/debian/tmp make -C coq install make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/coq' make -f Makefile.coq install make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/coq' INSTALL ott_list_predicate.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_repeat.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_mem.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_base.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_support.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_nth.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_core.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_distinct.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_predicate.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_repeat.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_mem.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_base.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_support.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_nth.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_core.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_distinct.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_predicate.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_repeat.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_mem.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_base.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_support.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_nth.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_core.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_distinct.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq//user-contrib/Ott/ make[4]: Entering directory '/build/reproducible-path/ott-0.33+ds/coq' make[4]: Leaving directory '/build/reproducible-path/ott-0.33+ds/coq' make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/coq' make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/coq' DESTDIR=/build/reproducible-path/ott-0.33+ds/debian/tmp make -C src install make[2]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' mkdir ../bin make opt make[3]: Entering directory '/build/reproducible-path/ott-0.33+ds/src' ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c location.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c types.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c auxl.ml File "auxl.ml", lines 405-412, characters 7-19: 405 | .......( match hse with 406 | | Hom_index _ | Hom_terminal _ -> [] 407 | | Hom_string s -> 408 | let strs = Str.split (Str.regexp "[ \t]+") s in 409 | let ntrs_hom = List.filter (fun st -> List.mem st defined_ntrs) strs in 410 | if promote 411 | then List.map (promote_ntr xd) ntrs_hom 412 | else ntrs_hom ). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) File "auxl.ml", lines 467-471, characters 7-59: 467 | .......( match hse with 468 | | Hom_index _ | Hom_terminal _ -> [] 469 | | Hom_string s -> 470 | let strs = Str.split (Str.regexp "[ \t]+") s in 471 | List.filter (fun st -> List.mem st defined_mvrs) strs ). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) File "auxl.ml", lines 1839-1854, characters 4-42: 1839 | ....( match stre with 1840 | | Struct_md mvr -> "metavar def: "^mvr 1841 | | Struct_rs ntrs -> "rule def: "^(String.concat " " ntrs) 1842 | | Struct_srs xs -> "subrule def: "^ 1843 | (String.concat " " ... 1851 | | Struct_axs xs -> "aux def: "^ 1852 | (String.concat " " xs) 1853 | | Struct_fun_or_defnclass s -> "fundefn_class def: "^s 1854 | | Struct_embed (_,h,_) -> "embed: "^h) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Struct_crs _ ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c merge.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c global_option.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c grammar_parser.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c grammar_lexer.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c version.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c grammar_pp.ml File "grammar_pp.ml", lines 1875-2131, characters 6-25: 1875 | ......( match m with 1876 | | Lex _ | Menhir _ -> Auxl.errorm m "pp_mse" 1877 | | Ascii ao -> 1878 | pp_auxfn m xd f ^ ""^pp_LPAREN ^ "" 1879 | ^ pp_ntlist ... 2128 | else 2129 | ( "(flat_map (fun "^pat_fun^" => "^pp_body^ pat_fun_end ^ ") " 2130 | ^ de1i.de1_compound_id 2131 | ^ ")", [], [] ) ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _) (However, some guarded clause may match this value.) File "grammar_pp.ml", lines 4022-4025, characters 16-45: 4022 | ................(match hse with 4023 | | Hom_string _ -> arity_of_homspec hs' 4024 | | Hom_index i -> max (1+i) (arity_of_homspec hs') 4025 | | Hom_terminal _ -> arity_of_homspec hs') Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Hom_ln_free_index (_, _) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c parse_table.ml File "parse_table.ml", line 914, characters 47-50: 914 | prod_action = (fun [r] -> r); ^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: r::_::_ ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c glr.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c new_term_parser.ml File "new_term_parser.ml", lines 150-177, characters 11-29: 150 | ...........function 151 | | "[" -> "lbrac" 152 | | "]" -> "rbrac" 153 | | "!" -> "excl" 154 | | "\"" -> "doublequote" ... 174 | | "}" -> "rcurly" 175 | | "|" -> "bar" 176 | | "~" -> "tilde" 177 | | "-" -> "minus". Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: "" File "new_term_parser.ml", line 289, characters 14-39: 289 | let res_charl [Res_char c; Res_charl l] = ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::Res_charl l::_::_ File "new_term_parser.ml", line 292, characters 20-45: 292 | let res_cons_string [Res_char c; Res_charl l] = ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::Res_charl l::_::_ File "new_term_parser.ml", line 295, characters 14-39: 295 | let res_stlil [Res_stli a; Res_stlil b] = Res_stlil (a::b);; ^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli a::Res_stlil b::_::_ File "new_term_parser.ml", lines 342-346, characters 67-66: 342 | ...................................................................function 343 | [] -> [] 344 | | Res_ignore::rl -> process_prod_res rl 345 | | Res_ste ste::rl -> ste::process_prod_res rl 346 | | Res_st st::rl -> Ste_st (dummy_loc, st)::process_prod_res rl Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Res_none|Res_stli _|Res_stlil _|Res_char _|Res_charl _|Res_string _| Res_int _|Res_si _|Res_sil _)::_ File "new_term_parser.ml", line 382, characters 19-32: 382 | (fun [Res_stlil x] -> elc x); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stlil x::_::_ File "new_term_parser.ml", line 401, characters 13-25: 401 | (fun [Res_stli x]-> Res_stlil [x]); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli x::_::_ File "new_term_parser.ml", line 416, characters 21-30: 416 | (fun [x; _; y] -> res_stlil [x; y]) ^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::y::_::_ File "new_term_parser.ml", lines 463-466, characters 31-64: 463 | ...............................[Res_stli (Stli_single (_, es1)); 464 | _; 465 | Res_int n'; 466 | Res_stli (Stli_single (_, es2))]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli (Stli_single (_, es1))::_::Res_int n':: Res_stli (Stli_single (_, es2))::_::_ File "new_term_parser.ml", lines 476-481, characters 31-64: 476 | ...............................[Res_stli (Stli_single (_, es1)); 477 | _; 478 | _; 479 | Res_int n'; 480 | _; 481 | Res_stli (Stli_single (_, es2))]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli (Stli_single (_, es1))::_::_::Res_int n'::_:: Res_stli (Stli_single (_, es2))::_::_ File "new_term_parser.ml", lines 488-489, characters 23-26: 488 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 489 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_::_ File "new_term_parser.ml", lines 508-511, characters 23-26: 508 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 509 | _; 510 | _; Res_string ivr'; 511 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_:: Res_string ivr'::_::_::_ File "new_term_parser.ml", lines 536-544, characters 23-26: 536 | .......................[_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 537 | _; 538 | _; 539 | Res_string lower; 540 | _; 541 | Res_int dotlength; 542 | _; 543 | Res_si si'; 544 | _]... Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_stli (Stli_single (_, es))::_::_::Res_string ivr::_::_:: Res_string lower::_::Res_int dotlength::_::Res_si si'::_::_::_ File "new_term_parser.ml", line 560, characters 23-35: 560 | (fun [Res_stli x] -> Res_stlil [x])); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_stli x::_::_ File "new_term_parser.ml", line 574, characters 29-38: 574 | (fun [x; _; y] -> res_stlil [x; y])); ^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::y::_::_ File "new_term_parser.ml", line 603, characters 20-27: 603 | (fun (_::rl) -> build_res rl) in ^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "new_term_parser.ml", line 609, characters 20-27: 609 | (fun (_::rl) -> build_res rl) in ^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: [] File "new_term_parser.ml", line 628, characters 17-23: 628 | (fun [_; x] -> x) ^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::x::_::_ File "new_term_parser.ml", line 638, characters 18-32: 638 | (fun [_; Res_sil l] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil l::_::_ File "new_term_parser.ml", line 649, characters 23-37: 649 | (fun [_; Res_sil l] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil l::_::_ File "new_term_parser.ml", line 664, characters 11-25: 664 | (fun [_; Res_sil x] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil x::_::_ File "new_term_parser.ml", line 695, characters 19-39: 695 | (fun (_::Res_string s::_) -> Res_ste (Ste_metavar (dummy_loc, mvd.mvd_name, (s, [])))) ^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _:: (Res_ignore|Res_none|Res_st _|Res_ste _|Res_stli _|Res_stlil _|Res_char _| Res_charl _|Res_int _|Res_si _|Res_sil _)::_ File "new_term_parser.ml", line 703, characters 21-38: 703 | (fun [_; Res_string s] -> ^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_string s::_::_ File "new_term_parser.ml", line 710, characters 21-38: 710 | (fun [_; Res_string s] -> ^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_string s::_::_ File "new_term_parser.ml", line 715, characters 21-59: 715 | (fun [((Res_ste (Ste_var (_, _, s))) as x)] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_ste (Ste_var (_, _, s))::_::_ File "new_term_parser.ml", line 742, characters 11-23: 742 | (fun [Res_char c] -> Res_charl [c]); ^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char c::_::_ File "new_term_parser.ml", line 748, characters 11-24: 748 | (fun [Res_charl s] -> Res_string (Auxl.string_of_char_list s)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl s::_::_ File "new_term_parser.ml", line 761, characters 11-33: 761 | (fun [Res_si s; Res_sil sl] -> Res_sil (s::sl)); ^^^^^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_si s::Res_sil sl::_::_ File "new_term_parser.ml", line 767, characters 11-24: 767 | (fun [Res_charl l] -> Res_si (Si_num (Auxl.string_of_char_list l))); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl l::_::_ File "new_term_parser.ml", line 771, characters 11-16: 771 | (fun [rsi] -> rsi); ^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: rsi::_::_ File "new_term_parser.ml", line 794, characters 11-24: 794 | (fun [Res_charl c] -> Res_charl ('_'::c)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl c::_::_ File "new_term_parser.ml", line 796, characters 11-24: 796 | (fun [Res_charl c] -> Res_charl ('\''::c)); ^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_charl c::_::_ File "new_term_parser.ml", line 831, characters 11-25: 831 | (fun [Res_string s] -> Res_si (Si_var (s, 0))); ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_string s::_::_ File "new_term_parser.ml", line 835, characters 11-25: 835 | (fun [Res_string s] -> Res_si (Si_var (s, -1))); ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_string s::_::_ File "new_term_parser.ml", line 846, characters 18-32: 846 | (fun [_; Res_sil x] -> ^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil x::_::_ File "new_term_parser.ml", line 858, characters 18-21: 858 | (fun [x] -> x); ^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: x::_::_ ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c term_parser.ml File "term_parser.ml", lines 1139-1172, characters 2-11: 1139 | ..let Ascii oldopts = pp_ascii_opts_default in 1140 | let opts = Ascii {oldopts with ppa_colour = !Auxl.colour} in 1141 | let sts = parse_complete lookup ntr concrete s in 1142 | let sts = transform sts in 1143 | match sts with ... 1169 | begin 1170 | report_error (Some l) (sstart ^ concat "" intermed); 1171 | St_uninterpreted(l, "multiple parses") 1172 | end Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq {coq_quantified_vars_from_de={ _ }; coq_non_local_hyp_defn={ _ }; coq_non_local_hyp_defn_vars={ _ }; coq_list_types={ _ }; coq_list_aux_defns={defined={ _ }; newly_defined={ _ }}; coq_library={contents=(_, _)}; coq_locally_nameless={ _ }; _ }| Isa {isa_library={contents=(_, _)}; _ }|Hol {hol_library={contents=(_, _)}}| Lem {lem_library={contents=(_, _)}}| Twf {twf_current_defn={ _ }; twf_library={contents=(_, _)}}|Tex { _ }| Caml {caml_library={contents=(_, _)}; _ }| Lex {ppm_caml_opts={caml_library={contents=(_, _)}; _ }; _ }| Menhir {ppm_caml_opts={caml_library={contents=(_, _)}; _ }; _ }) File "term_parser.ml", line 1222, characters 30-48: 1222 | List.map (fun (Ntp.Gtp.Res_st s) -> s) res ^^^^^^^^^^^^^^^^^^ Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Res_ignore|Res_none|Res_ste _|Res_stli _|Res_stlil _|Res_char _|Res_charl _| Res_string _|Res_int _|Res_si _|Res_sil _) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c dependency.ml File "dependency.ml", lines 571-579, characters 2-74: 571 | ..match m with 572 | | Isa io when io.ppi_isa_primrec -> isa_primrec_collapse m xd funcs 573 | | Isa io when not io.ppi_isa_primrec -> isa_fun_collapse m xd funcs 574 | | Hol _ -> hol_collapse m xd funcs 575 | | Lem _ -> lem_collapse m xd funcs 576 | | Coq _ -> coq_collapse m xd funcs 577 | | Twf _ -> twf_collapse m xd funcs 578 | | Caml _ -> caml_collapse m xd funcs 579 | | Tex _ | Ascii _ -> Auxl.error None "internal: collapse of Tex-Ascii\n" Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Isa _|Lex _|Menhir _) (However, some guarded clause may match this value.) File "dependency.ml", lines 584-714, characters 2-53: 584 | ..match m with 585 | | Tex _ | Ascii _ -> Auxl.error None "internal: print of Tex-Ascii\n" 586 | | Isa io -> 587 | let print_lemma block = 588 | if ( List.exists ... 711 | (* (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ "FOO1" ^ h2 ^ "FOO2"^ h3 ^ "FOO3"^s) block))*) 712 | (List.map (fun (_,((h1,h2,h3),s,_)) -> h1 ^ h2 ^ h3 ^ s ^ " end\n") block)) 713 | ^ "\n") in 714 | String.concat "" (List.map print_block sorting) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Lex _|Menhir _) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c bounds.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c context_pp.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c quotient_rules.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c grammar_typecheck.ml File "grammar_typecheck.ml", lines 54-56, characters 4-82: 54 | ....match (xs,keys) with 55 | | ([],[]) -> None 56 | | (x::xs, key::keys) -> if (List.mem key keys) then Some x else helper xs keys. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: ([], _::_) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c transform.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c substs_pp.ml File "substs_pp.ml", lines 333-336, characters 10-11: 333 | ..........(match m with 334 | | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr ^ " list" 335 | | Lem _ -> "list " ^Grammar_pp.pp_nt_or_mv_root_ty m xd ntmvr 336 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) File "substs_pp.ml", lines 1400-1412, characters 3-4: 1400 | ...(match m with 1401 | | Caml _ -> 1402 | "(" 1403 | ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 1404 | ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this ... 1409 | ^ Grammar_pp.pp_nt_or_mv_root_ty m xd subst.sb_that 1410 | ^ "*" ^ Grammar_pp.pp_nontermroot_ty m xd subst.sb_this 1411 | ^ ")" 1412 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) File "substs_pp.ml", lines 1747-1876, characters 3-8: 1747 | ...( match m with 1748 | | Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.error (Some p.prod_loc) "pp_fv_symterm_list_body" 1749 | | Isa io when io.ppi_isa_primrec -> 1750 | let args = 1751 | String.concat "_" ... 1873 | ("(flat_map (fun (pat_:"^de1i.de1_coq_type_of_pattern^") => match pat_ with " ^ de1i.de1_pattern ^ " => "^pp_body^" end) " 1874 | ^ de1i.de1_compound_id 1875 | ^ ")"), funcs 1876 | ).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Twf _) (However, some guarded clause may match this value.) File "substs_pp.ml", lines 2030-2033, characters 5-6: 2030 | .....(match m with 2031 | | Caml _ -> Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that ^ " list" 2032 | | Lem _ -> " list " ^ Grammar_pp.pp_nt_or_mv_root_ty m xd fv.fv_that 2033 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _|Hol _|Twf _|Ascii _|Tex _|Lex _|Menhir _) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c subrules_pp.ml File "subrules_pp.ml", lines 167-368, characters 8-2: 167 | ........( match m with 168 | | Isa io when io.ppi_isa_primrec -> 169 | let typ = 170 | Auxl.the (Grammar_pp.pp_elements 171 | m xd ((Si_punct "_")::sie) elbu.elb_es true false true true) ^ " list" in ... 365 | [ " %{ TWELF NOT IMPLEMENTED }%"], deps, [] 366 | | Tex _ | Ascii _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_subelement" 367 | 368 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Coq _|Isa _) (However, some guarded clause may match this value.) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c embed_pp.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c defns.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c ln_transform.ml File "ln_transform.ml", lines 1057-1067, characters 4-7: 1057 | ....match mse with 1058 | | Empty -> 1059 | "0",[] 1060 | | MetaVarExp mv -> 1061 | "1",[] (* FZ is this correct in the general case? *) ... 1064 | | Aux (f1,nt1) -> 1065 | let name = arity_name f1 (Auxl.promote_ntr xd_transformed (Auxl.primary_ntr_of_ntr xd_transformed (fst nt1))) in 1066 | name ^ " " ^ Grammar_pp.pp_nonterm m xd_transformed nt1, 1067 | [name] Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (NonTermExp _|MetaVarListExp (_, _)|NonTermListExp (_, _)|AuxList (_, _, _)) ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c coq_induct.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c system_pp.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c lex_menhir_pp.ml File "lex_menhir_pp.ml", lines 274-285, characters 10-11: 274 | ..........(match ocamllex_hom_opt, ocamllex_remove_hom with 275 | | Some ocamllex_hom, false -> 276 | Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, Some ocamllex_hom, ocamllex_of_string_hom_opt)) 277 | | None, false -> 278 | (* hack: default to ocamllex-remove *) ... 282 | Auxl.error (Some mvd.mvd_loc) ("ocamllex output: both ocamllex and ocamllex-remove hom for "^mvd.mvd_name^"\n") 283 | | None, true -> 284 | Some (token_name_of mvd.mvd_name, mvd.mvd_name, TK_metavar(ocaml_type, None, ocamllex_of_string_hom_opt)) 285 | ) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: (Some ocamllex_hom, true) File "lex_menhir_pp.ml", line 281, characters 12-36: 281 | | Some ocamllex_hom, false -> ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 11 [redundant-case]: this match case is unused. File "lex_menhir_pp.ml", lines 331-335, characters 13-42: 331 | .............(match ocaml_type with 332 | | "string" -> "" 333 | | "int" -> "int_of_string" 334 | | "float" -> "float_of_string" 335 | | "bool" -> "bool_of_string") Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: "" ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c align.ml ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -c main.ml echo Makefile location.cmx types.cmx auxl.cmx merge.cmx global_option.cmx grammar_lexer.cmx grammar_parser.cmx version.cmx grammar_pp.cmx parse_table.cmx glr.cmx new_term_parser.cmx term_parser.cmx dependency.cmx bounds.cmx context_pp.cmx quotient_rules.cmx grammar_typecheck.cmx transform.cmx substs_pp.cmx subrules_pp.cmx embed_pp.cmx defns.cmx ln_transform.cmx coq_induct.cmx system_pp.cmx lex_menhir_pp.cmx align.cmx main.cmx align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex Makefile location.cmx types.cmx auxl.cmx merge.cmx global_option.cmx grammar_lexer.cmx grammar_parser.cmx version.cmx grammar_pp.cmx parse_table.cmx glr.cmx new_term_parser.cmx term_parser.cmx dependency.cmx bounds.cmx context_pp.cmx quotient_rules.cmx grammar_typecheck.cmx transform.cmx substs_pp.cmx subrules_pp.cmx embed_pp.cmx defns.cmx ln_transform.cmx coq_induct.cmx system_pp.cmx lex_menhir_pp.cmx align.cmx main.cmx align.cmi bounds.cmi coq_induct.cmi defns.cmi dependency.cmi embed_pp.cmi grammar_typecheck.cmi merge.cmi subrules_pp.cmi substs_pp.cmi system_pp.cmi lex_menhir_pp.cmi transform.cmi term_parser.cmi version.tex ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -v The OCaml native-code compiler, version 5.2.0 Standard library directory: /usr/lib/aarch64-linux-gnu/ocaml/5.2.0 ocamlfind ocamlopt -package str -package ocamlgraph -linkpkg -w y -g -dtypes -unsafe -inline 9 -o ott.opt location.cmx types.cmx auxl.cmx merge.cmx global_option.cmx grammar_lexer.cmx grammar_parser.cmx version.cmx grammar_pp.cmx parse_table.cmx glr.cmx new_term_parser.cmx term_parser.cmx dependency.cmx bounds.cmx context_pp.cmx quotient_rules.cmx grammar_typecheck.cmx transform.cmx substs_pp.cmx subrules_pp.cmx embed_pp.cmx defns.cmx ln_transform.cmx coq_induct.cmx system_pp.cmx lex_menhir_pp.cmx align.cmx main.cmx ln -s -f ott.opt ott make[3]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' cp ./ott ../bin/ott make[2]: Leaving directory '/build/reproducible-path/ott-0.33+ds/src' make[1]: Leaving directory '/build/reproducible-path/ott-0.33+ds' dh_install dh_ocamldoc dh_installdocs dh_installchangelogs dh_installman dh_perl dh_link dh_strip_nondeterminism dh_compress dh_fixperms dh_missing dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dpkg-shlibdeps: warning: diversions involved - output may be incorrect diversion by libc6 from: /lib/ld-linux-aarch64.so.1 dpkg-shlibdeps: warning: diversions involved - output may be incorrect diversion by libc6 to: /lib/ld-linux-aarch64.so.1.usr-is-merged dh_installdeb dh_coq dh_ocaml dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'libcoq-ott' in '../libcoq-ott_0.33+ds-4_arm64.deb'. dpkg-deb: building package 'ott-tools' in '../ott-tools_0.33+ds-4_arm64.deb'. dpkg-deb: building package 'ott-tools-dbgsym' in '../ott-tools-dbgsym_0.33+ds-4_arm64.deb'. dpkg-genbuildinfo --build=binary -O../ott_0.33+ds-4_arm64.buildinfo dpkg-genchanges --build=binary -O../ott_0.33+ds-4_arm64.changes dpkg-genchanges: info: binary-only upload (no source code included) dpkg-source --after-build . 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/288991/tmp/hooks/B01_cleanup starting I: user script /srv/workspace/pbuilder/288991/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/288991 and its subdirectories I: Current time: Thu Dec 25 15:53:26 +14 2025 I: pbuilder-time-stamp: 1766627606