Mon Apr 22 00:02:26 UTC 2024 I: starting to build ott/trixie/armhf on jenkins on '2024-04-22 00:02' Mon Apr 22 00:02:26 UTC 2024 I: The jenkins build log is/was available at https://jenkins.debian.net/userContent/reproducible/debian/build_service/armhf_9/3705/console.log Mon Apr 22 00:02:26 UTC 2024 I: Downloading source for trixie/ott=0.33+ds-2 --2024-04-22 00:02:26-- http://deb.debian.org/debian/pool/main/o/ott/ott_0.33%2bds-2.dsc Connecting to 46.16.76.132:3128... connected. Proxy request sent, awaiting response... 200 OK Length: 2109 (2.1K) [text/prs.lines.tag] Saving to: ‘ott_0.33+ds-2.dsc’ 0K .. 100% 241M=0s 2024-04-22 00:02:26 (241 MB/s) - ‘ott_0.33+ds-2.dsc’ saved [2109/2109] Mon Apr 22 00:02:26 UTC 2024 I: ott_0.33+ds-2.dsc -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 Format: 3.0 (quilt) Source: ott Binary: libcoq-ott, ott-tools Architecture: any Version: 0.33+ds-2 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/ott-lang/ott Standards-Version: 4.6.2 Vcs-Browser: https://salsa.debian.org/ocaml-team/ott Vcs-Git: https://salsa.debian.org/ocaml-team/ott.git Testsuite: autopkgtest Testsuite-Triggers: coq Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, help2man, hevea, libcoq-core-ocaml-dev, libcoq-stdlib, libocamlgraph-ocaml-dev, pandoc Package-List: libcoq-ott deb ocaml optional arch=any ott-tools deb ocaml optional arch=any Checksums-Sha1: fc63f2061e80024965d44533336541733ccdd788 1140368 ott_0.33+ds.orig.tar.xz c9943bd2c775c529a0725bcc4775f5c161fc2896 6820 ott_0.33+ds-2.debian.tar.xz Checksums-Sha256: 345cf6b2359a39174ab61e4d83d2d2a325f8aa2e08b6483cb267672ee11bde73 1140368 ott_0.33+ds.orig.tar.xz 7541edfcdc19333f6fc2cb885b79d553dd885d7529bbe0b80780914c19fa51bf 6820 ott_0.33+ds-2.debian.tar.xz Files: 2d36c7cb4901ba8c5ba757c6108e1ad9 1140368 ott_0.33+ds.orig.tar.xz 1b374be442a6e475742fad885df4d45e 6820 ott_0.33+ds-2.debian.tar.xz -----BEGIN PGP SIGNATURE----- iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmWEWxUSHGpwdXlkdEBk ZWJpYW4ub3JnAAoJEATFO9f+AwVR1eYP/00KCI6zVCnddUkP8yWKCMV76U0BS7xy AQeJKMDRqIm/NXJM4JnYC4pX+YsKhiA1W4yuZo5qGSH4J715Oz1qakrSsoyex505 3pic67JP57Ze1xQjrNTnUEkmLwrCp8bBmVgUWZujiaMMKGmLtDrAsIUwgcsKqQlv ikbnCa95WS1hibU1NpGDcOG0CuQVjXfSh/0ANR+S5TqyYHuMcTaMjhlGLkmGM2qP jZ0s30zY+NcacCIhAZdg3oRU/UljJsDu9k+HeDZNtFxE4vS0DMbQYNF8fnc48F13 vPJZOp+bIQ9nL5kKKKsDPoCrVubli8YAZYwu+V/aheW+kXEGzGoAsUAIKjRSWhZJ DlxvzEN9dZIn3oMx9+qAlLPaxuD815yfdNQ/p3+X41nEBOXFGMtzEiZm8c5GpV2l iNwyW+Fns9TvCbG5pjg+7e3yrkJmFAsXbS8HVBc7F5bsGUrXeo+UyHGZqB2GWb0B memcER25XdDOtjw7tRL21e62Fdj+OM+ezvYrA1o2czN61XE7ikIoxL35VfpOc7JE mRhx3/oFG9JLqOu+mifbxmMkTheP5b1fRVZQdie1CNWpbM3lQEU5leWWAYBr5bp/ kSMP1lD0JBxKwxLbX2rg4RlFk/LRX1U+mudSeVT8bQGGijY2fMHTRDQYpbzNXK04 MGkCjx1EKAKj =sd6v -----END PGP SIGNATURE----- Mon Apr 22 00:02:26 UTC 2024 I: Checking whether the package is not for us Mon Apr 22 00:02:26 UTC 2024 I: Starting 1st build on remote node virt32a-armhf-rb.debian.net. Mon Apr 22 00:02:26 UTC 2024 I: Preparing to do remote build '1' on virt32a-armhf-rb.debian.net. Mon Apr 22 00:16:19 UTC 2024 I: Deleting $TMPDIR on virt32a-armhf-rb.debian.net. I: pbuilder: network access will be disabled during build I: Current time: Sun Apr 21 12:02:37 -12 2024 I: pbuilder-time-stamp: 1713744157 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/trixie-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-2.dsc] I: copying [./ott_0.33+ds.orig.tar.xz] I: copying [./ott_0.33+ds-2.debian.tar.xz] I: Extracting source gpgv: Signature made Thu Dec 21 15:34:45 2023 gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 gpgv: issuer "jpuydt@debian.org" gpgv: Can't check signature: No public key dpkg-source: warning: cannot verify inline signature for ./ott_0.33+ds-2.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-2.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying typos.patch I: Not using root during the build. I: Installing the build-deps I: user script /srv/workspace/pbuilder/9041/tmp/hooks/D02_print_environment starting I: set BUILDDIR='/build/reproducible-path' BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' BUILDUSERNAME='pbuilder1' BUILD_ARCH='armhf' DEBIAN_FRONTEND='noninteractive' DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3 ' DISTRIBUTION='trixie' HOME='/root' HOST_ARCH='armhf' IFS=' ' INVOCATION_ID='e5906f1c91bd47c498a9a1a9ca58d79e' LANG='C' LANGUAGE='en_US:en' LC_ALL='C' MAIL='/var/mail/root' OPTIND='1' PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' PBCURRENTCOMMANDLINEOPERATION='build' PBUILDER_OPERATION='build' PBUILDER_PKGDATADIR='/usr/share/pbuilder' PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' PBUILDER_SYSCONFDIR='/etc' PPID='9041' PS1='# ' PS2='> ' PS4='+ ' PWD='/' SHELL='/bin/bash' SHLVL='2' SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/pbuilderrc_Y1DR --distribution trixie --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/trixie-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/b1 --logfile b1/build.log ott_0.33+ds-2.dsc' SUDO_GID='113' SUDO_UID='107' SUDO_USER='jenkins' TERM='unknown' TZ='/usr/share/zoneinfo/Etc/GMT+12' USER='root' _='/usr/bin/systemd-run' http_proxy='http://10.0.0.15:3142/' I: uname -a Linux virt32a 6.1.0-20-armmp-lpae #1 SMP Debian 6.1.85-1 (2024-04-11) armv7l GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Apr 21 07:14 /bin -> usr/bin I: user script /srv/workspace/pbuilder/9041/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: armhf 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 ... 19635 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-6-common{a} imagemagick-6.q16{a} intltool-debian{a} libarchive-zip-perl{a} libavahi-client3{a} libavahi-common-data{a} libavahi-common3{a} libbrotli1{a} libbsd0{a} libcairo2{a} libcompiler-libs-ocaml-dev{a} libcoq-core-ocaml{a} libcoq-core-ocaml-dev{a} libcoq-stdlib{a} libcups2{a} libdav1d7{a} libdbus-1-3{a} libde265-0{a} libdebhelper-perl{a} libdeflate0{a} libelf1{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-0{a} libgmp-dev{a} libgmp3-dev{a} libgmpxx4ldbl{a} libgraphite2-3{a} libgs-common{a} libgs10{a} libgs10-common{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} libkpathsea6{a} liblcms2-2{a} liblerc4{a} liblocale-gettext-perl{a} liblqr-1-0{a} libltdl7{a} liblua5.4-0{a} libmagic-mgc{a} libmagic1{a} libmagickcore-6.q16-7{a} libmagickwand-6.q16-7{a} libncurses-dev{a} libncurses6{a} libnetpbm11{a} libocamlgraph-ocaml-dev{a} libopenjp2-7{a} libpaper-utils{a} libpaper1{a} libpipeline1{a} libpixman-1-0{a} libpng16-16{a} libpotrace0{a} libptexenc1{a} libpython3-stdlib{a} libpython3.11-minimal{a} libpython3.11-stdlib{a} libraw23{a} libreadline8{a} libsharpyuv0{a} libsm6{a} libstdlib-ocaml{a} libstdlib-ocaml-dev{a} libsub-override-perl{a} libsynctex2{a} libteckit0{a} libtexlua53-5{a} libtiff6{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} libxt6{a} libyaml-0-2{a} libzarith-ocaml{a} libzarith-ocaml-dev{a} libzzip-0-13{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.11{a} python3.11-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 ledit libarchive-cpio-perl libfile-mimeinfo-perl libglib2.0-data libgpm2 libheif-plugin-aomenc libheif-plugin-x265 libltdl-dev libmagickcore-6.q16-7-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, 161 newly installed, 0 to remove and 0 not upgraded. Need to get 407 MB of archives. After unpacking 1627 MB will be used. Writing extended state information... Get: 1 http://deb.debian.org/debian trixie/main armhf liblocale-gettext-perl armhf 1.07-6+b1 [14.6 kB] Get: 2 http://deb.debian.org/debian trixie/main armhf libfftw3-double3 armhf 3.3.10-1+b1 [328 kB] Get: 3 http://deb.debian.org/debian trixie/main armhf libexpat1 armhf 2.6.2-1 [83.5 kB] Get: 4 http://deb.debian.org/debian trixie/main armhf libbrotli1 armhf 1.1.0-2+b3 [284 kB] Get: 5 http://deb.debian.org/debian trixie/main armhf libpng16-16 armhf 1.6.43-1 [262 kB] Get: 6 http://deb.debian.org/debian trixie/main armhf libfreetype6 armhf 2.13.2+dfsg-1+b1 [371 kB] Get: 7 http://deb.debian.org/debian trixie/main armhf libfontenc1 armhf 1:1.1.8-1 [20.6 kB] Get: 8 http://deb.debian.org/debian trixie/main armhf x11-common all 1:7.7+23 [252 kB] Get: 9 http://deb.debian.org/debian trixie/main armhf xfonts-encodings all 1:1.0.4-2.2 [577 kB] Get: 10 http://deb.debian.org/debian trixie/main armhf xfonts-utils armhf 1:7.7+6 [84.5 kB] Get: 11 http://deb.debian.org/debian trixie/main armhf fonts-urw-base35 all 20200910-8 [10.8 MB] Get: 12 http://deb.debian.org/debian trixie/main armhf fontconfig-config armhf 2.15.0-1.1 [317 kB] Get: 13 http://deb.debian.org/debian trixie/main armhf libfontconfig1 armhf 2.15.0-1.1 [370 kB] Get: 14 http://deb.debian.org/debian trixie/main armhf libsharpyuv0 armhf 1.3.2-0.4 [105 kB] Get: 15 http://deb.debian.org/debian trixie/main armhf libdav1d7 armhf 1.4.1-1 [262 kB] Get: 16 http://deb.debian.org/debian trixie/main armhf libheif-plugin-dav1d armhf 1.17.6-1 [9252 B] Get: 17 http://deb.debian.org/debian trixie/main armhf libde265-0 armhf 1.0.15-1 [145 kB] Get: 18 http://deb.debian.org/debian trixie/main armhf libheif-plugin-libde265 armhf 1.17.6-1 [12.0 kB] Get: 19 http://deb.debian.org/debian trixie/main armhf libheif1 armhf 1.17.6-1 [242 kB] Get: 20 http://deb.debian.org/debian trixie/main armhf libjbig0 armhf 2.1-6.1+b1 [27.3 kB] Get: 21 http://deb.debian.org/debian trixie/main armhf libjpeg62-turbo armhf 1:2.1.5-2+b2 [143 kB] Get: 22 http://deb.debian.org/debian trixie/main armhf liblcms2-2 armhf 2.14-2+b1 [126 kB] Get: 23 http://deb.debian.org/debian trixie/main armhf libglib2.0-0 armhf 2.78.4-1 [1281 kB] Get: 24 http://deb.debian.org/debian trixie/main armhf liblqr-1-0 armhf 0.4.2-2.1 [23.5 kB] Get: 25 http://deb.debian.org/debian trixie/main armhf libltdl7 armhf 2.4.7-7 [390 kB] Get: 26 http://deb.debian.org/debian trixie/main armhf libopenjp2-7 armhf 2.5.0-2+b2 [170 kB] Get: 27 http://deb.debian.org/debian trixie/main armhf libraw23 armhf 0.21.2-2 [359 kB] Get: 28 http://deb.debian.org/debian trixie/main armhf libdeflate0 armhf 1.20-1 [35.9 kB] Get: 29 http://deb.debian.org/debian trixie/main armhf liblerc4 armhf 4.0.0+ds-4+b1 [137 kB] Get: 30 http://deb.debian.org/debian trixie/main armhf libwebp7 armhf 1.3.2-0.4 [261 kB] Get: 31 http://deb.debian.org/debian trixie/main armhf libtiff6 armhf 4.5.1+git230720-4 [301 kB] Get: 32 http://deb.debian.org/debian trixie/main armhf libwebpdemux2 armhf 1.3.2-0.4 [106 kB] Get: 33 http://deb.debian.org/debian trixie/main armhf libwebpmux3 armhf 1.3.2-0.4 [116 kB] Get: 34 http://deb.debian.org/debian trixie/main armhf libxau6 armhf 1:1.0.9-1 [19.0 kB] Get: 35 http://deb.debian.org/debian trixie/main armhf libbsd0 armhf 0.12.2-1 [127 kB] Get: 36 http://deb.debian.org/debian trixie/main armhf libxdmcp6 armhf 1:1.1.2-3 [24.9 kB] Get: 37 http://deb.debian.org/debian trixie/main armhf libxcb1 armhf 1.15-1 [140 kB] Get: 38 http://deb.debian.org/debian trixie/main armhf libx11-data all 2:1.8.7-1 [328 kB] Get: 39 http://deb.debian.org/debian trixie/main armhf libx11-6 armhf 2:1.8.7-1 [735 kB] Get: 40 http://deb.debian.org/debian trixie/main armhf libxext6 armhf 2:1.3.4-1+b1 [47.8 kB] Get: 41 http://deb.debian.org/debian trixie/main armhf libicu72 armhf 72.1-4+b1 [9070 kB] Get: 42 http://deb.debian.org/debian trixie/main armhf libxml2 armhf 2.9.14+dfsg-1.3+b2 [599 kB] Get: 43 http://deb.debian.org/debian trixie/main armhf imagemagick-6-common all 8:6.9.12.98+dfsg1-5 [66.9 kB] Get: 44 http://deb.debian.org/debian trixie/main armhf libmagickcore-6.q16-7 armhf 8:6.9.12.98+dfsg1-5+b1 [1552 kB] Get: 45 http://deb.debian.org/debian trixie/main armhf libmagickwand-6.q16-7 armhf 8:6.9.12.98+dfsg1-5+b1 [301 kB] Get: 46 http://deb.debian.org/debian trixie/main armhf poppler-data all 0.4.12-1 [1601 kB] Get: 47 http://deb.debian.org/debian trixie/main armhf libpython3.11-minimal armhf 3.11.8-1 [802 kB] Get: 48 http://deb.debian.org/debian trixie/main armhf python3.11-minimal armhf 3.11.8-1 [1707 kB] Get: 49 http://deb.debian.org/debian trixie/main armhf python3-minimal armhf 3.11.6-1 [26.2 kB] Get: 50 http://deb.debian.org/debian trixie/main armhf media-types all 10.1.0 [26.9 kB] Get: 51 http://deb.debian.org/debian trixie/main armhf netbase all 6.4 [12.8 kB] Get: 52 http://deb.debian.org/debian trixie/main armhf tzdata all 2024a-1 [255 kB] Get: 53 http://deb.debian.org/debian trixie/main armhf readline-common all 8.2-3 [69.1 kB] Get: 54 http://deb.debian.org/debian trixie/main armhf libreadline8 armhf 8.2-3+b1 [144 kB] Get: 55 http://deb.debian.org/debian trixie/main armhf libpython3.11-stdlib armhf 3.11.8-1 [1709 kB] Get: 56 http://deb.debian.org/debian trixie/main armhf python3.11 armhf 3.11.8-1 [597 kB] Get: 57 http://deb.debian.org/debian trixie/main armhf libpython3-stdlib armhf 3.11.6-1 [9224 B] Get: 58 http://deb.debian.org/debian trixie/main armhf python3 armhf 3.11.6-1 [26.2 kB] Get: 59 http://deb.debian.org/debian trixie/main armhf sensible-utils all 0.0.22 [22.4 kB] Get: 60 http://deb.debian.org/debian trixie/main armhf libmagic-mgc armhf 1:5.45-2+b1 [314 kB] Get: 61 http://deb.debian.org/debian trixie/main armhf libmagic1 armhf 1:5.45-2+b1 [97.9 kB] Get: 62 http://deb.debian.org/debian trixie/main armhf file armhf 1:5.45-2+b1 [42.2 kB] Get: 63 http://deb.debian.org/debian trixie/main armhf gettext-base armhf 0.21-14+b1 [157 kB] Get: 64 http://deb.debian.org/debian trixie/main armhf libuchardet0 armhf 0.0.8-1+b1 [65.7 kB] Get: 65 http://deb.debian.org/debian trixie/main armhf groff-base armhf 1.23.0-3 [1088 kB] Get: 66 http://deb.debian.org/debian trixie/main armhf bsdextrautils armhf 2.39.3-6 [81.2 kB] Get: 67 http://deb.debian.org/debian trixie/main armhf libpipeline1 armhf 1.5.7-2 [33.3 kB] Get: 68 http://deb.debian.org/debian trixie/main armhf man-db armhf 2.12.0-3 [1367 kB] Get: 69 http://deb.debian.org/debian trixie/main armhf ucf all 3.0043+nmu1 [55.2 kB] Get: 70 http://deb.debian.org/debian trixie/main armhf m4 armhf 1.4.19-4 [264 kB] Get: 71 http://deb.debian.org/debian trixie/main armhf autoconf all 2.71-3 [332 kB] Get: 72 http://deb.debian.org/debian trixie/main armhf autotools-dev all 20220109.1 [51.6 kB] Get: 73 http://deb.debian.org/debian trixie/main armhf automake all 1:1.16.5-1.3 [823 kB] Get: 74 http://deb.debian.org/debian trixie/main armhf autopoint all 0.21-14 [496 kB] Get: 75 http://deb.debian.org/debian trixie/main armhf libcoq-stdlib armhf 8.18.0+dfsg-1 [23.2 MB] Get: 76 http://deb.debian.org/debian trixie/main armhf libstdlib-ocaml armhf 4.14.1-1 [464 kB] Get: 77 http://deb.debian.org/debian trixie/main armhf ocaml-base armhf 4.14.1-1 [358 kB] Get: 78 http://deb.debian.org/debian trixie/main armhf libfindlib-ocaml armhf 1.9.6-1+b2 [167 kB] Get: 79 http://deb.debian.org/debian trixie/main armhf libzarith-ocaml armhf 1.13-2+b1 [101 kB] Get: 80 http://deb.debian.org/debian trixie/main armhf libcoq-core-ocaml armhf 8.18.0+dfsg-1 [22.9 MB] Get: 81 http://deb.debian.org/debian trixie/main armhf libstdlib-ocaml-dev armhf 4.14.1-1 [7137 kB] Get: 82 http://deb.debian.org/debian trixie/main armhf libcompiler-libs-ocaml-dev armhf 4.14.1-1 [32.2 MB] Get: 83 http://deb.debian.org/debian trixie/main armhf ocaml-interp armhf 4.14.1-1 [6458 kB] Get: 84 http://deb.debian.org/debian trixie/main armhf libncurses6 armhf 6.4+20240113-1 [81.8 kB] Get: 85 http://deb.debian.org/debian trixie/main armhf libncurses-dev armhf 6.4+20240113-1 [309 kB] Get: 86 http://deb.debian.org/debian trixie/main armhf ocaml armhf 4.14.1-1 [66.5 MB] Get: 87 http://deb.debian.org/debian trixie/main armhf ocaml-findlib armhf 1.9.6-1+b2 [468 kB] Get: 88 http://deb.debian.org/debian trixie/main armhf coq armhf 8.18.0+dfsg-1 [78.4 MB] Get: 89 http://deb.debian.org/debian trixie/main armhf libdebhelper-perl all 13.15.3 [88.0 kB] Get: 90 http://deb.debian.org/debian trixie/main armhf libtool all 2.4.7-7 [517 kB] Get: 91 http://deb.debian.org/debian trixie/main armhf dh-autoreconf all 20 [17.1 kB] Get: 92 http://deb.debian.org/debian trixie/main armhf libarchive-zip-perl all 1.68-1 [104 kB] Get: 93 http://deb.debian.org/debian trixie/main armhf libsub-override-perl all 0.10-1 [10.6 kB] Get: 94 http://deb.debian.org/debian trixie/main armhf libfile-stripnondeterminism-perl all 1.13.1-1 [19.4 kB] Get: 95 http://deb.debian.org/debian trixie/main armhf dh-strip-nondeterminism all 1.13.1-1 [8620 B] Get: 96 http://deb.debian.org/debian trixie/main armhf libelf1 armhf 0.190-1+b1 [171 kB] Get: 97 http://deb.debian.org/debian trixie/main armhf dwz armhf 0.15-1 [101 kB] Get: 98 http://deb.debian.org/debian trixie/main armhf gettext armhf 0.21-14+b1 [1230 kB] Get: 99 http://deb.debian.org/debian trixie/main armhf intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get: 100 http://deb.debian.org/debian trixie/main armhf po-debconf all 1.0.21+nmu1 [248 kB] Get: 101 http://deb.debian.org/debian trixie/main armhf debhelper all 13.15.3 [901 kB] Get: 102 http://deb.debian.org/debian trixie/main armhf dh-coq all 0.8 [6676 B] Get: 103 http://deb.debian.org/debian trixie/main armhf dh-ocaml all 2.0 [75.1 kB] Get: 104 http://deb.debian.org/debian trixie/main armhf libgs-common all 10.02.1~dfsg-3 [147 kB] Get: 105 http://deb.debian.org/debian trixie/main armhf libgs10-common all 10.02.1~dfsg-3 [474 kB] Get: 106 http://deb.debian.org/debian trixie/main armhf libavahi-common-data armhf 0.8-13+b1 [111 kB] Get: 107 http://deb.debian.org/debian trixie/main armhf libavahi-common3 armhf 0.8-13+b1 [40.1 kB] Get: 108 http://deb.debian.org/debian trixie/main armhf libdbus-1-3 armhf 1.14.10-4 [180 kB] Get: 109 http://deb.debian.org/debian trixie/main armhf libavahi-client3 armhf 0.8-13+b1 [43.4 kB] Get: 110 http://deb.debian.org/debian trixie/main armhf libcups2 armhf 2.4.7-1+b1 [212 kB] Get: 111 http://deb.debian.org/debian trixie/main armhf libidn12 armhf 1.42-2 [77.7 kB] Get: 112 http://deb.debian.org/debian trixie/main armhf libijs-0.35 armhf 0.35-15.1+b1 [13.4 kB] Get: 113 http://deb.debian.org/debian trixie/main armhf libjbig2dec0 armhf 0.20-1+b1 [56.1 kB] Get: 114 http://deb.debian.org/debian trixie/main armhf libpaper1 armhf 1.1.29 [11.9 kB] Get: 115 http://deb.debian.org/debian trixie/main armhf libice6 armhf 2:1.0.10-1 [51.9 kB] Get: 116 http://deb.debian.org/debian trixie/main armhf libsm6 armhf 2:1.2.3-1 [33.0 kB] Get: 117 http://deb.debian.org/debian trixie/main armhf libxt6 armhf 1:1.2.1-1.1 [157 kB] Get: 118 http://deb.debian.org/debian trixie/main armhf libgs10 armhf 10.02.1~dfsg-3 [2134 kB] Get: 119 http://deb.debian.org/debian trixie/main armhf ghostscript armhf 10.02.1~dfsg-3 [49.6 kB] Get: 120 http://deb.debian.org/debian trixie/main armhf help2man armhf 1.49.3 [198 kB] Get: 121 http://deb.debian.org/debian trixie/main armhf libnetpbm11 armhf 2:11.05.02-1 [164 kB] Get: 122 http://deb.debian.org/debian trixie/main armhf netpbm armhf 2:11.05.02-1 [1890 kB] Get: 123 http://deb.debian.org/debian trixie/main armhf tex-common all 6.18 [32.5 kB] Get: 124 http://deb.debian.org/debian trixie/main armhf libpaper-utils armhf 1.1.29 [8400 B] Get: 125 http://deb.debian.org/debian trixie/main armhf libkpathsea6 armhf 2023.20230311.66589-9 [144 kB] Get: 126 http://deb.debian.org/debian trixie/main armhf libptexenc1 armhf 2023.20230311.66589-9 [42.8 kB] Get: 127 http://deb.debian.org/debian trixie/main armhf libsynctex2 armhf 2023.20230311.66589-9 [48.5 kB] Get: 128 http://deb.debian.org/debian trixie/main armhf libtexlua53-5 armhf 2023.20230311.66589-9 [82.2 kB] Get: 129 http://deb.debian.org/debian trixie/main armhf t1utils armhf 1.41-4 [54.7 kB] Get: 130 http://deb.debian.org/debian trixie/main armhf libpixman-1-0 armhf 0.42.2-1+b1 [476 kB] Get: 131 http://deb.debian.org/debian trixie/main armhf libxcb-render0 armhf 1.15-1 [114 kB] Get: 132 http://deb.debian.org/debian trixie/main armhf libxcb-shm0 armhf 1.15-1 [106 kB] Get: 133 http://deb.debian.org/debian trixie/main armhf libxrender1 armhf 1:0.9.10-1.1 [30.1 kB] Get: 134 http://deb.debian.org/debian trixie/main armhf libcairo2 armhf 1.18.0-1+b1 [441 kB] Get: 135 http://deb.debian.org/debian trixie/main armhf libgraphite2-3 armhf 1.3.14-2 [63.2 kB] Get: 136 http://deb.debian.org/debian trixie/main armhf libharfbuzz0b armhf 8.3.0-2 [2155 kB] Get: 137 http://deb.debian.org/debian trixie/main armhf libpotrace0 armhf 1.16-2+b1 [22.6 kB] Get: 138 http://deb.debian.org/debian trixie/main armhf libteckit0 armhf 2.5.12+ds1-1 [259 kB] Get: 139 http://deb.debian.org/debian trixie/main armhf libxmu6 armhf 2:1.1.3-3 [52.6 kB] Get: 140 http://deb.debian.org/debian trixie/main armhf libxpm4 armhf 1:3.5.17-1 [49.5 kB] Get: 141 http://deb.debian.org/debian trixie/main armhf libxaw7 armhf 2:1.0.14-1 [167 kB] Get: 142 http://deb.debian.org/debian trixie/main armhf libxi6 armhf 2:1.8.1-1 [73.8 kB] Get: 143 http://deb.debian.org/debian trixie/main armhf libzzip-0-13 armhf 0.13.72+dfsg.1-1.1+b1 [52.3 kB] Get: 144 http://deb.debian.org/debian trixie/main armhf texlive-binaries armhf 2023.20230311.66589-9 [6071 kB] Get: 145 http://deb.debian.org/debian trixie/main armhf xdg-utils all 1.1.3-4.1 [75.5 kB] Get: 146 http://deb.debian.org/debian trixie/main armhf texlive-base all 2023.20240207-1 [22.0 MB] Get: 147 http://deb.debian.org/debian trixie/main armhf hicolor-icon-theme all 0.17-2 [11.4 kB] Get: 148 http://deb.debian.org/debian trixie/main armhf imagemagick-6.q16 armhf 8:6.9.12.98+dfsg1-5+b1 [290 kB] Get: 149 http://deb.debian.org/debian trixie/main armhf imagemagick armhf 8:6.9.12.98+dfsg1-5+b1 [19.5 kB] Get: 150 http://deb.debian.org/debian trixie/main armhf hevea armhf 2.36-2+b1 [1787 kB] Get: 151 http://deb.debian.org/debian trixie/main armhf libfindlib-ocaml-dev armhf 1.9.6-1+b2 [164 kB] Get: 152 http://deb.debian.org/debian trixie/main armhf libgmpxx4ldbl armhf 2:6.3.0+dfsg-2+b1 [328 kB] Get: 153 http://deb.debian.org/debian trixie/main armhf libgmp-dev armhf 2:6.3.0+dfsg-2+b1 [591 kB] Get: 154 http://deb.debian.org/debian trixie/main armhf libgmp3-dev armhf 2:6.3.0+dfsg-2+b1 [322 kB] Get: 155 http://deb.debian.org/debian trixie/main armhf libzarith-ocaml-dev armhf 1.13-2+b1 [101 kB] Get: 156 http://deb.debian.org/debian trixie/main armhf libcoq-core-ocaml-dev armhf 8.18.0+dfsg-1 [44.8 MB] Get: 157 http://deb.debian.org/debian trixie/main armhf liblua5.4-0 armhf 5.4.6-3 [122 kB] Get: 158 http://deb.debian.org/debian trixie/main armhf libocamlgraph-ocaml-dev armhf 2.1.0-1+b1 [5094 kB] Get: 159 http://deb.debian.org/debian trixie/main armhf libyaml-0-2 armhf 0.2.5-1 [46.8 kB] Get: 160 http://deb.debian.org/debian trixie/main armhf pandoc-data all 3.1.3-1 [445 kB] Get: 161 http://deb.debian.org/debian trixie/main armhf pandoc armhf 3.1.3+ds-2 [28.5 MB] Fetched 407 MB in 1min 37s (4188 kB/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 ... 19635 files and directories currently installed.) Preparing to unpack .../00-liblocale-gettext-perl_1.07-6+b1_armhf.deb ... Unpacking liblocale-gettext-perl (1.07-6+b1) ... Selecting previously unselected package libfftw3-double3:armhf. Preparing to unpack .../01-libfftw3-double3_3.3.10-1+b1_armhf.deb ... Unpacking libfftw3-double3:armhf (3.3.10-1+b1) ... Selecting previously unselected package libexpat1:armhf. Preparing to unpack .../02-libexpat1_2.6.2-1_armhf.deb ... Unpacking libexpat1:armhf (2.6.2-1) ... Selecting previously unselected package libbrotli1:armhf. Preparing to unpack .../03-libbrotli1_1.1.0-2+b3_armhf.deb ... Unpacking libbrotli1:armhf (1.1.0-2+b3) ... Selecting previously unselected package libpng16-16:armhf. Preparing to unpack .../04-libpng16-16_1.6.43-1_armhf.deb ... Unpacking libpng16-16:armhf (1.6.43-1) ... Selecting previously unselected package libfreetype6:armhf. Preparing to unpack .../05-libfreetype6_2.13.2+dfsg-1+b1_armhf.deb ... Unpacking libfreetype6:armhf (2.13.2+dfsg-1+b1) ... Selecting previously unselected package libfontenc1:armhf. Preparing to unpack .../06-libfontenc1_1%3a1.1.8-1_armhf.deb ... Unpacking libfontenc1:armhf (1:1.1.8-1) ... Selecting previously unselected package x11-common. Preparing to unpack .../07-x11-common_1%3a7.7+23_all.deb ... Unpacking x11-common (1:7.7+23) ... 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+6_armhf.deb ... Unpacking xfonts-utils (1:7.7+6) ... 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_armhf.deb ... Unpacking fontconfig-config (2.15.0-1.1) ... Selecting previously unselected package libfontconfig1:armhf. Preparing to unpack .../12-libfontconfig1_2.15.0-1.1_armhf.deb ... Unpacking libfontconfig1:armhf (2.15.0-1.1) ... Selecting previously unselected package libsharpyuv0:armhf. Preparing to unpack .../13-libsharpyuv0_1.3.2-0.4_armhf.deb ... Unpacking libsharpyuv0:armhf (1.3.2-0.4) ... Selecting previously unselected package libdav1d7:armhf. Preparing to unpack .../14-libdav1d7_1.4.1-1_armhf.deb ... Unpacking libdav1d7:armhf (1.4.1-1) ... Selecting previously unselected package libheif-plugin-dav1d:armhf. Preparing to unpack .../15-libheif-plugin-dav1d_1.17.6-1_armhf.deb ... Unpacking libheif-plugin-dav1d:armhf (1.17.6-1) ... Selecting previously unselected package libde265-0:armhf. Preparing to unpack .../16-libde265-0_1.0.15-1_armhf.deb ... Unpacking libde265-0:armhf (1.0.15-1) ... Selecting previously unselected package libheif-plugin-libde265:armhf. Preparing to unpack .../17-libheif-plugin-libde265_1.17.6-1_armhf.deb ... Unpacking libheif-plugin-libde265:armhf (1.17.6-1) ... Selecting previously unselected package libheif1:armhf. Preparing to unpack .../18-libheif1_1.17.6-1_armhf.deb ... Unpacking libheif1:armhf (1.17.6-1) ... Selecting previously unselected package libjbig0:armhf. Preparing to unpack .../19-libjbig0_2.1-6.1+b1_armhf.deb ... Unpacking libjbig0:armhf (2.1-6.1+b1) ... Selecting previously unselected package libjpeg62-turbo:armhf. Preparing to unpack .../20-libjpeg62-turbo_1%3a2.1.5-2+b2_armhf.deb ... Unpacking libjpeg62-turbo:armhf (1:2.1.5-2+b2) ... Selecting previously unselected package liblcms2-2:armhf. Preparing to unpack .../21-liblcms2-2_2.14-2+b1_armhf.deb ... Unpacking liblcms2-2:armhf (2.14-2+b1) ... Selecting previously unselected package libglib2.0-0:armhf. Preparing to unpack .../22-libglib2.0-0_2.78.4-1_armhf.deb ... Unpacking libglib2.0-0:armhf (2.78.4-1) ... Selecting previously unselected package liblqr-1-0:armhf. Preparing to unpack .../23-liblqr-1-0_0.4.2-2.1_armhf.deb ... Unpacking liblqr-1-0:armhf (0.4.2-2.1) ... Selecting previously unselected package libltdl7:armhf. Preparing to unpack .../24-libltdl7_2.4.7-7_armhf.deb ... Unpacking libltdl7:armhf (2.4.7-7) ... Selecting previously unselected package libopenjp2-7:armhf. Preparing to unpack .../25-libopenjp2-7_2.5.0-2+b2_armhf.deb ... Unpacking libopenjp2-7:armhf (2.5.0-2+b2) ... Selecting previously unselected package libraw23:armhf. Preparing to unpack .../26-libraw23_0.21.2-2_armhf.deb ... Unpacking libraw23:armhf (0.21.2-2) ... Selecting previously unselected package libdeflate0:armhf. Preparing to unpack .../27-libdeflate0_1.20-1_armhf.deb ... Unpacking libdeflate0:armhf (1.20-1) ... Selecting previously unselected package liblerc4:armhf. Preparing to unpack .../28-liblerc4_4.0.0+ds-4+b1_armhf.deb ... Unpacking liblerc4:armhf (4.0.0+ds-4+b1) ... Selecting previously unselected package libwebp7:armhf. Preparing to unpack .../29-libwebp7_1.3.2-0.4_armhf.deb ... Unpacking libwebp7:armhf (1.3.2-0.4) ... Selecting previously unselected package libtiff6:armhf. Preparing to unpack .../30-libtiff6_4.5.1+git230720-4_armhf.deb ... Unpacking libtiff6:armhf (4.5.1+git230720-4) ... Selecting previously unselected package libwebpdemux2:armhf. Preparing to unpack .../31-libwebpdemux2_1.3.2-0.4_armhf.deb ... Unpacking libwebpdemux2:armhf (1.3.2-0.4) ... Selecting previously unselected package libwebpmux3:armhf. Preparing to unpack .../32-libwebpmux3_1.3.2-0.4_armhf.deb ... Unpacking libwebpmux3:armhf (1.3.2-0.4) ... Selecting previously unselected package libxau6:armhf. Preparing to unpack .../33-libxau6_1%3a1.0.9-1_armhf.deb ... Unpacking libxau6:armhf (1:1.0.9-1) ... Selecting previously unselected package libbsd0:armhf. Preparing to unpack .../34-libbsd0_0.12.2-1_armhf.deb ... Unpacking libbsd0:armhf (0.12.2-1) ... Selecting previously unselected package libxdmcp6:armhf. Preparing to unpack .../35-libxdmcp6_1%3a1.1.2-3_armhf.deb ... Unpacking libxdmcp6:armhf (1:1.1.2-3) ... Selecting previously unselected package libxcb1:armhf. Preparing to unpack .../36-libxcb1_1.15-1_armhf.deb ... Unpacking libxcb1:armhf (1.15-1) ... Selecting previously unselected package libx11-data. Preparing to unpack .../37-libx11-data_2%3a1.8.7-1_all.deb ... Unpacking libx11-data (2:1.8.7-1) ... Selecting previously unselected package libx11-6:armhf. Preparing to unpack .../38-libx11-6_2%3a1.8.7-1_armhf.deb ... Unpacking libx11-6:armhf (2:1.8.7-1) ... Selecting previously unselected package libxext6:armhf. Preparing to unpack .../39-libxext6_2%3a1.3.4-1+b1_armhf.deb ... Unpacking libxext6:armhf (2:1.3.4-1+b1) ... Selecting previously unselected package libicu72:armhf. Preparing to unpack .../40-libicu72_72.1-4+b1_armhf.deb ... Unpacking libicu72:armhf (72.1-4+b1) ... Selecting previously unselected package libxml2:armhf. Preparing to unpack .../41-libxml2_2.9.14+dfsg-1.3+b2_armhf.deb ... Unpacking libxml2:armhf (2.9.14+dfsg-1.3+b2) ... Selecting previously unselected package imagemagick-6-common. Preparing to unpack .../42-imagemagick-6-common_8%3a6.9.12.98+dfsg1-5_all.deb ... Unpacking imagemagick-6-common (8:6.9.12.98+dfsg1-5) ... Selecting previously unselected package libmagickcore-6.q16-7:armhf. Preparing to unpack .../43-libmagickcore-6.q16-7_8%3a6.9.12.98+dfsg1-5+b1_armhf.deb ... Unpacking libmagickcore-6.q16-7:armhf (8:6.9.12.98+dfsg1-5+b1) ... Selecting previously unselected package libmagickwand-6.q16-7:armhf. Preparing to unpack .../44-libmagickwand-6.q16-7_8%3a6.9.12.98+dfsg1-5+b1_armhf.deb ... Unpacking libmagickwand-6.q16-7:armhf (8:6.9.12.98+dfsg1-5+b1) ... Selecting previously unselected package poppler-data. Preparing to unpack .../45-poppler-data_0.4.12-1_all.deb ... Unpacking poppler-data (0.4.12-1) ... Selecting previously unselected package libpython3.11-minimal:armhf. Preparing to unpack .../46-libpython3.11-minimal_3.11.8-1_armhf.deb ... Unpacking libpython3.11-minimal:armhf (3.11.8-1) ... Selecting previously unselected package python3.11-minimal. Preparing to unpack .../47-python3.11-minimal_3.11.8-1_armhf.deb ... Unpacking python3.11-minimal (3.11.8-1) ... Setting up libpython3.11-minimal:armhf (3.11.8-1) ... Setting up libexpat1:armhf (2.6.2-1) ... Setting up python3.11-minimal (3.11.8-1) ... 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 ... 21711 files and directories currently installed.) Preparing to unpack .../0-python3-minimal_3.11.6-1_armhf.deb ... Unpacking python3-minimal (3.11.6-1) ... Selecting previously unselected package media-types. Preparing to unpack .../1-media-types_10.1.0_all.deb ... Unpacking media-types (10.1.0) ... Selecting previously unselected package netbase. Preparing to unpack .../2-netbase_6.4_all.deb ... Unpacking netbase (6.4) ... Selecting previously unselected package tzdata. Preparing to unpack .../3-tzdata_2024a-1_all.deb ... Unpacking tzdata (2024a-1) ... Selecting previously unselected package readline-common. Preparing to unpack .../4-readline-common_8.2-3_all.deb ... Unpacking readline-common (8.2-3) ... Selecting previously unselected package libreadline8:armhf. Preparing to unpack .../5-libreadline8_8.2-3+b1_armhf.deb ... Unpacking libreadline8:armhf (8.2-3+b1) ... Selecting previously unselected package libpython3.11-stdlib:armhf. Preparing to unpack .../6-libpython3.11-stdlib_3.11.8-1_armhf.deb ... Unpacking libpython3.11-stdlib:armhf (3.11.8-1) ... Selecting previously unselected package python3.11. Preparing to unpack .../7-python3.11_3.11.8-1_armhf.deb ... Unpacking python3.11 (3.11.8-1) ... Selecting previously unselected package libpython3-stdlib:armhf. Preparing to unpack .../8-libpython3-stdlib_3.11.6-1_armhf.deb ... Unpacking libpython3-stdlib:armhf (3.11.6-1) ... Setting up python3-minimal (3.11.6-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 ... 22699 files and directories currently installed.) Preparing to unpack .../000-python3_3.11.6-1_armhf.deb ... Unpacking python3 (3.11.6-1) ... Selecting previously unselected package sensible-utils. Preparing to unpack .../001-sensible-utils_0.0.22_all.deb ... Unpacking sensible-utils (0.0.22) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../002-libmagic-mgc_1%3a5.45-2+b1_armhf.deb ... Unpacking libmagic-mgc (1:5.45-2+b1) ... Selecting previously unselected package libmagic1:armhf. Preparing to unpack .../003-libmagic1_1%3a5.45-2+b1_armhf.deb ... Unpacking libmagic1:armhf (1:5.45-2+b1) ... Selecting previously unselected package file. Preparing to unpack .../004-file_1%3a5.45-2+b1_armhf.deb ... Unpacking file (1:5.45-2+b1) ... Selecting previously unselected package gettext-base. Preparing to unpack .../005-gettext-base_0.21-14+b1_armhf.deb ... Unpacking gettext-base (0.21-14+b1) ... Selecting previously unselected package libuchardet0:armhf. Preparing to unpack .../006-libuchardet0_0.0.8-1+b1_armhf.deb ... Unpacking libuchardet0:armhf (0.0.8-1+b1) ... Selecting previously unselected package groff-base. Preparing to unpack .../007-groff-base_1.23.0-3_armhf.deb ... Unpacking groff-base (1.23.0-3) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../008-bsdextrautils_2.39.3-6_armhf.deb ... Unpacking bsdextrautils (2.39.3-6) ... Selecting previously unselected package libpipeline1:armhf. Preparing to unpack .../009-libpipeline1_1.5.7-2_armhf.deb ... Unpacking libpipeline1:armhf (1.5.7-2) ... Selecting previously unselected package man-db. Preparing to unpack .../010-man-db_2.12.0-3_armhf.deb ... Unpacking man-db (2.12.0-3) ... 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_armhf.deb ... Unpacking m4 (1.4.19-4) ... Selecting previously unselected package autoconf. Preparing to unpack .../013-autoconf_2.71-3_all.deb ... Unpacking autoconf (2.71-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.21-14_all.deb ... Unpacking autopoint (0.21-14) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../017-libcoq-stdlib_8.18.0+dfsg-1_armhf.deb ... Unpacking libcoq-stdlib (8.18.0+dfsg-1) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../018-libstdlib-ocaml_4.14.1-1_armhf.deb ... Unpacking libstdlib-ocaml (4.14.1-1) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../019-ocaml-base_4.14.1-1_armhf.deb ... Unpacking ocaml-base (4.14.1-1) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../020-libfindlib-ocaml_1.9.6-1+b2_armhf.deb ... Unpacking libfindlib-ocaml (1.9.6-1+b2) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../021-libzarith-ocaml_1.13-2+b1_armhf.deb ... Unpacking libzarith-ocaml (1.13-2+b1) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../022-libcoq-core-ocaml_8.18.0+dfsg-1_armhf.deb ... Unpacking libcoq-core-ocaml (8.18.0+dfsg-1) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../023-libstdlib-ocaml-dev_4.14.1-1_armhf.deb ... Unpacking libstdlib-ocaml-dev (4.14.1-1) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../024-libcompiler-libs-ocaml-dev_4.14.1-1_armhf.deb ... Unpacking libcompiler-libs-ocaml-dev (4.14.1-1) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../025-ocaml-interp_4.14.1-1_armhf.deb ... Unpacking ocaml-interp (4.14.1-1) ... Selecting previously unselected package libncurses6:armhf. Preparing to unpack .../026-libncurses6_6.4+20240113-1_armhf.deb ... Unpacking libncurses6:armhf (6.4+20240113-1) ... Selecting previously unselected package libncurses-dev:armhf. Preparing to unpack .../027-libncurses-dev_6.4+20240113-1_armhf.deb ... Unpacking libncurses-dev:armhf (6.4+20240113-1) ... Selecting previously unselected package ocaml. Preparing to unpack .../028-ocaml_4.14.1-1_armhf.deb ... Unpacking ocaml (4.14.1-1) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../029-ocaml-findlib_1.9.6-1+b2_armhf.deb ... Unpacking ocaml-findlib (1.9.6-1+b2) ... Selecting previously unselected package coq. Preparing to unpack .../030-coq_8.18.0+dfsg-1_armhf.deb ... Unpacking coq (8.18.0+dfsg-1) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../031-libdebhelper-perl_13.15.3_all.deb ... Unpacking libdebhelper-perl (13.15.3) ... Selecting previously unselected package libtool. Preparing to unpack .../032-libtool_2.4.7-7_all.deb ... Unpacking libtool (2.4.7-7) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../033-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../034-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libsub-override-perl. Preparing to unpack .../035-libsub-override-perl_0.10-1_all.deb ... Unpacking libsub-override-perl (0.10-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../036-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../037-dh-strip-nondeterminism_1.13.1-1_all.deb ... Unpacking dh-strip-nondeterminism (1.13.1-1) ... Selecting previously unselected package libelf1:armhf. Preparing to unpack .../038-libelf1_0.190-1+b1_armhf.deb ... Unpacking libelf1:armhf (0.190-1+b1) ... Selecting previously unselected package dwz. Preparing to unpack .../039-dwz_0.15-1_armhf.deb ... Unpacking dwz (0.15-1) ... Selecting previously unselected package gettext. Preparing to unpack .../040-gettext_0.21-14+b1_armhf.deb ... Unpacking gettext (0.21-14+b1) ... 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.15.3_all.deb ... Unpacking debhelper (13.15.3) ... Selecting previously unselected package dh-coq. Preparing to unpack .../044-dh-coq_0.8_all.deb ... Unpacking dh-coq (0.8) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../045-dh-ocaml_2.0_all.deb ... Unpacking dh-ocaml (2.0) ... Selecting previously unselected package libgs-common. Preparing to unpack .../046-libgs-common_10.02.1~dfsg-3_all.deb ... Unpacking libgs-common (10.02.1~dfsg-3) ... Selecting previously unselected package libgs10-common. Preparing to unpack .../047-libgs10-common_10.02.1~dfsg-3_all.deb ... Unpacking libgs10-common (10.02.1~dfsg-3) ... Selecting previously unselected package libavahi-common-data:armhf. Preparing to unpack .../048-libavahi-common-data_0.8-13+b1_armhf.deb ... Unpacking libavahi-common-data:armhf (0.8-13+b1) ... Selecting previously unselected package libavahi-common3:armhf. Preparing to unpack .../049-libavahi-common3_0.8-13+b1_armhf.deb ... Unpacking libavahi-common3:armhf (0.8-13+b1) ... Selecting previously unselected package libdbus-1-3:armhf. Preparing to unpack .../050-libdbus-1-3_1.14.10-4_armhf.deb ... Unpacking libdbus-1-3:armhf (1.14.10-4) ... Selecting previously unselected package libavahi-client3:armhf. Preparing to unpack .../051-libavahi-client3_0.8-13+b1_armhf.deb ... Unpacking libavahi-client3:armhf (0.8-13+b1) ... Selecting previously unselected package libcups2:armhf. Preparing to unpack .../052-libcups2_2.4.7-1+b1_armhf.deb ... Unpacking libcups2:armhf (2.4.7-1+b1) ... Selecting previously unselected package libidn12:armhf. Preparing to unpack .../053-libidn12_1.42-2_armhf.deb ... Unpacking libidn12:armhf (1.42-2) ... Selecting previously unselected package libijs-0.35:armhf. Preparing to unpack .../054-libijs-0.35_0.35-15.1+b1_armhf.deb ... Unpacking libijs-0.35:armhf (0.35-15.1+b1) ... Selecting previously unselected package libjbig2dec0:armhf. Preparing to unpack .../055-libjbig2dec0_0.20-1+b1_armhf.deb ... Unpacking libjbig2dec0:armhf (0.20-1+b1) ... Selecting previously unselected package libpaper1:armhf. Preparing to unpack .../056-libpaper1_1.1.29_armhf.deb ... Unpacking libpaper1:armhf (1.1.29) ... Selecting previously unselected package libice6:armhf. Preparing to unpack .../057-libice6_2%3a1.0.10-1_armhf.deb ... Unpacking libice6:armhf (2:1.0.10-1) ... Selecting previously unselected package libsm6:armhf. Preparing to unpack .../058-libsm6_2%3a1.2.3-1_armhf.deb ... Unpacking libsm6:armhf (2:1.2.3-1) ... Selecting previously unselected package libxt6:armhf. Preparing to unpack .../059-libxt6_1%3a1.2.1-1.1_armhf.deb ... Unpacking libxt6:armhf (1:1.2.1-1.1) ... Selecting previously unselected package libgs10:armhf. Preparing to unpack .../060-libgs10_10.02.1~dfsg-3_armhf.deb ... Unpacking libgs10:armhf (10.02.1~dfsg-3) ... Selecting previously unselected package ghostscript. Preparing to unpack .../061-ghostscript_10.02.1~dfsg-3_armhf.deb ... Unpacking ghostscript (10.02.1~dfsg-3) ... Selecting previously unselected package help2man. Preparing to unpack .../062-help2man_1.49.3_armhf.deb ... Unpacking help2man (1.49.3) ... Selecting previously unselected package libnetpbm11:armhf. Preparing to unpack .../063-libnetpbm11_2%3a11.05.02-1_armhf.deb ... Unpacking libnetpbm11:armhf (2:11.05.02-1) ... Selecting previously unselected package netpbm. Preparing to unpack .../064-netpbm_2%3a11.05.02-1_armhf.deb ... Unpacking netpbm (2:11.05.02-1) ... Selecting previously unselected package tex-common. Preparing to unpack .../065-tex-common_6.18_all.deb ... Unpacking tex-common (6.18) ... Selecting previously unselected package libpaper-utils. Preparing to unpack .../066-libpaper-utils_1.1.29_armhf.deb ... Unpacking libpaper-utils (1.1.29) ... Selecting previously unselected package libkpathsea6:armhf. Preparing to unpack .../067-libkpathsea6_2023.20230311.66589-9_armhf.deb ... Unpacking libkpathsea6:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libptexenc1:armhf. Preparing to unpack .../068-libptexenc1_2023.20230311.66589-9_armhf.deb ... Unpacking libptexenc1:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libsynctex2:armhf. Preparing to unpack .../069-libsynctex2_2023.20230311.66589-9_armhf.deb ... Unpacking libsynctex2:armhf (2023.20230311.66589-9) ... Selecting previously unselected package libtexlua53-5:armhf. Preparing to unpack .../070-libtexlua53-5_2023.20230311.66589-9_armhf.deb ... Unpacking libtexlua53-5:armhf (2023.20230311.66589-9) ... Selecting previously unselected package t1utils. Preparing to unpack .../071-t1utils_1.41-4_armhf.deb ... Unpacking t1utils (1.41-4) ... Selecting previously unselected package libpixman-1-0:armhf. Preparing to unpack .../072-libpixman-1-0_0.42.2-1+b1_armhf.deb ... Unpacking libpixman-1-0:armhf (0.42.2-1+b1) ... Selecting previously unselected package libxcb-render0:armhf. Preparing to unpack .../073-libxcb-render0_1.15-1_armhf.deb ... Unpacking libxcb-render0:armhf (1.15-1) ... Selecting previously unselected package libxcb-shm0:armhf. Preparing to unpack .../074-libxcb-shm0_1.15-1_armhf.deb ... Unpacking libxcb-shm0:armhf (1.15-1) ... Selecting previously unselected package libxrender1:armhf. Preparing to unpack .../075-libxrender1_1%3a0.9.10-1.1_armhf.deb ... Unpacking libxrender1:armhf (1:0.9.10-1.1) ... Selecting previously unselected package libcairo2:armhf. Preparing to unpack .../076-libcairo2_1.18.0-1+b1_armhf.deb ... Unpacking libcairo2:armhf (1.18.0-1+b1) ... Selecting previously unselected package libgraphite2-3:armhf. Preparing to unpack .../077-libgraphite2-3_1.3.14-2_armhf.deb ... Unpacking libgraphite2-3:armhf (1.3.14-2) ... Selecting previously unselected package libharfbuzz0b:armhf. Preparing to unpack .../078-libharfbuzz0b_8.3.0-2_armhf.deb ... Unpacking libharfbuzz0b:armhf (8.3.0-2) ... Selecting previously unselected package libpotrace0:armhf. Preparing to unpack .../079-libpotrace0_1.16-2+b1_armhf.deb ... Unpacking libpotrace0:armhf (1.16-2+b1) ... Selecting previously unselected package libteckit0:armhf. Preparing to unpack .../080-libteckit0_2.5.12+ds1-1_armhf.deb ... Unpacking libteckit0:armhf (2.5.12+ds1-1) ... Selecting previously unselected package libxmu6:armhf. Preparing to unpack .../081-libxmu6_2%3a1.1.3-3_armhf.deb ... Unpacking libxmu6:armhf (2:1.1.3-3) ... Selecting previously unselected package libxpm4:armhf. Preparing to unpack .../082-libxpm4_1%3a3.5.17-1_armhf.deb ... Unpacking libxpm4:armhf (1:3.5.17-1) ... Selecting previously unselected package libxaw7:armhf. Preparing to unpack .../083-libxaw7_2%3a1.0.14-1_armhf.deb ... Unpacking libxaw7:armhf (2:1.0.14-1) ... Selecting previously unselected package libxi6:armhf. Preparing to unpack .../084-libxi6_2%3a1.8.1-1_armhf.deb ... Unpacking libxi6:armhf (2:1.8.1-1) ... Selecting previously unselected package libzzip-0-13:armhf. Preparing to unpack .../085-libzzip-0-13_0.13.72+dfsg.1-1.1+b1_armhf.deb ... Unpacking libzzip-0-13:armhf (0.13.72+dfsg.1-1.1+b1) ... Selecting previously unselected package texlive-binaries. Preparing to unpack .../086-texlive-binaries_2023.20230311.66589-9_armhf.deb ... Unpacking texlive-binaries (2023.20230311.66589-9) ... Selecting previously unselected package xdg-utils. Preparing to unpack .../087-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 .../088-texlive-base_2023.20240207-1_all.deb ... Unpacking texlive-base (2023.20240207-1) ... Selecting previously unselected package hicolor-icon-theme. Preparing to unpack .../089-hicolor-icon-theme_0.17-2_all.deb ... Unpacking hicolor-icon-theme (0.17-2) ... Selecting previously unselected package imagemagick-6.q16. Preparing to unpack .../090-imagemagick-6.q16_8%3a6.9.12.98+dfsg1-5+b1_armhf.deb ... Unpacking imagemagick-6.q16 (8:6.9.12.98+dfsg1-5+b1) ... Selecting previously unselected package imagemagick. Preparing to unpack .../091-imagemagick_8%3a6.9.12.98+dfsg1-5+b1_armhf.deb ... Unpacking imagemagick (8:6.9.12.98+dfsg1-5+b1) ... Selecting previously unselected package hevea. Preparing to unpack .../092-hevea_2.36-2+b1_armhf.deb ... Unpacking hevea (2.36-2+b1) ... Selecting previously unselected package libfindlib-ocaml-dev. Preparing to unpack .../093-libfindlib-ocaml-dev_1.9.6-1+b2_armhf.deb ... Unpacking libfindlib-ocaml-dev (1.9.6-1+b2) ... Selecting previously unselected package libgmpxx4ldbl:armhf. Preparing to unpack .../094-libgmpxx4ldbl_2%3a6.3.0+dfsg-2+b1_armhf.deb ... Unpacking libgmpxx4ldbl:armhf (2:6.3.0+dfsg-2+b1) ... Selecting previously unselected package libgmp-dev:armhf. Preparing to unpack .../095-libgmp-dev_2%3a6.3.0+dfsg-2+b1_armhf.deb ... Unpacking libgmp-dev:armhf (2:6.3.0+dfsg-2+b1) ... Selecting previously unselected package libgmp3-dev:armhf. Preparing to unpack .../096-libgmp3-dev_2%3a6.3.0+dfsg-2+b1_armhf.deb ... Unpacking libgmp3-dev:armhf (2:6.3.0+dfsg-2+b1) ... Selecting previously unselected package libzarith-ocaml-dev. Preparing to unpack .../097-libzarith-ocaml-dev_1.13-2+b1_armhf.deb ... Unpacking libzarith-ocaml-dev (1.13-2+b1) ... Selecting previously unselected package libcoq-core-ocaml-dev. Preparing to unpack .../098-libcoq-core-ocaml-dev_8.18.0+dfsg-1_armhf.deb ... Unpacking libcoq-core-ocaml-dev (8.18.0+dfsg-1) ... Selecting previously unselected package liblua5.4-0:armhf. Preparing to unpack .../099-liblua5.4-0_5.4.6-3_armhf.deb ... Unpacking liblua5.4-0:armhf (5.4.6-3) ... Selecting previously unselected package libocamlgraph-ocaml-dev. Preparing to unpack .../100-libocamlgraph-ocaml-dev_2.1.0-1+b1_armhf.deb ... Unpacking libocamlgraph-ocaml-dev (2.1.0-1+b1) ... Selecting previously unselected package libyaml-0-2:armhf. Preparing to unpack .../101-libyaml-0-2_0.2.5-1_armhf.deb ... Unpacking libyaml-0-2:armhf (0.2.5-1) ... Selecting previously unselected package pandoc-data. Preparing to unpack .../102-pandoc-data_3.1.3-1_all.deb ... Unpacking pandoc-data (3.1.3-1) ... Selecting previously unselected package pandoc. Preparing to unpack .../103-pandoc_3.1.3+ds-2_armhf.deb ... Unpacking pandoc (3.1.3+ds-2) ... Setting up media-types (10.1.0) ... Setting up libpipeline1:armhf (1.5.7-2) ... Setting up libgraphite2-3:armhf (1.3.14-2) ... Setting up liblcms2-2:armhf (2.14-2+b1) ... Setting up libpixman-1-0:armhf (0.42.2-1+b1) ... Setting up libsharpyuv0:armhf (1.3.2-0.4) ... Setting up libxau6:armhf (1:1.0.9-1) ... Setting up imagemagick-6-common (8:6.9.12.98+dfsg1-5) ... Setting up libicu72:armhf (72.1-4+b1) ... Setting up liblerc4:armhf (4.0.0+ds-4+b1) ... Setting up bsdextrautils (2.39.3-6) ... Setting up hicolor-icon-theme (0.17-2) ... Setting up libmagic-mgc (1:5.45-2+b1) ... Setting up dh-coq (0.8) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libyaml-0-2:armhf (0.2.5-1) ... Setting up libglib2.0-0:armhf (2.78.4-1) ... No schema files found: doing nothing. Setting up libijs-0.35:armhf (0.35-15.1+b1) ... Setting up libdebhelper-perl (13.15.3) ... Setting up libgs-common (10.02.1~dfsg-3) ... Setting up libbrotli1:armhf (1.1.0-2+b3) ... Setting up x11-common (1:7.7+23) ... invoke-rc.d: could not determine current runlevel Setting up X socket directories... /tmp/.X11-unix /tmp/.ICE-unix. Setting up dh-ocaml (2.0) ... Setting up libmagic1:armhf (1:5.45-2+b1) ... Setting up libnetpbm11:armhf (2:11.05.02-1) ... Setting up libdeflate0:armhf (1.20-1) ... Setting up gettext-base (0.21-14+b1) ... Setting up m4 (1.4.19-4) ... Setting up libzzip-0-13:armhf (0.13.72+dfsg.1-1.1+b1) ... Setting up file (1:5.45-2+b1) ... Setting up libjbig0:armhf (2.1-6.1+b1) ... Setting up poppler-data (0.4.12-1) ... Setting up tzdata (2024a-1) ... Current default time zone: 'Etc/UTC' Local time is now: Mon Apr 22 00:10:03 UTC 2024. Universal Time is now: Mon Apr 22 00:10:03 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up libfontenc1:armhf (1:1.1.8-1) ... Setting up autotools-dev (20220109.1) ... Setting up libcoq-stdlib (8.18.0+dfsg-1) ... Setting up libgmpxx4ldbl:armhf (2:6.3.0+dfsg-2+b1) ... Setting up libjpeg62-turbo:armhf (1:2.1.5-2+b2) ... Setting up libx11-data (2:1.8.7-1) ... Setting up libjbig2dec0:armhf (0.20-1+b1) ... Setting up libteckit0:armhf (2.5.12+ds1-1) ... Setting up libavahi-common-data:armhf (0.8-13+b1) ... Setting up libncurses6:armhf (6.4+20240113-1) ... Setting up libdbus-1-3:armhf (1.14.10-4) ... Setting up xfonts-encodings (1:1.0.4-2.2) ... Setting up t1utils (1.41-4) ... Setting up libtexlua53-5:armhf (2023.20230311.66589-9) ... Setting up libstdlib-ocaml (4.14.1-1) ... Setting up libpng16-16:armhf (1.6.43-1) ... Setting up libidn12:armhf (1.42-2) ... Setting up autopoint (0.21-14) ... Setting up ocaml-base (4.14.1-1) ... Setting up libltdl7:armhf (2.4.7-7) ... Setting up libfftw3-double3:armhf (3.3.10-1+b1) ... Setting up libkpathsea6:armhf (2023.20230311.66589-9) ... Setting up autoconf (2.71-3) ... Setting up libwebp7:armhf (1.3.2-0.4) ... Setting up libdav1d7:armhf (1.4.1-1) ... Setting up liblqr-1-0:armhf (0.4.2-2.1) ... Setting up sensible-utils (0.0.22) ... Setting up libtiff6:armhf (4.5.1+git230720-4) ... Setting up libuchardet0:armhf (0.0.8-1+b1) ... Setting up liblua5.4-0:armhf (5.4.6-3) ... Setting up libopenjp2-7:armhf (2.5.0-2+b2) ... Setting up libsub-override-perl (0.10-1) ... Setting up netbase (6.4) ... Setting up pandoc-data (3.1.3-1) ... Setting up libraw23:armhf (0.21.2-2) ... Setting up libde265-0:armhf (1.0.15-1) ... Setting up libwebpmux3:armhf (1.3.2-0.4) ... Setting up libbsd0:armhf (0.12.2-1) ... Setting up libelf1:armhf (0.190-1+b1) ... Setting up readline-common (8.2-3) ... Setting up libxml2:armhf (2.9.14+dfsg-1.3+b2) ... 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-6+b1) ... Setting up libsynctex2:armhf (2023.20230311.66589-9) ... Setting up libpotrace0:armhf (1.16-2+b1) ... 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.13.1-1) ... Setting up libice6:armhf (2:1.0.10-1) ... Setting up libxdmcp6:armhf (1:1.1.2-3) ... Setting up libncurses-dev:armhf (6.4+20240113-1) ... Setting up libxcb1:armhf (1.15-1) ... Setting up gettext (0.21-14+b1) ... Setting up libgmp-dev:armhf (2:6.3.0+dfsg-2+b1) ... Setting up libtool (2.4.7-7) ... Setting up libstdlib-ocaml-dev (4.14.1-1) ... Setting up libxcb-render0:armhf (1.15-1) ... Setting up libwebpdemux2:armhf (1.3.2-0.4) ... Setting up libreadline8:armhf (8.2-3+b1) ... Setting up libavahi-common3:armhf (0.8-13+b1) ... Setting up libfindlib-ocaml (1.9.6-1+b2) ... Setting up libxcb-shm0:armhf (1.15-1) ... Setting up libzarith-ocaml (1.13-2+b1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up help2man (1.49.3) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (4.14.1-1) ... Setting up ocaml-interp (4.14.1-1) ... Setting up libptexenc1:armhf (2023.20230311.66589-9) ... Setting up pandoc (3.1.3+ds-2) ... Setting up libfreetype6:armhf (2.13.2+dfsg-1+b1) ... Setting up ocaml-findlib (1.9.6-1+b2) ... Setting up ucf (3.0043+nmu1) ... Setting up dh-strip-nondeterminism (1.13.1-1) ... Setting up dwz (0.15-1) ... Setting up libcoq-core-ocaml (8.18.0+dfsg-1) ... Setting up groff-base (1.23.0-3) ... Setting up libgmp3-dev:armhf (2:6.3.0+dfsg-2+b1) ... Setting up libx11-6:armhf (2:1.8.7-1) ... Setting up libharfbuzz0b:armhf (8.3.0-2) ... Setting up libsm6:armhf (2:1.2.3-1) ... Setting up libavahi-client3:armhf (0.8-13+b1) ... Setting up libpaper1:armhf (1.1.29) ... Creating config file /etc/papersize with new version Setting up libxpm4:armhf (1:3.5.17-1) ... Setting up libxrender1:armhf (1:0.9.10-1.1) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up libpython3.11-stdlib:armhf (3.11.8-1) ... Setting up libxext6:armhf (2:1.3.4-1+b1) ... Setting up libpaper-utils (1.1.29) ... Setting up ocaml (4.14.1-1) ... Setting up xfonts-utils (1:7.7+6) ... Setting up man-db (2.12.0-3) ... 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 netpbm (2:11.05.02-1) ... Setting up libxt6:armhf (1:1.2.1-1.1) ... Setting up libfindlib-ocaml-dev (1.9.6-1+b2) ... Setting up libcups2:armhf (2.4.7-1+b1) ... Setting up libzarith-ocaml-dev (1.13-2+b1) ... Setting up libpython3-stdlib:armhf (3.11.6-1) ... Setting up libocamlgraph-ocaml-dev (2.1.0-1+b1) ... Setting up python3.11 (3.11.8-1) ... Setting up libxmu6:armhf (2:1.1.3-3) ... Setting up libxi6:armhf (2:1.8.1-1) ... Setting up debhelper (13.15.3) ... Setting up python3 (3.11.6-1) ... Setting up libxaw7:armhf (2:1.0.14-1) ... Setting up fonts-urw-base35 (20200910-8) ... Setting up coq (8.18.0+dfsg-1) ... Setting up libcoq-core-ocaml-dev (8.18.0+dfsg-1) ... Setting up libgs10-common (10.02.1~dfsg-3) ... Setting up fontconfig-config (2.15.0-1.1) ... Setting up libfontconfig1:armhf (2.15.0-1.1) ... Setting up libgs10:armhf (10.02.1~dfsg-3) ... Setting up ghostscript (10.02.1~dfsg-3) ... Setting up libcairo2:armhf (1.18.0-1+b1) ... Setting up texlive-binaries (2023.20230311.66589-9) ... 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 (2023.20240207-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:armhf (1.17.6-1) ... Setting up libheif-plugin-libde265:armhf (1.17.6-1) ... Setting up libheif1:armhf (1.17.6-1) ... Setting up libmagickcore-6.q16-7:armhf (8:6.9.12.98+dfsg1-5+b1) ... Setting up libmagickwand-6.q16-7:armhf (8:6.9.12.98+dfsg1-5+b1) ... Setting up imagemagick-6.q16 (8:6.9.12.98+dfsg1-5+b1) ... update-alternatives: using /usr/bin/compare-im6.q16 to provide /usr/bin/compare (compare) in auto mode update-alternatives: using /usr/bin/compare-im6.q16 to provide /usr/bin/compare-im6 (compare-im6) in auto mode update-alternatives: using /usr/bin/animate-im6.q16 to provide /usr/bin/animate (animate) in auto mode update-alternatives: using /usr/bin/animate-im6.q16 to provide /usr/bin/animate-im6 (animate-im6) in auto mode update-alternatives: using /usr/bin/convert-im6.q16 to provide /usr/bin/convert (convert) in auto mode update-alternatives: using /usr/bin/convert-im6.q16 to provide /usr/bin/convert-im6 (convert-im6) in auto mode update-alternatives: using /usr/bin/composite-im6.q16 to provide /usr/bin/composite (composite) in auto mode update-alternatives: using /usr/bin/composite-im6.q16 to provide /usr/bin/composite-im6 (composite-im6) in auto mode update-alternatives: using /usr/bin/conjure-im6.q16 to provide /usr/bin/conjure (conjure) in auto mode update-alternatives: using /usr/bin/conjure-im6.q16 to provide /usr/bin/conjure-im6 (conjure-im6) in auto mode update-alternatives: using /usr/bin/import-im6.q16 to provide /usr/bin/import (import) in auto mode update-alternatives: using /usr/bin/import-im6.q16 to provide /usr/bin/import-im6 (import-im6) in auto mode update-alternatives: using /usr/bin/identify-im6.q16 to provide /usr/bin/identify (identify) in auto mode update-alternatives: using /usr/bin/identify-im6.q16 to provide /usr/bin/identify-im6 (identify-im6) in auto mode update-alternatives: using /usr/bin/stream-im6.q16 to provide /usr/bin/stream (stream) in auto mode update-alternatives: using /usr/bin/stream-im6.q16 to provide /usr/bin/stream-im6 (stream-im6) in auto mode update-alternatives: using /usr/bin/display-im6.q16 to provide /usr/bin/display (display) in auto mode update-alternatives: using /usr/bin/display-im6.q16 to provide /usr/bin/display-im6 (display-im6) in auto mode update-alternatives: using /usr/bin/montage-im6.q16 to provide /usr/bin/montage (montage) in auto mode update-alternatives: using /usr/bin/montage-im6.q16 to provide /usr/bin/montage-im6 (montage-im6) in auto mode update-alternatives: using /usr/bin/mogrify-im6.q16 to provide /usr/bin/mogrify (mogrify) in auto mode update-alternatives: using /usr/bin/mogrify-im6.q16 to provide /usr/bin/mogrify-im6 (mogrify-im6) in auto mode Setting up hevea (2.36-2+b1) ... Setting up imagemagick (8:6.9.12.98+dfsg1-5+b1) ... Processing triggers for libc-bin (2.37-15) ... 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: Running cd /build/reproducible-path/ott-0.33+ds/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../ott_0.33+ds-2_source.changes dpkg-buildpackage: info: source package ott dpkg-buildpackage: info: source version 0.33+ds-2 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Julien Puydt dpkg-source --before-build . dpkg-buildpackage: info: host architecture armhf 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 63, characters 57-66: Warning: Notation plus_comm is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_base.v", line 63, characters 57-66: Warning: Notation plus_comm is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_base.v", line 63, characters 57-66: Warning: Notation plus_comm is deprecated since 8.16. The Arith.Plus file is obsolete. Use Nat.add_comm instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] 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 File "./ott_list_nth.v", line 38, characters 31-38: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_nth.v", line 44, characters 35-42: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_nth.v", line 44, characters 35-42: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_nth.v", line 44, characters 35-42: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_nth.v", line 68, characters 45-52: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_nth.v", line 68, characters 45-52: Warning: Notation le_Sn_O is deprecated since 8.16. The Arith.Le file is obsolete. Use Nat.nle_succ_0 instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] COQC ott_list_takedrop.v File "./ott_list_takedrop.v", line 54, characters 34-37: Warning: Notation min is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 79, characters 42-45: Warning: Notation min is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 82, characters 12-15: Warning: Notation min is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 82, characters 12-15: Warning: Notation min is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 172, 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 172, 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 172, 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 181, 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 181, 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 181, 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 198, 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 198, 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 212, characters 12-19: Warning: Notation min_dec is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_dec instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] File "./ott_list_takedrop.v", line 212, characters 12-19: Warning: Notation min_dec is deprecated since 8.16. The Arith.Min file is obsolete. Use Nat.min_dec instead. [deprecated-syntactic-definition-since-8.16,deprecated-since-8.16,deprecated-syntactic-definition,deprecated,default] COQC ott_list_predicate.v COQC ott_list_mem.v File "./ott_list_mem.v", line 151, characters 22-30: Warning: Tactic elimtype is deprecated since 8.18. Use [elim] instead. [deprecated-tactic-since-8.18,deprecated-since-8.18,deprecated-tactic,deprecated,default] COQC ott_list_flat_map.v COQC ott_list_repeat.v COQC ott_list_distinct.v File "./ott_list_distinct.v", line 165, characters 39-47: Warning: Tactic elimtype is deprecated since 8.18. Use [elim] instead. [deprecated-tactic-since-8.18,deprecated-since-8.18,deprecated-tactic,deprecated,default] 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 42-56: 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: _::_::_ 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 10-30: 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", lines 289-290, characters 14-18: 289 | ..............[Res_char c; Res_charl l] = 290 | Res_charl (c::l).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char _::Res_charl _::_::_ File "new_term_parser.ml", lines 292-293, characters 20-46: 292 | ....................[Res_char c; Res_charl l] = 293 | Res_string (Auxl.string_of_char_list (c::l)).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char _::Res_charl _::_::_ File "new_term_parser.ml", line 295, characters 14-58: 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 _::Res_stlil _::_::_ 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 14-42: 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 _::_::_ File "new_term_parser.ml", line 401, characters 8-42: 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 _::_::_ File "new_term_parser.ml", line 416, characters 16-51: 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: _::_::_::_::_ File "new_term_parser.ml", lines 463-467, characters 26-65: 463 | ..........................(fun [Res_stli (Stli_single (_, es1)); 464 | _; 465 | Res_int n'; 466 | Res_stli (Stli_single (_, es2))] -> 467 | process_dot_listform_res es1 n' 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 (_, _))::_::Res_int _::Res_stli (Stli_single (_, _)):: _::_ File "new_term_parser.ml", lines 476-482, characters 26-65: 476 | ..........................(fun [Res_stli (Stli_single (_, es1)); 477 | _; 478 | _; 479 | Res_int n'; 480 | _; 481 | Res_stli (Stli_single (_, es2))] -> 482 | process_dot_listform_res es1 n' 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 (_, _))::_::_::Res_int _::_:: Res_stli (Stli_single (_, _))::_::_ File "new_term_parser.ml", lines 488-500, characters 18-53: 488 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 489 | _] -> 490 | let es'' = 491 | List.map 492 | (Merge.abstract_indexvar_symterm_element ivr 0) ... 497 | stl_elements = es''; 498 | stl_loc = dummy_loc} 499 | in 500 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::_ File "new_term_parser.ml", lines 508-523, characters 18-53: 508 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 509 | _; 510 | _; Res_string ivr'; 511 | _] -> 512 | let es'' = ... 520 | let stlb = {stl_bound = b; 521 | stl_elements = es''; 522 | stl_loc = dummy_loc} in 523 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::Res_string _::_:: _::_ File "new_term_parser.ml", lines 536-557, characters 18-53: 536 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 537 | _; 538 | _; 539 | Res_string lower; 540 | _; ... 554 | let stlb = {stl_bound = b; 555 | stl_elements = es''; 556 | stl_loc = dummy_loc} in 557 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::Res_string _::_:: Res_int _::_::Res_si _::_::_::_ File "new_term_parser.ml", line 560, characters 18-53: 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 _::_::_ File "new_term_parser.ml", line 574, characters 24-59: 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: _::_::_::_::_ File "new_term_parser.ml", line 603, characters 15-44: 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 15-44: 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 12-29: 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: _::_::_::_ File "new_term_parser.ml", lines 638-639, characters 13-63: 638 | .............(fun [_; Res_sil l] -> 639 | Res_st (St_nonterm (dummy_loc, ntr, (nt', l)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", lines 649-653, characters 18-55: 649 | ..................(fun [_; Res_sil l] -> 650 | Res_st (St_nontermsub (dummy_loc, 651 | ntl, 652 | Auxl.promote_ntr xd ntr, 653 | (nt', l)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", lines 664-665, characters 6-59: 664 | ......(fun [_; Res_sil x] -> 665 | Res_ste (Ste_metavar (dummy_loc, name, (mvr, x)))) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", line 695, characters 14-100: 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", lines 703-707, characters 16-68: 703 | ................(fun [_; Res_string s] -> 704 | if is_tm s then 705 | raise Reject_parse 706 | else 707 | Res_ste (Ste_var (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_string _::_::_ File "new_term_parser.ml", lines 710-711, characters 16-66: 710 | ................(fun [_; Res_string s] -> 711 | Res_ste (Ste_var (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_string _::_::_ File "new_term_parser.ml", lines 715-719, characters 16-23: 715 | ................(fun [((Res_ste (Ste_var (_, _, s))) as x)] -> 716 | if is_tm s then 717 | raise Reject_parse 718 | else 719 | 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 (_, _, _))::_::_ File "new_term_parser.ml", line 742, characters 6-41: 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 _::_::_ File "new_term_parser.ml", line 748, characters 6-68: 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 _::_::_ File "new_term_parser.ml", line 761, characters 6-53: 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 _::Res_sil _::_::_ File "new_term_parser.ml", line 767, characters 6-73: 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 _::_::_ File "new_term_parser.ml", line 771, characters 6-24: 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: _::_::_ File "new_term_parser.ml", line 794, characters 6-47: 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 _::_::_ File "new_term_parser.ml", line 796, characters 6-48: 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 _::_::_ File "new_term_parser.ml", line 831, characters 6-52: 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 _::_::_ File "new_term_parser.ml", line 835, characters 6-53: 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 _::_::_ File "new_term_parser.ml", lines 846-847, characters 13-61: 846 | .............(fun [_; Res_sil x] -> 847 | Res_st (St_nonterm (dummy_loc, "", (nt, x)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", line 858, characters 13-27: 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: _::_::_ 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 25-54: 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 _, 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 37-61: 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 4.14.1 Standard library directory: /usr/lib/ocaml 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:2: Warning: Suppressing nested a element ./README.tex:66: Warning: Suppressing nested a element ./README.tex:84: Warning: Suppressing nested a element ./README.tex:109: Warning: Suppressing nested a element ./README.tex:118: Warning: Suppressing nested a element ./README.tex:125: Warning: Suppressing nested a element ./README.tex:151: Warning: Suppressing nested a element ./README.tex:160: Warning: Suppressing nested a element ./README.tex:177: Warning: Suppressing nested a element ./README.tex:206: Warning: Command not found: \noalign ./README.tex:206: Warning: Command not found: \noalign ./README.tex:206: Warning: Command not found: \noalign ./README.tex:212: Warning: Suppressing nested a element ./README.tex:215: Warning: Suppressing nested a element ./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: \endHighlighting ./README.tex:227: Warning: Command not found: \endShaded ./README.tex:233: Warning: Command not found: \Shaded ./README.tex:234: Warning: Command not found: \Highlighting ./README.tex:235: Warning: Command not found: \NormalTok ./README.tex:236: Warning: Command not found: \NormalTok ./README.tex:236: Warning: Command not found: \textquotesingle ./README.tex:237: Warning: Command not found: \NormalTok ./README.tex:237: Warning: Command not found: \textquotesingle ./README.tex:238: Warning: Command not found: \endHighlighting ./README.tex:239: Warning: Command not found: \endShaded ./README.tex:242: Warning: Suppressing nested a element ./README.tex:250: Warning: Suppressing nested a element ./README.tex:263: Warning: Suppressing nested a element ./README.tex:275: Warning: Suppressing nested a element ./README.tex:302: Warning: Command not found: \noalign ./README.tex:302: Warning: Command not found: \noalign ./README.tex:302: Warning: Command not found: \noalign ./README.tex:305: Warning: Suppressing nested a element ./README.tex:480: Warning: Suppressing nested a element ./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:2: Warning: Suppressing nested a element ./README.tex:66: Warning: Suppressing nested a element ./README.tex:84: Warning: Suppressing nested a element ./README.tex:109: Warning: Suppressing nested a element ./README.tex:118: Warning: Suppressing nested a element ./README.tex:125: Warning: Suppressing nested a element ./README.tex:151: Warning: Suppressing nested a element ./README.tex:160: Warning: Suppressing nested a element ./README.tex:177: Warning: Suppressing nested a element ./README.tex:206: Warning: Command not found: \noalign ./README.tex:206: Warning: Command not found: \noalign ./README.tex:206: Warning: Command not found: \noalign ./README.tex:212: Warning: Suppressing nested a element ./README.tex:215: Warning: Suppressing nested a element ./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: \endHighlighting ./README.tex:227: Warning: Command not found: \endShaded ./README.tex:233: Warning: Command not found: \Shaded ./README.tex:234: Warning: Command not found: \Highlighting ./README.tex:235: Warning: Command not found: \NormalTok ./README.tex:236: Warning: Command not found: \NormalTok ./README.tex:236: Warning: Command not found: \textquotesingle ./README.tex:237: Warning: Command not found: \NormalTok ./README.tex:237: Warning: Command not found: \textquotesingle ./README.tex:238: Warning: Command not found: \endHighlighting ./README.tex:239: Warning: Command not found: \endShaded ./README.tex:242: Warning: Suppressing nested a element ./README.tex:250: Warning: Suppressing nested a element ./README.tex:263: Warning: Suppressing nested a element ./README.tex:275: Warning: Suppressing nested a element ./README.tex:302: Warning: Command not found: \noalign ./README.tex:302: Warning: Command not found: \noalign ./README.tex:302: Warning: Command not found: \noalign ./README.tex:305: Warning: Suppressing nested a element ./README.tex:480: Warning: Suppressing nested a element ./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: 106: latex: not found This is dvips(k) 2023.1 (TeX Live 2023) Copyright 2023 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/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_repeat.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_mem.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_base.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_support.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_nth.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_core.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_distinct.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.vo /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_predicate.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_repeat.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_mem.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_base.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_support.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_nth.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_core.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_distinct.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.v /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_predicate.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_takedrop.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_repeat.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_mem.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_base.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_eq_dec.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_support.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_nth.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_core.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_distinct.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/coq//user-contrib/Ott/ INSTALL ott_list_flat_map.glob /build/reproducible-path/ott-0.33+ds/debian/tmp//usr/lib/ocaml/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 42-56: 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: _::_::_ 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 10-30: 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", lines 289-290, characters 14-18: 289 | ..............[Res_char c; Res_charl l] = 290 | Res_charl (c::l).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char _::Res_charl _::_::_ File "new_term_parser.ml", lines 292-293, characters 20-46: 292 | ....................[Res_char c; Res_charl l] = 293 | Res_string (Auxl.string_of_char_list (c::l)).. Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: Res_char _::Res_charl _::_::_ File "new_term_parser.ml", line 295, characters 14-58: 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 _::Res_stlil _::_::_ 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 14-42: 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 _::_::_ File "new_term_parser.ml", line 401, characters 8-42: 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 _::_::_ File "new_term_parser.ml", line 416, characters 16-51: 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: _::_::_::_::_ File "new_term_parser.ml", lines 463-467, characters 26-65: 463 | ..........................(fun [Res_stli (Stli_single (_, es1)); 464 | _; 465 | Res_int n'; 466 | Res_stli (Stli_single (_, es2))] -> 467 | process_dot_listform_res es1 n' 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 (_, _))::_::Res_int _::Res_stli (Stli_single (_, _)):: _::_ File "new_term_parser.ml", lines 476-482, characters 26-65: 476 | ..........................(fun [Res_stli (Stli_single (_, es1)); 477 | _; 478 | _; 479 | Res_int n'; 480 | _; 481 | Res_stli (Stli_single (_, es2))] -> 482 | process_dot_listform_res es1 n' 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 (_, _))::_::_::Res_int _::_:: Res_stli (Stli_single (_, _))::_::_ File "new_term_parser.ml", lines 488-500, characters 18-53: 488 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 489 | _] -> 490 | let es'' = 491 | List.map 492 | (Merge.abstract_indexvar_symterm_element ivr 0) ... 497 | stl_elements = es''; 498 | stl_loc = dummy_loc} 499 | in 500 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::_ File "new_term_parser.ml", lines 508-523, characters 18-53: 508 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 509 | _; 510 | _; Res_string ivr'; 511 | _] -> 512 | let es'' = ... 520 | let stlb = {stl_bound = b; 521 | stl_elements = es''; 522 | stl_loc = dummy_loc} in 523 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::Res_string _::_:: _::_ File "new_term_parser.ml", lines 536-557, characters 18-53: 536 | ..................(fun [_; Res_stli (Stli_single (_, es)); _; _; Res_string ivr; 537 | _; 538 | _; 539 | Res_string lower; 540 | _; ... 554 | let stlb = {stl_bound = b; 555 | stl_elements = es''; 556 | stl_loc = dummy_loc} in 557 | Res_stli (Stli_listform stlb)). 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 (_, _))::_::_::Res_string _::_::_::Res_string _::_:: Res_int _::_::Res_si _::_::_::_ File "new_term_parser.ml", line 560, characters 18-53: 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 _::_::_ File "new_term_parser.ml", line 574, characters 24-59: 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: _::_::_::_::_ File "new_term_parser.ml", line 603, characters 15-44: 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 15-44: 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 12-29: 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: _::_::_::_ File "new_term_parser.ml", lines 638-639, characters 13-63: 638 | .............(fun [_; Res_sil l] -> 639 | Res_st (St_nonterm (dummy_loc, ntr, (nt', l)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", lines 649-653, characters 18-55: 649 | ..................(fun [_; Res_sil l] -> 650 | Res_st (St_nontermsub (dummy_loc, 651 | ntl, 652 | Auxl.promote_ntr xd ntr, 653 | (nt', l)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", lines 664-665, characters 6-59: 664 | ......(fun [_; Res_sil x] -> 665 | Res_ste (Ste_metavar (dummy_loc, name, (mvr, x)))) Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", line 695, characters 14-100: 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", lines 703-707, characters 16-68: 703 | ................(fun [_; Res_string s] -> 704 | if is_tm s then 705 | raise Reject_parse 706 | else 707 | Res_ste (Ste_var (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_string _::_::_ File "new_term_parser.ml", lines 710-711, characters 16-66: 710 | ................(fun [_; Res_string s] -> 711 | Res_ste (Ste_var (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_string _::_::_ File "new_term_parser.ml", lines 715-719, characters 16-23: 715 | ................(fun [((Res_ste (Ste_var (_, _, s))) as x)] -> 716 | if is_tm s then 717 | raise Reject_parse 718 | else 719 | 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 (_, _, _))::_::_ File "new_term_parser.ml", line 742, characters 6-41: 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 _::_::_ File "new_term_parser.ml", line 748, characters 6-68: 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 _::_::_ File "new_term_parser.ml", line 761, characters 6-53: 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 _::Res_sil _::_::_ File "new_term_parser.ml", line 767, characters 6-73: 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 _::_::_ File "new_term_parser.ml", line 771, characters 6-24: 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: _::_::_ File "new_term_parser.ml", line 794, characters 6-47: 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 _::_::_ File "new_term_parser.ml", line 796, characters 6-48: 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 _::_::_ File "new_term_parser.ml", line 831, characters 6-52: 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 _::_::_ File "new_term_parser.ml", line 835, characters 6-53: 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 _::_::_ File "new_term_parser.ml", lines 846-847, characters 13-61: 846 | .............(fun [_; Res_sil x] -> 847 | Res_st (St_nonterm (dummy_loc, "", (nt, x)))). Warning 8 [partial-match]: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::Res_sil _::_::_ File "new_term_parser.ml", line 858, characters 13-27: 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: _::_::_ 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 25-54: 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 _, 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 4.14.1 Standard library directory: /usr/lib/ocaml 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 dh_installdeb dh_coq dh_ocaml dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'libcoq-ott' in '../libcoq-ott_0.33+ds-2_armhf.deb'. dpkg-deb: building package 'ott-tools-dbgsym' in '../ott-tools-dbgsym_0.33+ds-2_armhf.deb'. dpkg-deb: building package 'ott-tools' in '../ott-tools_0.33+ds-2_armhf.deb'. dpkg-genbuildinfo --build=binary -O../ott_0.33+ds-2_armhf.buildinfo dpkg-genchanges --build=binary -O../ott_0.33+ds-2_armhf.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: 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/9041 and its subdirectories I: Current time: Sun Apr 21 12:16:10 -12 2024 I: pbuilder-time-stamp: 1713744970 Mon Apr 22 00:16:22 UTC 2024 I: 1st build successful. Starting 2nd build on remote node virt64z-armhf-rb.debian.net. Mon Apr 22 00:16:22 UTC 2024 I: Preparing to do remote build '2' on virt64z-armhf-rb.debian.net. Mon Apr 22 00:20:02 UTC 2024 I: Deleting $TMPDIR on virt64z-armhf-rb.debian.net. Mon Apr 22 00:20:05 UTC 2024 I: ott_0.33+ds-2_armhf.changes: Format: 1.8 Date: Thu, 21 Dec 2023 16:34:16 +0100 Source: ott Binary: libcoq-ott ott-tools ott-tools-dbgsym Architecture: armhf Version: 0.33+ds-2 Distribution: unstable Urgency: medium Maintainer: Debian OCaml Maintainers Changed-By: Julien Puydt Description: libcoq-ott - Ott tool (Coq plugin) ott-tools - Ott tool (executable) Closes: 1049273 Changes: ott (0.33+ds-2) unstable; urgency=medium . * Fix d/rules clean target (Closes: #1049273). Checksums-Sha1: adcac7f4089562fd8d79d6000fbae7953c0a7667 159856 libcoq-ott_0.33+ds-2_armhf.deb 227ee8a10a82457b3f6fae819095c7fc9c638c0c 338764 ott-tools-dbgsym_0.33+ds-2_armhf.deb 26b8db3b149dcb64b0cb0822e69812e00cef2e78 1286960 ott-tools_0.33+ds-2_armhf.deb 4660d87cd16a293ae981ba6bfb25453bc0298465 9782 ott_0.33+ds-2_armhf.buildinfo Checksums-Sha256: 0393bb1a8447315c3c2ad929fdb6d2ba99b17b095d1fcd07653a754d9f3d294d 159856 libcoq-ott_0.33+ds-2_armhf.deb 25a126e359ead9728a17ad922b9123181068e6eb9a7c147ced4171a18c6a4963 338764 ott-tools-dbgsym_0.33+ds-2_armhf.deb 298755f6fd17a34ba2832717b00bca5ee288e2efb7562fcfa543c9e179e86415 1286960 ott-tools_0.33+ds-2_armhf.deb b42d33495b7395e17ed2de1fd045ecc41b4f4f43a19f0fc3af397a3b7384d309 9782 ott_0.33+ds-2_armhf.buildinfo Files: 85eff37bcc9c6887d13213259cbbc0a9 159856 ocaml optional libcoq-ott_0.33+ds-2_armhf.deb fce09f4a3ace94a89986372b3cfff821 338764 debug optional ott-tools-dbgsym_0.33+ds-2_armhf.deb 0d5e1350b53ebb385bb1e0822ecb4e15 1286960 ocaml optional ott-tools_0.33+ds-2_armhf.deb 6e9e7143822aedaca9d0d0c65083b501 9782 ocaml optional ott_0.33+ds-2_armhf.buildinfo Mon Apr 22 00:20:06 UTC 2024 I: diffoscope 265 will be used to compare the two builds: Running as unit: rb-diffoscope-armhf_9-3705.service # Profiling output for: /usr/bin/diffoscope --timeout 7200 --html /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/ott_0.33+ds-2.diffoscope.html --text /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/ott_0.33+ds-2.diffoscope.txt --json /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/ott_0.33+ds-2.diffoscope.json --profile=- /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/b1/ott_0.33+ds-2_armhf.changes /srv/reproducible-results/rbuild-debian/r-b-build.rLLqENrm/b2/ott_0.33+ds-2_armhf.changes ## command (total time: 0.000s) 0.000s 1 call cmp (internal) ## has_same_content_as (total time: 0.000s) 0.000s 1 call abc.DotChangesFile ## main (total time: 0.413s) 0.413s 2 calls outputs 0.000s 1 call cleanup ## recognizes (total time: 0.039s) 0.039s 12 calls diffoscope.comparators.binary.FilesystemFile ## specialize (total time: 0.000s) 0.000s 1 call specialize Finished with result: success Main processes terminated with: code=exited/status=0 Service runtime: 770ms CPU time consumed: 769ms Mon Apr 22 00:20:07 UTC 2024 I: diffoscope 265 found no differences in the changes files, and a .buildinfo file also exists. Mon Apr 22 00:20:07 UTC 2024 I: ott from trixie built successfully and reproducibly on armhf. Mon Apr 22 00:20:08 UTC 2024 I: Submitting .buildinfo files to external archives: Mon Apr 22 00:20:08 UTC 2024 I: Submitting 12K b1/ott_0.33+ds-2_armhf.buildinfo.asc Mon Apr 22 00:20:09 UTC 2024 I: Submitting 12K b2/ott_0.33+ds-2_armhf.buildinfo.asc Mon Apr 22 00:20:10 UTC 2024 I: Done submitting .buildinfo files to http://buildinfo.debian.net/api/submit. Mon Apr 22 00:20:10 UTC 2024 I: Done submitting .buildinfo files. Mon Apr 22 00:20:10 UTC 2024 I: Removing signed ott_0.33+ds-2_armhf.buildinfo.asc files: removed './b1/ott_0.33+ds-2_armhf.buildinfo.asc' removed './b2/ott_0.33+ds-2_armhf.buildinfo.asc'