Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-equations/coq-equations_1.3-8.15-2+b1_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coq-equations-1.3-8.15-2+b1wsx03ypl/coq-equations_1.3-8.15-2+b1_amd64.buildinfo Get source package info: coq-equations=1.3-8.15-2 Source URL: http://snapshot.notset.fr/mr/package/coq-equations/1.3-8.15-2/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 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 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:12.1.0-3 cpp-12=12.1.0-7 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 g++=4:12.1.0-3 g++-12=12.1.0-7 gcc=4:12.1.0-3 gcc-12=12.1.0-7 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 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan8=12.1.0-7 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 libbinutils=2.38.90.20220713-2 libblkid1=2.38-5 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 libcap-ng0=0.8.3-1+b1 libcap2=1:2.44-1 libcc1-0=12.1.0-7 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-hott=8.15-3 libcoq-stdlib=8.15.2+dfsg-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 libdb5.3=5.3.28+dfsg1-0.10 libdebconfclient0=0.263 libdebhelper-perl=13.8 libdpkg-perl=1.21.9 libelf1=0.187-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-12-dev=12.1.0-7 libgcc-s1=12.1.0-7 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-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 libgssapi-krb5-2=1.20-1 libicu71=71.1-3 libisl23=0.25-1 libitm1=12.1.0-7 libk5crypto3=1.20-1 libkeyutils1=1.6.3-1 libkrb5-3=1.20-1 libkrb5support0=1.20-1 liblsan0=12.1.0-7 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmount1=2.38-5 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libocamlgraph-ocaml-dev=2.0.0-3+b1 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libperl5.34=5.34.0-5 libpipeline1=1.5.6-1 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 libseccomp2=2.5.4-1+b1 libselinux1=3.4-1+b1 libsigsegv2=2.14-1 libsmartcols1=2.38-5 libsqlite3-0=3.39.2-1 libssl3=3.0.5-1 libstdc++-12-dev=12.1.0-7 libstdc++6=12.1.0-7 libsub-override-perl=0.09-3 libsystemd0=251.3-1 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 libtsan2=12.1.0-7 libubsan1=12.1.0-7 libuchardet0=0.0.7-1 libudev1=251.3-1 libunistring2=1.0-1 libuuid1=2.38-5 libxml2=2.9.14+dfsg-1+b1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.18.14-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 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 patch=2.7.6-7 perl=5.34.0-5 perl-base=5.34.0-5 perl-modules-5.34=5.34.0-5 po-debconf=1.0.21+nmu1 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 tar=1.34+dfsg-1 util-linux=2.38-5 util-linux-extra=2.38-5 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/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ 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-equations=1.3-8.15-2 && mkdir -p /build/coq-equations-UEjyco && dpkg-source --no-check -x /*.dsc /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && cd /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && { printf '%s' 'coq-equations (1.3-8.15-2+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 Build Daemon (x86-grnet-01) Wed, 27 Jul 2022 00:40:41 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-equations-UEjyco" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882441" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-equations-UEjyco /tmp/coq-equations-1.3-8.15-2+b1wsx03ypl bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220728T094517Z 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.c1F6mGCs5L 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.c1F6mGCs5L 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/20220728T094517Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z 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 (990 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 ... 4629 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/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.c1F6mGCs5L Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm InRelease [157 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources [12.1 MB] Get:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages [11.5 MB] Fetched 23.8 MB in 19s (1223 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.c1F6mGCs5L I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-equations=1.3-8.15-2 && mkdir -p /build/coq-equations-UEjyco && dpkg-source --no-check -x /*.dsc /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && cd /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && { printf '%s' 'coq-equations (1.3-8.15-2+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 Build Daemon (x86-grnet-01) Wed, 27 Jul 2022 00:40:41 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-equations-UEjyco"' exec /tmp/mmdebstrap.c1F6mGCs5L Reading package lists... NOTICE: 'coq-equations' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/coq-equations.git Please use: git clone https://salsa.debian.org/ocaml-team/coq-equations.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 1100 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-equations 1.3-8.15-2 (dsc) [2161 B] Get:2 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-equations 1.3-8.15-2 (tar) [1096 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-equations 1.3-8.15-2 (diff) [2144 B] Fetched 1100 kB in 1s (1020 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coq-equations_1.3-8.15-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coq-equations in /build/coq-equations-UEjyco/coq-equations-1.3-8.15 dpkg-source: info: unpacking coq-equations_1.3-8.15.orig.tar.gz dpkg-source: info: unpacking coq-equations_1.3-8.15-2.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-equations-UEjyco/coq-equations-1.3-8.15 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882441" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.c1F6mGCs5L dpkg-buildpackage: info: source package coq-equations dpkg-buildpackage: info: source version 1.3-8.15-2+b1 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by amd64 Build Daemon (x86-grnet-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-equations-UEjyco/coq-equations-1.3-8.15' # doesn't work make[1]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' 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 debian/rules override_dh_auto_configure make[1]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' ./configure.sh --enable-hott make[1]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' dh_auto_build -a make -j10 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make -f Makefile.coq make[2]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' COQDEP VFILES COQPP src/g_equations.mlg CAMLDEP src/extra_tactics.mli CAMLDEP src/noconf.mli *** Warning: in file theories/Init.v, declared ML module ltac_plugin has not been found! *** Warning: in file theories/Init.v, declared ML module cc_plugin has not been found! *** Warning: in file theories/Init.v, declared ML module extraction_plugin has not been found! CAMLDEP src/noconf_hom.mli CAMLDEP src/equations.mli CAMLDEP src/principles.mli CAMLDEP src/principles_proofs.mli CAMLDEP src/covering.mli CAMLDEP src/splitting.mli CAMLDEP src/simplify.mli CAMLDEP src/context_map.mli CAMLDEP src/syntax.mli CAMLDEP src/depelim.mli CAMLDEP src/eqdec.mli CAMLDEP src/subterm.mli CAMLDEP src/sigma_types.mli CAMLDEP src/ederive.mli CAMLDEP src/equations_common.mli OCAMLLIBDEP src/equations_plugin.mllib CAMLDEP src/equations_plugin_mod.ml CAMLDEP src/extra_tactics.ml CAMLDEP src/noconf.ml CAMLDEP src/noconf_hom.ml CAMLDEP src/equations.ml CAMLDEP src/principles.ml CAMLDEP src/principles_proofs.ml CAMLDEP src/covering.ml CAMLDEP src/splitting.ml CAMLDEP src/simplify.ml CAMLDEP src/context_map.ml CAMLDEP src/syntax.ml CAMLDEP src/depelim.ml CAMLDEP src/eqdec.ml CAMLDEP src/subterm.ml CAMLDEP src/sigma_types.ml CAMLDEP src/ederive.ml CAMLDEP src/equations_common.ml CAMLDEP src/g_equations.ml CAMLC -c src/equations_common.mli CAMLC -c src/ederive.mli CAMLC -c src/subterm.mli CAMLC -c src/noconf_hom.mli CAMLC -c src/noconf.mli CAMLC -c src/extra_tactics.mli CAMLOPT -c src/equations_plugin_mod.ml CAMLOPT -c src/ederive.ml CAMLOPT -c src/equations_common.ml CAMLC -c src/syntax.mli CAMLC -c src/eqdec.mli CAMLC -c src/context_map.mli CAMLC -c src/depelim.mli CAMLC -c src/sigma_types.mli CAMLC -c src/simplify.mli CAMLC -c src/splitting.mli CAMLC -c src/covering.mli CAMLC -c src/principles_proofs.mli CAMLC -c src/equations.mli CAMLC -c src/principles.mli CAMLOPT -c src/syntax.ml CAMLOPT -c src/eqdec.ml CAMLOPT -c src/extra_tactics.ml CAMLOPT -c src/context_map.ml CAMLOPT -c src/sigma_types.ml CAMLOPT -c src/simplify.ml CAMLOPT -c src/subterm.ml CAMLOPT -c src/splitting.ml CAMLOPT -c src/covering.ml CAMLOPT -c src/depelim.ml CAMLOPT -c src/noconf_hom.ml CAMLOPT -c src/noconf.ml CAMLOPT -c src/principles_proofs.ml CAMLOPT -c src/principles.ml CAMLOPT -c src/equations.ml CAMLOPT -c src/g_equations.ml CAMLOPT -a -o src/equations_plugin.cmxa CAMLOPT -shared -o src/equations_plugin.cmxs COQC theories/Init.v COQC theories/Signature.v COQC theories/Prop/Logic.v COQC theories/Type/Logic.v COQC theories/Type/FunctionalExtensionality.v COQC theories/Type/Relation.v COQC theories/CoreTactics.v COQC theories/Prop/Classes.v COQC theories/Type/Relation_Properties.v COQC theories/Prop/EqDec.v COQC theories/Type/WellFounded.v COQC theories/Type/Classes.v COQC theories/Prop/DepElim.v COQC theories/Type/EqDec.v COQC theories/Prop/Constants.v COQC theories/Prop/FunctionalInduction.v COQC theories/Prop/TransparentEquations.v COQC theories/Prop/OpaqueEquations.v COQC theories/Prop/Subterm.v COQC theories/Type/DepElim.v COQC theories/Prop/Tactics.v COQC theories/Type/Constants.v COQC theories/Type/FunctionalInduction.v COQC theories/Type/Subterm.v COQC theories/Prop/NoConfusion.v COQC theories/Type/Tactics.v COQC theories/Prop/EqDecInstances.v COQC theories/Type/EqDecInstances.v COQC theories/Type/NoConfusion.v COQC theories/Type/Loader.v COQC theories/Type/Telescopes.v COQC theories/Type/WellFoundedInstances.v COQC theories/Prop/Loader.v COQC theories/Prop/Telescopes.v COQC theories/Prop/Equations.v COQC theories/Type/All.v COQC theories/Prop/NoConfusion_UIP.v COQC theories/Prop/NoCycle.v make[2]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' test -f Makefile.hott && make -f Makefile.hott || true make[2]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' COQDEP VFILES *** Warning: in file theories/Init.v, declared ML module ltac_plugin has not been found! *** Warning: in file theories/Init.v, declared ML module cc_plugin has not been found! *** Warning: in file theories/Init.v, declared ML module extraction_plugin has not been found! COQC theories/HoTT/Logic.v COQC theories/HoTT/Relation.v COQC theories/HoTT/Relation_Properties.v COQC theories/HoTT/WellFounded.v COQC theories/HoTT/Classes.v COQC theories/HoTT/EqDec.v COQC theories/HoTT/DepElim.v COQC theories/HoTT/FunctionalInduction.v COQC theories/HoTT/Constants.v COQC theories/HoTT/Subterm.v COQC theories/HoTT/Tactics.v COQC theories/HoTT/NoConfusion.v COQC theories/HoTT/EqDecInstances.v COQC theories/HoTT/Loader.v COQC theories/HoTT/Telescopes.v COQC theories/HoTT/WellFoundedInstances.v COQC theories/HoTT/All.v COQC test-suite/BasicsHoTT.v COQC test-suite/issues/issue389.v File "./test-suite/BasicsHoTT.v", line 166, characters 0-39: Warning: The default value for Typeclasses Opaque and Typeclasses Transparent locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding typeclass transparency hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Typeclasses Transparent foo." [deprecated-typeclasses-transparency-without-locality,deprecated] make[2]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[1]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' 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-equations-UEjyco/coq-equations-1.3-8.15' make install DESTDIR=debian/tmp make[2]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make -f Makefile.coq install make[3]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' INSTALL theories/Init.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Prop/Logic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Classes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDec.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDecInstances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Subterm.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/DepElim.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Constants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion_UIP.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/FunctionalInduction.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Loader.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Telescopes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/TransparentEquations.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/OpaqueEquations.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoCycle.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Equations.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Type/Logic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalExtensionality.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation_Properties.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFounded.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Classes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDec.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/DepElim.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Subterm.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Constants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDecInstances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/NoConfusion.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalInduction.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Loader.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Telescopes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFoundedInstances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/All.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Init.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Prop/Logic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Classes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDec.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDecInstances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Subterm.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/DepElim.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Constants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion_UIP.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/FunctionalInduction.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Loader.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Telescopes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/TransparentEquations.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/OpaqueEquations.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoCycle.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Equations.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Type/Logic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalExtensionality.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation_Properties.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFounded.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Classes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDec.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/DepElim.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Subterm.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Constants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDecInstances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/NoConfusion.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalInduction.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Loader.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Telescopes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFoundedInstances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/All.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Init.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Prop/Logic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Classes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDec.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/EqDecInstances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Subterm.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/DepElim.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Constants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoConfusion_UIP.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/FunctionalInduction.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Loader.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Telescopes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/TransparentEquations.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/OpaqueEquations.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/NoCycle.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Prop/Equations.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Prop INSTALL theories/Type/Logic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalExtensionality.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Relation_Properties.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFounded.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Classes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDec.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/DepElim.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Subterm.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Constants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/EqDecInstances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/NoConfusion.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/FunctionalInduction.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Loader.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/Telescopes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/WellFoundedInstances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL theories/Type/All.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//Type INSTALL src/g_equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin_mod.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin.cmxs debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin.cmxa debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/g_equations.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin_mod.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ make[4]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[4]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[3]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' test -f Makefile.hott && make -f Makefile.hott install || true make[3]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' INSTALL theories/Init.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/HoTT/Logic.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation_Properties.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFounded.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Classes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDec.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/DepElim.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/FunctionalInduction.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Constants.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Subterm.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/NoConfusion.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDecInstances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Loader.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Telescopes.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFoundedInstances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/All.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT SKIP test-suite/BasicsHoTT.vo since it has no logical path SKIP test-suite/issues/issue389.vo since it has no logical path INSTALL theories/Init.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/HoTT/Logic.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation_Properties.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFounded.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Classes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDec.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/DepElim.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/FunctionalInduction.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Constants.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Subterm.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/NoConfusion.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDecInstances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Loader.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Telescopes.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFoundedInstances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/All.v debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT SKIP test-suite/BasicsHoTT.v since it has no logical path SKIP test-suite/issues/issue389.v since it has no logical path INSTALL theories/Init.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/Signature.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/CoreTactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL theories/HoTT/Logic.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Relation_Properties.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFounded.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Classes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDec.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/DepElim.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/FunctionalInduction.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Constants.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Subterm.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/NoConfusion.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/EqDecInstances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Loader.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/Telescopes.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/WellFoundedInstances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT INSTALL theories/HoTT/All.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations//HoTT SKIP test-suite/BasicsHoTT.glob since it has no logical path SKIP test-suite/issues/issue389.glob since it has no logical path INSTALL src/g_equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin_mod.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmi debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin.cmxs debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin.cmxa debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/g_equations.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_common.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/ederive.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/sigma_types.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/subterm.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/eqdec.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/depelim.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/syntax.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/context_map.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/simplify.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/splitting.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/covering.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles_proofs.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/principles.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/noconf_hom.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/extra_tactics.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ INSTALL src/equations_plugin_mod.cmx debian/tmp//usr/lib/ocaml/coq//user-contrib/Equations/ make[4]: Entering directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[4]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[3]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[2]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' make[1]: Leaving directory '/build/coq-equations-UEjyco/coq-equations-1.3-8.15' dh_install -a dh_ocamldoc -a dh_installdocs -a dh_installchangelogs -a dh_installexamples -a 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 dpkg-gencontrol: warning: package libcoq-equations: substitution variable ${ocaml:Depends} unused, but is defined dpkg-gencontrol: warning: package libcoq-equations: substitution variable ${ocaml:Depends} unused, but is defined dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-equations-dbgsym' in '../libcoq-equations-dbgsym_1.3-8.15-2+b1_amd64.deb'. dpkg-deb: building package 'libcoq-equations' in '../libcoq-equations_1.3-8.15-2+b1_amd64.deb'. dpkg-genbuildinfo --build=any -O../coq-equations_1.3-8.15-2+b1_amd64.buildinfo dpkg-genchanges --build=any -O../coq-equations_1.3-8.15-2+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-equations-UEjyco /tmp/coq-equations-1.3-8.15-2+b1wsx03ypl I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.c1F6mGCs5L... I: success in 753.5580 seconds md5: libcoq-equations-dbgsym_1.3-8.15-2+b1_amd64.deb: OK md5: Value of 'md5' differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb md5: Size differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb sha1: libcoq-equations-dbgsym_1.3-8.15-2+b1_amd64.deb: OK sha1: Value of 'sha1' differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb sha1: Size differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb sha256: libcoq-equations-dbgsym_1.3-8.15-2+b1_amd64.deb: OK sha256: Value of 'sha256' differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb sha256: Size differs for libcoq-equations_1.3-8.15-2+b1_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-equations_1.3-8.15-2+b1_amd64.deb: RetryError[]