Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-iris/coq-iris_3.6.0-1+b1_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coq-iris-3.6.0-1+b1uivvbe47/coq-iris_3.6.0-1+b1_amd64.buildinfo Get source package info: coq-iris=3.6.0-1 Source URL: http://snapshot.notset.fr/mr/package/coq-iris/3.6.0-1/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6.1 biber=2.17-3 binutils=2.38.90.20220713-2 binutils-common=2.38.90.20220713-2 binutils-x86-64-linux-gnu=2.38.90.20220713-2 bsdextrautils=2.38-5 bsdutils=1:2.38-5 build-essential=12.9 bzip2=1.0.8-5 ca-certificates=20211016 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.3.0-5 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.8 debianutils=5.7-0.2 dh-autoreconf=20 dh-coq=0.3 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.9 dpkg-dev=1.21.9 dwz=0.14-1 file=1:5.41-4 findutils=4.9.0-3 fontconfig-config=2.13.1-4.4 fonts-dejavu-core=2.37-2 fonts-gfs-baskerville=1.1-6 fonts-gfs-porson=1.1-7 fonts-lmodern=2.005-1 g++=4:11.2.0-2 g++-11=11.3.0-5 gcc=4:11.2.0-2 gcc-11=11.3.0-5 gcc-11-base=11.3.0-5 gcc-12-base=12.1.0-7 gettext=0.21-6 gettext-base=0.21-6 grep=3.7-1 groff-base=1.22.4-8 gzip=1.12-1 hostname=3.23 init-system-helpers=1.64 intltool-debian=0.35.0+20060710.5 latexmk=1:4.77-1 libacl1=2.3.1-1 libalgorithm-c3-perl=0.11-1 libapache-pom-java=18-1 libarchive-zip-perl=1.68-1 libasan6=11.3.0-5 libatomic1=12.1.0-7 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libautovivification-perl=0.18-2 libb-hooks-endofscope-perl=0.26-1 libb-hooks-op-check-perl=0.22-2 libbinutils=2.38.90.20220713-2 libblkid1=2.38-5 libbrotli1=1.0.9-2+b3 libbsd0=0.11.6-1 libbtparse2=0.88-3+b3 libbusiness-isbn-data-perl=20210112.006-1 libbusiness-isbn-perl=3.006-1 libbusiness-ismn-perl=1.202-1 libbusiness-issn-perl=1.005-1 libbz2-1.0=1.0.8-5 libc-bin=2.33-8 libc-dev-bin=2.33-8 libc6=2.33-8 libc6-dev=2.33-8 libcairo2=1.16.0-6 libcap-ng0=0.8.3-1 libcap2=1:2.44-1 libcc1-0=12.1.0-7 libclass-accessor-perl=0.51-1 libclass-c3-perl=0.35-1 libclass-data-inheritable-perl=0.08-3 libclass-inspector-perl=1.36-2 libclass-method-modifiers-perl=2.13-1 libclass-singleton-perl=1.6-1 libclone-perl=0.45-1+b2 libcom-err2=1.46.5-2 libcommons-logging-java=1.2-3 libcommons-parent-java=43-1 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-stdlib=8.15.2+dfsg-2 libcoq-stdpp=1.7.0-2 libcrypt-dev=1:4.4.28-2 libcrypt1=1:4.4.28-2 libctf-nobfd0=2.38.90.20220713-2 libctf0=2.38.90.20220713-2 libdata-compare-perl=1.27-2 libdata-dump-perl=1.25-1 libdata-optlist-perl=0.112-1 libdata-uniqid-perl=0.12-2 libdate-simple-perl=3.0300-3+b2 libdatetime-calendar-julian-perl=0.107-1 libdatetime-format-builder-perl=0.8300-1 libdatetime-format-strptime-perl=1.7900-1 libdatetime-locale-perl=1:1.35-1 libdatetime-perl=2:1.57-1 libdatetime-timezone-perl=1:2.52-1+2022a libdatrie1=0.2.13-2 libdb5.3=5.3.28+dfsg1-0.10 libdebconfclient0=0.263 libdebhelper-perl=13.8 libdevel-callchecker-perl=0.008-1+b3 libdevel-stacktrace-perl=2.0400-1 libdpkg-perl=1.21.9 libdynaloader-functions-perl=0.003-2 libelf1=0.187-1 libencode-eucjpascii-perl=0.03-1+b1 libencode-eucjpms-perl=0.07-3+b10 libencode-hanextra-perl=0.23-6 libencode-jis2k-perl=0.03-2 libencode-locale-perl=1.05-2 libencode-perl=3.18-1 libeval-closure-perl=0.14-2 libexception-class-perl=1.45-1 libexpat1=2.4.8-1 libexporter-tiny-perl=1.002002-1 libffi8=3.4.2-4 libfile-find-rule-perl=0.34-2 libfile-listing-perl=6.15-1 libfile-sharedir-perl=1.118-1 libfile-slurper-perl=0.013-1 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libfontbox-java=1:1.8.16-2 libfontconfig1=2.13.1-4.4 libfontenc1=1:1.1.4-1 libfreetype6=2.12.1+dfsg-3 libgcc-11-dev=11.3.0-5 libgcc-s1=12.1.0-7 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libglib2.0-0=2.72.3-1 libgmp-dev=2:6.2.1+dfsg1-1 libgmp10=2:6.2.1+dfsg1-1 libgmp3-dev=2:6.2.1+dfsg1-1 libgmpxx4ldbl=2:6.2.1+dfsg1-1 libgomp1=12.1.0-7 libgpg-error0=1.45-2 libgprofng0=2.38.90.20220713-2 libgraphite2-3=1.3.14-1 libgssapi-krb5-2=1.19.2-2+b2 libharfbuzz0b=2.7.4-1+b1 libhtml-parser-perl=3.78-1 libhtml-tagset-perl=3.20-4 libhtml-tree-perl=5.07-2 libhttp-cookies-perl=6.10-1 libhttp-date-perl=6.05-1 libhttp-message-perl=6.37-1 libhttp-negotiate-perl=6.01-1 libice6=2:1.0.10-1 libicu71=71.1-3 libio-html-perl=1.004-3 libio-socket-ssl-perl=2.074-2 libipc-run3-perl=0.048-2 libisl23=0.25-1 libitm1=12.1.0-7 libk5crypto3=1.19.2-2+b2 libkeyutils1=1.6.3-1 libkpathsea6=2022.20220321.62855-4 libkrb5-3=1.19.2-2+b2 libkrb5support0=1.19.2-2+b2 liblingua-translit-perl=0.29-1 liblist-allutils-perl=0.19-1 liblist-moreutils-perl=0.430-2 liblist-moreutils-xs-perl=0.430-3 liblist-someutils-perl=0.58-1 liblist-utilsby-perl=0.12-1 liblog-log4perl-perl=1.55-1 liblsan0=12.1.0-7 liblwp-mediatypes-perl=6.04-1 liblwp-protocol-https-perl=6.10-1 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmd0=1.0.4-2 libmime-charset-perl=1.012.2-1 libmodule-implementation-perl=0.09-2 libmodule-runtime-perl=0.016-2 libmount1=2.38-5 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libmro-compat-perl=0.15-1 libnamespace-autoclean-perl=0.29-1 libnamespace-clean-perl=0.27-2 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnet-http-perl=6.22-1 libnet-ssleay-perl=1.92-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libnumber-compare-perl=0.03-2 libpackage-stash-perl=0.40-1 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpaper-utils=1.1.28+b1 libpaper1=1.1.28+b1 libparams-classify-perl=0.015-2 libparams-util-perl=1.102-1+b2 libparams-validate-perl=1.30-1+b2 libparams-validationcompiler-perl=0.30-1 libparse-recdescent-perl=1.967015+dfsg-3 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libpdfbox-java=1:1.8.16-2 libperl5.34=5.34.0-5 libpipeline1=1.5.6-1 libpixman-1-0=0.40.0-1 libpng16-16=1.6.37-5 libptexenc1=2022.20220321.62855-4 libpython3-stdlib=3.10.5-3 libpython3.10-minimal=3.10.5-1 libpython3.10-stdlib=3.10.5-1 libquadmath0=12.1.0-7 libreadline8=8.1.2-1.2 libreadonly-perl=2.050-3 libregexp-common-perl=2017060201-2 libregexp-ipv6-perl=0.03-3 librole-tiny-perl=2.002004-1 libscalar-list-utils-perl=1:1.62-1 libseccomp2=2.5.4-1 libselinux1=3.4-1 libsigsegv2=2.14-1 libsm6=2:1.2.3-1 libsmartcols1=2.38-5 libsombok3=2.4.0-2+b1 libsort-key-perl=1.33-3 libspecio-perl=0.48-1 libsqlite3-0=3.39.1-1 libssl3=3.0.4-2 libstdc++-11-dev=11.3.0-5 libstdc++6=12.1.0-7 libsub-exporter-perl=0.988-1 libsub-exporter-progressive-perl=0.001013-2 libsub-identify-perl=0.14-2 libsub-install-perl=0.928-2 libsub-name-perl=0.26-1+b2 libsub-override-perl=0.09-3 libsub-quote-perl=2.006006-1 libsynctex2=2022.20220321.62855-4 libsystemd0=251.3-1 libteckit0=2.5.11+ds1-1 libtexlua53-5=2022.20220321.62855-4 libtexluajit2=2022.20220321.62855-4 libtext-bibtex-perl=0.88-3+b3 libtext-csv-perl=2.01-1 libtext-csv-xs-perl=1.48-1 libtext-glob-perl=0.11-2 libtext-roman-perl=3.5-3 libthai-data=0.1.29-1 libthai0=0.1.29-1 libtie-cycle-perl=1.226-1 libtimedate-perl=2.3300-2 libtinfo6=6.3+20220423-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.7-4 libtry-tiny-perl=0.31-1 libtsan0=11.3.0-5 libubsan1=12.1.0-7 libuchardet0=0.0.7-1 libudev1=251.3-1 libunicode-linebreak-perl=0.0.20190101-1+b4 libunistring2=1.0-1 liburi-perl=5.12-1 libuuid1=2.38-5 libvariable-magic-perl=0.62-2 libwww-perl=6.67-1 libwww-robotrules-perl=6.02-1 libx11-6=2:1.7.5-1 libx11-data=2:1.7.5-1 libxau6=1:1.0.9-1 libxaw7=2:1.0.14-1 libxcb-render0=1.14-3 libxcb-shm0=1.14-3 libxcb1=1.14-3 libxdmcp6=1:1.1.2-3 libxext6=2:1.3.4-1 libxi6=2:1.8-1 libxml-libxml-perl=2.0207+dfsg+really+2.0134-1 libxml-libxml-simple-perl=1.01-1 libxml-libxslt-perl=2.002000-1 libxml-namespacesupport-perl=1.12-2 libxml-sax-base-perl=1.09-2 libxml-sax-perl=1.02+dfsg-3 libxml-writer-perl=0.900-1 libxml2=2.9.14+dfsg-1 libxmu6=2:1.1.3-3 libxpm4=1:3.5.12-1 libxrender1=1:0.9.10-1.1 libxslt1.1=1.1.35-1 libxstring-perl=0.005-1+b2 libxt6=1:1.2.1-1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 libzzip-0-13=0.13.72+dfsg.1-1.1 linux-libc-dev=5.18.5-1 lmodern=2.005-1 login=1:4.11.1+dfsg1-2 lsb-base=11.2 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3.1 media-types=8.0.0 ncurses-base=6.3+20220423-2 ncurses-bin=6.3+20220423-2 netbase=6.3 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 openssl=3.0.4-2 patch=2.7.6-7 perl=5.34.0-5 perl-base=5.34.0-5 perl-modules-5.34=5.34.0-5 perl-openssl-defaults=7+b1 po-debconf=1.0.21+nmu1 preview-latex-style=12.2-1 python3=3.10.5-3 python3-minimal=3.10.5-3 python3.10=3.10.5-1 python3.10-minimal=3.10.5-1 readline-common=8.1.2-1.2 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.03-1 t1utils=1.41-4 tar=1.34+dfsg-1 tex-common=6.17 texlive-base=2022.20220605-1 texlive-bibtex-extra=2022.20220605-1 texlive-binaries=2022.20220321.62855-4 texlive-fonts-extra=2022.20220605-1 texlive-fonts-recommended=2022.20220605-1 texlive-lang-greek=2022.20220605-1 texlive-latex-base=2022.20220605-1 texlive-latex-extra=2022.20220605-1 texlive-latex-recommended=2022.20220605-1 texlive-pictures=2022.20220605-1 texlive-science=2022.20220605-1 ucf=3.0043 util-linux=2.38-5 util-linux-extra=2.38-5 x11-common=1:7.7+23 xdg-utils=1.1.3-4.1 xfonts-encodings=1:1.0.4-2.1 xfonts-utils=1:7.7+6 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220724T155906Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220724T155906Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220722T085138Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d coq-iris=3.6.0-1 && mkdir -p /build/coq-iris-UspITt && dpkg-source --no-check -x /*.dsc /build/coq-iris-UspITt/coq-iris-3.6.0 && cd /build/coq-iris-UspITt/coq-iris-3.6.0 && { printf '%s' 'coq-iris (3.6.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * rebuild on buildd -- amd64 / i386 Build Daemon (x86-csail-01) Fri, 22 Jul 2022 09:28:43 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-iris-UspITt" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-iris-UspITt/coq-iris-3.6.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658482123" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-iris-UspITt /tmp/coq-iris-3.6.0-1+b1uivvbe47 bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220722T085138Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: null I: using /tmp/mmdebstrap.ejg1LQycSD as tempdir I: running apt-get update... I: downloading packages with apt... I: extracting archives... I: installing essential packages... I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "apt-get --yes install fakeroot util-linux"' exec /tmp/mmdebstrap.ejg1LQycSD Reading package lists... Building dependency tree... util-linux is already the newest version (2.38-5). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 136 kB of archives. After this operation, 401 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220722T085138Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220722T085138Z unstable/main amd64 fakeroot amd64 1.29-1 [87.3 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 136 kB in 0s (982 kB/s) Selecting previously unselected package libfakeroot:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 4625 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.29-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.29-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.29-1_amd64.deb ... Unpacking fakeroot (1.29-1) ... Setting up libfakeroot:amd64 (1.29-1) ... Setting up fakeroot (1.29-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-8) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220724T155906Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220724T155906Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220722T085138Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.ejg1LQycSD Get:1 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm InRelease [157 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20220722T085138Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main Sources [12.1 MB] Get:4 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main amd64 Packages [11.5 MB] Fetched 23.7 MB in 19s (1221 kB/s) Reading package lists... I: installing remaining packages inside the chroot... I: running --customize-hook in shell: sh -c 'chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash' exec /tmp/mmdebstrap.ejg1LQycSD I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-iris=3.6.0-1 && mkdir -p /build/coq-iris-UspITt && dpkg-source --no-check -x /*.dsc /build/coq-iris-UspITt/coq-iris-3.6.0 && cd /build/coq-iris-UspITt/coq-iris-3.6.0 && { printf '%s' 'coq-iris (3.6.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * rebuild on buildd -- amd64 / i386 Build Daemon (x86-csail-01) Fri, 22 Jul 2022 09:28:43 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-iris-UspITt"' exec /tmp/mmdebstrap.ejg1LQycSD Reading package lists... NOTICE: 'coq-iris' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/coq-iris.git Please use: git clone https://salsa.debian.org/ocaml-team/coq-iris.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 679 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main coq-iris 3.6.0-1 (dsc) [2147 B] Get:2 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main coq-iris 3.6.0-1 (tar) [665 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220724T155906Z bookworm/main coq-iris 3.6.0-1 (diff) [11.9 kB] Fetched 679 kB in 1s (1158 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coq-iris_3.6.0-1.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coq-iris in /build/coq-iris-UspITt/coq-iris-3.6.0 dpkg-source: info: unpacking coq-iris_3.6.0.orig.tar.gz dpkg-source: info: unpacking coq-iris_3.6.0-1.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-iris-UspITt/coq-iris-3.6.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658482123" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.ejg1LQycSD dpkg-buildpackage: info: source package coq-iris dpkg-buildpackage: info: source version 3.6.0-1+b1 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by amd64 / i386 Build Daemon (x86-csail-01) dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq,ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' # doesn't work like this make[1]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with coq,ocaml dh_update_autotools_config -a dh_autoreconf -a dh_ocamlinit -a dh_auto_configure -a debian/rules override_dh_auto_build make[1]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make -C tex make[2]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0/tex' latexmk iris -pdf Rc files read: /etc/LatexMk Latexmk: This is Latexmk, John Collins, 17 Mar. 2022. Version 4.77, version: 4.77. Latexmk: applying rule 'pdflatex'... Rule 'pdflatex': File changes, etc: Changed files, or newly in use since previous run(s): iris.tex Rule 'pdflatex': The following rules & subrules became out-of-date: pdflatex ------------ Run number 1 of rule 'pdflatex' ------------ ------------ Running 'pdflatex -recorder "iris.tex"' ------------ This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./iris.tex LaTeX2e <2021-11-15> patch level 1 L3 programming layer <2022-06-02> (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2021/10/04 v1.4n Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo)) (/usr/share/texmf/tex/latex/lm/lmodern.sty) (/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty (/usr/share/texmf/tex/latex/lm/t1lmr.fd)) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty (/usr/share/texlive/texmf-dist/tex/generic/babel/txtbabel.def) (/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf)) (/usr/share/texlive/texmf-dist/tex/generic/babel/locale/en/babel-english.tex) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.sty (/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty)) (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.sty (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.def)) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-dm.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-compat.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/standard.bbx)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.cfg) (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty))) (./setup.tex (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) (/usr/share/texlive/texmf-dist/tex/latex/mathpartir/mathpartir.sty) (./pftools.sty (./locallabel.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabbing/Tabbing.sty) (/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def))) (./iris.sty (/usr/share/texlive/texmf-dist/tex/latex/faktor/faktor.sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/pgf.revision.tex))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.de f))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonomet ric.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.cod e.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerari thmetics.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfint.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct. code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformation s.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.t ex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex)) ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex ) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65 .sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18 .sty)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgffor.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/math/pgfmath.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarytopaths.code.tex))) (/usr/share/texlive/texmf-dist/tex/latex/scalerel/scalerel.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty) (/usr/share/texlive/texmf-dist/tex/latex/dashbox/dashbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/tensor/tensor.sty) (/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty (/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty)) (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mathtools.sty (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mhsetup.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.geometric.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.geometric.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.misc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.misc.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.symbols.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.symbols.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.arrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.arrows.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.callouts.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.callouts.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.multipart.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.multipart.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryarrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarycalc.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta. code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty) (/usr/share/texlive/texmf-dist/tex/latex/semantic/semantic.sty Semantic Package v2.0(epsilon) [2003/10/28] CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ Loading features: (/usr/share/texlive/texmf-dist/tex/latex/semantic/ligature.sty) math mode ligatures, (/usr/share/texlive/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, (/usr/share/texlive/texmf-dist/tex/latex/semantic/tdiagram.sty) T diagrams, (/usr/share/texlive/texmf-dist/tex/latex/semantic/reserved.sty) reserved words, (/usr/share/texlive/texmf-dist/tex/latex/semantic/shrthand.sty ) short hands, and general definitions. ) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.sty (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.def) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))) (./iris.aux) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) *geometry* driver: auto-detecting *geometry* detected driver: pdftex (/usr/share/texlive/texmf-dist/tex/latex/biblatex/lbx/english.lbx) No file iris.bbl. (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (/usr/share/texmf/tex/latex/lm/ot1lmr.fd) (/usr/share/texmf/tex/latex/lm/omllmm.fd) (/usr/share/texmf/tex/latex/lm/omslmsy.fd) (/usr/share/texmf/tex/latex/lm/omxlmex.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) (/usr/share/texmf/tex/latex/lm/t1lmtt.fd) [1{/var/lib/texmf/fonts/map/pdftex/up dmap/pdftex.map}] No file iris.toc. [2] LaTeX Warning: Citation 'iris-ground-up' on page 3 undefined on input line 39. LaTeX Warning: Citation 'iris-ground-up' on page 3 undefined on input line 39. [3] (./algebra.tex LaTeX Warning: Citation 'catlogic' on page 4 undefined on input line 6. LaTeX Warning: Reference `ofe-mono' on page 4 undefined on input line 18. LaTeX Warning: Reference `ofe-limit' on page 4 undefined on input line 18. (/usr/share/texmf/tex/latex/lm/t1lmss.fd) [4] LaTeX Warning: Citation 'America-Rutten:JCSS89' on page 5 undefined on input li ne 98. LaTeX Warning: Citation 'birkedal:metric-space' on page 5 undefined on input li ne 98. [5] LaTeX Warning: Reference `ra-valid-op' on page 6 undefined on input line 128. LaTeX Warning: Reference `ra-core-id' on page 6 undefined on input line 134. LaTeX Warning: Reference `ra-core-idem' on page 6 undefined on input line 135. LaTeX Warning: Reference `ra-core-mono' on page 6 undefined on input line 135. LaTeX Warning: Reference `ra-incl' on page 6 undefined on input line 135. [6] LaTeX Warning: Reference `camera-extend' on page 7 undefined on input line 188. [7]) [8] (./constructions.tex LaTeX Warning: Reference `UPred-canonical' on page 9 undefined on input line 48 . [9] [10] [11] LaTeX Warning: Reference `sum-swap' on page 12 undefined on input line 213. [12] LaTeX Warning: Citation 'caresl' on page 13 undefined on input line 286. [13] LaTeX Warning: Reference `ra-incl' on page 14 undefined on input line 321. ) [14] (./base-logic.tex LaTeX Warning: Hyper reference `lem:camera-unit-total-core' on page 15 undefine d on input line 5. LaTeX Warning: Reference `lem:camera-unit-total-core' on page 15 undefined on i nput line 5. [15] [16] [17] LaTeX Warning: Reference `upd-update' on page 18 undefined on input line 451. ) [18] (./model.tex LaTeX Warning: Citation 'catlogic' on page 19 undefined on input line 4. [19] LaTeX Warning: Hyper reference `thm:banach' on page 20 undefined on input line 105. LaTeX Warning: Reference `thm:banach' on page 20 undefined on input line 105. [20] LaTeX Warning: Hyper reference `sec:base-logic' on page 21 undefined on input l ine 127. LaTeX Warning: Reference `sec:base-logic' on page 21 undefined on input line 12 7. ) [21] (./extended-logic.tex LaTeX Warning: Reference `upd-intro' on page 22 undefined on input line 28. LaTeX Warning: Reference `upd-mono' on page 22 undefined on input line 29. LaTeX Warning: Reference `upd-trans' on page 22 undefined on input line 29. LaTeX Warning: Reference `upd-intro' on page 22 undefined on input line 37. LaTeX Warning: Reference `pers-elim' on page 22 undefined on input line 41. LaTeX Warning: Reference `pers-mono' on page 22 undefined on input line 42. LaTeX Warning: Reference `upd-update' on page 22 undefined on input line 54. [22] LaTeX Warning: Reference `upd-frame' on page 23 undefined on input line 68. [23] LaTeX Warning: Reference `later-mono' on page 24 undefined on input line 149. LaTeX Warning: Reference `Loeb' on page 24 undefined on input line 184. LaTeX Warning: Citation 'Loeb' on page 24 undefined on input line 184. LaTeX Warning: Hyper reference `sec:proof-rules' on page 24 undefined on input line 193. LaTeX Warning: Reference `sec:proof-rules' on page 24 undefined on input line 1 93. [24] LaTeX Warning: Reference `ex0-mono' on page 25 undefined on input line 228. LaTeX Warning: Reference `ex0-idem' on page 25 undefined on input line 228. LaTeX Warning: Reference `ex0-elim' on page 25 undefined on input line 238. [25] LaTeX Warning: Hyper reference `sec:base-logic' on page 26 undefined on input l ine 306. LaTeX Warning: Reference `sec:base-logic' on page 26 undefined on input line 30 6. LaTeX Warning: Hyper reference `thm:america_rutten' on page 26 undefined on inp ut line 334. LaTeX Warning: Reference `thm:america_rutten' on page 26 undefined on input lin e 334. [26] LaTeX Warning: Hyper reference `sec:base-logic' on page 27 undefined on input l ine 343. LaTeX Warning: Reference `sec:base-logic' on page 27 undefined on input line 34 3. LaTeX Warning: Hyper reference `sec:base-logic' on page 27 undefined on input l ine 348. LaTeX Warning: Reference `sec:base-logic' on page 27 undefined on input line 34 8. [27]) [28] (./language.tex (/usr/share/texmf/tex/latex/lm/ts1lmr.fd) Underfull \hbox (badness 10000) in paragraph at lines 11--14 Underfull \hbox (badness 10000) in paragraph at lines 36--37 Underfull \hbox (badness 10000) in paragraph at lines 38--39 Underfull \hbox (badness 10000) in paragraph at lines 40--41 [29]) [30] (./program-logic.tex LaTeX Warning: Hyper reference `sec:language' on page 31 undefined on input lin e 5. LaTeX Warning: Reference `sec:language' on page 31 undefined on input line 5. LaTeX Warning: Hyper reference `sec:composable-resources' on page 31 undefined on input line 7. LaTeX Warning: Reference `sec:composable-resources' on page 31 undefined on inp ut line 7. LaTeX Warning: Hyper reference `sec:base-logic' on page 31 undefined on input l ine 47. LaTeX Warning: Reference `sec:base-logic' on page 31 undefined on input line 47 . [31] LaTeX Warning: Hyper reference `sec:namespaces' on page 32 undefined on input l ine 84. LaTeX Warning: Reference `sec:namespaces' on page 32 undefined on input line 84 . [32] Overfull \hbox (7.57344pt too wide) detected at line 155 [] [33] [34] LaTeX Warning: Hyper reference `sec:model' on page 35 undefined on input line 2 43. LaTeX Warning: Reference `sec:model' on page 35 undefined on input line 243. [35] [36] Overfull \hbox (3.87889pt too wide) detected at line 311 [] \OMS/lmsy/m/n/10 ` 8\OML/lmm/m/it/10 ^^[[]; []: []\OMS/lmsy/m/n/10 9\OML/lmm /m/it/10 s; S; ^^H; ^^H[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; \OT1/lmr/m /n/10 0\OML/lmm/m/it/10 ; []; \OT1/lmr/m/n/10 0) \OMS/lmsy/m/n/10 ^^C [][] \OML /lmm/m/it/10 e[] [] \OMS/lmsy/m/n/10 ^^C \OT1/lmr/m/n/10 (\OMS/lmsy/m/n/10 8\OM L/lmm/m/it/10 ^^[[]; n[]; n[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; n[]\OT 1/lmr/m/n/10 ()\OML/lmm/m/it/10 ; n[]\OT1/lmr/m/n/10 ) [] \OML/lmm/m/it/10 ^^[ [] \OMS/lmsy/m/n/10 2 \OT1/lmr/m/n/10 ^^F) LaTeX Warning: Hyper reference `sec:invariants' on page 37 undefined on input l ine 388. LaTeX Warning: Reference `sec:invariants' on page 37 undefined on input line 38 8. [37] LaTeX Warning: Hyper reference `sec:invariants' on page 38 undefined on input l ine 410. LaTeX Warning: Reference `sec:invariants' on page 38 undefined on input line 41 0. LaTeX Warning: Reference `inv-open' on page 38 undefined on input line 433. LaTeX Warning: Reference `inv-open-timeless' on page 38 undefined on input line 433. [38] LaTeX Warning: Reference `vs-trans' on page 39 undefined on input line 445. LaTeX Warning: Reference `Ht-atomic' on page 39 undefined on input line 445. LaTeX Warning: Reference `inv-open' on page 39 undefined on input line 470. [39]) [40] (./derived.tex LaTeX Warning: Hyper reference `sec:invariants' on page 41 undefined on input l ine 5. LaTeX Warning: Reference `sec:invariants' on page 41 undefined on input line 5. LaTeX Warning: Reference `CInv-cancel' on page 41 undefined on input line 31. [41] LaTeX Warning: Citation 'iris2' on page 42 undefined on input line 96. [42] [43]) [44] (./paradoxes.tex LaTeX Warning: Hyper reference `app:section:invariants-without-a-later' on page 45 undefined on input line 10. LaTeX Warning: Reference `app:section:invariants-without-a-later' on page 45 un defined on input line 10. LaTeX Warning: Citation 'dodds:higher-order-sync' on page 45 undefined on input line 11. LaTeX Warning: Citation 'iris2' on page 45 undefined on input line 11. LaTeX Warning: Hyper reference `sec:base-logic' on page 45 undefined on input l ine 12. LaTeX Warning: Reference `sec:base-logic' on page 45 undefined on input line 12 . LaTeX Warning: Reference `sprop-alloc' on page 45 undefined on input line 32. LaTeX Warning: Reference `sprop-agree' on page 45 undefined on input line 32. LaTeX Warning: Reference `sprop-agree' on page 45 undefined on input line 36. LaTeX Warning: Hyper reference `thm:counterexample-1' on page 45 undefined on i nput line 39. LaTeX Warning: Reference `thm:counterexample-1' on page 45 undefined on input l ine 39. LaTeX Warning: Reference `sprop-persist' on page 45 undefined on input line 44. LaTeX Warning: Reference `sprop-alloc' on page 45 undefined on input line 46. LaTeX Warning: Reference `sprop-agree' on page 45 undefined on input line 57. [45] LaTeX Warning: Hyper reference `thm:counterexample-1' on page 46 undefined on i nput line 69. LaTeX Warning: Reference `thm:counterexample-1' on page 46 undefined on input l ine 69. LaTeX Warning: Hyper reference `thm:counterexample-1' on page 46 undefined on i nput line 70. LaTeX Warning: Reference `thm:counterexample-1' on page 46 undefined on input l ine 70. LaTeX Warning: Reference `sprop-alloc' on page 46 undefined on input line 75. LaTeX Warning: Reference `inv-open' on page 46 undefined on input line 81. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 89. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 98. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 102. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 106. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Warning: Reference `sprop-alloc' on page 46 undefined on input line 131. LaTeX Warning: Reference `sprop-persist' on page 46 undefined on input line 131 . LaTeX Warning: Reference `sprop-agree' on page 46 undefined on input line 132. LaTeX Warning: Hyper reference `lem:counterexample-invariants-saved-prop-agree' on page 46 undefined on input line 149. LaTeX Warning: Reference `lem:counterexample-invariants-saved-prop-agree' on pa ge 46 undefined on input line 149. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Warning: Reference `eq:inv-persistent' on page 46 undefined on input line 158. [46] LaTeX Warning: Reference `sprop-agree' on page 47 undefined on input line 166. LaTeX Warning: Reference `sprop-alloc' on page 47 undefined on input line 166. LaTeX Warning: Reference `eq:start-alloc' on page 47 undefined on input line 17 4. LaTeX Warning: Reference `eq:update-weaken-mask' on page 47 undefined on input line 174. LaTeX Warning: Reference `eq:inv-alloc' on page 47 undefined on input line 178. LaTeX Warning: Reference `eq:inv-open' on page 47 undefined on input line 199. LaTeX Warning: Reference `eq:start-finish' on page 47 undefined on input line 2 02. LaTeX Warning: Reference `eq:inv-open' on page 47 undefined on input line 211. LaTeX Warning: Reference `eq:start-not-finished' on page 47 undefined on input line 213. [47] LaTeX Warning: Hyper reference `lem:counterexample-invariants-saved-prop-agree' on page 48 undefined on input line 225. LaTeX Warning: Reference `lem:counterexample-invariants-saved-prop-agree' on pa ge 48 undefined on input line 225. LaTeX Warning: Hyper reference `sec:saved-prop-no-later' on page 48 undefined o n input line 227. LaTeX Warning: Reference `sec:saved-prop-no-later' on page 48 undefined on inpu t line 227. LaTeX Warning: Hyper reference `lem:counterexample-invariants-saved-prop-agree' on page 48 undefined on input line 228. LaTeX Warning: Reference `lem:counterexample-invariants-saved-prop-agree' on pa ge 48 undefined on input line 228. LaTeX Warning: Reference `sprop-agree' on page 48 undefined on input line 228. LaTeX Warning: Hyper reference `thm:counterexample-1' on page 48 undefined on i nput line 228. LaTeX Warning: Reference `thm:counterexample-1' on page 48 undefined on input l ine 228. ) [48] LaTeX Warning: Empty bibliography on input line 72. (./iris.aux) LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. Package rerunfilecheck Warning: File `iris.out' has changed. (rerunfilecheck) Rerun to get outlines right (rerunfilecheck) or use package `bookmark'. Package biblatex Warning: Please (re)run Biber on the file: (biblatex) iris (biblatex) and rerun LaTeX afterwards. ) (see the transcript file for additional information){/usr/share/texmf/fonts/enc /dvips/lm/lm-ec.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/sh are/texmf/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm -mathit.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texmf/fo nts/enc/dvips/lm/lm-mathex.enc} Output written on iris.pdf (48 pages, 802805 bytes). Transcript written on iris.log. Latexmk: Missing bbl file 'iris.bbl' in following: No file iris.bbl. Latexmk: Missing input file 'iris.toc' (or dependence on it) from following: 'No file iris.toc.' Latexmk: Getting log file 'iris.log' Latexmk: Examining 'iris.fls' Latexmk: Examining 'iris.log' Latexmk: References changed. Latexmk: References changed. Latexmk: Log file says output to 'iris.pdf' Latexmk: applying rule 'biber iris'... Rule 'biber iris': File changes, etc: Changed files, or newly in use since previous run(s): iris.bcf Rule 'biber iris': The following rules & subrules became out-of-date: biber iris ------------ Run number 1 of rule 'biber iris' ------------ ------------ Running 'biber "iris.bcf"' ------------ INFO - This is Biber 2.17 INFO - Logfile is 'iris.blg' INFO - Reading 'iris.bcf' INFO - Found 8 citekeys in bib section 0 INFO - Processing section 0 INFO - Looking for bibtex file 'bib.bib' for section 0 INFO - LaTeX decoding ... INFO - Found BibTeX data source 'bib.bib' INFO - Overriding locale 'en-US' defaults 'normalization = NFD' with 'normalization = prenormalized' INFO - Overriding locale 'en-US' defaults 'variable = shifted' with 'variable = non-ignorable' INFO - Sorting list 'nty/global//global/global' of type 'entry' with template 'nty' and locale 'en-US' INFO - No sort tailoring available for locale 'en-US' INFO - Writing 'iris.bbl' with encoding 'UTF-8' INFO - Output to iris.bbl Latexmk: Found biber source file(s) [bib.bib iris.bcf] Latexmk: applying rule 'pdflatex'... Rule 'pdflatex': File changes, etc: Changed files, or newly in use since previous run(s): iris.aux iris.bbl iris.out iris.toc Rule 'pdflatex': The following rules & subrules became out-of-date: pdflatex ------------ Run number 2 of rule 'pdflatex' ------------ ------------ Running 'pdflatex -recorder "iris.tex"' ------------ This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./iris.tex LaTeX2e <2021-11-15> patch level 1 L3 programming layer <2022-06-02> (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2021/10/04 v1.4n Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo)) (/usr/share/texmf/tex/latex/lm/lmodern.sty) (/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty (/usr/share/texmf/tex/latex/lm/t1lmr.fd)) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty (/usr/share/texlive/texmf-dist/tex/generic/babel/txtbabel.def) (/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf)) (/usr/share/texlive/texmf-dist/tex/generic/babel/locale/en/babel-english.tex) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.sty (/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty)) (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.sty (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.def)) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-dm.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-compat.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/standard.bbx)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.cfg) (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty))) (./setup.tex (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) (/usr/share/texlive/texmf-dist/tex/latex/mathpartir/mathpartir.sty) (./pftools.sty (./locallabel.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabbing/Tabbing.sty) (/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def))) (./iris.sty (/usr/share/texlive/texmf-dist/tex/latex/faktor/faktor.sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/pgf.revision.tex))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.de f))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonomet ric.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.cod e.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerari thmetics.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfint.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct. code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformation s.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.t ex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex)) ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex ) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65 .sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18 .sty)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgffor.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/math/pgfmath.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarytopaths.code.tex))) (/usr/share/texlive/texmf-dist/tex/latex/scalerel/scalerel.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty) (/usr/share/texlive/texmf-dist/tex/latex/dashbox/dashbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/tensor/tensor.sty) (/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty (/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty)) (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mathtools.sty (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mhsetup.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.geometric.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.geometric.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.misc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.misc.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.symbols.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.symbols.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.arrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.arrows.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.callouts.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.callouts.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.multipart.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.multipart.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryarrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarycalc.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta. code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty) (/usr/share/texlive/texmf-dist/tex/latex/semantic/semantic.sty Semantic Package v2.0(epsilon) [2003/10/28] CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ Loading features: (/usr/share/texlive/texmf-dist/tex/latex/semantic/ligature.sty) math mode ligatures, (/usr/share/texlive/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, (/usr/share/texlive/texmf-dist/tex/latex/semantic/tdiagram.sty) T diagrams, (/usr/share/texlive/texmf-dist/tex/latex/semantic/reserved.sty) reserved words, (/usr/share/texlive/texmf-dist/tex/latex/semantic/shrthand.sty ) short hands, and general definitions. ) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.sty (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.def) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))) (./iris.aux) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) *geometry* driver: auto-detecting *geometry* detected driver: pdftex (/usr/share/texlive/texmf-dist/tex/latex/biblatex/lbx/english.lbx) (./iris.bbl) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (./iris.out) (./iris.out) (/usr/share/texmf/tex/latex/lm/ot1lmr.fd) (/usr/share/texmf/tex/latex/lm/omllmm.fd) (/usr/share/texmf/tex/latex/lm/omslmsy.fd) (/usr/share/texmf/tex/latex/lm/omxlmex.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) (/usr/share/texmf/tex/latex/lm/t1lmtt.fd) [1{/var/lib/texmf/fonts/map/pdftex/up dmap/pdftex.map}] (./iris.toc [2]) [3] [4] (./algebra.tex (/usr/share/texmf/tex/latex/lm/t1lmss.fd) [5] [6] [7] [8]) [9] (./constructions.tex [10] [11] [12] [13] [14]) [15] (./base-logic.tex [16] [17] [18]) [19] (./model.tex [20] [21]) [22] (./extended-logic.tex [23] [24] [25] [26] [27] [28]) [29] (./language.tex (/usr/share/texmf/tex/latex/lm/ts1lmr.fd) Underfull \hbox (badness 10000) in paragraph at lines 11--14 Underfull \hbox (badness 10000) in paragraph at lines 36--37 Underfull \hbox (badness 10000) in paragraph at lines 38--39 Underfull \hbox (badness 10000) in paragraph at lines 40--41 [30]) [31] (./program-logic.tex [32] [33] Overfull \hbox (7.57344pt too wide) detected at line 155 [] [34] [35] [36] [37] Overfull \hbox (3.87889pt too wide) detected at line 311 [] \OMS/lmsy/m/n/10 ` 8\OML/lmm/m/it/10 ^^[[]; []: []\OMS/lmsy/m/n/10 9\OML/lmm /m/it/10 s; S; ^^H; ^^H[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; \OT1/lmr/m /n/10 0\OML/lmm/m/it/10 ; []; \OT1/lmr/m/n/10 0) \OMS/lmsy/m/n/10 ^^C [][] \OML /lmm/m/it/10 e[] [] \OMS/lmsy/m/n/10 ^^C \OT1/lmr/m/n/10 (\OMS/lmsy/m/n/10 8\OM L/lmm/m/it/10 ^^[[]; n[]; n[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; n[]\OT 1/lmr/m/n/10 ()\OML/lmm/m/it/10 ; n[]\OT1/lmr/m/n/10 ) [] \OML/lmm/m/it/10 ^^[ [] \OMS/lmsy/m/n/10 2 \OT1/lmr/m/n/10 ^^F) [38] [39] [40]) [41] (./derived.tex [42] [43] [44]) [45] (./paradoxes.tex [46] LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 89. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 98. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 102. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 106. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. [47] [48]) [49] [50] (./iris.aux) LaTeX Warning: There were undefined references. LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right. Package biblatex Warning: Please rerun LaTeX. ) (see the transcript file for additional information){/usr/share/texmf/fonts/enc /dvips/lm/lm-ec.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/sh are/texmf/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm -mathit.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texmf/fo nts/enc/dvips/lm/lm-mathex.enc} Output written on iris.pdf (50 pages, 819433 bytes). Transcript written on iris.log. Latexmk: Getting log file 'iris.log' Latexmk: Examining 'iris.fls' Latexmk: Examining 'iris.log' Latexmk: Found input bbl file 'iris.bbl' Latexmk: References changed. Latexmk: Log file says output to 'iris.pdf' Latexmk: Found biber source file(s) [bib.bib iris.bcf] Latexmk: applying rule 'pdflatex'... Rule 'pdflatex': File changes, etc: Changed files, or newly in use since previous run(s): iris.aux iris.run.xml iris.toc Rule 'pdflatex': The following rules & subrules became out-of-date: pdflatex ------------ Run number 3 of rule 'pdflatex' ------------ ------------ Running 'pdflatex -recorder "iris.tex"' ------------ This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./iris.tex LaTeX2e <2021-11-15> patch level 1 L3 programming layer <2022-06-02> (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2021/10/04 v1.4n Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo)) (/usr/share/texmf/tex/latex/lm/lmodern.sty) (/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty (/usr/share/texmf/tex/latex/lm/t1lmr.fd)) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty (/usr/share/texlive/texmf-dist/tex/generic/babel/txtbabel.def) (/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf)) (/usr/share/texlive/texmf-dist/tex/generic/babel/locale/en/babel-english.tex) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.sty (/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty)) (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.sty (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.def)) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-dm.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-compat.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/standard.bbx)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.cfg) (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty))) (./setup.tex (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) (/usr/share/texlive/texmf-dist/tex/latex/mathpartir/mathpartir.sty) (./pftools.sty (./locallabel.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabbing/Tabbing.sty) (/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def))) (./iris.sty (/usr/share/texlive/texmf-dist/tex/latex/faktor/faktor.sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/pgf.revision.tex))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.de f))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonomet ric.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.cod e.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerari thmetics.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfint.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct. code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformation s.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.t ex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex)) ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex ) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65 .sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18 .sty)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgffor.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/math/pgfmath.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarytopaths.code.tex))) (/usr/share/texlive/texmf-dist/tex/latex/scalerel/scalerel.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty) (/usr/share/texlive/texmf-dist/tex/latex/dashbox/dashbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/tensor/tensor.sty) (/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty (/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty)) (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mathtools.sty (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mhsetup.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.geometric.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.geometric.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.misc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.misc.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.symbols.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.symbols.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.arrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.arrows.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.callouts.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.callouts.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.multipart.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.multipart.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryarrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarycalc.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta. code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty) (/usr/share/texlive/texmf-dist/tex/latex/semantic/semantic.sty Semantic Package v2.0(epsilon) [2003/10/28] CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ Loading features: (/usr/share/texlive/texmf-dist/tex/latex/semantic/ligature.sty) math mode ligatures, (/usr/share/texlive/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, (/usr/share/texlive/texmf-dist/tex/latex/semantic/tdiagram.sty) T diagrams, (/usr/share/texlive/texmf-dist/tex/latex/semantic/reserved.sty) reserved words, (/usr/share/texlive/texmf-dist/tex/latex/semantic/shrthand.sty ) short hands, and general definitions. ) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.sty (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.def) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))) (./iris.aux) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) *geometry* driver: auto-detecting *geometry* detected driver: pdftex (/usr/share/texlive/texmf-dist/tex/latex/biblatex/lbx/english.lbx) (./iris.bbl) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (./iris.out) (./iris.out) (/usr/share/texmf/tex/latex/lm/ot1lmr.fd) (/usr/share/texmf/tex/latex/lm/omllmm.fd) (/usr/share/texmf/tex/latex/lm/omslmsy.fd) (/usr/share/texmf/tex/latex/lm/omxlmex.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) (/usr/share/texmf/tex/latex/lm/t1lmtt.fd) [1{/var/lib/texmf/fonts/map/pdftex/up dmap/pdftex.map}] (./iris.toc [2]) [3] [4] (./algebra.tex (/usr/share/texmf/tex/latex/lm/t1lmss.fd) [5] [6] [7] [8]) [9] (./constructions.tex [10] [11] [12] [13] [14]) [15] (./base-logic.tex [16] [17] [18]) [19] (./model.tex [20] [21]) [22] (./extended-logic.tex [23] [24] [25] [26] [27] [28]) [29] (./language.tex (/usr/share/texmf/tex/latex/lm/ts1lmr.fd) Underfull \hbox (badness 10000) in paragraph at lines 11--14 Underfull \hbox (badness 10000) in paragraph at lines 36--37 Underfull \hbox (badness 10000) in paragraph at lines 38--39 Underfull \hbox (badness 10000) in paragraph at lines 40--41 [30]) [31] (./program-logic.tex [32] [33] Overfull \hbox (7.57344pt too wide) detected at line 155 [] [34] [35] [36] [37] Overfull \hbox (3.87889pt too wide) detected at line 311 [] \OMS/lmsy/m/n/10 ` 8\OML/lmm/m/it/10 ^^[[]; []: []\OMS/lmsy/m/n/10 9\OML/lmm /m/it/10 s; S; ^^H; ^^H[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; \OT1/lmr/m /n/10 0\OML/lmm/m/it/10 ; []; \OT1/lmr/m/n/10 0) \OMS/lmsy/m/n/10 ^^C [][] \OML /lmm/m/it/10 e[] [] \OMS/lmsy/m/n/10 ^^C \OT1/lmr/m/n/10 (\OMS/lmsy/m/n/10 8\OM L/lmm/m/it/10 ^^[[]; n[]; n[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; n[]\OT 1/lmr/m/n/10 ()\OML/lmm/m/it/10 ; n[]\OT1/lmr/m/n/10 ) [] \OML/lmm/m/it/10 ^^[ [] \OMS/lmsy/m/n/10 2 \OT1/lmr/m/n/10 ^^F) [38] [39] [40]) [41] (./derived.tex [42] [43] [44]) [45] (./paradoxes.tex [46] LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 89. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 98. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 102. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 106. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. [47] [48]) [49] [50] (./iris.aux) ) (see the transcript file for additional information){/usr/share/texmf/fonts/enc /dvips/lm/lm-ec.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/sh are/texmf/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm -mathit.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texmf/fo nts/enc/dvips/lm/lm-mathex.enc} Output written on iris.pdf (50 pages, 819430 bytes). Transcript written on iris.log. Latexmk: Getting log file 'iris.log' Latexmk: Examining 'iris.fls' Latexmk: Examining 'iris.log' Latexmk: Found input bbl file 'iris.bbl' Latexmk: Log file says output to 'iris.pdf' Latexmk: Found biber source file(s) [bib.bib iris.bcf] Latexmk: applying rule 'pdflatex'... Rule 'pdflatex': File changes, etc: Changed files, or newly in use since previous run(s): iris.run.xml Rule 'pdflatex': The following rules & subrules became out-of-date: pdflatex ------------ Run number 4 of rule 'pdflatex' ------------ ------------ Running 'pdflatex -recorder "iris.tex"' ------------ This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022/Debian) (preloaded format=pdflatex) restricted \write18 enabled. entering extended mode (./iris.tex LaTeX2e <2021-11-15> patch level 1 L3 programming layer <2022-06-02> (/usr/share/texlive/texmf-dist/tex/latex/base/article.cls Document Class: article 2021/10/04 v1.4n Standard LaTeX document class (/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo)) (/usr/share/texmf/tex/latex/lm/lmodern.sty) (/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty (/usr/share/texmf/tex/latex/lm/t1lmr.fd)) (/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty) (/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty (/usr/share/texlive/texmf-dist/tex/generic/babel/txtbabel.def) (/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf)) (/usr/share/texlive/texmf-dist/tex/generic/babel/locale/en/babel-english.tex) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty) (/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def) (/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/geometry/geometry.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/ifvtex.sty (/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty))) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.sty (/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty (/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty) (/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)) (/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty (/usr/share/texlive/texmf-dist/tex/generic/kvsetkeys/kvsetkeys.sty)) (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.sty (/usr/share/texlive/texmf-dist/tex/latex/logreq/logreq.def)) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty) (/usr/share/texlive/texmf-dist/tex/latex/url/url.sty) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-dm.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-compat.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.def) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx (/usr/share/texlive/texmf-dist/tex/latex/biblatex/bbx/standard.bbx)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/biblatex.cfg) (/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def)) (/usr/share/texlive/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty (/usr/share/texlive/texmf-dist/tex/latex/l3packages/xparse/xparse.sty))) (./setup.tex (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty) (/usr/share/texlive/texmf-dist/tex/latex/mathpartir/mathpartir.sty) (./pftools.sty (./locallabel.sty) (/usr/share/texlive/texmf-dist/tex/latex/tabbing/Tabbing.sty) (/usr/share/texlive/texmf-dist/tex/latex/xcolor/xcolor.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg) (/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def))) (./iris.sty (/usr/share/texlive/texmf-dist/tex/latex/faktor/faktor.sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/frontendlayer/tikz.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgf.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfrcs.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-common-lists.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfutil-latex.def ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfrcs.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/pgf.revision.tex))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/basiclayer/pgfcore.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty) (/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg))) (/usr/share/texlive/texmf-dist/tex/latex/pgf/systemlayer/pgfsys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeysfiltered.code.t ex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgf.cfg) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-pdftex.def (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsys-common-pdf.de f))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsyssoftpath.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/systemlayer/pgfsysprotocol.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcore.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathcalc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathutil.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathparser.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.basic.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.trigonomet ric.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.random.cod e.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.comparison .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.base.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.round.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.misc.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfunctions.integerari thmetics.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmathfloat.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfint.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepoints.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathconstruct. code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathusage.code .tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorescopes.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoregraphicstate.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransformation s.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorequick.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreobjects.code.t ex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepathprocessing .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorearrows.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreshade.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreimage.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoreexternal.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorelayers.code.te x) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcoretransparency.c ode.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorepatterns.code. tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/basiclayer/pgfcorerdf.code.tex)) ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleshapes.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmoduleplot.code.tex ) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-0-65 .sty) (/usr/share/texlive/texmf-dist/tex/latex/pgf/compatibility/pgfcomp-version-1-18 .sty)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgffor.sty (/usr/share/texlive/texmf-dist/tex/latex/pgf/utilities/pgfkeys.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgfkeys.code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/pgf/math/pgfmath.sty (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/utilities/pgffor.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/math/pgfmath.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/tikz.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryplothandlers .code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/modules/pgfmodulematrix.code.tex ) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarytopaths.code.tex))) (/usr/share/texlive/texmf-dist/tex/latex/scalerel/scalerel.sty (/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty) (/usr/share/texlive/texmf-dist/tex/latex/dashbox/dashbox.sty) (/usr/share/texlive/texmf-dist/tex/latex/tensor/tensor.sty) (/usr/share/texlive/texmf-dist/tex/latex/xifthen/xifthen.sty (/usr/share/texlive/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty)) (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mathtools.sty (/usr/share/texlive/texmf-dist/tex/latex/mathtools/mhsetup.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?' option. (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty)) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty) (/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.geometric.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.geometric.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.misc.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.misc.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.symbols.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.symbols.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.arrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.arrows.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.callouts.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.callouts.code.tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryshapes.multipart.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/shapes/pgflibraryshape s.multipart.code.tex))) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibraryarrows.code.tex (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.code. tex)) (/usr/share/texlive/texmf-dist/tex/generic/pgf/frontendlayer/tikz/libraries/tik zlibrarycalc.code.tex) (/usr/share/texlive/texmf-dist/tex/generic/pgf/libraries/pgflibraryarrows.meta. code.tex)) (/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty) (/usr/share/texlive/texmf-dist/tex/latex/semantic/semantic.sty Semantic Package v2.0(epsilon) [2003/10/28] CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $ Loading features: (/usr/share/texlive/texmf-dist/tex/latex/semantic/ligature.sty) math mode ligatures, (/usr/share/texlive/texmf-dist/tex/latex/semantic/infernce.sty) inference rules, (/usr/share/texlive/texmf-dist/tex/latex/semantic/tdiagram.sty) T diagrams, (/usr/share/texlive/texmf-dist/tex/latex/semantic/reserved.sty) reserved words, (/usr/share/texlive/texmf-dist/tex/latex/semantic/shrthand.sty ) short hands, and general definitions. ) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.sty (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.def) (/usr/share/texlive/texmf-dist/tex/latex/csquotes/csquotes.cfg)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty (/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty) (/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty) (/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty) (/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty) (/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty (/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty) (/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def) (/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty) (/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def) (/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty (/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty)) (/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty)) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def (/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty) (/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty (/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))) (./iris.aux) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) *geometry* driver: auto-detecting *geometry* detected driver: pdftex (/usr/share/texlive/texmf-dist/tex/latex/biblatex/lbx/english.lbx) (./iris.bbl) (/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] ) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty (/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg)) (./iris.out) (./iris.out) (/usr/share/texmf/tex/latex/lm/ot1lmr.fd) (/usr/share/texmf/tex/latex/lm/omllmm.fd) (/usr/share/texmf/tex/latex/lm/omslmsy.fd) (/usr/share/texmf/tex/latex/lm/omxlmex.fd) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd) (/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) (/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd) (/usr/share/texmf/tex/latex/lm/t1lmtt.fd) [1{/var/lib/texmf/fonts/map/pdftex/up dmap/pdftex.map}] (./iris.toc [2]) [3] [4] (./algebra.tex (/usr/share/texmf/tex/latex/lm/t1lmss.fd) [5] [6] [7] [8]) [9] (./constructions.tex [10] [11] [12] [13] [14]) [15] (./base-logic.tex [16] [17] [18]) [19] (./model.tex [20] [21]) [22] (./extended-logic.tex [23] [24] [25] [26] [27] [28]) [29] (./language.tex (/usr/share/texmf/tex/latex/lm/ts1lmr.fd) Underfull \hbox (badness 10000) in paragraph at lines 11--14 Underfull \hbox (badness 10000) in paragraph at lines 36--37 Underfull \hbox (badness 10000) in paragraph at lines 38--39 Underfull \hbox (badness 10000) in paragraph at lines 40--41 [30]) [31] (./program-logic.tex [32] [33] Overfull \hbox (7.57344pt too wide) detected at line 155 [] [34] [35] [36] [37] Overfull \hbox (3.87889pt too wide) detected at line 311 [] \OMS/lmsy/m/n/10 ` 8\OML/lmm/m/it/10 ^^[[]; []: []\OMS/lmsy/m/n/10 9\OML/lmm /m/it/10 s; S; ^^H; ^^H[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; \OT1/lmr/m /n/10 0\OML/lmm/m/it/10 ; []; \OT1/lmr/m/n/10 0) \OMS/lmsy/m/n/10 ^^C [][] \OML /lmm/m/it/10 e[] [] \OMS/lmsy/m/n/10 ^^C \OT1/lmr/m/n/10 (\OMS/lmsy/m/n/10 8\OM L/lmm/m/it/10 ^^[[]; n[]; n[]: S\OT1/lmr/m/n/10 (\OML/lmm/m/it/10 ^^[[]; n[]\OT 1/lmr/m/n/10 ()\OML/lmm/m/it/10 ; n[]\OT1/lmr/m/n/10 ) [] \OML/lmm/m/it/10 ^^[ [] \OMS/lmsy/m/n/10 2 \OT1/lmr/m/n/10 ^^F) [38] [39] [40]) [41] (./derived.tex [42] [43] [44]) [45] (./paradoxes.tex [46] LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 89. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 98. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 102. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 106. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 110. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 113. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 116. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 119. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 122. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. LaTeX Font Warning: Font shape `T1/lmr/m/scit' undefined (Font) using `T1/lmr/m/scsl' instead on input line 156. [47] [48]) [49] [50] (./iris.aux) ) (see the transcript file for additional information){/usr/share/texmf/fonts/enc /dvips/lm/lm-ec.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-mathsy.enc}{/usr/sh are/texmf/fonts/enc/dvips/lm/lm-ts1.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm -mathit.enc}{/usr/share/texmf/fonts/enc/dvips/lm/lm-rm.enc}{/usr/share/texmf/fo nts/enc/dvips/lm/lm-mathex.enc} Output written on iris.pdf (50 pages, 819430 bytes). Transcript written on iris.log. Latexmk: Getting log file 'iris.log' Latexmk: Examining 'iris.fls' Latexmk: Examining 'iris.log' Latexmk: Found input bbl file 'iris.bbl' Latexmk: Log file says output to 'iris.pdf' Latexmk: Found biber source file(s) [bib.bib iris.bcf] Latexmk: All targets (iris.pdf) are up-to-date make[2]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0/tex' make make[2]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' "coq_makefile" -f _CoqProject -o Makefile.coq make[3]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' COQDEP VFILES COQDEP TESTFILES COQLINT COQC iris/prelude/options.v COQC iris/prelude/prelude.v COQC iris/algebra/ofe.v COQC iris/algebra/monoid.v COQC iris/algebra/cmra.v COQC iris/algebra/updates.v COQC iris/algebra/local_updates.v COQC iris/algebra/proofmode_classes.v COQC iris/algebra/frac.v COQC iris/algebra/dfrac.v COQC iris/algebra/agree.v COQC iris/algebra/big_op.v COQC iris/algebra/view.v COQC iris/algebra/auth.v COQC iris/algebra/excl.v COQC iris/algebra/list.v COQC iris/algebra/gset.v COQC iris/algebra/gmap.v COQC iris/algebra/lib/gmap_view.v COQC iris/bi/notation.v COQC iris/bi/interface.v COQC iris/bi/derived_connectives.v COQC iris/bi/extensions.v COQC iris/bi/derived_laws.v COQC iris/bi/derived_laws_later.v COQC iris/bi/big_op.v COQC iris/bi/internal_eq.v COQC iris/bi/plainly.v COQC iris/bi/updates.v COQC iris/bi/embedding.v COQC iris/bi/bi.v COQC iris/bi/telescopes.v COQC iris/proofmode/base.v COQC iris/proofmode/tokens.v COQC iris/proofmode/sel_patterns.v COQC iris/proofmode/intro_patterns.v COQC iris/proofmode/spec_patterns.v COQC iris/proofmode/environments.v COQC iris/proofmode/ident_name.v COQC iris/proofmode/modalities.v COQC iris/proofmode/classes.v COQC iris/proofmode/modality_instances.v COQC iris/proofmode/coq_tactics.v COQC iris/proofmode/reduction.v COQC iris/proofmode/string_ident.v COQC iris/proofmode/notation.v COQC iris/proofmode/ltac_tactics.v COQC iris/proofmode/class_instances.v COQC iris/proofmode/class_instances_later.v COQC iris/proofmode/class_instances_updates.v COQC iris/proofmode/class_instances_embedding.v COQC iris/proofmode/class_instances_plainly.v COQC iris/proofmode/class_instances_internal_eq.v COQC iris/proofmode/frame_instances.v COQC iris/proofmode/proofmode.v COQC iris/algebra/coPset.v COQC iris/algebra/functions.v COQC iris/algebra/cofe_solver.v COQC iris/base_logic/upred.v COQC iris/base_logic/bi.v COQC iris/base_logic/derived.v COQC iris/base_logic/proofmode.v COQC iris/algebra/csum.v COQC iris/algebra/lib/excl_auth.v COQC iris/base_logic/algebra.v COQC iris/base_logic/base_logic.v COQC iris/base_logic/lib/iprop.v COQC iris/base_logic/lib/own.v COQC iris/base_logic/lib/wsat.v COQC iris/base_logic/lib/fancy_updates.v COQC iris/base_logic/lib/invariants.v COQTEST tests/algebra.v (ref: tests/algebra.ref) COQC iris/proofmode/tactics.v COQC iris/bi/lib/laterable.v COQC iris/bi/lib/fixpoint.v COQC iris/bi/lib/atomic.v COQC iris/bi/weakestpre.v COQC iris/program_logic/language.v COQC iris/program_logic/weakestpre.v COQC iris/program_logic/atomic.v COQC iris/program_logic/ectx_language.v COQC iris/program_logic/ectxi_language.v COQC iris_heap_lang/locations.v COQC iris_heap_lang/lang.v COQC iris_heap_lang/tactics.v COQC iris/bi/lib/fractional.v COQC iris/algebra/reservation_map.v COQC iris/base_logic/lib/ghost_map.v COQC iris/base_logic/lib/gen_heap.v COQC iris/base_logic/lib/proph_map.v COQC iris/base_logic/lib/gen_inv_heap.v COQC iris/program_logic/total_weakestpre.v COQC iris/program_logic/lifting.v COQC iris/program_logic/ectx_lifting.v COQC iris/program_logic/total_lifting.v COQC iris/program_logic/total_ectx_lifting.v COQC iris_heap_lang/notation.v COQC iris_heap_lang/class_instances.v COQC iris_heap_lang/primitive_laws.v COQC iris_heap_lang/derived_laws.v COQC iris_heap_lang/proofmode.v COQC iris_heap_lang/lib/atomic_heap.v COQTEST tests/atomic.v (ref: tests/atomic.ref) COQTEST tests/bi.v (ref: tests/bi.ref) COQC iris/bi/ascii.v COQTEST tests/bi_ascii_parsing.v (ref: tests/bi_ascii_parsing.ref) COQC iris/program_logic/adequacy.v COQC iris_heap_lang/adequacy.v COQTEST tests/heap_lang.v (ref: tests/heap_lang.ref) COQC iris_heap_lang/pretty.v COQC iris_staging/heap_lang/interpreter.v COQTEST tests/heap_lang_interpreter.v (ref: tests/heap_lang_interpreter.ref) COQTEST tests/heap_lang_printing.v (ref: tests/heap_lang_printing.ref) COQTEST tests/heap_lang_printing2.v (ref: tests/heap_lang_printing2.ref) COQTEST tests/heap_lang_proph.v (ref: tests/heap_lang_proph.ref) COQTEST tests/heapprop.v (ref: tests/heapprop.ref) COQC iris_deprecated/base_logic/viewshifts.v COQC iris_deprecated/program_logic/hoare.v COQTEST tests/ipm_paper.v (ref: tests/ipm_paper.ref) COQC iris/bi/monpred.v COQC iris/proofmode/monpred.v COQTEST tests/iris_notation.v (ref: tests/iris_notation.ref) COQTEST tests/list_reverse.v (ref: tests/list_reverse.ref) COQTEST tests/mosel_paper.v (ref: tests/mosel_paper.ref) COQC iris_heap_lang/lib/assert.v COQC iris_heap_lang/lib/spawn.v COQC iris_heap_lang/lib/par.v COQTEST tests/one_shot.v (ref: tests/one_shot.ref) COQTEST tests/one_shot_once.v (ref: tests/one_shot_once.ref) COQTEST tests/proofmode.v (ref: tests/proofmode.ref) COQC iris/base_logic/lib/cancelable_invariants.v COQC iris/base_logic/lib/na_invariants.v COQTEST tests/proofmode_ascii.v (ref: tests/proofmode_ascii.ref) COQTEST tests/proofmode_iris.v (ref: tests/proofmode_iris.ref) COQTEST tests/proofmode_monpred.v (ref: tests/proofmode_monpred.ref) COQC iris/si_logic/siprop.v COQC iris/si_logic/bi.v COQTEST tests/proofmode_siprop.v (ref: tests/proofmode_siprop.ref) COQTEST tests/string_ident.v (ref: tests/string_ident.ref) COQTEST tests/telescopes.v (ref: tests/telescopes.ref) COQTEST tests/tree_sum.v (ref: tests/tree_sum.ref) COQC iris/algebra/cmra_big_op.v COQC iris/algebra/sts.v COQC iris/algebra/numbers.v COQC iris/algebra/vector.v COQC iris/algebra/gmultiset.v COQC iris/algebra/ufrac.v COQC iris/algebra/dyn_reservation_map.v COQC iris/algebra/max_prefix_list.v COQC iris/algebra/lib/frac_auth.v COQC iris/algebra/lib/ufrac_auth.v COQC iris/algebra/lib/dfrac_agree.v COQC iris/algebra/lib/mono_nat.v COQC iris/algebra/lib/mono_list.v COQC iris/algebra/lib/gset_bij.v COQC iris/bi/lib/counterexamples.v COQC iris/bi/lib/core.v COQC iris/bi/lib/relations.v COQC iris/base_logic/bupd_alt.v COQC iris/base_logic/lib/saved_prop.v COQC iris/base_logic/lib/boxes.v COQC iris/base_logic/lib/fancy_updates_from_vs.v COQC iris/base_logic/lib/ghost_var.v COQC iris/base_logic/lib/mono_nat.v COQC iris/base_logic/lib/gset_bij.v COQC iris/program_logic/total_adequacy.v COQC iris/program_logic/ownp.v COQC iris_heap_lang/metatheory.v COQC iris_heap_lang/total_adequacy.v COQC iris_heap_lang/proph_erasure.v COQC iris_heap_lang/lib/lock.v COQC iris_heap_lang/lib/spin_lock.v COQC iris_heap_lang/lib/ticket_lock.v COQC iris_heap_lang/lib/nondet_bool.v COQC iris_heap_lang/lib/lazy_coin.v COQC iris_heap_lang/lib/clairvoyant_coin.v COQC iris_heap_lang/lib/counter.v COQC iris_heap_lang/lib/increment.v COQC iris_heap_lang/lib/diverge.v COQC iris_heap_lang/lib/arith.v COQC iris_heap_lang/lib/array.v COQC iris_staging/algebra/list.v COQC iris_staging/algebra/monotone.v COQC iris_staging/base_logic/algebra.v COQC iris_staging/base_logic/mono_list.v COQC iris_deprecated/base_logic/auth.v COQC iris_deprecated/base_logic/sts.v make[3]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[2]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[1]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make install DESTDIR=debian/tmp make[2]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[3]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' INSTALL iris/prelude/options.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/prelude/prelude.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/algebra/monoid.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/big_op.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra_big_op.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/sts.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/numbers.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/view.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/auth.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmap.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ofe.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cofe_solver.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/agree.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/excl.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/functions.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/frac.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dfrac.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/csum.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/list.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/vector.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/updates.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/local_updates.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gset.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmultiset.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/coPset.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/proofmode_classes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ufrac.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/reservation_map.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dyn_reservation_map.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/max_prefix_list.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/lib/excl_auth.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/frac_auth.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/ufrac_auth.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/dfrac_agree.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gmap_view.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_nat.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_list.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gset_bij.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/si_logic/siprop.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/si_logic/bi.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/bi/notation.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/interface.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_connectives.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/extensions.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws_later.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/plainly.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/internal_eq.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/big_op.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/updates.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/ascii.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/bi.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/monpred.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/embedding.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/weakestpre.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/telescopes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/lib/counterexamples.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fixpoint.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fractional.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/laterable.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/atomic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/core.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/relations.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/base_logic/upred.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bi.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/derived.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/proofmode.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/base_logic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/algebra.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bupd_alt.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/lib/iprop.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/own.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/saved_prop.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/wsat.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/invariants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/boxes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/na_invariants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/cancelable_invariants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_heap.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_inv_heap.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates_from_vs.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/proph_map.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_var.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/mono_nat.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gset_bij.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_map.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/program_logic/adequacy.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/lifting.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/weakestpre.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_weakestpre.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_adequacy.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/language.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_language.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectxi_language.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_lifting.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ownp.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_lifting.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_ectx_lifting.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/atomic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/proofmode/base.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ident_name.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/string_ident.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tokens.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/coq_tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ltac_tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/environments.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/reduction.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/intro_patterns.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/spec_patterns.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/sel_patterns.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/notation.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/classes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_later.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_updates.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_embedding.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_plainly.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_internal_eq.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/frame_instances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/monpred.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modalities.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modality_instances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/proofmode.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris_heap_lang/locations.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lang.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/class_instances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/pretty.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/metatheory.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/primitive_laws.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/derived_laws.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/notation.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proofmode.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/adequacy.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/total_adequacy.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proph_erasure.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lib/spawn.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/par.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/assert.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lock.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/spin_lock.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/ticket_lock.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/nondet_bool.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lazy_coin.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/clairvoyant_coin.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/counter.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/atomic_heap.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/increment.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/diverge.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/arith.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/array.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_staging/algebra/list.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_staging/base_logic/algebra.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/base_logic/mono_list.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/heap_lang/interpreter.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//heap_lang INSTALL iris_staging/algebra/monotone.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_deprecated/base_logic/auth.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/sts.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/viewshifts.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/program_logic/hoare.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//program_logic INSTALL iris/prelude/options.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/prelude/prelude.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/algebra/monoid.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/big_op.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra_big_op.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/sts.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/numbers.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/view.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/auth.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmap.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ofe.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cofe_solver.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/agree.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/excl.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/functions.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/frac.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dfrac.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/csum.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/list.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/vector.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/updates.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/local_updates.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gset.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmultiset.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/coPset.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/proofmode_classes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ufrac.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/reservation_map.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dyn_reservation_map.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/max_prefix_list.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/lib/excl_auth.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/frac_auth.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/ufrac_auth.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/dfrac_agree.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gmap_view.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_nat.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_list.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gset_bij.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/si_logic/siprop.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/si_logic/bi.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/bi/notation.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/interface.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_connectives.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/extensions.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws_later.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/plainly.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/internal_eq.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/big_op.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/updates.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/ascii.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/bi.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/monpred.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/embedding.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/weakestpre.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/telescopes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/lib/counterexamples.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fixpoint.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fractional.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/laterable.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/atomic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/core.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/relations.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/base_logic/upred.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bi.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/derived.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/proofmode.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/base_logic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/algebra.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bupd_alt.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/lib/iprop.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/own.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/saved_prop.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/wsat.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/invariants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/boxes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/na_invariants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/cancelable_invariants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_heap.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_inv_heap.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates_from_vs.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/proph_map.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_var.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/mono_nat.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gset_bij.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_map.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/program_logic/adequacy.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/lifting.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/weakestpre.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_weakestpre.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_adequacy.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/language.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_language.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectxi_language.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_lifting.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ownp.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_lifting.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_ectx_lifting.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/atomic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/proofmode/base.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ident_name.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/string_ident.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tokens.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/coq_tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ltac_tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/environments.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/reduction.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/intro_patterns.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/spec_patterns.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/sel_patterns.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/notation.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/classes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_later.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_updates.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_embedding.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_plainly.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_internal_eq.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/frame_instances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/monpred.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modalities.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modality_instances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/proofmode.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris_heap_lang/locations.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lang.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/class_instances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/pretty.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/metatheory.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/primitive_laws.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/derived_laws.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/notation.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proofmode.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/adequacy.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/total_adequacy.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proph_erasure.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lib/spawn.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/par.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/assert.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lock.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/spin_lock.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/ticket_lock.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/nondet_bool.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lazy_coin.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/clairvoyant_coin.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/counter.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/atomic_heap.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/increment.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/diverge.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/arith.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/array.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_staging/algebra/list.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_staging/base_logic/algebra.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/base_logic/mono_list.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/heap_lang/interpreter.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//heap_lang INSTALL iris_staging/algebra/monotone.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_deprecated/base_logic/auth.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/sts.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/viewshifts.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/program_logic/hoare.v debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//program_logic INSTALL iris/prelude/options.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/prelude/prelude.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/prelude/ INSTALL iris/algebra/monoid.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/big_op.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cmra_big_op.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/sts.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/numbers.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/view.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/auth.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmap.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ofe.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/cofe_solver.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/agree.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/excl.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/functions.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/frac.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dfrac.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/csum.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/list.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/vector.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/updates.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/local_updates.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gset.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/gmultiset.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/coPset.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/proofmode_classes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/ufrac.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/reservation_map.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/dyn_reservation_map.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/max_prefix_list.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra/ INSTALL iris/algebra/lib/excl_auth.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/frac_auth.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/ufrac_auth.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/dfrac_agree.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gmap_view.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_nat.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/mono_list.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/algebra/lib/gset_bij.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/algebra//lib INSTALL iris/si_logic/siprop.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/si_logic/bi.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/si_logic/ INSTALL iris/bi/notation.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/interface.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_connectives.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/extensions.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/derived_laws_later.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/plainly.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/internal_eq.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/big_op.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/updates.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/ascii.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/bi.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/monpred.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/embedding.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/weakestpre.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/telescopes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi/ INSTALL iris/bi/lib/counterexamples.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fixpoint.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/fractional.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/laterable.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/atomic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/core.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/bi/lib/relations.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/bi//lib INSTALL iris/base_logic/upred.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bi.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/derived.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/proofmode.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/base_logic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/algebra.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/bupd_alt.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic/ INSTALL iris/base_logic/lib/iprop.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/own.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/saved_prop.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/wsat.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/invariants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/boxes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/na_invariants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/cancelable_invariants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_heap.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gen_inv_heap.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/fancy_updates_from_vs.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/proph_map.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_var.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/mono_nat.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/gset_bij.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/base_logic/lib/ghost_map.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/base_logic//lib INSTALL iris/program_logic/adequacy.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/lifting.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/weakestpre.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_weakestpre.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_adequacy.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/language.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_language.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectxi_language.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ectx_lifting.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/ownp.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_lifting.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/total_ectx_lifting.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/program_logic/atomic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/program_logic/ INSTALL iris/proofmode/base.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ident_name.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/string_ident.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tokens.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/coq_tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/ltac_tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/environments.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/reduction.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/intro_patterns.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/spec_patterns.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/sel_patterns.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/notation.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/classes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_later.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_updates.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_embedding.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_plainly.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/class_instances_internal_eq.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/frame_instances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/monpred.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modalities.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/modality_instances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris/proofmode/proofmode.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/proofmode/ INSTALL iris_heap_lang/locations.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lang.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/class_instances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/pretty.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/metatheory.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/primitive_laws.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/derived_laws.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/notation.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proofmode.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/adequacy.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/total_adequacy.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/proph_erasure.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang/ INSTALL iris_heap_lang/lib/spawn.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/par.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/assert.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lock.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/spin_lock.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/ticket_lock.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/nondet_bool.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/lazy_coin.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/clairvoyant_coin.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/counter.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/atomic_heap.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/increment.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/diverge.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/arith.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_heap_lang/lib/array.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/heap_lang//lib INSTALL iris_staging/algebra/list.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_staging/base_logic/algebra.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/base_logic/mono_list.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//base_logic INSTALL iris_staging/heap_lang/interpreter.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//heap_lang INSTALL iris_staging/algebra/monotone.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/staging//algebra INSTALL iris_deprecated/base_logic/auth.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/sts.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/base_logic/viewshifts.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//base_logic INSTALL iris_deprecated/program_logic/hoare.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/iris/deprecated//program_logic make[4]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[4]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[3]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[2]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' make[1]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' dh_install -a dh_ocamldoc -a dh_installdocs -a debian/rules override_dh_installchangelogs make[1]: Entering directory '/build/coq-iris-UspITt/coq-iris-3.6.0' dh_installchangelogs CHANGELOG.md make[1]: Leaving directory '/build/coq-iris-UspITt/coq-iris-3.6.0' dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_ocaml -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-iris' in '../libcoq-iris_3.6.0-1+b1_amd64.deb'. dpkg-genbuildinfo --build=any -O../coq-iris_3.6.0-1+b1_amd64.buildinfo dpkg-genchanges --build=any -O../coq-iris_3.6.0-1+b1_amd64.changes dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/coq-iris-UspITt /tmp/coq-iris-3.6.0-1+b1uivvbe47 I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.ejg1LQycSD... I: success in 2858.3067 seconds md5: Value of 'md5' differs for libcoq-iris_3.6.0-1+b1_amd64.deb md5: Size differs for libcoq-iris_3.6.0-1+b1_amd64.deb sha1: Value of 'sha1' differs for libcoq-iris_3.6.0-1+b1_amd64.deb sha1: Size differs for libcoq-iris_3.6.0-1+b1_amd64.deb sha256: Value of 'sha256' differs for libcoq-iris_3.6.0-1+b1_amd64.deb sha256: Size differs for libcoq-iris_3.6.0-1+b1_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-iris_3.6.0-1+b1_amd64.deb: RetryError[]