Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/a/aac-tactics/aac-tactics_8.11.0-1+b1_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/aac-tactics-8.11.0-1+b1ptk1_atc/aac-tactics_8.11.0-1+b1_amd64.buildinfo Get source package info: aac-tactics=8.11.0-1 Source URL: http://snapshot.notset.fr/mr/package/aac-tactics/8.11.0-1/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=adduser=3.118 adwaita-icon-theme=3.36.0-1 autoconf=2.69-11.1 automake=1:1.16.1-4 autopoint=0.19.8.1-10 autotools-dev=20180224.1 base-files=11 base-passwd=3.5.47 bash=5.0-6 binutils=2.34-6 binutils-common=2.34-6 binutils-x86-64-linux-gnu=2.34-6 bsdmainutils=11.1.2+b1 bsdutils=1:2.34-0.1 build-essential=12.8 bzip2=1.0.8-2 coq=8.11.0-1+b1 coq-theories=8.11.0-1+b1 coreutils=8.30-3+b1 cpp=4:9.2.1-3.1 cpp-9=9.3.0-10 dash=0.5.10.2-7 dbus=1.12.16-2 dbus-user-session=1.12.16-2 dconf-gsettings-backend=0.36.0-1 dconf-service=0.36.0-1 debconf=1.5.73 debhelper=12.10 debianutils=4.9.1 dh-autoreconf=19 dh-ocaml=1.1.1 dh-strip-nondeterminism=1.7.0-1 dictionaries-common=1.28.1 diffutils=1:3.7-3 dmsetup=2:1.02.167-1+b1 dpkg=1.19.7 dpkg-dev=1.19.7 dwz=0.13-5 emacsen-common=3.0.4 fdisk=2.34-0.1 file=1:5.38-4 findutils=4.7.0-1 fontconfig=2.13.1-3 fontconfig-config=2.13.1-3 fonts-dejavu-core=2.37-1 g++=4:9.2.1-3.1 g++-9=9.3.0-10 gcc=4:9.2.1-3.1 gcc-10-base=10-20200402-1 gcc-9=9.3.0-10 gcc-9-base=9.3.0-10 gettext=0.19.8.1-10 gettext-base=0.19.8.1-10 gir1.2-atk-1.0=2.36.0-2 gir1.2-atspi-2.0=2.36.0-2 gir1.2-freedesktop=1.64.0-2 gir1.2-gdkpixbuf-2.0=2.40.0+dfsg-4 gir1.2-glib-2.0=1.64.0-2 gir1.2-gtk-2.0=2.24.32-4 gir1.2-gtk-3.0=3.24.17-3 gir1.2-gtksource-3.0=3.24.11-2 gir1.2-harfbuzz-0.0=2.6.4-1 gir1.2-pango-1.0=1.44.7-3 glib-networking=2.64.1-1 glib-networking-common=2.64.1-1 glib-networking-services=2.64.1-1 grep=3.4-1 groff-base=1.22.4-4 gsettings-desktop-schemas=3.36.0-1 gtk-update-icon-cache=3.24.17-3 gzip=1.10-2 hicolor-icon-theme=0.17-2 hostname=3.23 hunspell-en-us=1:2019.10.06-1 icu-devtools=63.2-3 init-system-helpers=1.57 intltool-debian=0.35.0+20060710.5 libacl1=2.2.53-6 libapparmor1=2.13.4-1 libarchive-zip-perl=1.68-1 libargon2-1=0~20171227-0.2 libasan5=9.3.0-10 libaspell15=0.60.8-1 libatk-bridge2.0-0=2.34.1-3 libatk-bridge2.0-dev=2.34.1-3 libatk1.0-0=2.36.0-2 libatk1.0-data=2.36.0-2 libatk1.0-dev=2.36.0-2 libatomic1=10-20200402-1 libatspi2.0-0=2.36.0-2 libatspi2.0-dev=2.36.0-2 libattr1=1:2.4.48-5 libaudit-common=1:2.8.5-3 libaudit1=1:2.8.5-3 libavahi-client3=0.7-5 libavahi-common-data=0.7-5 libavahi-common3=0.7-5 libbinutils=2.34-6 libblkid-dev=2.34-0.1 libblkid1=2.34-0.1 libbrotli1=1.0.7-6 libbsd0=0.10.0-1 libbz2-1.0=1.0.8-2 libc-bin=2.30-4 libc-dev-bin=2.30-4 libc6=2.30-4 libc6-dev=2.30-4 libcairo-gobject2=1.16.0-4 libcairo-script-interpreter2=1.16.0-4 libcairo2=1.16.0-4 libcairo2-dev=1.16.0-4 libcairo2-ocaml=0.6.1+dfsg-3 libcairo2-ocaml-dev=0.6.1+dfsg-3 libcap-ng0=0.7.9-2.1+b2 libcap2=1:2.33-1 libcc1-0=10-20200402-1 libcolord2=1.4.4-2 libcom-err2=1.45.6-1 libcoq-ocaml=8.11.0-1+b1 libcoq-ocaml-dev=8.11.0-1+b1 libcroco3=0.6.13-1 libcrypt-dev=1:4.4.16-1 libcrypt1=1:4.4.16-1 libcryptsetup12=2:2.3.1-1 libctf-nobfd0=2.34-6 libctf0=2.34-6 libcups2=2.3.1-11 libdatrie-dev=0.2.12-3 libdatrie1=0.2.12-3 libdb5.3=5.3.28+dfsg1-0.6 libdbus-1-3=1.12.16-2 libdbus-1-dev=1.12.16-2 libdconf1=0.36.0-1 libdebconfclient0=0.251 libdebhelper-perl=12.10 libdevmapper1.02.1=2:1.02.167-1+b1 libdpkg-perl=1.19.7 libdrm-amdgpu1=2.4.101-1 libdrm-common=2.4.101-1 libdrm-intel1=2.4.101-1 libdrm-nouveau2=2.4.101-1 libdrm-radeon1=2.4.101-1 libdrm2=2.4.101-1 libedit2=3.1-20191231-1 libegl-dev=1.3.1-1 libegl-mesa0=20.0.4-1 libegl1=1.3.1-1 libegl1-mesa-dev=20.0.4-1 libelf1=0.176-1.1 libenchant-2-2=2.2.8-1 libenchant-2-dev=2.2.8-1 libepoxy-dev=1.5.4-1 libepoxy0=1.5.4-1 libexpat1=2.2.9-1 libexpat1-dev=2.2.9-1 libfdisk1=2.34-0.1 libffi-dev=3.3-4 libffi7=3.3-4 libfile-stripnondeterminism-perl=1.7.0-1 libfindlib-ocaml=1.8.1-1+b1 libfontconfig-dev=2.13.1-3 libfontconfig1=2.13.1-3 libfontconfig1-dev=2.13.1-3 libfreetype-dev=2.10.1-2 libfreetype6=2.10.1-2 libfreetype6-dev=2.10.1-2 libfribidi-dev=1.0.8-2 libfribidi0=1.0.8-2 libgbm1=20.0.4-1 libgcc-9-dev=9.3.0-10 libgcc-s1=10-20200402-1 libgcrypt20=1.8.5-5 libgdbm-compat4=1.18.1-5 libgdbm6=1.18.1-5 libgdk-pixbuf2.0-0=2.40.0+dfsg-4 libgdk-pixbuf2.0-bin=2.40.0+dfsg-4 libgdk-pixbuf2.0-common=2.40.0+dfsg-4 libgdk-pixbuf2.0-dev=2.40.0+dfsg-4 libgirepository-1.0-1=1.64.0-2 libgl-dev=1.3.1-1 libgl1=1.3.1-1 libgl1-mesa-dev=20.0.4-1 libgl1-mesa-dri=20.0.4-1 libglapi-mesa=20.0.4-1 libgles-dev=1.3.1-1 libgles1=1.3.1-1 libgles2=1.3.1-1 libglib2.0-0=2.64.1-1 libglib2.0-bin=2.64.1-1 libglib2.0-data=2.64.1-1 libglib2.0-dev=2.64.1-1 libglib2.0-dev-bin=2.64.1-1 libglvnd-dev=1.3.1-1 libglvnd0=1.3.1-1 libglx-dev=1.3.1-1 libglx-mesa0=20.0.4-1 libglx0=1.3.1-1 libgmp10=2:6.2.0+dfsg-4 libgnutls30=3.6.13-2 libgomp1=10-20200402-1 libgpg-error0=1.37-1 libgraphite2-3=1.3.14-1 libgraphite2-dev=1.3.14-1 libgssapi-krb5-2=1.17-7 libgtk-3-0=3.24.17-3 libgtk-3-common=3.24.17-3 libgtk-3-dev=3.24.17-3 libgtk2.0-0=2.24.32-4 libgtk2.0-common=2.24.32-4 libgtk2.0-dev=2.24.32-4 libgtksourceview-3.0-1=3.24.11-2 libgtksourceview-3.0-common=3.24.11-2 libgtksourceview-3.0-dev=3.24.11-2 libgtkspell-dev=2.0.16-1.3 libgtkspell0=2.0.16-1.3 libharfbuzz-dev=2.6.4-1 libharfbuzz-gobject0=2.6.4-1 libharfbuzz-icu0=2.6.4-1 libharfbuzz0b=2.6.4-1 libhogweed5=3.5.1+really3.5.1-2 libhunspell-1.7-0=1.7.0-2+b1 libice-dev=2:1.0.9-2 libice6=2:1.0.9-2 libicu-dev=63.2-3 libicu63=63.2-3 libidn2-0=2.3.0-1 libip4tc2=1.8.4-3 libisl22=0.22.1-1 libitm1=10-20200402-1 libjbig0=2.1-3.1+b2 libjpeg62-turbo=1:1.5.2-2+b1 libjson-c4=0.13.1+dfsg-7 libjson-glib-1.0-0=1.4.4-2 libjson-glib-1.0-common=1.4.4-2 libk5crypto3=1.17-7 libkeyutils1=1.6.1-2 libkmod2=27-2 libkrb5-3=1.17-7 libkrb5support0=1.17-7 liblablgtk3-ocaml=3.1.0-2 liblablgtk3-ocaml-dev=3.1.0-2 liblablgtksourceview3-ocaml=3.1.0-2 liblablgtksourceview3-ocaml-dev=3.1.0-2 liblcms2-2=2.9-4+b1 libllvm9=1:9.0.1-11 liblsan0=10-20200402-1 liblz4-1=1.9.2-2 liblzma5=5.2.4-1+b1 liblzo2-2=2.10-2 libmagic-mgc=1:5.38-4 libmagic1=1:5.38-4 libmount-dev=2.34-0.1 libmount1=2.34-0.1 libmpc3=1.1.0-1 libmpdec2=2.4.2-3 libmpfr6=4.0.2-1 libncurses-dev=6.2-1 libncurses5-dev=6.2-1 libncurses6=6.2-1 libncursesw6=6.2-1 libnettle7=3.5.1+really3.5.1-2 libnum-ocaml=1.3-1 libnum-ocaml-dev=1.3-1 libopengl-dev=1.3.1-1 libopengl0=1.3.1-1 libp11-kit0=0.23.20-1 libpam-modules=1.3.1-5 libpam-modules-bin=1.3.1-5 libpam-runtime=1.3.1-5 libpam-systemd=245.4-2 libpam0g=1.3.1-5 libpango-1.0-0=1.44.7-3 libpango1.0-dev=1.44.7-3 libpangocairo-1.0-0=1.44.7-3 libpangoft2-1.0-0=1.44.7-3 libpangoxft-1.0-0=1.44.7-3 libpciaccess0=0.14-1 libpcre16-3=2:8.39-12+b1 libpcre2-16-0=10.34-7 libpcre2-32-0=10.34-7 libpcre2-8-0=10.34-7 libpcre2-dev=10.34-7 libpcre2-posix2=10.34-7 libpcre3=2:8.39-12+b1 libpcre3-dev=2:8.39-12+b1 libpcre32-3=2:8.39-12+b1 libpcrecpp0v5=2:8.39-12+b1 libperl5.30=5.30.0-9 libpipeline1=1.5.2-2 libpixman-1-0=0.36.0-1 libpixman-1-dev=0.36.0-1 libpng-dev=1.6.37-2 libpng16-16=1.6.37-2 libproxy1v5=0.4.15-9 libpsl5=0.21.0-1 libpthread-stubs0-dev=0.4-1 libpython3-stdlib=3.8.2-3 libpython3.8-minimal=3.8.2-1+b1 libpython3.8-stdlib=3.8.2-1+b1 libquadmath0=10-20200402-1 libreadline8=8.0-4 librest-0.7-0=0.8.1-1+b1 librsvg2-2=2.48.2-1 librsvg2-common=2.48.2-1 libseccomp2=2.4.3-1 libselinux1=3.0-1+b2 libselinux1-dev=3.0-1+b2 libsemanage-common=3.0-1 libsemanage1=3.0-1+b2 libsensors-config=1:3.6.0-2 libsensors5=1:3.6.0-2 libsepol1=3.0-1 libsepol1-dev=3.0-1 libsigsegv2=2.12-2 libsm-dev=2:1.2.3-1 libsm6=2:1.2.3-1 libsmartcols1=2.34-0.1 libsoup-gnome2.4-1=2.70.0-1 libsoup2.4-1=2.70.0-1 libsqlite3-0=3.31.1-4 libssl1.1=1.1.1f-1 libstdc++-9-dev=9.3.0-10 libstdc++6=10-20200402-1 libsub-override-perl=0.09-2 libsystemd0=245.4-2 libtasn1-6=4.16.0-2 libtext-iconv-perl=1.7-7 libthai-data=0.1.28-3 libthai-dev=0.1.28-3 libthai0=0.1.28-3 libtiff5=4.1.0+git191117-2 libtinfo6=6.2-1 libtool=2.4.6-14 libtsan0=10-20200402-1 libubsan1=10-20200402-1 libuchardet0=0.0.6-3 libudev1=245.4-2 libunistring2=0.9.10-2 libuuid1=2.34-0.1 libvulkan1=1.2.135.0-2 libwayland-bin=1.18.0-1 libwayland-client0=1.18.0-1 libwayland-cursor0=1.18.0-1 libwayland-dev=1.18.0-1 libwayland-egl1=1.18.0-1 libwayland-server0=1.18.0-1 libwebp6=0.6.1-2+b1 libx11-6=2:1.6.9-2 libx11-data=2:1.6.9-2 libx11-dev=2:1.6.9-2 libx11-xcb1=2:1.6.9-2 libxau-dev=1:1.0.8-1+b2 libxau6=1:1.0.8-1+b2 libxcb-dri2-0=1.14-2 libxcb-dri3-0=1.14-2 libxcb-glx0=1.14-2 libxcb-present0=1.14-2 libxcb-render0=1.14-2 libxcb-render0-dev=1.14-2 libxcb-shm0=1.14-2 libxcb-shm0-dev=1.14-2 libxcb-sync1=1.14-2 libxcb-xfixes0=1.14-2 libxcb1=1.14-2 libxcb1-dev=1.14-2 libxcomposite-dev=1:0.4.4-2 libxcomposite1=1:0.4.4-2 libxcursor-dev=1:1.2.0-2 libxcursor1=1:1.2.0-2 libxdamage-dev=1:1.1.5-1 libxdamage1=1:1.1.5-1 libxdmcp-dev=1:1.1.2-3 libxdmcp6=1:1.1.2-3 libxext-dev=2:1.3.3-1+b2 libxext6=2:1.3.3-1+b2 libxfixes-dev=1:5.0.3-1 libxfixes3=1:5.0.3-1 libxft-dev=2.3.2-2 libxft2=2.3.2-2 libxi-dev=2:1.7.9-1 libxi6=2:1.7.9-1 libxinerama-dev=2:1.1.4-2 libxinerama1=2:1.1.4-2 libxkbcommon-dev=0.10.0-1 libxkbcommon0=0.10.0-1 libxml2=2.9.10+dfsg-4 libxml2-dev=2.9.10+dfsg-4 libxml2-utils=2.9.10+dfsg-4 libxrandr-dev=2:1.5.1-1 libxrandr2=2:1.5.1-1 libxrender-dev=1:0.9.10-1 libxrender1=1:0.9.10-1 libxshmfence1=1.3-1 libxtst-dev=2:1.2.3-1 libxtst6=2:1.2.3-1 libxxf86vm1=1:1.1.4-1+b2 libz3-4=4.8.7-4 libzstd1=1.4.4+dfsg-3 linux-libc-dev=5.5.13-2 login=1:4.8.1-1 lsb-base=11.1.0 m4=1.4.18-4 make=4.2.1-1.2 man-db=2.9.1-1 mawk=1.3.4.20200120-2 mime-support=3.64 mount=2.34-0.1 ncurses-base=6.2-1 ncurses-bin=6.2-1 ocaml-base-nox=4.08.1-8 ocaml-compiler-libs=4.08.1-8 ocaml-findlib=1.8.1-1+b1 ocaml-interp=4.08.1-8 ocaml-nox=4.08.1-8 pango1.0-tools=1.44.7-3 passwd=1:4.8.1-1 patch=2.7.6-6 perl=5.30.0-9 perl-base=5.30.0-9 perl-modules-5.30=5.30.0-9 pkg-config=0.29-6 po-debconf=1.0.21 python3=3.8.2-3 python3-distutils=3.8.2-2 python3-lib2to3=3.8.2-2 python3-minimal=3.8.2-3 python3.8=3.8.2-1+b1 python3.8-minimal=3.8.2-1+b1 readline-common=8.0-4 sed=4.7-1 sensible-utils=0.0.12+nmu1 shared-mime-info=1.15-1 systemd=245.4-2 systemd-sysv=245.4-2 systemd-timesyncd=245.4-2 sysvinit-utils=2.96-3 tar=1.30+dfsg-7 ucf=3.0038+nmu1 util-linux=2.34-0.1 uuid-dev=2.34-0.1 wayland-protocols=1.20-1 x11-common=1:7.7+20 x11proto-composite-dev=1:2019.2-1 x11proto-core-dev=2019.2-1 x11proto-damage-dev=1:2019.2-1 x11proto-dev=2019.2-1 x11proto-fixes-dev=1:2019.2-1 x11proto-input-dev=2019.2-1 x11proto-randr-dev=2019.2-1 x11proto-record-dev=2019.2-1 x11proto-xext-dev=2019.2-1 x11proto-xinerama-dev=2019.2-1 xkb-data=2.29-2 xorg-sgml-doctools=1:1.11-1 xtrans-dev=1.4.0-1 xz-utils=5.2.4-1+b1 zlib1g=1:1.2.11.dfsg-2 zlib1g-dev=1:1.2.11.dfsg-2 --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/20200323T101008Z/ bullseye main deb-src http://snapshot.notset.fr/archive/debian/20200323T101008Z/ bullseye main deb http://snapshot.notset.fr/archive/debian/20200410T084926Z/ 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 aac-tactics=8.11.0-1 && mkdir -p /build/aac-tactics-9ZXkKW && dpkg-source --no-check -x /*.dsc /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && cd /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && { printf '%s' 'aac-tactics (8.11.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * coq changed from rd419 to fis13 -- amd64 Build Daemon (x86-grnet-01) Fri, 10 Apr 2020 13:02:29 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/aac-tactics-9ZXkKW" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1586523749" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/aac-tactics-9ZXkKW /tmp/aac-tactics-8.11.0-1+b1ptk1_atc bullseye /dev/null deb http://snapshot.notset.fr/archive/debian/20200410T084926Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: tar I: using /tmp/mmdebstrap.f5lJfyhhoT 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.f5lJfyhhoT Reading package lists... Building dependency tree... util-linux is already the newest version (2.34-0.1). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 132 kB of archives. After this operation, 393 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20200410T084926Z unstable/main amd64 libfakeroot amd64 1.24-1 [45.7 kB] Get:2 http://snapshot.notset.fr/archive/debian/20200410T084926Z unstable/main amd64 fakeroot amd64 1.24-1 [85.9 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 132 kB in 0s (670 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 ... 4505 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.24-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.24-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.24-1_amd64.deb ... Unpacking fakeroot (1.24-1) ... Setting up libfakeroot:amd64 (1.24-1) ... Setting up fakeroot (1.24-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.30-4) ... 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/20200323T101008Z/ bullseye main deb-src http://snapshot.notset.fr/archive/debian/20200323T101008Z/ bullseye main deb http://snapshot.notset.fr/archive/debian/20200410T084926Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.f5lJfyhhoT Get:1 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye InRelease [116 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20200410T084926Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main Sources [10.4 MB] Get:4 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main amd64 Packages [10.2 MB] Fetched 20.7 MB in 18s (1149 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.f5lJfyhhoT I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d aac-tactics=8.11.0-1 && mkdir -p /build/aac-tactics-9ZXkKW && dpkg-source --no-check -x /*.dsc /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && cd /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && { printf '%s' 'aac-tactics (8.11.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * coq changed from rd419 to fis13 -- amd64 Build Daemon (x86-grnet-01) Fri, 10 Apr 2020 13:02:29 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/aac-tactics-9ZXkKW"' exec /tmp/mmdebstrap.f5lJfyhhoT Reading package lists... NOTICE: 'aac-tactics' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/aac-tactics.git Please use: git clone https://salsa.debian.org/ocaml-team/aac-tactics.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 71.1 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main aac-tactics 8.11.0-1 (dsc) [2178 B] Get:2 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main aac-tactics 8.11.0-1 (tar) [65.4 kB] Get:3 http://snapshot.notset.fr/archive/debian/20200323T101008Z bullseye/main aac-tactics 8.11.0-1 (diff) [3520 B] Fetched 71.1 kB in 0s (521 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'aac-tactics_8.11.0-1.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting aac-tactics in /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 dpkg-source: info: unpacking aac-tactics_8.11.0.orig.tar.gz dpkg-source: info: unpacking aac-tactics_8.11.0-1.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1586523749" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.f5lJfyhhoT dpkg-buildpackage: info: source package aac-tactics dpkg-buildpackage: info: source version 8.11.0-1+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 ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make clean make[2]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' coq_makefile -f _CoqProject -o Makefile.coq /usr/bin/make -f Makefile.coq cleanall make[3]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' rm -f src/aac.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac_plugin.cmo rm -f src/aac.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi src/aac_plugin.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi rm -f src/aac_plugin.cma rm -f src/aac.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac_plugin.cmx rm -f src/aac_plugin.cmxa rm -f src/aac_plugin.cmxs src/aac_plugin.cmxs rm -f src/aac.o src/coq.o src/helper.o src/search_monad.o src/matcher.o src/theory.o src/print.o src/aac_rewrite.o src/aac_plugin.o rm -f src/aac_plugin.a rm -f src/aac.ml rm -f src/aac.mlg.d src/coq.ml.d src/helper.ml.d src/search_monad.ml.d src/matcher.ml.d src/theory.ml.d src/print.ml.d src/aac_rewrite.ml.d src/aac_plugin.mlpack.d src/coq.mli.d src/helper.mli.d src/search_monad.mli.d src/matcher.mli.d src/theory.mli.d src/print.mli.d src/aac_rewrite.mli.d .Makefile.coq.d rm -f find . -name .coq-native -type d -empty -delete rm -f theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo rm -f theories/Utils.vio theories/Constants.vio theories/AAC.vio theories/Instances.vio theories/Tutorial.vio theories/Caveats.vio rm -f theories/Utils.vos theories/Constants.vos theories/AAC.vos theories/Instances.vos theories/Tutorial.vos theories/Caveats.vos rm -f theories/Utils.vok theories/Constants.vok theories/AAC.vok theories/Instances.vok theories/Tutorial.vok theories/Caveats.vok rm -f theories/Utils.v.beautified theories/Constants.v.beautified theories/AAC.v.beautified theories/Instances.v.beautified theories/Tutorial.v.beautified theories/Caveats.v.beautified theories/Utils.v.old theories/Constants.v.old theories/AAC.v.old theories/Instances.v.old theories/Tutorial.v.old theories/Caveats.v.old rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex rm -f theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob rm -f theories/Utils.tex theories/Constants.tex theories/AAC.tex theories/Instances.tex theories/Tutorial.tex theories/Caveats.tex rm -f theories/Utils.g.tex theories/Constants.g.tex theories/AAC.g.tex theories/Instances.g.tex theories/Tutorial.g.tex theories/Caveats.g.tex rm -f pretty-timed-success.ok rm -rf html mlihtml rm -f theories/.Utils.aux theories/.Constants.aux theories/.AAC.aux theories/.Instances.aux theories/.Tutorial.aux theories/.Caveats.aux rm -f time-of-build.log time-of-build-before.log time-of-build-after.log time-of-build-pretty.log time-of-build-both.log rm -f theories/Utils.v.timing theories/Constants.v.timing theories/AAC.v.timing theories/Instances.v.timing theories/Tutorial.v.timing theories/Caveats.v.timing rm -f theories/Utils.v.before-timing theories/Constants.v.before-timing theories/AAC.v.before-timing theories/Instances.v.before-timing theories/Tutorial.v.before-timing theories/Caveats.v.before-timing rm -f theories/Utils.v.after-timing theories/Constants.v.after-timing theories/AAC.v.after-timing theories/Instances.v.after-timing theories/Tutorial.v.after-timing theories/Caveats.v.after-timing rm -f theories/Utils.v.timing.diff theories/Constants.v.timing.diff theories/AAC.v.timing.diff theories/Instances.v.timing.diff theories/Tutorial.v.timing.diff theories/Caveats.v.timing.diff make[3]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' rm -f Makefile.coq Makefile.coq.conf make[2]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' make[1]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with 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/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make Makefile.coq make[2]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' coq_makefile -f _CoqProject -o Makefile.coq make[2]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make -f Makefile.coq opt byte html make[2]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' "coqdep" -vos -dyndep var -f _CoqProject > ".Makefile.coq.d" || ( RV=$?; rm -f ".Makefile.coq.d"; exit $RV ) "coqpp" src/aac.mlg "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.mli" > "src/aac_rewrite.mli.d" || ( RV=$?; rm -f "src/aac_rewrite.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.mli" > "src/print.mli.d" || ( RV=$?; rm -f "src/print.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.mli" > "src/theory.mli.d" || ( RV=$?; rm -f "src/theory.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.mli" > "src/matcher.mli.d" || ( RV=$?; rm -f "src/matcher.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.mli" > "src/search_monad.mli.d" || ( RV=$?; rm -f "src/search_monad.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.mli" > "src/helper.mli.d" || ( RV=$?; rm -f "src/helper.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.mli" > "src/coq.mli.d" || ( RV=$?; rm -f "src/coq.mli.d"; exit $RV ) "coqdep" -I src -c "src/aac_plugin.mlpack" > "src/aac_plugin.mlpack.d" || ( RV=$?; rm -f "src/aac_plugin.mlpack.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.ml" > "src/aac_rewrite.ml.d" || ( RV=$?; rm -f "src/aac_rewrite.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.ml" > "src/print.ml.d" || ( RV=$?; rm -f "src/print.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.ml" > "src/theory.ml.d" || ( RV=$?; rm -f "src/theory.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.ml" > "src/matcher.ml.d" || ( RV=$?; rm -f "src/matcher.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.ml" > "src/search_monad.ml.d" || ( RV=$?; rm -f "src/search_monad.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.ml" > "src/helper.ml.d" || ( RV=$?; rm -f "src/helper.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.ml" > "src/coq.ml.d" || ( RV=$?; rm -f "src/coq.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac.ml" > "src/aac.mlg.d" || ( RV=$?; rm -f "src/aac.mlg.d"; exit $RV ) /usr/bin/make all "OPT:=-opt" -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make --no-print-directory -f "Makefile.coq" pre-all if [ "8.11.0" != "8.11.0" ]; then\ echo "W: This Makefile was generated by Coq 8.11.0";\ echo "W: while the current Coq version is 8.11.0";\ fi /usr/bin/make --no-print-directory -f "Makefile.coq" real-all "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Utils.v "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Constants.v "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/coq.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/coq.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/helper.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/helper.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/search_monad.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/search_monad.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/matcher.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/matcher.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/matcher.ml", line 191, characters 26-44: 191 | let nf_term_compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/theory.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/theory.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/theory.ml", line 868, characters 24-42: 868 | cap t (List.sort (Pervasives.compare) indices) ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/print.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/print.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/print.ml", line 83, characters 42-60: 83 | let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/aac_rewrite.mli findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/aac_rewrite.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/aac.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -linkpkg -dontlink unix,str -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -pack -o src/aac_plugin.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac.cmx findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -linkpkg -dontlink unix,str -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -a -o src/aac_plugin.cmxa src/aac_plugin.cmx findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" opt -linkpkg -dontlink unix,str -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 \ -shared -linkall -o src/aac_plugin.cmxs src/aac_plugin.cmxa findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/AAC.v "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Instances.v "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Tutorial.v All solutions: occurrence 0: transitivity through forall x : X, plus x x 1 possible(s) substitution(s) 0: [x: f (a + a); ] occurrence 1: transitivity through forall x : X, plus (f (x + x)) (f (a + a)) 1 possible(s) substitution(s) 0: [x: a; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 4 possible(s) substitution(s) 0: [x: c; y: dot (d * c * d) b; ] 1: [x: dot c d; y: dot (c * d) b; ] 2: [x: dot (c * d) c; y: dot d b; ] 3: [x: dot (c * d * c) d; y: b; ] occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 1 possible(s) substitution(s) 0: [x: plus (c * d) (c * d); y: b; ] All solutions: occurrence 0: transitivity through forall x : X, dot (a * x) a 1 possible(s) substitution(s) 0: [x: 1; ] All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: a; y: c; z: dot b c; ] 1: [x: a; y: dot b c; z: c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * c) 2 possible(s) substitution(s) 0: [x: a; y: dot b c; z: b; ] 1: [x: a; y: b; z: dot b c; ] occurrence 2: transitivity through forall x y z : X, plus (x * y + x * z) (a * b * c) 2 possible(s) substitution(s) 0: [x: a; y: c; z: b; ] 1: [x: a; y: b; z: c; ] File "./theories/Tutorial.v", line 215, characters 6-24: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z) 6 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: dot a b; ] 1: [x: a; y: plus (b * c) c; z: b; ] 2: [x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ] 3: [x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ] 4: [x: 1; y: dot a b; z: dot a (b * c + c); ] 5: [x: a; y: b; z: plus (b * c) c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: 0; ] 1: [x: 1; y: 0; z: dot a (b * c + c); ] occurrence 2: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * b) 4 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: c; ] 1: [x: 1; y: 0; z: plus (b * c) c; ] 2: [x: 1; y: plus (b * c) c; z: 0; ] 3: [x: 1; y: c; z: dot b c; ] occurrence 3: transitivity through forall x y z : X, plus (a * (x * y + x * z + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: 0; ] 1: [x: 1; y: 0; z: dot b c; ] occurrence 4: transitivity through forall x y z : X, plus (x * y + x * z) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: dot a b; z: 0; ] 1: [x: 1; y: 0; z: dot a b; ] occurrence 5: transitivity through forall x y z : X, plus (a * (b * (x * y + x * z) + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 6: transitivity through forall x y z : X, plus (a * ((x * y + x * z) * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 7: transitivity through forall x y z : X, plus (a * (x * y + x * z + b * c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 8: transitivity through forall x y z : X, plus ((x * y + x * z) * (b * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 9: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 10: transitivity through forall x y z : X, plus ((x * y + x * z) * b) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 11: transitivity through plus (a * (b * c + c)) ((1 * 1 + 1 * 0) * (a * b)) occurrence 12: transitivity through plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0)) occurrence 13: transitivity through plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b)) occurrence 14: transitivity through plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c))) occurrence 15: transitivity through plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0)) occurrence 16: transitivity through plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c)) occurrence 17: transitivity through plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0))) occurrence 18: transitivity through plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c))) occurrence 19: transitivity through plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0))) occurrence 20: transitivity through plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c))) occurrence 21: transitivity through plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c))) occurrence 22: transitivity through dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0) occurrence 23: transitivity through dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b) occurrence 24: transitivity through plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b)) occurrence 25: transitivity through plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1)) occurrence 26: transitivity through plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b)) occurrence 27: transitivity through plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c))) occurrence 28: transitivity through plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1)) occurrence 29: transitivity through plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c)) occurrence 30: transitivity through plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1))) occurrence 31: transitivity through plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c))) occurrence 32: transitivity through plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1))) occurrence 33: transitivity through plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c))) occurrence 34: transitivity through plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c))) occurrence 35: transitivity through dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1) occurrence 36: transitivity through dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b) occurrence 37: transitivity through plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0) occurrence 38: transitivity through plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0))) occurrence 39: transitivity through plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b) occurrence 40: transitivity through plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0))) occurrence 41: transitivity through plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0)))) occurrence 42: transitivity through plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c)) occurrence 43: transitivity through plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c)) occurrence 44: transitivity through plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1) occurrence 45: transitivity through plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1))) occurrence 46: transitivity through plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b) occurrence 47: transitivity through plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1))) occurrence 48: transitivity through plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1)))) occurrence 49: transitivity through plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c)) occurrence 50: transitivity through plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c)) occurrence 51: transitivity through plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0))) occurrence 52: transitivity through plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b)) occurrence 53: transitivity through plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b)) occurrence 54: transitivity through plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0))) occurrence 55: transitivity through plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0)))) occurrence 56: transitivity through plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c))) occurrence 57: transitivity through plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c))) occurrence 58: transitivity through plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c))) occurrence 59: transitivity through plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c))) occurrence 60: transitivity through plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1))) occurrence 61: transitivity through plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b)) occurrence 62: transitivity through plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b)) occurrence 63: transitivity through plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1))) occurrence 64: transitivity through plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1)))) occurrence 65: transitivity through plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c))) occurrence 66: transitivity through plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c))) occurrence 67: transitivity through plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c))) occurrence 68: transitivity through plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c))) All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] File "./theories/Tutorial.v", line 369, characters 4-37: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z occurrence 1: transitivity through (Z.abs a + - (Z.abs b + 0))%Z occurrence 2: transitivity through (Z.abs a + - Z.abs (b + 0))%Z occurrence 3: transitivity through (- Z.abs b + Z.abs (a + 0))%Z File "./theories/Tutorial.v", line 370, characters 4-40: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Caveats.v All solutions: occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z 1 possible(s) substitution(s) 0: [x: a; ] occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z 1 possible(s) substitution(s) 0: [x: b; ] File "./theories/Caveats.v", line 282, characters 4-32: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through dot y 1 occurrence 1: transitivity through dot 1 y File "./theories/Caveats.v", line 283, characters 4-35: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 300, characters 4-18: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 308, characters 4-23: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 331, characters 2-19: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c * b + a + 0)%nat occurrence 1: transitivity through (a + b * (c + 0))%nat occurrence 2: transitivity through (a + c * (b + 0))%nat File "./theories/Caveats.v", line 350, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c + b + a + 0)%nat File "./theories/Caveats.v", line 353, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((c + b + a) * 1)%nat occurrence 1: transitivity through (c + a + b * 1)%nat occurrence 2: transitivity through (a + (c + b) * 1)%nat occurrence 3: transitivity through (b + a + c * 1)%nat occurrence 4: transitivity through (c + (b + a) * 1)%nat occurrence 5: transitivity through (c + b + a * 1)%nat occurrence 6: transitivity through (b + (c + a) * 1)%nat All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] File "./theories/Caveats.v", line 366, characters 2-22: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 2: transitivity through (a * b + c + a * a * (1 * 1 + 0 * 1))%nat occurrence 3: transitivity through (c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat occurrence 4: transitivity through (a * a + c + a * b * (1 * 1 + 0 * 1))%nat occurrence 5: transitivity through (a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 6: transitivity through (a * b + a * a + c * (1 * 1 + 0 * 1))%nat occurrence 7: transitivity through (a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat File "./theories/Caveats.v", line 369, characters 2-20: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat occurrence 1: transitivity through (a * b + c + a * a * 1)%nat occurrence 2: transitivity through (c + (a * b + a * a) * 1)%nat occurrence 3: transitivity through (a * a + c + a * b * 1)%nat occurrence 4: transitivity through (a * b + (a * a + c) * 1)%nat occurrence 5: transitivity through (a * b + a * a + c * 1)%nat occurrence 6: transitivity through (a * a + (a * b + c) * 1)%nat /usr/bin/make --no-print-directory -f "Makefile.coq" post-all make[3]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make all "OPT:=-byte" -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make --no-print-directory -f "Makefile.coq" pre-all if [ "8.11.0" != "8.11.0" ]; then\ echo "W: This Makefile was generated by Coq 8.11.0";\ echo "W: while the current Coq version is 8.11.0";\ fi /usr/bin/make --no-print-directory -f "Makefile.coq" real-all "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/coq.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/helper.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/search_monad.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/matcher.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/matcher.ml", line 191, characters 26-44: 191 | let nf_term_compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/theory.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/theory.ml", line 868, characters 24-42: 868 | cap t (List.sort (Pervasives.compare) indices) ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/print.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src File "src/print.ml", line 83, characters 42-60: 83 | let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/aac_rewrite.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 src/aac.ml findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -linkpkg -dontlink unix,str -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -pack -o src/aac_plugin.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac.cmo findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "/usr/bin/ocamlfind" ocamlc -linkpkg -dontlink unix,str -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58 -safe-string -strict-sequence -I src -I "/usr/lib/coq//config" -I "/usr/lib/coq//lib" -I "/usr/lib/coq//clib" -I "/usr/lib/coq//kernel" -I "/usr/lib/coq//library" -I "/usr/lib/coq//engine" -I "/usr/lib/coq//pretyping" -I "/usr/lib/coq//interp" -I "/usr/lib/coq//gramlib" -I "/usr/lib/coq//gramlib/.pack" -I "/usr/lib/coq//parsing" -I "/usr/lib/coq//proofs" -I "/usr/lib/coq//tactics" -I "/usr/lib/coq//toplevel" -I "/usr/lib/coq//printing" -I "/usr/lib/coq//ide" -I "/usr/lib/coq//stm" -I "/usr/lib/coq//vernac" -I "/usr/lib/coq//plugins/btauto" -I "/usr/lib/coq//plugins/cc" -I "/usr/lib/coq//plugins/derive" -I "/usr/lib/coq//plugins/extraction" -I "/usr/lib/coq//plugins/firstorder" -I "/usr/lib/coq//plugins/fourier" -I "/usr/lib/coq//plugins/funind" -I "/usr/lib/coq//plugins/ltac" -I "/usr/lib/coq//plugins/micromega" -I "/usr/lib/coq//plugins/nsatz" -I "/usr/lib/coq//plugins/omega" -I "/usr/lib/coq//plugins/rtauto" -I "/usr/lib/coq//plugins/setoid_ring" -I "/usr/lib/coq//plugins/ssr" -I "/usr/lib/coq//plugins/ssrmatching" -I "/usr/lib/coq//plugins/syntax" -warn-error +a-3 -a -o src/aac_plugin.cma src/aac_plugin.cmo findlib: [WARNING] Interface coq.cmi occurs in several directories: /usr/lib/coq/ide, src "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/AAC.v "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Instances.v "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Tutorial.v All solutions: occurrence 0: transitivity through forall x : X, plus x x 1 possible(s) substitution(s) 0: [x: f (a + a); ] occurrence 1: transitivity through forall x : X, plus (f (x + x)) (f (a + a)) 1 possible(s) substitution(s) 0: [x: a; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 4 possible(s) substitution(s) 0: [x: c; y: dot (d * c * d) b; ] 1: [x: dot c d; y: dot (c * d) b; ] 2: [x: dot (c * d) c; y: dot d b; ] 3: [x: dot (c * d * c) d; y: b; ] occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 1 possible(s) substitution(s) 0: [x: plus (c * d) (c * d); y: b; ] All solutions: occurrence 0: transitivity through forall x : X, dot (a * x) a 1 possible(s) substitution(s) 0: [x: 1; ] All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: a; y: c; z: dot b c; ] 1: [x: a; y: dot b c; z: c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * c) 2 possible(s) substitution(s) 0: [x: a; y: dot b c; z: b; ] 1: [x: a; y: b; z: dot b c; ] occurrence 2: transitivity through forall x y z : X, plus (x * y + x * z) (a * b * c) 2 possible(s) substitution(s) 0: [x: a; y: c; z: b; ] 1: [x: a; y: b; z: c; ] File "./theories/Tutorial.v", line 215, characters 6-24: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z) 6 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: dot a b; ] 1: [x: a; y: plus (b * c) c; z: b; ] 2: [x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ] 3: [x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ] 4: [x: 1; y: dot a b; z: dot a (b * c + c); ] 5: [x: a; y: b; z: plus (b * c) c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: 0; ] 1: [x: 1; y: 0; z: dot a (b * c + c); ] occurrence 2: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * b) 4 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: c; ] 1: [x: 1; y: 0; z: plus (b * c) c; ] 2: [x: 1; y: plus (b * c) c; z: 0; ] 3: [x: 1; y: c; z: dot b c; ] occurrence 3: transitivity through forall x y z : X, plus (a * (x * y + x * z + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: 0; ] 1: [x: 1; y: 0; z: dot b c; ] occurrence 4: transitivity through forall x y z : X, plus (x * y + x * z) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: dot a b; z: 0; ] 1: [x: 1; y: 0; z: dot a b; ] occurrence 5: transitivity through forall x y z : X, plus (a * (b * (x * y + x * z) + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 6: transitivity through forall x y z : X, plus (a * ((x * y + x * z) * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 7: transitivity through forall x y z : X, plus (a * (x * y + x * z + b * c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 8: transitivity through forall x y z : X, plus ((x * y + x * z) * (b * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 9: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 10: transitivity through forall x y z : X, plus ((x * y + x * z) * b) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 11: transitivity through plus (a * (b * c + c)) ((1 * 1 + 1 * 0) * (a * b)) occurrence 12: transitivity through plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0)) occurrence 13: transitivity through plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b)) occurrence 14: transitivity through plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c))) occurrence 15: transitivity through plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0)) occurrence 16: transitivity through plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c)) occurrence 17: transitivity through plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0))) occurrence 18: transitivity through plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c))) occurrence 19: transitivity through plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0))) occurrence 20: transitivity through plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c))) occurrence 21: transitivity through plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c))) occurrence 22: transitivity through dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0) occurrence 23: transitivity through dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b) occurrence 24: transitivity through plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b)) occurrence 25: transitivity through plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1)) occurrence 26: transitivity through plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b)) occurrence 27: transitivity through plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c))) occurrence 28: transitivity through plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1)) occurrence 29: transitivity through plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c)) occurrence 30: transitivity through plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1))) occurrence 31: transitivity through plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c))) occurrence 32: transitivity through plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1))) occurrence 33: transitivity through plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c))) occurrence 34: transitivity through plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c))) occurrence 35: transitivity through dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1) occurrence 36: transitivity through dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b) occurrence 37: transitivity through plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0) occurrence 38: transitivity through plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0))) occurrence 39: transitivity through plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b) occurrence 40: transitivity through plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0))) occurrence 41: transitivity through plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0)))) occurrence 42: transitivity through plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c)) occurrence 43: transitivity through plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c)) occurrence 44: transitivity through plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1) occurrence 45: transitivity through plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1))) occurrence 46: transitivity through plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b) occurrence 47: transitivity through plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1))) occurrence 48: transitivity through plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1)))) occurrence 49: transitivity through plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c)) occurrence 50: transitivity through plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c)) occurrence 51: transitivity through plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0))) occurrence 52: transitivity through plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b)) occurrence 53: transitivity through plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b)) occurrence 54: transitivity through plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0))) occurrence 55: transitivity through plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0)))) occurrence 56: transitivity through plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c))) occurrence 57: transitivity through plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c))) occurrence 58: transitivity through plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c))) occurrence 59: transitivity through plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c))) occurrence 60: transitivity through plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1))) occurrence 61: transitivity through plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b)) occurrence 62: transitivity through plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b)) occurrence 63: transitivity through plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1))) occurrence 64: transitivity through plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1)))) occurrence 65: transitivity through plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c))) occurrence 66: transitivity through plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c))) occurrence 67: transitivity through plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c))) occurrence 68: transitivity through plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c))) All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] File "./theories/Tutorial.v", line 369, characters 4-37: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z occurrence 1: transitivity through (Z.abs a + - (Z.abs b + 0))%Z occurrence 2: transitivity through (Z.abs a + - Z.abs (b + 0))%Z occurrence 3: transitivity through (- Z.abs b + Z.abs (a + 0))%Z File "./theories/Tutorial.v", line 370, characters 4-40: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing "coqc" -q -w +default -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Caveats.v All solutions: occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z 1 possible(s) substitution(s) 0: [x: a; ] occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z 1 possible(s) substitution(s) 0: [x: b; ] File "./theories/Caveats.v", line 282, characters 4-32: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through dot y 1 occurrence 1: transitivity through dot 1 y File "./theories/Caveats.v", line 283, characters 4-35: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 300, characters 4-18: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 308, characters 4-23: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 331, characters 2-19: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c * b + a + 0)%nat occurrence 1: transitivity through (a + b * (c + 0))%nat occurrence 2: transitivity through (a + c * (b + 0))%nat File "./theories/Caveats.v", line 350, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c + b + a + 0)%nat File "./theories/Caveats.v", line 353, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((c + b + a) * 1)%nat occurrence 1: transitivity through (c + a + b * 1)%nat occurrence 2: transitivity through (a + (c + b) * 1)%nat occurrence 3: transitivity through (b + a + c * 1)%nat occurrence 4: transitivity through (c + (b + a) * 1)%nat occurrence 5: transitivity through (c + b + a * 1)%nat occurrence 6: transitivity through (b + (c + a) * 1)%nat All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] File "./theories/Caveats.v", line 366, characters 2-22: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 2: transitivity through (a * b + c + a * a * (1 * 1 + 0 * 1))%nat occurrence 3: transitivity through (c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat occurrence 4: transitivity through (a * a + c + a * b * (1 * 1 + 0 * 1))%nat occurrence 5: transitivity through (a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 6: transitivity through (a * b + a * a + c * (1 * 1 + 0 * 1))%nat occurrence 7: transitivity through (a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat File "./theories/Caveats.v", line 369, characters 2-20: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat occurrence 1: transitivity through (a * b + c + a * a * 1)%nat occurrence 2: transitivity through (c + (a * b + a * a) * 1)%nat occurrence 3: transitivity through (a * a + c + a * b * 1)%nat occurrence 4: transitivity through (a * b + (a * a + c) * 1)%nat occurrence 5: transitivity through (a * b + a * a + c * 1)%nat occurrence 6: transitivity through (a * a + (a * b + c) * 1)%nat /usr/bin/make --no-print-directory -f "Makefile.coq" post-all make[3]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' mkdir -p html "coqdoc" \ -toc -interpolate -utf8 -html -Q theories AAC_tactics -Q src AAC_tactics -d html theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v make[2]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' make[1]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_auto_test -a create-stamp debian/debhelper-build-stamp dh_testroot -a dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' /usr/bin/make -f Makefile.coq install install-byte DSTROOT=/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp make[2]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' code=0; for f in theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob src/aac_plugin.cmi src/aac_plugin.cmxs src/aac_plugin.cmxs src/aac_plugin.cmxa src/aac_plugin.cmx; do\ if ! [ -f "$f" ]; then >&2 echo $f does not exist; code=1; fi \ done; exit $code for f in theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob src/aac_plugin.cmi src/aac_plugin.cmxs src/aac_plugin.cmxs src/aac_plugin.cmxa src/aac_plugin.cmx; do\ df="`"coq_makefile" -destination-of "$f" -I src -Q theories AAC_tactics -Q src AAC_tactics `";\ if [ "$?" != "0" -o -z "$df" ]; then\ echo SKIP "$f" since it has no logical path;\ else\ install -d "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df" &&\ install -m 0644 "$f" "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df" &&\ echo INSTALL "$f" "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df";\ fi;\ done INSTALL theories/Utils.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.vo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Utils.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.v /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Utils.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.glob /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmi /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxs /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxs /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxa /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmx /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ /usr/bin/make install-extra -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' make[3]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' for f in src/aac_plugin.cmo src/aac_plugin.cma; do\ df="`"coq_makefile" -destination-of "$f" -I src -Q theories AAC_tactics -Q src AAC_tactics `";\ if [ "$?" != "0" -o -z "$df" ]; then\ echo SKIP "$f" since it has no logical path;\ else\ install -d "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df" &&\ install -m 0644 "$f" "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df" &&\ echo INSTALL "$f" "/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/$df";\ fi;\ done INSTALL src/aac_plugin.cmo /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cma /build/aac-tactics-9ZXkKW/aac-tactics-8.11.0/debian/tmp//usr/lib/coq//user-contrib/AAC_tactics/ make[2]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' make[1]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_install -a dh_ocamldoc -a Warning: Element Rewrite not found Warning: Element Rewrite not found dh_installdocs -a dh_installchangelogs -a dh_lintian -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a debian/rules override_dh_missing make[1]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_missing --fail-missing make[1]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_dwz -a dwz: debian/libaac-tactics-ocaml/usr/lib/coq/user-contrib/AAC_tactics/aac_plugin.cmxs: .debug_info section not present dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_ocaml -a debian/rules override_dh_gencontrol make[1]: Entering directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_gencontrol -- -VF:CoqABI="8.11.0+4.08.1" dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml-dev: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml: substitution variable ${shlibs:Depends} used, but is not defined make[1]: Leaving directory '/build/aac-tactics-9ZXkKW/aac-tactics-8.11.0' dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libaac-tactics-ocaml' in '../libaac-tactics-ocaml_8.11.0-1+b1_amd64.deb'. dpkg-deb: building package 'libaac-tactics-ocaml-dbgsym' in '../libaac-tactics-ocaml-dbgsym_8.11.0-1+b1_amd64.deb'. dpkg-deb: building package 'libaac-tactics-ocaml-dev' in '../libaac-tactics-ocaml-dev_8.11.0-1+b1_amd64.deb'. dpkg-genbuildinfo --build=any dpkg-genchanges --build=any >../aac-tactics_8.11.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/aac-tactics-9ZXkKW /tmp/aac-tactics-8.11.0-1+b1ptk1_atc I: cleaning package lists and apt cache... I: creating tarball... I: done I: removing tempdir /tmp/mmdebstrap.f5lJfyhhoT... I: success in 3851.7516 seconds md5: libaac-tactics-ocaml-dbgsym_8.11.0-1+b1_amd64.deb: OK md5: libaac-tactics-ocaml-dev_8.11.0-1+b1_amd64.deb: OK md5: libaac-tactics-ocaml_8.11.0-1+b1_amd64.deb: OK sha1: libaac-tactics-ocaml-dbgsym_8.11.0-1+b1_amd64.deb: OK sha1: libaac-tactics-ocaml-dev_8.11.0-1+b1_amd64.deb: OK sha1: libaac-tactics-ocaml_8.11.0-1+b1_amd64.deb: OK sha256: libaac-tactics-ocaml-dbgsym_8.11.0-1+b1_amd64.deb: OK sha256: libaac-tactics-ocaml-dev_8.11.0-1+b1_amd64.deb: OK sha256: libaac-tactics-ocaml_8.11.0-1+b1_amd64.deb: OK Checksums: OK