Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/w/why3/why3_1.3.3-1+b4_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/why3-1.3.3-1+b40nz0l5bo/why3_1.3.3-1+b4_amd64.buildinfo Get source package info: why3=1.3.3-1 Source URL: http://snapshot.notset.fr/mr/package/why3/1.3.3-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.38.0-1 autoconf=2.69-14 automake=1:1.16.3-2 autopoint=0.21-3 autotools-dev=20180224.1+nmu1 base-files=11 base-passwd=3.5.48 bash=5.1-2 binutils=2.35.1-7 binutils-common=2.35.1-7 binutils-x86-64-linux-gnu=2.35.1-7 bsdextrautils=2.36.1-6 bsdutils=1:2.36.1-6 build-essential=12.9 bzip2=1.0.8-4 coq=8.12.0-3+b3 coq-theories=8.12.0-3+b3 coreutils=8.32-4+b1 cpp=4:10.2.1-1 cpp-10=10.2.1-6 dash=0.5.11+git20200708+dd9ef66-5 dbus=1.12.20-1 dbus-user-session=1.12.20-1 dconf-gsettings-backend=0.38.0-1 dconf-service=0.38.0-1 debconf=1.5.74 debhelper=13.3.1 debianutils=4.11.2 dh-autoreconf=19 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.10.0-1 diffutils=1:3.7-5 dmsetup=2:1.02.175-2 dpkg=1.20.7.1 dpkg-dev=1.20.7.1 dwz=0.13+20210118-1 file=1:5.39-3 findutils=4.8.0-1 fontconfig=2.13.1-4.2 fontconfig-config=2.13.1-4.2 fonts-dejavu-core=2.37-2 g++=4:10.2.1-1 g++-10=10.2.1-6 gcc=4:10.2.1-1 gcc-10=10.2.1-6 gcc-10-base=10.2.1-6 gettext=0.21-3 gettext-base=0.21-3 gir1.2-atk-1.0=2.36.0-2 gir1.2-atspi-2.0=2.38.0-2 gir1.2-freedesktop=1.66.1-1+b1 gir1.2-gdkpixbuf-2.0=2.42.2+dfsg-1 gir1.2-glib-2.0=1.66.1-1+b1 gir1.2-gtk-3.0=3.24.24-1 gir1.2-gtksource-3.0=3.24.11-2 gir1.2-harfbuzz-0.0=2.7.4-1 gir1.2-pango-1.0=1.46.2-3 glib-networking=2.66.0-2 glib-networking-common=2.66.0-2 glib-networking-services=2.66.0-2 grep=3.6-1 groff-base=1.22.4-5 gsettings-desktop-schemas=3.38.0-2 gtk-update-icon-cache=3.24.24-1 gzip=1.10-2 hicolor-icon-theme=0.17-2 hostname=3.23 icu-devtools=67.1-6 init-system-helpers=1.60 intltool-debian=0.35.0+20060710.5 libacl1=2.2.53-9 libapparmor1=2.13.6-7 libarchive-zip-perl=1.68-1 libargon2-1=0~20171227-0.2 libasan6=10.2.1-6 libatk-bridge2.0-0=2.38.0-1 libatk-bridge2.0-dev=2.38.0-1 libatk1.0-0=2.36.0-2 libatk1.0-data=2.36.0-2 libatk1.0-dev=2.36.0-2 libatomic1=10.2.1-6 libatspi2.0-0=2.38.0-2 libatspi2.0-dev=2.38.0-2 libattr1=1:2.4.48-6 libaudit-common=1:3.0-2 libaudit1=1:3.0-2 libavahi-client3=0.8-3 libavahi-common-data=0.8-3 libavahi-common3=0.8-3 libbinutils=2.35.1-7 libblkid-dev=2.36.1-6 libblkid1=2.36.1-6 libbrotli-dev=1.0.9-2+b2 libbrotli1=1.0.9-2+b2 libbsd0=0.10.0-1 libbz2-1.0=1.0.8-4 libc-bin=2.31-9 libc-dev-bin=2.31-9 libc6=2.31-9 libc6-dev=2.31-9 libcairo-gobject2=1.16.0-5 libcairo-script-interpreter2=1.16.0-5 libcairo2=1.16.0-5 libcairo2-dev=1.16.0-5 libcairo2-ocaml=0.6.1+dfsg-6 libcairo2-ocaml-dev=0.6.1+dfsg-6 libcap-ng0=0.7.9-2.2+b1 libcap2=1:2.44-1 libcc1-0=10.2.1-6 libcolord2=1.4.5-3 libcom-err2=1.45.6-1 libcoq-ocaml=8.12.0-3+b3 libcoq-ocaml-dev=8.12.0-3+b3 libcrypt-dev=1:4.4.17-1 libcrypt1=1:4.4.17-1 libcryptsetup12=2:2.3.4-2 libctf-nobfd0=2.35.1-7 libctf0=2.35.1-7 libcups2=2.3.3op1-7 libdatrie-dev=0.2.12-3 libdatrie1=0.2.12-3 libdb5.3=5.3.28+dfsg1-0.6 libdbus-1-3=1.12.20-1 libdbus-1-dev=1.12.20-1 libdconf1=0.38.0-1 libdebconfclient0=0.256 libdebhelper-perl=13.3.1 libdeflate0=1.7-1 libdevmapper1.02.1=2:1.02.175-2 libdpkg-perl=1.20.7.1 libdrm-amdgpu1=2.4.103-2 libdrm-common=2.4.103-2 libdrm-intel1=2.4.103-2 libdrm-nouveau2=2.4.103-2 libdrm-radeon1=2.4.103-2 libdrm2=2.4.103-2 libedit2=3.1-20191231-2+b1 libegl-dev=1.3.2-1 libegl-mesa0=20.3.3-1 libegl1=1.3.2-1 libegl1-mesa-dev=20.3.3-1 libelf1=0.182-3 libepoxy-dev=1.5.4-1 libepoxy0=1.5.4-1 libexpat1=2.2.10-1 libexpat1-dev=2.2.10-1 libffi-dev=3.3-5 libffi7=3.3-5 libfile-stripnondeterminism-perl=1.10.0-1 libfindlib-ocaml=1.8.1-2 libfontconfig-dev=2.13.1-4.2 libfontconfig1=2.13.1-4.2 libfontconfig1-dev=2.13.1-4.2 libfreetype-dev=2.10.4+dfsg-1 libfreetype6=2.10.4+dfsg-1 libfreetype6-dev=2.10.4+dfsg-1 libfribidi-dev=1.0.8-2 libfribidi0=1.0.8-2 libgbm1=20.3.3-1 libgcc-10-dev=10.2.1-6 libgcc-s1=10.2.1-6 libgcrypt20=1.8.7-2 libgdbm-compat4=1.19-2 libgdbm6=1.19-2 libgdk-pixbuf-2.0-0=2.42.2+dfsg-1 libgdk-pixbuf-2.0-dev=2.42.2+dfsg-1 libgdk-pixbuf-xlib-2.0-0=2.40.2-2 libgdk-pixbuf2.0-0=2.40.2-2 libgdk-pixbuf2.0-bin=2.42.2+dfsg-1 libgdk-pixbuf2.0-common=2.42.2+dfsg-1 libgirepository-1.0-1=1.66.1-1+b1 libgl-dev=1.3.2-1 libgl1=1.3.2-1 libgl1-mesa-dev=20.3.3-1 libgl1-mesa-dri=20.3.3-1 libglapi-mesa=20.3.3-1 libgles-dev=1.3.2-1 libgles1=1.3.2-1 libgles2=1.3.2-1 libglib2.0-0=2.66.4-1 libglib2.0-bin=2.66.4-1 libglib2.0-data=2.66.4-1 libglib2.0-dev=2.66.4-1 libglib2.0-dev-bin=2.66.4-1 libglvnd-dev=1.3.2-1 libglvnd0=1.3.2-1 libglx-dev=1.3.2-1 libglx-mesa0=20.3.3-1 libglx0=1.3.2-1 libgmp-dev=2:6.2.1+dfsg-1 libgmp10=2:6.2.1+dfsg-1 libgmp3-dev=2:6.2.1+dfsg-1 libgmpxx4ldbl=2:6.2.1+dfsg-1 libgnutls30=3.7.0-5 libgomp1=10.2.1-6 libgpg-error0=1.38-2 libgraphite2-3=1.3.14-1 libgraphite2-dev=1.3.14-1 libgssapi-krb5-2=1.18.3-4 libgtk-3-0=3.24.24-1 libgtk-3-common=3.24.24-1 libgtk-3-dev=3.24.24-1 libgtksourceview-3.0-1=3.24.11-2 libgtksourceview-3.0-common=3.24.11-2 libgtksourceview-3.0-dev=3.24.11-2 libharfbuzz-dev=2.7.4-1 libharfbuzz-gobject0=2.7.4-1 libharfbuzz-icu0=2.7.4-1 libharfbuzz0b=2.7.4-1 libhogweed6=3.6-2 libice-dev=2:1.0.10-1 libice6=2:1.0.10-1 libicu-dev=67.1-6 libicu67=67.1-6 libidn2-0=2.3.0-5 libip4tc2=1.8.7-1 libisl23=0.23-1 libitm1=10.2.1-6 libjbig0=2.1-3.1+b2 libjpeg62-turbo=1:2.0.5-2 libjson-c5=0.15-1 libjson-glib-1.0-0=1.6.0-2 libjson-glib-1.0-common=1.6.0-2 libk5crypto3=1.18.3-4 libkeyutils1=1.6.1-2 libkmod2=28-1 libkrb5-3=1.18.3-4 libkrb5support0=1.18.3-4 liblablgtk3-ocaml=3.1.1+official-1+b1 liblablgtk3-ocaml-dev=3.1.1+official-1+b1 liblablgtksourceview3-ocaml=3.1.1+official-1+b1 liblablgtksourceview3-ocaml-dev=3.1.1+official-1+b1 liblcms2-2=2.12~rc1-2 libllvm11=1:11.0.1-2 liblsan0=10.2.1-6 liblz4-1=1.9.3-1 liblzma5=5.2.5-1.0 liblzo2-2=2.10-2 libmagic-mgc=1:5.39-3 libmagic1=1:5.39-3 libmenhir-ocaml-dev=20201216-1 libmount-dev=2.36.1-6 libmount1=2.36.1-6 libmpc3=1.2.0-1 libmpdec3=2.5.1~rc1-2 libmpfr6=4.1.0-3 libncurses-dev=6.2+20201114-2 libncurses5-dev=6.2+20201114-2 libncurses6=6.2+20201114-2 libncursesw6=6.2+20201114-2 libnettle8=3.6-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libnum-ocaml=1.4-1 libnum-ocaml-dev=1.4-1 libocamlgraph-ocaml-dev=1.8.8-1.1+b2 libopengl-dev=1.3.2-1 libopengl0=1.3.2-1 libp11-kit0=0.23.22-1 libpam-modules=1.4.0-2 libpam-modules-bin=1.4.0-2 libpam-runtime=1.4.0-2 libpam-systemd=247.2-5 libpam0g=1.4.0-2 libpango-1.0-0=1.46.2-3 libpango1.0-dev=1.46.2-3 libpangocairo-1.0-0=1.46.2-3 libpangoft2-1.0-0=1.46.2-3 libpangoxft-1.0-0=1.46.2-3 libpciaccess0=0.16-1 libpcre16-3=2:8.39-13 libpcre2-16-0=10.36-2 libpcre2-32-0=10.36-2 libpcre2-8-0=10.36-2 libpcre2-dev=10.36-2 libpcre2-posix2=10.36-2 libpcre3=2:8.39-13 libpcre3-dev=2:8.39-13 libpcre32-3=2:8.39-13 libpcrecpp0v5=2:8.39-13 libperl5.32=5.32.0-6 libpipeline1=1.5.3-1 libpixman-1-0=0.40.0-1 libpixman-1-dev=0.40.0-1 libpng-dev=1.6.37-3 libpng16-16=1.6.37-3 libproxy1v5=0.4.17-1 libpsl5=0.21.0-1.1 libpthread-stubs0-dev=0.4-1 libpython3-stdlib=3.9.1-1 libpython3.9-minimal=3.9.1-3 libpython3.9-stdlib=3.9.1-3 libquadmath0=10.2.1-6 libreadline8=8.1-1 librest-0.7-0=0.8.1-1.1 libseccomp2=2.5.1-1 libselinux1=3.1-2+b2 libselinux1-dev=3.1-2+b2 libsemanage-common=3.1-1 libsemanage1=3.1-1+b2 libsensors-config=1:3.6.0-5 libsensors5=1:3.6.0-5 libsepol1=3.1-1 libsepol1-dev=3.1-1 libsigsegv2=2.12-3 libsm-dev=2:1.2.3-1 libsm6=2:1.2.3-1 libsmartcols1=2.36.1-6 libsoup-gnome2.4-1=2.72.0-2 libsoup2.4-1=2.72.0-2 libsqlite3-0=3.34.1-1 libsqlite3-dev=3.34.1-1 libsqlite3-ocaml=5.0.2-1+b1 libsqlite3-ocaml-dev=5.0.2-1+b1 libssl1.1=1.1.1i-2 libstdc++-10-dev=10.2.1-6 libstdc++6=10.2.1-6 libsub-override-perl=0.09-2 libsystemd0=247.2-5 libtasn1-6=4.16.0-2 libthai-data=0.1.28-3 libthai-dev=0.1.28-3 libthai0=0.1.28-3 libtiff5=4.2.0-1 libtinfo6=6.2+20201114-2 libtirpc-common=1.3.1-1 libtirpc-dev=1.3.1-1 libtirpc3=1.3.1-1 libtool=2.4.6-15 libtsan0=10.2.1-6 libubsan1=10.2.1-6 libuchardet0=0.0.7-1 libudev1=247.2-5 libunistring2=0.9.10-4 libuuid1=2.36.1-6 libvulkan1=1.2.162.0-1 libwayland-bin=1.18.0-2~exp1.1 libwayland-client0=1.18.0-2~exp1.1 libwayland-cursor0=1.18.0-2~exp1.1 libwayland-dev=1.18.0-2~exp1.1 libwayland-egl1=1.18.0-2~exp1.1 libwayland-server0=1.18.0-2~exp1.1 libwebp6=0.6.1-2+b1 libx11-6=2:1.7.0-2 libx11-data=2:1.7.0-2 libx11-dev=2:1.7.0-2 libx11-xcb1=2:1.7.0-2 libxau-dev=1:1.0.8-1+b2 libxau6=1:1.0.8-1+b2 libxcb-dri2-0=1.14-2.1 libxcb-dri3-0=1.14-2.1 libxcb-glx0=1.14-2.1 libxcb-present0=1.14-2.1 libxcb-render0=1.14-2.1 libxcb-render0-dev=1.14-2.1 libxcb-shm0=1.14-2.1 libxcb-shm0-dev=1.14-2.1 libxcb-sync1=1.14-2.1 libxcb-xfixes0=1.14-2.1 libxcb1=1.14-2.1 libxcb1-dev=1.14-2.1 libxcomposite-dev=1:0.4.5-1 libxcomposite1=1:0.4.5-1 libxcursor-dev=1:1.2.0-2 libxcursor1=1:1.2.0-2 libxdamage-dev=1:1.1.5-2 libxdamage1=1:1.1.5-2 libxdmcp-dev=1:1.1.2-3 libxdmcp6=1:1.1.2-3 libxext-dev=2:1.3.3-1.1 libxext6=2:1.3.3-1.1 libxfixes-dev=1:5.0.3-2 libxfixes3=1:5.0.3-2 libxft-dev=2.3.2-2 libxft2=2.3.2-2 libxi-dev=2:1.7.10-1 libxi6=2:1.7.10-1 libxinerama-dev=2:1.1.4-2 libxinerama1=2:1.1.4-2 libxkbcommon-dev=1.0.3-2 libxkbcommon0=1.0.3-2 libxml2=2.9.10+dfsg-6.3+b1 libxml2-dev=2.9.10+dfsg-6.3+b1 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.9-1 libzarith-ocaml=1.11-1 libzarith-ocaml-dev=1.11-1 libzip-ocaml=1.10-1+b1 libzip-ocaml-dev=1.10-1+b1 libzstd1=1.4.8+dfsg-1 linux-libc-dev=5.10.5-1 login=1:4.8.1-1 lsb-base=11.1.0 m4=1.4.18-5 mailcap=3.68 make=4.3-4 man-db=2.9.3-2 mawk=1.3.4.20200120-2 media-types=4.0.0 menhir=20201216-1 mime-support=3.66 mount=2.36.1-6 ncurses-base=6.2+20201114-2 ncurses-bin=6.2+20201114-2 ocaml-base-nox=4.11.1-4 ocaml-compiler-libs=4.11.1-4 ocaml-findlib=1.8.1-2 ocaml-interp=4.11.1-4 ocaml-nox=4.11.1-4 pango1.0-tools=1.46.2-3 passwd=1:4.8.1-1 patch=2.7.6-7 perl=5.32.0-6 perl-base=5.32.0-6 perl-modules-5.32=5.32.0-6 pkg-config=0.29.2-1 po-debconf=1.0.21+nmu1 python3=3.9.1-1 python3-distutils=3.9.1-2 python3-lib2to3=3.9.1-2 python3-minimal=3.9.1-1 python3.9=3.9.1-3 python3.9-minimal=3.9.1-3 readline-common=8.1-1 sed=4.7-1 sensible-utils=0.0.14 shared-mime-info=2.0-1 systemd=247.2-5 systemd-sysv=247.2-5 systemd-timesyncd=247.2-5 sysvinit-utils=2.96-5 tar=1.32+dfsg-1 tex-common=6.15 tzdata=2020f-1 ucf=3.0043 util-linux=2.36.1-6 uuid-dev=2.36.1-6 wayland-protocols=1.20-1 x11-common=1:7.7+21 x11proto-core-dev=2020.1-1 x11proto-dev=2020.1-1 x11proto-input-dev=2020.1-1 x11proto-randr-dev=2020.1-1 x11proto-record-dev=2020.1-1 x11proto-xext-dev=2020.1-1 x11proto-xinerama-dev=2020.1-1 xkb-data=2.29-2 xorg-sgml-doctools=1:1.11-1.1 xtrans-dev=1.4.0-1 xz-utils=5.2.5-1.0 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/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20210121T144334Z/ 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 why3=1.3.3-1 && mkdir -p /build/why3-GGVL5z && dpkg-source --no-check -x /*.dsc /build/why3-GGVL5z/why3-1.3.3 && cd /build/why3-GGVL5z/why3-1.3.3 && { printf '%s' 'why3 (1.3.3-1+b4) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuilt with menhir 20201216-1 -- amd64 / i386 Build Daemon (x86-ubc-01) Sat, 23 Jan 2021 17:30:05 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/why3-GGVL5z" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/why3-GGVL5z/why3-1.3.3 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1611423005" dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/why3-GGVL5z /tmp/why3-1.3.3-1+b40nz0l5bo bullseye /dev/null deb http://snapshot.notset.fr/archive/debian/20210121T144334Z 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.lXjGN1XehT 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.lXjGN1XehT Reading package lists... Building dependency tree... util-linux is already the newest version (2.36.1-6). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 134 kB of archives. After this operation, 397 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20210121T144334Z unstable/main amd64 libfakeroot amd64 1.25.3-1.1 [47.0 kB] Get:2 http://snapshot.notset.fr/archive/debian/20210121T144334Z unstable/main amd64 fakeroot amd64 1.25.3-1.1 [87.0 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 134 kB in 0s (1116 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 ... 4661 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.25.3-1.1_amd64.deb ... Unpacking libfakeroot:amd64 (1.25.3-1.1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.25.3-1.1_amd64.deb ... Unpacking fakeroot (1.25.3-1.1) ... Setting up libfakeroot:amd64 (1.25.3-1.1) ... Setting up fakeroot (1.25.3-1.1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.31-9) ... 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/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20210121T144334Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.lXjGN1XehT Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm InRelease [81.6 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20210121T144334Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources [11.4 MB] Get:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages [11.1 MB] Fetched 22.6 MB in 20s (1142 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.lXjGN1XehT I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d why3=1.3.3-1 && mkdir -p /build/why3-GGVL5z && dpkg-source --no-check -x /*.dsc /build/why3-GGVL5z/why3-1.3.3 && cd /build/why3-GGVL5z/why3-1.3.3 && { printf '%s' 'why3 (1.3.3-1+b4) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuilt with menhir 20201216-1 -- amd64 / i386 Build Daemon (x86-ubc-01) Sat, 23 Jan 2021 17:30:05 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/why3-GGVL5z"' exec /tmp/mmdebstrap.lXjGN1XehT Reading package lists... NOTICE: 'why3' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/why3.git Please use: git clone https://salsa.debian.org/ocaml-team/why3.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 5829 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main why3 1.3.3-1 (dsc) [2839 B] Get:2 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main why3 1.3.3-1 (tar) [5808 kB] Get:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main why3 1.3.3-1 (diff) [18.4 kB] Fetched 5829 kB in 5s (1207 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'why3_1.3.3-1.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting why3 in /build/why3-GGVL5z/why3-1.3.3 dpkg-source: info: unpacking why3_1.3.3.orig.tar.gz dpkg-source: info: unpacking why3_1.3.3-1.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying hardening-flags I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/why3-GGVL5z/why3-1.3.3 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1611423005" dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.lXjGN1XehT dpkg-buildpackage: info: source package why3 dpkg-buildpackage: info: source version 1.3.3-1+b4 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by amd64 / i386 Build Daemon (x86-ubc-01) dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with ocaml,tex dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with ocaml,tex dh_update_autotools_config -a dh_autoreconf -a aclocal: warning: autoconf input should be named 'configure.ac', not 'configure.in' dh_ocamlinit -a debian/rules override_dh_auto_configure make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' autoconf dh_auto_configure -- \ --disable-emacs-compilation \ --libdir=/usr/lib/ocaml ./configure --build=x86_64-linux-gnu --prefix=/usr --includedir=\${prefix}/include --mandir=\${prefix}/share/man --infodir=\${prefix}/share/info --sysconfdir=/etc --localstatedir=/var --disable-option-checking --disable-silent-rules --libdir=\${prefix}/lib/x86_64-linux-gnu --runstatedir=/run --disable-maintainer-mode --disable-dependency-tracking --disable-emacs-compilation --libdir=/usr/lib/ocaml checking executable suffix... checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking for gcc option to accept ISO C99... none needed checking for gcc option to accept ISO Standard C... (cached) none needed checking for a thread-safe mkdir -p... /bin/mkdir -p checking for a BSD-compatible install... /usr/bin/install -c checking for ocamlc... ocamlc ocaml version is 4.11.1 ocaml library path is /usr/lib/ocaml checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt checking for menhir... menhir checking for ocamlfind... ocamlfind ocamlfind found compiler-libs in /usr/lib/ocaml/compiler-libs checking for sphinx-build... no configure: WARNING: Cannot find sphinx-build, Documentation disabled. ocamlfind found num in /usr/lib/ocaml/num checking for /usr/lib/ocaml/num/nums.cma... no checking for /usr/lib/ocaml/num/num.cmi... no checking for /usr/lib/ocaml/nums.cma... yes checking for /usr/lib/ocaml/num.cmi... yes ocamlfind found zarith in /usr/lib/ocaml/zarith checking for /usr/lib/ocaml/zarith/z.cmi... yes ocamlfind found camlzip in /usr/lib/ocaml/zip checking for /usr/lib/ocaml/zip/zip.cmi... yes ocamlfind found menhirLib in /usr/lib/ocaml/menhirLib checking for /usr/lib/ocaml/menhirLib/menhirLib.cmi... yes ocamlfind found seq in /usr/lib/ocaml/seq checking for /usr/lib/ocaml/seq/seq.cma... no checking for /usr/lib/ocaml/seq/seq.cmi... no checking for /usr/lib/ocaml/stdlib__seq.cmi... yes ocamlfind: Package `re' not found checking for /usr/lib/ocaml/re/re.cmx... no checking for /usr/lib/ocaml/re/re.cmi... no configure: WARNING: Library re not found. ocamlfind found lablgtk3 in /usr/lib/ocaml/lablgtk3 checking for /usr/lib/ocaml/lablgtk3/lablgtk.cma... no checking for /usr/lib/ocaml/lablgtk3/lablgtk3.cma... yes checking for /usr/lib/ocaml/lablgtk3/gtkButton.cmi... yes ocamlfind found lablgtk3-sourceview3 in /usr/lib/ocaml/lablgtk3-sourceview3 checking for /usr/lib/ocaml/lablgtk3-sourceview3/gSourceView3.cmi... yes ocamlfind: Package `js_of_ocaml' not found ocamlfind: Package `mlmpfr' not found checking for coqc... coqc checking Coq version... 8.12.0 checking for coqdep... coqdep checking for Flocq... File "./conftest.v", line 1, characters 15-28: Error: Cannot find a physical path bound to logical path matching suffix Flocq. no configure: WARNING: Cannot find Flocq. checking for pvs... no configure: WARNING: Cannot find pvs. checking for isabelle... no configure: WARNING: Cannot find isabelle. configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating lib/why3/META config.status: creating .merlin config.status: creating src/jessie/Makefile config.status: creating src/jessie/.merlin config.status: creating lib/coq/version config.status: creating lib/pvs/version config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.11.1 Library path : /usr/lib/ocaml Ocamlfind : yes Native compilation : yes Profiling : no Memory profiling : no (disabled by default) PPX : yes Javascript support : no (js_of_ocaml not found) Mpfr support : no (mlmpfr not found) Re support : no Components Why3 library : yes GTK IDE : yes (gtk3) Web IDE : no (Javascript support not available) GMP arithmetic : yes Compressed sessions : yes Hypothesis selection : no (broken) Frama-C support : no (disabled by default) Documentation : no (sphinx-build not found) Support for interactive proof assistants Coq : yes Version : 8.12.0 Library path : /usr/lib/coq Realization support : yes FP arithmetic : no (Flocq >= 3.1 not found) PVS : no (pvs not found) Isabelle : no (isabelle not found) Installable : yes Binary path : ${exec_prefix}/bin Library path : /usr/lib/ocaml/why3 Data path : ${prefix}/share/why3 OCaml library path : /usr/local/lib/ocaml/4.11.1/why3 Relocatable : no make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' debian/rules override_dh_auto_build-arch make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' /usr/bin/make all byte make[2]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' Ocamllex src/why3doc/doc_lexer.mll 125 states, 1119 transitions, table size 5226 bytes 1793 additional bytes used for bindings Ocamldep src/why3doc/doc_main.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/why3doc/doc_def.ml Ocamldep src/why3doc/doc_html.ml Ocamldep src/tools/why3pp.ml Ocamldep src/isabelle-client/isabelle_client_main.ml Coqdep lib/coq/for_drivers/ComputerOfEuclideanDivision.v Coqdep lib/coq/bv/BV_Gen.v Coqdep lib/coq/bv/Pow2int.v Coqdep lib/coq/option/Option.v Coqdep lib/coq/list/Permut.v Coqdep lib/coq/list/NumOcc.v Coqdep lib/coq/list/Distinct.v Coqdep lib/coq/list/Combine.v Coqdep lib/coq/list/RevAppend.v Coqdep lib/coq/list/NthNoOpt.v Coqdep lib/coq/list/HdTlNoOpt.v Coqdep lib/coq/list/Reverse.v Coqdep lib/coq/list/NthLengthAppend.v Coqdep lib/coq/list/Append.v Coqdep lib/coq/list/NthHdTl.v Coqdep lib/coq/list/HdTl.v Coqdep lib/coq/list/NthLength.v Coqdep lib/coq/list/Nth.v Coqdep lib/coq/list/Mem.v Coqdep lib/coq/list/Length.v Coqdep lib/coq/list/List.v Coqdep lib/coq/map/MapInjection.v Coqdep lib/coq/map/MapPermut.v Coqdep lib/coq/map/Occ.v Coqdep lib/coq/map/Const.v Coqdep lib/coq/map/Map.v Coqdep lib/coq/set/SetImpInt.v Coqdep lib/coq/set/SetImp.v Coqdep lib/coq/set/SetAppInt.v Coqdep lib/coq/set/SetApp.v Coqdep lib/coq/set/FsetSum.v Coqdep lib/coq/set/FsetInt.v Coqdep lib/coq/set/FsetInduction.v Coqdep lib/coq/set/Fset.v Coqdep lib/coq/set/Cardinal.v Coqdep lib/coq/set/Set.v Coqdep lib/coq/number/Coprime.v Coqdep lib/coq/number/Prime.v Coqdep lib/coq/number/Parity.v Coqdep lib/coq/number/Gcd.v Coqdep lib/coq/number/Divisibility.v Coqdep lib/coq/real/Trigonometry.v Coqdep lib/coq/real/Square.v Coqdep lib/coq/real/RealInfix.v Coqdep lib/coq/real/Real.v Coqdep lib/coq/real/PowerReal.v Coqdep lib/coq/real/PowerInt.v Coqdep lib/coq/real/MinMax.v Coqdep lib/coq/real/FromInt.v Coqdep lib/coq/real/ExpLog.v Coqdep lib/coq/real/Abs.v Coqdep lib/coq/bool/Bool.v Coqdep lib/coq/int/NumOf.v Coqdep lib/coq/int/Power.v Coqdep lib/coq/int/MinMax.v Coqdep lib/coq/int/Int.v Coqdep lib/coq/int/EuclideanDivision.v Coqdep lib/coq/int/Div2.v Coqdep lib/coq/int/ComputerDivision.v Coqdep lib/coq/int/Abs.v Coqdep lib/coq/int/Exponentiation.v Coqdep lib/coq/HighOrd.v Coqdep lib/coq/BuiltIn.v Ocamldep src/tools/why3shell.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/why3session/why3session_update.ml Ocamldep src/why3session/why3session_latex.ml Ocamldep src/why3session/why3session_html.ml Ocamldep src/why3session/why3session_info.ml Ocamldep src/why3session/why3session_lib.ml Ocamldep src/ide/why3web.ml Ocamldep src/ide/wserver.ml cp src/ide/gtkcompat3.ml src/ide/gtkcompat.ml Ocamldep src/ide/why3ide.ml Ocamldep src/ide/ide_utils.ml Ocamldep src/ide/gconfig.ml Ocamldep src/ide/gtkcompat.ml Ocamllex src/tools/why3wc.mll 307 states, 15627 transitions, table size 64350 bytes Ocamldep src/tools/why3wc.ml Ocamldep src/tools/why3replay.ml Ocamldep src/tools/why3realize.ml Ocamldep src/tools/why3prove.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3config.ml Ocamldep src/tools/main.ml Ocamllex plugins/tptp/tptp_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Menhir plugins/tptp/tptp_parser.mly Ocamllex plugins/python/py_lexer.mll 56 states, 651 transitions, table size 2940 bytes 1375 additional bytes used for bindings Menhir plugins/python/py_parser.mly Ocamllex plugins/microc/mc_lexer.mll 77 states, 473 transitions, table size 2354 bytes 1504 additional bytes used for bindings Menhir plugins/microc/mc_parser.mly Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings Ocamldep plugins/microc/mc_main.ml Ocamldep plugins/microc/mc_printer.ml Ocamldep plugins/microc/mc_lexer.ml Ocamldep plugins/microc/mc_parser.ml Ocamldep plugins/microc/mc_ast.ml Ocamldep plugins/python/py_main.ml Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/python/py_ast.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_ast.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/parser/genequlin.ml Generate src/util/config.ml Ocamllex src/util/rc.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Ocamllex src/util/lexlib.mll 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings Menhir src/util/json_parser.mly Ocamllex src/util/json_lexer.mll 52 states, 495 transitions, table size 2292 bytes cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml Ocamllex src/parser/lexer.mll 155 states, 4342 transitions, table size 18298 bytes 7537 additional bytes used for bindings Menhir src/parser/parser.mly rm -f src/parser/parser_messages.ml src/parser/parser_messages.ml.tmp menhir --explain --strict src/parser/parser.mly --update-errors \ src/parser/handcrafted.messages > src/parser/handcrafted.messages.temp Read 1 sample input sentences and 1 error messages. diff -b src/parser/handcrafted.messages src/parser/handcrafted.messages.temp > /dev/null; \ RET_CODE=$?; \ if [ $RET_CODE -ne 0 ]; then \ echo "Parsing error handling must be updated, the file 'src/parser/handcrafted.messages.temp' \ contains an updated version that must be checked before replacing 'src/parser/handcrafted.messages'"; \ exit 1; \ fi rm -f src/parser/handcrafted.messages.temp menhir --explain --strict src/parser/parser.mly --compile-errors \ src/parser/handcrafted.messages > src/parser/parser_messages.ml.tmp Read 1 sample input sentences and 1 error messages. mv src/parser/parser_messages.ml.tmp src/parser/parser_messages.ml Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 34 states, 1366 transitions, table size 5668 bytes Menhir src/driver/parse_smtv2_model_parser.mly Ocamllex src/driver/parse_smtv2_model_lexer.mll 266 states, 3281 transitions, table size 14720 bytes 3869 additional bytes used for bindings cp src/session/compress_z.ml src/session/compress.ml Ocamllex src/session/xml.mll 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings Ocamllex src/session/strategy_parser.mll 43 states, 639 transitions, table size 2814 bytes 1799 additional bytes used for bindings cp src/util/recompat.ml src/util/re.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/session/json_util.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/strategy.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.ml Ocamldep src/session/compress.ml Ocamldep src/printer/mathematica.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/smtv1.ml Ocamldep src/printer/why3printer.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/printer/cntexmp_printer.ml Ocamldep src/transform/reflection.ml Ocamldep src/transform/matching.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/intro_vc_vars_counterexmp.ml Ocamldep src/transform/congruence.ml Ocamldep src/transform/cut.ml Ocamldep src/transform/destruct.ml Ocamldep src/transform/ind_itp.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/subst.ml Ocamldep src/transform/apply.ml Ocamldep src/transform/case.ml Ocamldep src/transform/generic_arg_trans_utils.ml Ocamldep src/transform/eliminate_literal.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/abstract_quantifiers.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/report.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree.ml Ocamldep src/extract/cakeml.ml Ocamldep src/extract/ocaml.ml Ocamldep src/extract/c.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/extract/pdriver.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/extract/compile.ml Ocamldep src/extract/mltree.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/mlw/big_real.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/mlw/vc.ml Ocamldep src/mlw/typeinv.ml Ocamldep src/mlw/eval_match.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/ity.ml Ocamldep src/driver/parse_smtv2_model.ml Ocamldep src/driver/parse_smtv2_model_lexer.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/driver/parse_smtv2_model_parser.ml Ocamldep src/driver/smt2_model_defs.ml Ocamldep src/driver/autodetection.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/driver/driver_ast.ml Ocamldep src/driver/call_provers.ml Ocamldep src/driver/prove_client.ml Ocamldep src/core/model_parser.ml Ocamldep src/core/printer.ml Ocamldep src/core/trans.ml Ocamldep src/core/env.ml Ocamldep src/core/dterm.ml Ocamldep src/core/pretty.ml Ocamldep src/core/task.ml Ocamldep src/core/theory.ml Ocamldep src/core/coercion.ml Ocamldep src/core/decl.ml Ocamldep src/core/pattern.ml Ocamldep src/core/term.ml Ocamldep src/core/ty.ml Ocamldep src/core/ident.ml Ocamldep src/util/re.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/vector.ml Ocamldep src/util/constant.ml Ocamldep src/util/number.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/plugin.ml Ocamldep src/util/rc.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/warning.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/loc.ml Ocamldep src/util/debug.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_base.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/extset.ml Ocamldep src/util/extmap.ml Ocamldep src/util/pp.ml Ocamldep src/util/strings.ml Ocamldep src/util/lists.ml Ocamldep src/util/opt.ml Ocamldep src/util/util.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/config.ml mkdir lib/plugins Ocamlc src/util/config.ml Ocamlopt src/util/config.ml Ocamlc src/util/bigInt.mli Ocamlopt src/util/bigInt.ml Ocamlc src/util/mlmpfr_wrapper.mli Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlc src/util/util.mli Ocamlopt src/util/util.ml Ocamlc src/util/opt.mli Ocamlopt src/util/opt.ml Ocamlc src/util/lists.mli Ocamlopt src/util/lists.ml Ocamlc src/util/strings.mli Ocamlopt src/util/strings.ml Ocamlc src/util/pp.mli File "src/util/pp.mli", line 121, characters 33-51: 121 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ 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 File "src/util/pp.mli", line 124, characters 33-51: 124 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ 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 Ocamlopt src/util/pp.ml Ocamlc src/util/extmap.mli Ocamlopt src/util/extmap.ml Ocamlc src/util/extset.mli Ocamlopt src/util/extset.ml Ocamlc src/util/exthtbl.mli Ocamlopt src/util/exthtbl.ml Ocamlc src/util/weakhtbl.mli Ocamlopt src/util/weakhtbl.ml Ocamlc src/util/diffmap.mli Ocamlopt src/util/diffmap.ml Ocamlc src/util/hashcons.mli Ocamlopt src/util/hashcons.ml Ocamlc src/util/wstdlib.mli Ocamlopt src/util/wstdlib.ml Ocamlc src/util/exn_printer.mli Ocamlopt src/util/exn_printer.ml Ocamlc src/util/json_base.mli Ocamlopt src/util/json_base.ml Ocamlc src/util/json_parser.mli Ocamlopt src/util/json_parser.ml Ocamlc src/util/json_lexer.ml Ocamlopt src/util/json_lexer.ml Ocamlc src/util/debug.mli Ocamlopt src/util/debug.ml Ocamlc src/util/loc.mli Ocamlopt src/util/loc.ml File "src/util/loc.ml", line 67, characters 14-32: 67 | let 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 File "src/util/loc.ml", line 68, characters 12-26: 68 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ 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 Ocamlc src/util/lexlib.mli Ocamlopt src/util/lexlib.ml Ocamlc src/util/print_tree.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/cmdline.mli Ocamlopt src/util/cmdline.ml Ocamlc src/util/warning.mli Ocamlopt src/util/warning.ml Ocamlc src/util/sysutil.mli Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli Ocamlopt src/util/rc.ml Ocamlc src/util/plugin.mli Ocamlopt src/util/plugin.ml Ocamlc src/util/number.mli Ocamlopt src/util/number.ml Ocamlc src/util/constant.mli Ocamlopt src/util/constant.ml File "src/util/constant.ml", line 24, characters 14-32: 24 | let c = Pervasives.compare k1 k2 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 File "src/util/constant.ml", line 27, characters 14-32: 27 | let c = Pervasives.compare k1 k2 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 File "src/util/constant.ml", line 30, characters 6-24: 30 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ 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 Ocamlc src/util/vector.mli Ocamlopt src/util/vector.ml Ocamlc src/util/pqueue.mli Ocamlopt src/util/pqueue.ml Ocamlc src/util/re.ml Ocamlopt src/util/re.ml Ocamlc src/core/ident.mli Ocamlopt src/core/ident.ml Ocamlc src/core/ty.mli Ocamlopt src/core/ty.ml Ocamlc src/core/term.mli Ocamlopt src/core/term.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) 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 Ocamlc src/core/pattern.mli Ocamlopt src/core/pattern.ml Ocamlc src/core/decl.mli Ocamlopt src/core/decl.ml Ocamlc src/core/coercion.mli Ocamlopt src/core/coercion.ml Ocamlc src/core/theory.mli Ocamlopt src/core/theory.ml Ocamlc src/core/task.mli Ocamlopt src/core/task.ml Ocamlc src/core/pretty.mli Ocamlopt src/core/pretty.ml Ocamlc src/core/dterm.mli Ocamlopt src/core/dterm.ml Ocamlc src/core/env.mli Ocamlopt src/core/env.ml Ocamlc src/core/trans.mli Ocamlopt src/core/trans.ml Ocamlc src/core/printer.mli Ocamlopt src/core/printer.ml Ocamlc src/core/model_parser.mli Ocamlopt src/core/model_parser.ml Ocamlc src/driver/prove_client.mli Ocamlopt src/driver/prove_client.ml Ocamlc src/driver/call_provers.mli Ocamlopt src/driver/call_provers.ml Ocamlc src/driver/driver_ast.ml Ocamlopt src/driver/driver_ast.ml Ocamlc src/driver/driver_parser.mli Ocamlopt src/driver/driver_parser.ml Ocamlc src/driver/driver_lexer.mli Ocamlopt src/driver/driver_lexer.ml Ocamlc src/driver/driver.mli Ocamlopt src/driver/driver.ml Ocamlc src/driver/whyconf.mli Ocamlopt src/driver/whyconf.ml Ocamlc src/driver/autodetection.mli Ocamlopt src/driver/autodetection.ml Ocamlc src/driver/smt2_model_defs.mli Ocamlopt src/driver/smt2_model_defs.ml Ocamlc src/driver/parse_smtv2_model_parser.mli Ocamlopt src/driver/parse_smtv2_model_parser.ml Ocamlc src/driver/collect_data_model.mli Ocamlopt src/driver/collect_data_model.ml Ocamlc src/driver/parse_smtv2_model_lexer.ml Ocamlopt src/driver/parse_smtv2_model_lexer.ml Ocamlc src/driver/parse_smtv2_model.ml Ocamlopt src/driver/parse_smtv2_model.ml Ocamlc src/mlw/ity.mli Ocamlopt src/mlw/ity.ml Ocamlc src/mlw/expr.mli Ocamlopt src/mlw/expr.ml Ocamlc src/mlw/pdecl.mli Ocamlopt src/mlw/pdecl.ml Ocamlc src/mlw/eval_match.mli Ocamlopt src/mlw/eval_match.ml Ocamlc src/mlw/typeinv.mli Ocamlopt src/mlw/typeinv.ml Ocamlc src/mlw/vc.mli Ocamlopt src/mlw/vc.ml Ocamlc src/mlw/pmodule.mli Ocamlopt src/mlw/pmodule.ml Ocamlc src/mlw/dexpr.mli Ocamlopt src/mlw/dexpr.ml Ocamlc src/mlw/big_real.mli Ocamlopt src/mlw/big_real.ml Ocamlc src/mlw/pinterp.mli Ocamlopt src/mlw/pinterp.ml Ocamlc src/extract/mltree.ml Ocamlopt src/extract/mltree.ml Ocamlc src/extract/compile.mli Ocamlopt src/extract/compile.ml Linking src/util/ppx_debug_optim findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/lib/ocaml, /usr/lib/ocaml/compiler-libs Ocamlc src/extract/mlinterp.mli Ocamlopt src/extract/mlinterp.ml Ocamlc src/extract/pdriver.mli Ocamlopt src/extract/pdriver.ml Ocamlc src/extract/ml_printer.mli Ocamlopt src/extract/ml_printer.ml Ocamlc src/extract/c.ml Ocamlopt src/extract/c.ml Ocamlc src/extract/ocaml.ml Ocamlopt src/extract/ocaml.ml Ocamlc src/extract/cakeml.ml Ocamlopt src/extract/cakeml.ml Ocamlc src/parser/ptree.ml Ocamlopt src/parser/ptree.ml Ocamlc src/parser/glob.mli Ocamlopt src/parser/glob.ml Ocamlc src/parser/typing.mli Ocamlopt src/parser/typing.ml Ocamlc src/parser/parser_messages.ml Ocamlopt src/parser/parser_messages.ml Ocamlc src/parser/parser.mli Ocamlopt src/parser/parser.ml Ocamlc src/parser/report.mli Ocamlopt src/parser/report.ml Ocamlc src/parser/lexer.mli Ocamlopt src/parser/lexer.ml Ocamlc src/parser/mlw_printer.mli Ocamlopt src/parser/mlw_printer.ml Ocamlc src/transform/simplify_formula.mli Ocamlopt src/transform/simplify_formula.ml Ocamlc src/transform/inlining.mli Ocamlopt src/transform/inlining.ml Ocamlc src/transform/split_goal.mli Ocamlopt src/transform/split_goal.ml Ocamlc src/transform/args_wrapper.mli Ocamlopt src/transform/args_wrapper.ml Ocamlc src/transform/detect_polymorphism.mli Ocamlopt src/transform/detect_polymorphism.ml Ocamlc src/transform/reduction_engine.mli Ocamlopt src/transform/reduction_engine.ml Ocamlc src/transform/compute.mli Ocamlopt src/transform/compute.ml Ocamlc src/transform/eliminate_definition.mli Ocamlopt src/transform/eliminate_definition.ml Ocamlc src/transform/eliminate_algebraic.mli Ocamlopt src/transform/eliminate_algebraic.ml Ocamlc src/transform/abstract_quantifiers.ml Ocamlopt src/transform/abstract_quantifiers.ml Ocamlc src/transform/eliminate_unknown_types.ml Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlc src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlc src/transform/eliminate_symbol.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlc src/transform/eliminate_inductive.mli Ocamlopt src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.mli Ocamlopt src/transform/eliminate_let.ml Ocamlc src/transform/eliminate_if.mli Ocamlopt src/transform/eliminate_if.ml Ocamlc src/transform/libencoding.mli Ocamlopt src/transform/libencoding.ml Ocamlc src/transform/discriminate.mli Ocamlopt src/transform/discriminate.ml Ocamlc src/transform/encoding.mli Ocamlopt src/transform/encoding.ml Ocamlc src/transform/encoding_select.mli Ocamlopt src/transform/encoding_select.ml Ocamlc src/transform/encoding_guards_full.mli Ocamlopt src/transform/encoding_guards_full.ml Ocamlc src/transform/encoding_tags_full.mli Ocamlopt src/transform/encoding_tags_full.ml Ocamlc src/transform/encoding_guards.mli Ocamlopt src/transform/encoding_guards.ml Ocamlc src/transform/encoding_tags.mli Ocamlopt src/transform/encoding_tags.ml Ocamlc src/transform/encoding_twin.mli Ocamlopt src/transform/encoding_twin.ml Ocamlc src/transform/encoding_sort.mli Ocamlopt src/transform/encoding_sort.ml Ocamlc src/transform/simplify_array.mli Ocamlopt src/transform/simplify_array.ml Ocamlc src/transform/filter_trigger.mli Ocamlopt src/transform/filter_trigger.ml Ocamlc src/transform/abstraction.mli Ocamlopt src/transform/abstraction.ml Ocamlc src/transform/close_epsilon.mli Ocamlopt src/transform/close_epsilon.ml Ocamlc src/transform/lift_epsilon.mli Ocamlopt src/transform/lift_epsilon.ml Ocamlc src/transform/eliminate_epsilon.mli Ocamlopt src/transform/eliminate_epsilon.ml Ocamlc src/transform/intro_projections_counterexmp.mli Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/instantiate_predicate.mli Ocamlopt src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.mli Ocamlopt src/transform/smoke_detector.ml Ocamlc src/transform/prop_curry.ml Ocamlopt src/transform/prop_curry.ml Ocamlc src/transform/eliminate_literal.mli Ocamlopt src/transform/eliminate_literal.ml Ocamlc src/transform/generic_arg_trans_utils.mli Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/case.ml Ocamlopt src/transform/case.ml Ocamlc src/transform/apply.mli Ocamlopt src/transform/apply.ml Ocamlc src/transform/subst.mli Ocamlopt src/transform/subst.ml Ocamlc src/transform/introduction.mli Ocamlopt src/transform/introduction.ml Ocamlc src/transform/ind_itp.mli Ocamlopt src/transform/ind_itp.ml Ocamlc src/transform/destruct.mli Ocamlopt src/transform/destruct.ml Ocamlc src/transform/cut.ml Ocamlopt src/transform/cut.ml Ocamlc src/transform/congruence.ml Ocamlopt src/transform/congruence.ml Ocamlc src/transform/intro_vc_vars_counterexmp.mli Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlc src/transform/induction.mli Ocamlopt src/transform/induction.ml Ocamlc src/transform/induction_pr.mli Ocamlopt src/transform/induction_pr.ml Ocamlc src/transform/matching.ml File "src/transform/matching.ml", line 157, characters 15-33: 157 | let (--) = Pervasives.compare 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 File "src/transform/matching.ml", line 268, characters 16-34: 268 | let 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 Ocamlopt src/transform/matching.ml File "src/transform/matching.ml", line 157, characters 15-33: 157 | let (--) = Pervasives.compare 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 File "src/transform/matching.ml", line 268, characters 16-34: 268 | let 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 Ocamlc src/transform/reflection.mli Ocamlopt src/transform/reflection.ml Ocamlc src/printer/cntexmp_printer.mli Ocamlopt src/printer/cntexmp_printer.ml Ocamlc src/printer/alt_ergo.mli Ocamlopt src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.mli Ocamlopt src/printer/why3printer.ml Ocamlc src/printer/smtv1.mli Ocamlopt src/printer/smtv1.ml Ocamlc src/printer/smtv2.mli Ocamlopt src/printer/smtv2.ml Ocamlc src/printer/coq.mli Ocamlopt src/printer/coq.ml Ocamlc src/printer/pvs.ml Ocamlopt src/printer/pvs.ml Ocamlc src/printer/isabelle.ml Ocamlopt src/printer/isabelle.ml Ocamlc src/printer/simplify.mli Ocamlopt src/printer/simplify.ml Ocamlc src/printer/gappa.mli Ocamlopt src/printer/gappa.ml Ocamlc src/printer/cvc3.mli Ocamlopt src/printer/cvc3.ml Ocamlc src/printer/yices.ml Ocamlopt src/printer/yices.ml Ocamlc src/printer/mathematica.ml Ocamlopt src/printer/mathematica.ml Ocamlc src/session/compress.mli Ocamlopt src/session/compress.ml File "src/session/compress_z.ml", line 44, characters 23-33: 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 Ocamlc src/session/xml.mli Ocamlopt src/session/xml.ml Ocamlc src/session/termcode.mli Ocamlopt src/session/termcode.ml File "src/session/termcode.ml", line 1113, characters 24-42: 1113 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape 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 Ocamlc src/session/session_itp.mli Ocamlopt src/session/session_itp.ml Ocamlc src/session/strategy.mli Ocamlopt src/session/strategy.ml Ocamlc src/session/strategy_parser.mli Ocamlopt src/session/strategy_parser.ml Ocamlc src/session/controller_itp.mli Ocamlopt src/session/controller_itp.ml Ocamlc src/session/itp_communication.mli Ocamlopt src/session/itp_communication.ml Ocamlc src/session/server_utils.mli Ocamlopt src/session/server_utils.ml Ocamlc src/session/itp_server.mli Ocamlopt src/session/itp_server.ml Ocamlc src/session/json_util.mli Ocamlopt src/session/json_util.ml Ocamlc src/session/unix_scheduler.mli Ocamlopt src/session/unix_scheduler.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlc src/util/util.ml Ocamlc src/util/opt.ml Ocamlc src/util/lists.ml Ocamlc src/util/strings.ml Ocamlc src/util/pp.ml Ocamlc src/util/extmap.ml Ocamlc src/util/extset.ml Ocamlc src/util/exthtbl.ml Ocamlc src/util/weakhtbl.ml Ocamlc src/util/diffmap.ml Ocamlc src/util/hashcons.ml Ocamlc src/util/wstdlib.ml Ocamlc src/util/exn_printer.ml Ocamlc src/util/json_base.ml Ocamlc src/util/json_parser.ml Ocamlc src/util/debug.ml Ocamlc src/util/loc.ml File "src/util/loc.ml", line 67, characters 14-32: 67 | let 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 File "src/util/loc.ml", line 68, characters 12-26: 68 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ 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 Ocamlc src/util/lexlib.ml Ocamlc src/util/print_tree.ml Ocamlc src/util/cmdline.ml Ocamlc src/util/warning.ml Ocamlc src/util/sysutil.ml Ocamlc src/util/rc.ml Ocamlc src/util/plugin.ml Ocamlc src/util/number.ml Ocamlc src/util/constant.ml File "src/util/constant.ml", line 24, characters 14-32: 24 | let c = Pervasives.compare k1 k2 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 File "src/util/constant.ml", line 27, characters 14-32: 27 | let c = Pervasives.compare k1 k2 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 File "src/util/constant.ml", line 30, characters 6-24: 30 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ 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 Ocamlc src/util/vector.ml Ocamlc src/util/pqueue.ml Ocamlc src/core/ident.ml Ocamlc src/core/ty.ml Ocamlc src/core/term.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) 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 Ocamlc src/core/pattern.ml Ocamlc src/core/decl.ml Ocamlc src/core/coercion.ml Ocamlc src/core/theory.ml Ocamlc src/core/task.ml Ocamlc src/core/pretty.ml Ocamlc src/core/dterm.ml Ocamlc src/core/env.ml Ocamlc src/core/trans.ml Ocamlc src/core/printer.ml Ocamlc src/core/model_parser.ml Ocamlc src/driver/prove_client.ml Ocamlc src/driver/call_provers.ml Ocamlc src/driver/driver_parser.ml Ocamlc src/driver/driver_lexer.ml Ocamlc src/driver/driver.ml Ocamlc src/driver/whyconf.ml Ocamlc src/driver/autodetection.ml Ocamlc src/driver/smt2_model_defs.ml Ocamlc src/driver/parse_smtv2_model_parser.ml Ocamlc src/driver/collect_data_model.ml Ocamlc src/mlw/ity.ml Ocamlc src/mlw/expr.ml Ocamlc src/mlw/pdecl.ml Ocamlc src/mlw/eval_match.ml Ocamlc src/mlw/typeinv.ml Ocamlc src/mlw/vc.ml Ocamlc src/mlw/pmodule.ml Ocamlc src/mlw/dexpr.ml Ocamlc src/mlw/big_real.ml Ocamlc src/mlw/pinterp.ml Ocamlc src/extract/compile.ml Ocamlc src/extract/mlinterp.ml Ocamlc src/extract/pdriver.ml Ocamlc src/extract/ml_printer.ml Ocamlc src/parser/glob.ml Ocamlc src/parser/typing.ml Ocamlc src/parser/parser.ml Ocamlc src/parser/report.ml Ocamlc src/parser/lexer.ml Ocamlc src/parser/mlw_printer.ml Ocamlc src/transform/simplify_formula.ml Ocamlc src/transform/inlining.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/args_wrapper.ml Ocamlc src/transform/detect_polymorphism.ml Ocamlc src/transform/reduction_engine.ml Ocamlc src/transform/compute.ml Ocamlc src/transform/eliminate_definition.ml Ocamlc src/transform/eliminate_algebraic.ml Ocamlc src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.ml Ocamlc src/transform/eliminate_if.ml Ocamlc src/transform/libencoding.ml Ocamlc src/transform/discriminate.ml Ocamlc src/transform/encoding.ml Ocamlc src/transform/encoding_select.ml Ocamlc src/transform/encoding_guards_full.ml Ocamlc src/transform/encoding_tags_full.ml Ocamlc src/transform/encoding_guards.ml Ocamlc src/transform/encoding_tags.ml Ocamlc src/transform/encoding_twin.ml Ocamlc src/transform/encoding_sort.ml Ocamlc src/transform/simplify_array.ml Ocamlc src/transform/filter_trigger.ml Ocamlc src/transform/abstraction.ml Ocamlc src/transform/close_epsilon.ml Ocamlc src/transform/lift_epsilon.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/apply.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/introduction.ml Ocamlc src/transform/ind_itp.ml Ocamlc src/transform/destruct.ml Ocamlc src/transform/intro_vc_vars_counterexmp.ml Ocamlc src/transform/prepare_for_counterexmp.ml Ocamlc src/transform/induction.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/transform/reflection.ml Ocamlc src/printer/cntexmp_printer.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.ml Ocamlc src/printer/smtv1.ml Ocamlc src/printer/smtv2.ml Ocamlc src/printer/coq.ml Ocamlc src/printer/simplify.ml Ocamlc src/printer/gappa.ml Ocamlc src/printer/cvc3.ml Ocamlc src/session/compress.ml File "src/session/compress_z.ml", line 44, characters 23-33: 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 Ocamlc src/session/xml.ml Ocamlc src/session/termcode.ml File "src/session/termcode.ml", line 1113, characters 24-42: 1113 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape 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 Ocamlc src/session/session_itp.ml Ocamlc src/session/strategy.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.ml Ocamlc src/session/server_utils.ml Ocamlc src/session/itp_communication.ml Ocamlc src/session/itp_server.ml Ocamlc src/session/json_util.ml Ocamlc src/session/unix_scheduler.ml Linking lib/why3/why3.cmo Linking lib/why3/why3.cmx Ocamlc plugins/parser/genequlin.ml Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlc plugins/parser/dimacs.ml Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs Ocamlc plugins/tptp/tptp_ast.ml Ocamlopt plugins/tptp/tptp_ast.ml Ocamlc plugins/tptp/tptp_parser.mli Ocamlopt plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.mli Ocamlopt plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.mli Ocamlopt plugins/tptp/tptp_lexer.ml Ocamlc plugins/tptp/tptp_printer.mli Ocamlopt plugins/tptp/tptp_printer.ml Linking lib/plugins/tptp.cmxs Ocamlc plugins/python/py_ast.ml Ocamlopt plugins/python/py_ast.ml Ocamlc plugins/python/py_parser.mli Ocamlopt plugins/python/py_parser.ml Ocamlc plugins/python/py_lexer.ml Ocamlopt plugins/python/py_lexer.ml Ocamlc plugins/python/py_main.ml Ocamlopt plugins/python/py_main.ml Linking lib/plugins/python.cmxs Ocamlc plugins/microc/mc_ast.ml Ocamlopt plugins/microc/mc_ast.ml Ocamlc plugins/microc/mc_parser.mli Ocamlopt plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_lexer.ml Ocamlopt plugins/microc/mc_lexer.ml Ocamlc plugins/microc/mc_printer.mli Ocamlopt plugins/microc/mc_printer.ml Ocamlc plugins/microc/mc_main.ml Ocamlopt plugins/microc/mc_main.ml Linking lib/plugins/microc.cmxs Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs mkdir bin Ocamlc src/tools/main.ml Ocamlopt src/tools/main.ml Linking bin/why3.opt Ocamlc src/tools/why3config.ml Ocamlopt src/tools/why3config.ml Linking bin/why3config.opt Ocamlc src/tools/why3execute.ml Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.opt Ocamlc src/tools/why3extract.ml Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.opt Ocamlc src/tools/why3prove.ml Ocamlopt src/tools/why3prove.ml Linking bin/why3prove.opt Ocamlc src/tools/why3realize.ml Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.opt Ocamlc src/tools/why3replay.ml Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.opt Ocamlc src/tools/why3wc.ml Ocamlopt src/tools/why3wc.ml Linking bin/why3wc.opt Ocamlc src/ide/resetgc.c Ocamlc src/ide/gtkcompat.ml Ocamlopt src/ide/gtkcompat.ml Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlc src/ide/ide_utils.mli Ocamlopt src/ide/ide_utils.ml Ocamlc src/ide/why3ide.ml Ocamlopt src/ide/why3ide.ml Linking bin/why3ide.opt Ocamlc src/ide/wserver.mli Ocamlopt src/ide/wserver.ml Ocamlc src/ide/why3web.ml Ocamlopt src/ide/why3web.ml Linking bin/why3webserver.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml Ocamlc src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_info.ml Ocamlc src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_html.ml Ocamlc src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlc src/why3session/why3session_update.ml Ocamlopt src/why3session/why3session_update.ml Ocamlc src/why3session/why3session_main.ml Ocamlopt src/why3session/why3session_main.ml Linking bin/why3session.opt Ocamlc src/tools/why3shell.ml Ocamlopt src/tools/why3shell.ml Linking bin/why3shell.opt Ocamlc src/isabelle-client/isabelle_client_main.ml Ocamlopt src/isabelle-client/isabelle_client_main.ml Linking bin/isabelle_client.opt Ocamlc src/tools/why3pp.ml Ocamlopt src/tools/why3pp.ml Linking bin/why3pp.opt Ocamlc src/why3doc/doc_html.mli Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml Ocamlc src/why3doc/doc_lexer.ml Ocamlopt src/why3doc/doc_lexer.ml Ocamlc src/why3doc/doc_main.ml Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.opt gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/logging.o -c src/server/logging.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/arraylist.o -c src/server/arraylist.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/options.o -c src/server/options.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/queue.o -c src/server/queue.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/readbuf.o -c src/server/readbuf.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/request.o -c src/server/request.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/proc.o -c src/server/proc.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/writebuf.o -c src/server/writebuf.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/server-unix.o -c src/server/server-unix.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/server-win.o -c src/server/server-win.c gcc -Wall -Wl,-z,relro -o lib/why3server src/server/logging.o src/server/arraylist.o src/server/options.o src/server/queue.o src/server/readbuf.o src/server/request.o src/server/proc.o src/server/writebuf.o src/server/server-unix.o src/server/server-win.o gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/cpulimit-unix.o -c src/server/cpulimit-unix.c gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-GGVL5z/why3-1.3.3=. -fstack-protector-strong -Wformat -Werror=format-security -Wdate-time -D_FORTIFY_SOURCE=2 -o src/server/cpulimit-win.o -c src/server/cpulimit-win.c gcc -Wall -Wl,-z,relro -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Coqc lib/coq/BuiltIn.v Coqc lib/coq/HighOrd.v Coqc lib/coq/int/Int.v Coqc lib/coq/int/Exponentiation.v File "./lib/coq/int/Exponentiation.v", line 72, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/Abs.v File "./lib/coq/int/Abs.v", line 43, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/ComputerDivision.v File "./lib/coq/int/ComputerDivision.v", line 50, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/ComputerDivision.v", line 62, characters 0-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/ComputerDivision.v", line 65, characters 0-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/ComputerDivision.v", line 85, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/ComputerDivision.v", line 114, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/EuclideanDivision.v File "./lib/coq/int/EuclideanDivision.v", line 54, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 57, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 66, characters 0-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 70, characters 0-80: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 76, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 81, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 99, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/EuclideanDivision.v", line 137, characters 0-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/Div2.v File "./lib/coq/int/Div2.v", line 31, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/MinMax.v File "./lib/coq/int/MinMax.v", line 31, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/MinMax.v", line 47, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/Power.v File "./lib/coq/int/Power.v", line 60, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/int/NumOf.v File "./lib/coq/int/NumOf.v", line 53, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 56, characters 2-28: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 83, characters 2-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 86, characters 2-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 88, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 104, characters 2-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 113, characters 2-23: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 114, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 121, characters 2-42: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 133, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 144, characters 2-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 158, characters 2-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 176, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 177, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 180, characters 2-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 200, characters 2-59: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 201, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 204, characters 2-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 218, characters 2-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 219, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 221, characters 2-17: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 232, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 250, characters 0-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 263, characters 0-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 278, characters 2-76: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 282, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 283, characters 2-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 284, characters 2-62: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 309, characters 2-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 310, characters 2-61: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/int/NumOf.v", line 316, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/bool/Bool.v Coqc lib/coq/real/Real.v Coqc lib/coq/real/Abs.v Coqc lib/coq/real/ExpLog.v Coqc lib/coq/real/FromInt.v Coqc lib/coq/real/MinMax.v Coqc lib/coq/real/RealInfix.v Coqc lib/coq/real/PowerInt.v File "./lib/coq/real/PowerInt.v", line 67, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/real/PowerInt.v", line 68, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/real/PowerInt.v", line 132, characters 0-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/real/PowerInt.v", line 135, characters 0-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/real/PowerInt.v", line 138, characters 0-18: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/real/Square.v Coqc lib/coq/real/PowerReal.v Coqc lib/coq/real/Trigonometry.v Coqc lib/coq/number/Parity.v Coqc lib/coq/number/Divisibility.v Coqc lib/coq/number/Gcd.v Coqc lib/coq/number/Prime.v File "./lib/coq/number/Prime.v", line 87, characters 0-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 92, characters 0-18: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 98, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 105, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 106, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 115, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 122, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 133, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 135, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 142, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 145, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 146, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 154, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 155, characters 0-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 183, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/number/Prime.v", line 196, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/number/Coprime.v Coqc lib/coq/map/Map.v Coqc lib/coq/map/Const.v Coqc lib/coq/set/Set.v File "./lib/coq/set/Set.v", line 44, characters 0-16: Warning: Adding and removing hints in the core database implicitly is deprecated. Please specify a hint database. [implicit-core-hint-db,deprecated] Coqc lib/coq/set/Cardinal.v File "./lib/coq/set/Cardinal.v", line 307, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 433, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 468, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 471, characters 38-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 490, characters 6-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 523, characters 40-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 548, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 660, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 678, characters 31-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 732, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Cardinal.v", line 761, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/set/Fset.v File "./lib/coq/set/Fset.v", line 582, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/Fset.v", line 585, characters 17-23: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/set/FsetInduction.v Coqc lib/coq/set/FsetInt.v File "./lib/coq/set/FsetInt.v", line 52, characters 38-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 53, characters 69-75: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 58, characters 32-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 63, characters 31-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 82, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 118, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 136, characters 15-21: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 137, characters 28-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 143, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 145, characters 30-42: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 160, characters 38-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 184, characters 4-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 195, characters 4-10: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 221, characters 2-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 248, characters 6-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 251, characters 6-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 253, characters 38-62: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetInt.v", line 257, characters 21-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/set/FsetSum.v File "./lib/coq/set/FsetSum.v", line 195, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/set/FsetSum.v", line 258, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/set/SetApp.v Coqc lib/coq/set/SetAppInt.v Coqc lib/coq/set/SetImp.v Coqc lib/coq/set/SetImpInt.v Coqc lib/coq/map/Occ.v File "./lib/coq/map/Occ.v", line 38, characters 0-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 42, characters 0-43: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 73, characters 0-33: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 74, characters 0-20: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 81, characters 0-24: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 91, characters 0-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 151, characters 20-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 153, characters 41-50: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 155, characters 0-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 156, characters 0-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 161, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 163, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 164, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 169, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 171, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 172, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 186, characters 22-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 189, characters 43-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 191, characters 0-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 194, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 200, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 202, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 202, characters 7-13: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 205, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 212, characters 0-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 214, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 214, characters 7-13: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 217, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 232, characters 0-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 233, characters 28-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 236, characters 41-50: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 238, characters 0-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 239, characters 0-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 242, characters 2-18: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 247, characters 14-20: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 248, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 261, characters 0-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 262, characters 25-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 262, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 266, characters 41-50: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 268, characters 0-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 269, characters 25-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 269, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 271, characters 27-33: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 272, characters 39-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 272, characters 46-52: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 275, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 277, characters 17-23: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 289, characters 20-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 291, characters 20-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 294, characters 52-58: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 294, characters 59-65: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 296, characters 55-61: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 297, characters 62-68: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 298, characters 64-70: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 299, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 311, characters 0-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 314, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 314, characters 7-13: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 318, characters 41-50: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 320, characters 0-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 321, characters 47-53: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 321, characters 54-60: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 327, characters 9-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 327, characters 16-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 327, characters 41-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 327, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 329, characters 24-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 329, characters 31-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 335, characters 9-15: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 335, characters 16-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 335, characters 41-47: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 335, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 337, characters 24-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 337, characters 31-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 361, characters 0-42: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 361, characters 0-42: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 362, characters 0-48: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 362, characters 0-48: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 369, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/Occ.v", line 372, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/map/MapPermut.v Coqc lib/coq/map/MapInjection.v File "./lib/coq/map/MapInjection.v", line 47, characters 0-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 51, characters 0-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 64, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 69, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 75, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 77, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 78, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 88, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 92, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 95, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 121, characters 0-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 126, characters 0-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 138, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 151, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 186, characters 0-32: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 194, characters 2-60: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 209, characters 0-32: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 216, characters 0-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 251, characters 0-43: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 268, characters 0-65: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 270, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 272, characters 35-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 273, characters 0-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 276, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 278, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 281, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 282, characters 2-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 283, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 284, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 285, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 286, characters 52-58: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 287, characters 0-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 288, characters 48-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 289, characters 0-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 296, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 298, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 301, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 302, characters 2-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 303, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 304, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 305, characters 0-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 308, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 310, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 313, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 314, characters 2-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 315, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 316, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 320, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 322, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 325, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 327, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 330, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 331, characters 2-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 332, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 333, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 337, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 339, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/map/MapInjection.v", line 340, characters 0-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/List.v Coqc lib/coq/list/Length.v File "./lib/coq/list/Length.v", line 57, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/Mem.v Coqc lib/coq/option/Option.v Coqc lib/coq/list/Nth.v Coqc lib/coq/list/NthLength.v File "./lib/coq/list/NthLength.v", line 38, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLength.v", line 60, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLength.v", line 63, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLength.v", line 76, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLength.v", line 85, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/HdTl.v Coqc lib/coq/list/NthHdTl.v File "./lib/coq/list/NthHdTl.v", line 36, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/Append.v Coqc lib/coq/list/NthLengthAppend.v File "./lib/coq/list/NthLengthAppend.v", line 44, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLengthAppend.v", line 70, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NthLengthAppend.v", line 73, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/Reverse.v Coqc lib/coq/list/HdTlNoOpt.v Coqc lib/coq/list/NthNoOpt.v Coqc lib/coq/list/RevAppend.v Coqc lib/coq/list/Combine.v Coqc lib/coq/list/Distinct.v Coqc lib/coq/list/NumOcc.v File "./lib/coq/list/NumOcc.v", line 61, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/NumOcc.v", line 78, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/list/Permut.v File "./lib/coq/list/Permut.v", line 150, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/Permut.v", line 160, characters 4-10: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/list/Permut.v", line 178, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/bv/Pow2int.v Coqc lib/coq/bv/BV_Gen.v File "./lib/coq/bv/BV_Gen.v", line 41, characters 2-28: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 63, characters 2-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 70, characters 2-73: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 77, characters 2-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 78, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 84, characters 2-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 85, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 96, characters 2-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 104, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 108, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 115, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 119, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 127, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 132, characters 2-17: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 140, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 144, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 153, characters 2-32: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 163, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 176, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 185, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 204, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 212, characters 0-6: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 338, characters 2-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 341, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 351, characters 0-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 364, characters 2-33: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 365, characters 2-28: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 366, characters 2-32: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 388, characters 2-17: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 390, characters 2-23: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 392, characters 2-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 393, characters 2-41: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 394, characters 2-17: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 411, characters 2-86: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 441, characters 2-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 445, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 446, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 447, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 458, characters 2-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 460, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 479, characters 2-56: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 483, characters 2-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 492, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 493, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 494, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 505, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 506, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 529, characters 2-30: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 530, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 532, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 542, characters 2-49: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 547, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 549, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 555, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 561, characters 2-24: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 563, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 572, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 585, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 596, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 633, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 634, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 635, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 636, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 647, characters 2-32: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 649, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 650, characters 2-27: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 651, characters 2-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 657, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 663, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 685, characters 2-16: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 703, characters 2-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 712, characters 2-23: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 713, characters 2-65: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 720, characters 2-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 732, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 733, characters 2-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 734, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 739, characters 2-43: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 760, characters 10-16: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 765, characters 10-16: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 767, characters 6-12: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 774, characters 10-16: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 779, characters 10-16: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 781, characters 6-12: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 800, characters 2-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 801, characters 2-49: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 802, characters 2-29: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 836, characters 2-49: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 850, characters 2-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 868, characters 2-135: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 870, characters 2-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 879, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 883, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 884, characters 2-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 888, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 903, characters 2-35: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 908, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 923, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 929, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 930, characters 2-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 937, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 942, characters 2-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 948, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 948, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 973, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 974, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 980, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 980, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 982, characters 2-28: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 985, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 986, characters 2-57: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 987, characters 2-66: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 987, characters 2-66: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 992, characters 2-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 992, characters 2-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 996, characters 2-28: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1003, characters 2-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1003, characters 2-44: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1005, characters 2-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1021, characters 2-25: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1027, characters 2-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1038, characters 2-73: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1044, characters 2-40: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1046, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1047, characters 2-51: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1049, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1049, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1051, characters 2-26: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1058, characters 2-24: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1065, characters 2-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1065, characters 2-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1065, characters 2-46: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1068, characters 2-60: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1085, characters 2-101: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1093, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1094, characters 2-31: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1096, characters 2-101: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1247, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1252, characters 2-80: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1268, characters 2-96: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1279, characters 2-64: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1286, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1287, characters 2-49: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1288, characters 2-45: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1289, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1294, characters 2-48: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1320, characters 2-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1332, characters 2-76: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1333, characters 2-86: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1335, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1338, characters 2-60: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1340, characters 2-39: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1341, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1353, characters 2-65: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1462, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1463, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1463, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1463, characters 2-38: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1464, characters 2-36: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1465, characters 55-61: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1469, characters 36-42: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1832, characters 2-37: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1928, characters 6-54: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1962, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1974, characters 4-10: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1986, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 1990, characters 2-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2020, characters 2-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2021, characters 2-63: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2042, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2046, characters 2-22: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2047, characters 2-34: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/bv/BV_Gen.v", line 2053, characters 2-19: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Coqc lib/coq/for_drivers/ComputerOfEuclideanDivision.v File "./lib/coq/for_drivers/ComputerOfEuclideanDivision.v", line 82, characters 2-8: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/for_drivers/ComputerOfEuclideanDivision.v", line 90, characters 4-10: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] File "./lib/coq/for_drivers/ComputerOfEuclideanDivision.v", line 97, characters 4-10: Warning: omega is deprecated since 8.12; use “lia” instead. [omega-is-deprecated,deprecated] Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Linking lib/plugins/genequlin.cmo Linking lib/plugins/dimacs.cmo Ocamlc plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.ml Ocamlc plugins/tptp/tptp_printer.ml Linking lib/plugins/tptp.cmo Ocamlc plugins/python/py_parser.ml Linking lib/plugins/python.cmo Ocamlc plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_printer.ml Linking lib/plugins/microc.cmo Linking lib/why3/why3.cma Linking bin/why3.byte Linking bin/why3config.byte Linking bin/why3execute.byte Linking bin/why3extract.byte Linking bin/why3prove.byte Linking bin/why3realize.byte Linking bin/why3replay.byte Linking bin/why3wc.byte Ocamlc src/ide/gconfig.ml Ocamlc src/ide/ide_utils.ml Linking bin/why3ide.byte Ocamlc src/ide/wserver.ml Linking bin/why3webserver.byte Ocamlc src/why3session/why3session_lib.ml Linking bin/why3session.byte Linking bin/why3shell.byte Linking bin/isabelle_client.byte Linking bin/why3pp.byte Ocamlc src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.ml Linking bin/why3doc.byte make[2]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_auto_test -a create-stamp debian/debhelper-build-stamp dh_prep -a dh_installdirs -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' # do nothing make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' debian/rules override_dh_install-arch make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' dh build-arch --with ocaml,tex dh_update_autotools_config -a dh_autoreconf -a dh_autoreconf: warning: Only runs once, see dh-autoreconf(7) dh_ocamlinit -a debian/rules override_dh_auto_configure make[2]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' autoconf dh_auto_configure -- \ --disable-emacs-compilation \ --libdir=/usr/lib/ocaml ./configure --build=x86_64-linux-gnu --prefix=/usr --includedir=\${prefix}/include --mandir=\${prefix}/share/man --infodir=\${prefix}/share/info --sysconfdir=/etc --localstatedir=/var --disable-option-checking --disable-silent-rules --libdir=\${prefix}/lib/x86_64-linux-gnu --runstatedir=/run --disable-maintainer-mode --disable-dependency-tracking --disable-emacs-compilation --libdir=/usr/lib/ocaml checking executable suffix... checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether gcc accepts -g... yes checking for gcc option to accept ISO C89... none needed checking for gcc option to accept ISO C99... none needed checking for gcc option to accept ISO Standard C... (cached) none needed checking for a thread-safe mkdir -p... /bin/mkdir -p checking for a BSD-compatible install... /usr/bin/install -c checking for ocamlc... ocamlc ocaml version is 4.11.1 ocaml library path is /usr/lib/ocaml checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocamlopt.opt... ocamlopt.opt checking ocamlc.opt version... ok checking for ocamldep... ocamldep checking for ocamldep.opt... ocamldep.opt checking for ocamllex... ocamllex checking for ocamllex.opt... ocamllex.opt checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... ocamldoc.opt checking for menhir... menhir checking for ocamlfind... ocamlfind ocamlfind found compiler-libs in /usr/lib/ocaml/compiler-libs checking for sphinx-build... no configure: WARNING: Cannot find sphinx-build, Documentation disabled. ocamlfind found num in /usr/lib/ocaml/num checking for /usr/lib/ocaml/num/nums.cma... no checking for /usr/lib/ocaml/num/num.cmi... no checking for /usr/lib/ocaml/nums.cma... yes checking for /usr/lib/ocaml/num.cmi... yes ocamlfind found zarith in /usr/lib/ocaml/zarith checking for /usr/lib/ocaml/zarith/z.cmi... yes ocamlfind found camlzip in /usr/lib/ocaml/zip checking for /usr/lib/ocaml/zip/zip.cmi... yes ocamlfind found menhirLib in /usr/lib/ocaml/menhirLib checking for /usr/lib/ocaml/menhirLib/menhirLib.cmi... yes ocamlfind found seq in /usr/lib/ocaml/seq checking for /usr/lib/ocaml/seq/seq.cma... no checking for /usr/lib/ocaml/seq/seq.cmi... no checking for /usr/lib/ocaml/stdlib__seq.cmi... yes ocamlfind: Package `re' not found checking for /usr/lib/ocaml/re/re.cmx... no checking for /usr/lib/ocaml/re/re.cmi... no configure: WARNING: Library re not found. ocamlfind found lablgtk3 in /usr/lib/ocaml/lablgtk3 checking for /usr/lib/ocaml/lablgtk3/lablgtk.cma... no checking for /usr/lib/ocaml/lablgtk3/lablgtk3.cma... yes checking for /usr/lib/ocaml/lablgtk3/gtkButton.cmi... yes ocamlfind found lablgtk3-sourceview3 in /usr/lib/ocaml/lablgtk3-sourceview3 checking for /usr/lib/ocaml/lablgtk3-sourceview3/gSourceView3.cmi... yes ocamlfind: Package `js_of_ocaml' not found ocamlfind: Package `mlmpfr' not found checking for coqc... coqc checking Coq version... 8.12.0 checking for coqdep... coqdep checking for Flocq... File "./conftest.v", line 1, characters 15-28: Error: Cannot find a physical path bound to logical path matching suffix Flocq. no configure: WARNING: Cannot find Flocq. checking for pvs... no configure: WARNING: Cannot find pvs. checking for isabelle... no configure: WARNING: Cannot find isabelle. configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating lib/why3/META config.status: creating .merlin config.status: creating src/jessie/Makefile config.status: creating src/jessie/.merlin config.status: creating lib/coq/version config.status: creating lib/pvs/version config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.11.1 Library path : /usr/lib/ocaml Ocamlfind : yes Native compilation : yes Profiling : no Memory profiling : no (disabled by default) PPX : yes Javascript support : no (js_of_ocaml not found) Mpfr support : no (mlmpfr not found) Re support : no Components Why3 library : yes GTK IDE : yes (gtk3) Web IDE : no (Javascript support not available) GMP arithmetic : yes Compressed sessions : yes Hypothesis selection : no (broken) Frama-C support : no (disabled by default) Documentation : no (sphinx-build not found) Support for interactive proof assistants Coq : yes Version : 8.12.0 Library path : /usr/lib/coq Realization support : yes FP arithmetic : no (Flocq >= 3.1 not found) PVS : no (pvs not found) Isabelle : no (isabelle not found) Installable : yes Binary path : ${exec_prefix}/bin Library path : /usr/lib/ocaml/why3 Data path : ${prefix}/share/why3 OCaml library path : /usr/local/lib/ocaml/4.11.1/why3 Relocatable : no make[2]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' debian/rules override_dh_auto_build-arch make[2]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' /usr/bin/make all byte make[3]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' cp src/ide/gtkcompat3.ml src/ide/gtkcompat.ml Ocamldep src/ide/why3ide.ml Ocamldep src/ide/ide_utils.ml Ocamldep src/ide/gconfig.ml Ocamldep src/ide/gtkcompat.ml Generate src/util/config.ml cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml cp src/session/compress_z.ml src/session/compress.ml cp src/util/recompat.ml src/util/re.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/session/json_util.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/strategy.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.ml Ocamldep src/session/compress.ml Ocamldep src/printer/mathematica.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/smtv1.ml Ocamldep src/printer/why3printer.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/printer/cntexmp_printer.ml Ocamldep src/transform/reflection.ml Ocamldep src/transform/matching.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/intro_vc_vars_counterexmp.ml Ocamldep src/transform/congruence.ml Ocamldep src/transform/cut.ml Ocamldep src/transform/destruct.ml Ocamldep src/transform/ind_itp.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/subst.ml Ocamldep src/transform/apply.ml Ocamldep src/transform/case.ml Ocamldep src/transform/generic_arg_trans_utils.ml Ocamldep src/transform/eliminate_literal.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/abstract_quantifiers.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/report.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree.ml Ocamldep src/extract/cakeml.ml Ocamldep src/extract/ocaml.ml Ocamldep src/extract/c.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/extract/pdriver.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/extract/compile.ml Ocamldep src/extract/mltree.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/mlw/big_real.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/mlw/vc.ml Ocamldep src/mlw/typeinv.ml Ocamldep src/mlw/eval_match.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/ity.ml Ocamldep src/driver/parse_smtv2_model.ml Ocamldep src/driver/parse_smtv2_model_lexer.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/driver/parse_smtv2_model_parser.ml Ocamldep src/driver/smt2_model_defs.ml Ocamldep src/driver/autodetection.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/driver/driver_ast.ml Ocamldep src/driver/call_provers.ml Ocamldep src/driver/prove_client.ml Ocamldep src/core/model_parser.ml Ocamldep src/core/printer.ml Ocamldep src/core/trans.ml Ocamldep src/core/env.ml Ocamldep src/core/dterm.ml Ocamldep src/core/pretty.ml Ocamldep src/core/task.ml Ocamldep src/core/theory.ml Ocamldep src/core/coercion.ml Ocamldep src/core/decl.ml Ocamldep src/core/pattern.ml Ocamldep src/core/term.ml Ocamldep src/core/ty.ml Ocamldep src/core/ident.ml Ocamldep src/util/re.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/vector.ml Ocamldep src/util/constant.ml Ocamldep src/util/number.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/plugin.ml Ocamldep src/util/rc.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/warning.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/loc.ml Ocamldep src/util/debug.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_base.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/extset.ml Ocamldep src/util/extmap.ml Ocamldep src/util/pp.ml Ocamldep src/util/strings.ml Ocamldep src/util/lists.ml Ocamldep src/util/opt.ml Ocamldep src/util/util.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/config.ml Ocamlc src/util/config.ml Ocamlopt src/util/config.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlc src/util/re.ml Ocamlopt src/util/re.ml Ocamlopt src/core/ident.ml Ocamlopt src/core/ty.ml Ocamlopt src/core/term.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) 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 Ocamlopt src/core/pattern.ml Ocamlopt src/core/decl.ml Ocamlopt src/core/coercion.ml Ocamlopt src/core/theory.ml Ocamlopt src/core/task.ml Ocamlopt src/core/pretty.ml Ocamlopt src/core/dterm.ml Ocamlopt src/core/env.ml Ocamlopt src/core/trans.ml Ocamlopt src/core/printer.ml Ocamlopt src/core/model_parser.ml Ocamlopt src/driver/prove_client.ml Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/driver_parser.ml Ocamlopt src/driver/driver_lexer.ml Ocamlopt src/driver/driver.ml Ocamlc src/driver/whyconf.mli Ocamlopt src/driver/whyconf.ml Ocamlc src/driver/autodetection.mli Ocamlopt src/driver/autodetection.ml Ocamlopt src/driver/smt2_model_defs.ml Ocamlopt src/driver/parse_smtv2_model_parser.ml Ocamlopt src/driver/collect_data_model.ml Ocamlopt src/driver/parse_smtv2_model_lexer.ml Ocamlc src/driver/parse_smtv2_model.ml Ocamlopt src/driver/parse_smtv2_model.ml Ocamlopt src/mlw/ity.ml Ocamlopt src/mlw/expr.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/mlw/eval_match.ml Ocamlopt src/mlw/typeinv.ml Ocamlopt src/mlw/vc.ml Ocamlopt src/mlw/pmodule.ml Ocamlopt src/mlw/dexpr.ml Ocamlopt src/mlw/big_real.ml Ocamlopt src/mlw/pinterp.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/extract/compile.ml Ocamlopt src/extract/mlinterp.ml Ocamlopt src/extract/pdriver.ml Ocamlopt src/extract/ml_printer.ml Ocamlc src/extract/c.ml Ocamlopt src/extract/c.ml Ocamlopt src/extract/ocaml.ml Ocamlopt src/extract/cakeml.ml Ocamlopt src/parser/ptree.ml Ocamlopt src/parser/glob.ml Ocamlopt src/parser/typing.ml Ocamlopt src/parser/parser.ml Ocamlopt src/parser/report.ml Ocamlopt src/parser/lexer.ml Ocamlopt src/parser/mlw_printer.ml Ocamlopt src/transform/simplify_formula.ml Ocamlopt src/transform/inlining.ml Ocamlopt src/transform/split_goal.ml Ocamlopt src/transform/args_wrapper.ml Ocamlopt src/transform/detect_polymorphism.ml Ocamlopt src/transform/reduction_engine.ml Ocamlopt src/transform/compute.ml Ocamlopt src/transform/eliminate_definition.ml Ocamlopt src/transform/eliminate_algebraic.ml Ocamlopt src/transform/abstract_quantifiers.ml Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlopt src/transform/eliminate_inductive.ml Ocamlopt src/transform/eliminate_let.ml Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/transform/discriminate.ml Ocamlopt src/transform/encoding.ml Ocamlopt src/transform/encoding_select.ml Ocamlopt src/transform/encoding_guards_full.ml Ocamlopt src/transform/encoding_tags_full.ml Ocamlopt src/transform/encoding_guards.ml Ocamlopt src/transform/encoding_tags.ml Ocamlopt src/transform/encoding_twin.ml Ocamlopt src/transform/encoding_sort.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/lift_epsilon.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/eliminate_literal.ml Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlopt src/transform/case.ml Ocamlopt src/transform/apply.ml Ocamlopt src/transform/subst.ml Ocamlopt src/transform/introduction.ml Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/destruct.ml Ocamlopt src/transform/cut.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlopt src/transform/induction.ml Ocamlopt src/transform/induction_pr.ml Ocamlopt src/transform/matching.ml File "src/transform/matching.ml", line 157, characters 15-33: 157 | let (--) = Pervasives.compare 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 File "src/transform/matching.ml", line 268, characters 16-34: 268 | let 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 Ocamlopt src/transform/reflection.ml Ocamlopt src/printer/cntexmp_printer.ml Ocamlopt src/printer/alt_ergo.ml Ocamlopt src/printer/why3printer.ml Ocamlopt src/printer/smtv1.ml Ocamlopt src/printer/smtv2.ml Ocamlopt src/printer/coq.ml Ocamlc src/printer/pvs.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/simplify.ml Ocamlopt src/printer/gappa.ml Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/printer/mathematica.ml Ocamlopt src/session/compress.ml File "src/session/compress_z.ml", line 44, characters 23-33: 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 Ocamlopt src/session/termcode.ml File "src/session/termcode.ml", line 1113, characters 24-42: 1113 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape 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 Ocamlc src/session/session_itp.mli Ocamlopt src/session/session_itp.ml Ocamlc src/session/strategy.mli Ocamlopt src/session/strategy.ml Ocamlc src/session/strategy_parser.mli Ocamlopt src/session/strategy_parser.ml Ocamlc src/session/controller_itp.mli Ocamlopt src/session/controller_itp.ml Ocamlc src/session/itp_communication.mli Ocamlopt src/session/itp_communication.ml Ocamlc src/session/server_utils.mli Ocamlopt src/session/server_utils.ml Ocamlc src/session/itp_server.mli Ocamlopt src/session/itp_server.ml Ocamlc src/session/json_util.mli Ocamlopt src/session/json_util.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlc src/core/ident.ml Ocamlc src/core/model_parser.ml Ocamlc src/driver/prove_client.ml Ocamlc src/driver/call_provers.ml Ocamlc src/driver/driver.ml Ocamlc src/driver/whyconf.ml Ocamlc src/driver/autodetection.ml Ocamlc src/driver/collect_data_model.ml Ocamlc src/parser/report.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/reflection.ml Ocamlc src/printer/coq.ml Ocamlc src/session/compress.ml File "src/session/compress_z.ml", line 44, characters 23-33: 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 Ocamlc src/session/session_itp.ml Ocamlc src/session/strategy.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.ml Ocamlc src/session/server_utils.ml Ocamlc src/session/itp_communication.ml Ocamlc src/session/itp_server.ml Ocamlc src/session/json_util.ml Linking lib/why3/why3.cmo Linking lib/why3/why3.cmx Ocamlc plugins/parser/genequlin.ml Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlc plugins/parser/dimacs.ml Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs Ocamlc plugins/tptp/tptp_ast.ml Ocamlopt plugins/tptp/tptp_ast.ml Ocamlc plugins/tptp/tptp_parser.mli Ocamlopt plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.mli Ocamlopt plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.mli Ocamlopt plugins/tptp/tptp_lexer.ml Ocamlopt plugins/tptp/tptp_printer.ml Linking lib/plugins/tptp.cmxs Ocamlc plugins/python/py_ast.ml Ocamlopt plugins/python/py_ast.ml Ocamlc plugins/python/py_parser.mli Ocamlopt plugins/python/py_parser.ml Ocamlc plugins/python/py_lexer.ml Ocamlopt plugins/python/py_lexer.ml Ocamlc plugins/python/py_main.ml Ocamlopt plugins/python/py_main.ml Linking lib/plugins/python.cmxs Ocamlc plugins/microc/mc_ast.ml Ocamlopt plugins/microc/mc_ast.ml Ocamlc plugins/microc/mc_parser.mli Ocamlopt plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_lexer.ml Ocamlopt plugins/microc/mc_lexer.ml Ocamlc plugins/microc/mc_printer.mli Ocamlopt plugins/microc/mc_printer.ml Ocamlc plugins/microc/mc_main.ml Ocamlopt plugins/microc/mc_main.ml Linking lib/plugins/microc.cmxs Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs Ocamlc src/tools/main.ml Ocamlopt src/tools/main.ml Linking bin/why3.opt Ocamlc src/tools/why3config.ml Ocamlopt src/tools/why3config.ml Linking bin/why3config.opt Ocamlc src/tools/why3execute.ml Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.opt Ocamlc src/tools/why3extract.ml Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.opt Ocamlc src/tools/why3prove.ml Ocamlopt src/tools/why3prove.ml Linking bin/why3prove.opt Ocamlc src/tools/why3realize.ml Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.opt Ocamlc src/tools/why3replay.ml Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.opt Ocamlc src/ide/gtkcompat.ml Ocamlopt src/ide/gtkcompat.ml Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlc src/ide/why3ide.ml Ocamlopt src/ide/why3ide.ml Linking bin/why3ide.opt Ocamlopt src/ide/wserver.ml Ocamlc src/ide/why3web.ml Ocamlopt src/ide/why3web.ml Linking bin/why3webserver.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml Ocamlc src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_info.ml Ocamlc src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_html.ml Ocamlc src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlc src/why3session/why3session_update.ml Ocamlopt src/why3session/why3session_update.ml Ocamlc src/why3session/why3session_main.ml Ocamlopt src/why3session/why3session_main.ml Linking bin/why3session.opt Ocamlc src/tools/why3shell.ml Ocamlopt src/tools/why3shell.ml Linking bin/why3shell.opt Ocamlc src/isabelle-client/isabelle_client_main.ml Ocamlopt src/isabelle-client/isabelle_client_main.ml Linking bin/isabelle_client.opt Ocamlc src/tools/why3pp.ml Ocamlopt src/tools/why3pp.ml Linking bin/why3pp.opt Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml Ocamlc src/why3doc/doc_lexer.ml Ocamlopt src/why3doc/doc_lexer.ml Ocamlc src/why3doc/doc_main.ml Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.opt Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Linking lib/plugins/genequlin.cmo Linking lib/plugins/dimacs.cmo Ocamlc plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.ml Ocamlc plugins/tptp/tptp_printer.ml Linking lib/plugins/tptp.cmo Ocamlc plugins/python/py_parser.ml Linking lib/plugins/python.cmo Ocamlc plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_printer.ml Linking lib/plugins/microc.cmo Linking lib/why3/why3.cma Linking bin/why3.byte Linking bin/why3config.byte Linking bin/why3execute.byte Linking bin/why3extract.byte Linking bin/why3prove.byte Linking bin/why3realize.byte Linking bin/why3replay.byte Ocamlc src/ide/gconfig.ml Linking bin/why3ide.byte Ocamlc src/ide/wserver.ml Linking bin/why3webserver.byte Ocamlc src/why3session/why3session_lib.ml Linking bin/why3session.byte Linking bin/why3shell.byte Linking bin/isabelle_client.byte Linking bin/why3pp.byte Ocamlc src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.ml Linking bin/why3doc.byte make[3]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' make[2]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_auto_test -a create-stamp debian/debhelper-build-stamp /usr/bin/make install install-lib DESTDIR=/build/why3-GGVL5z/why3-1.3.3/debian/tmp make[2]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/plugins /usr/bin/install -c -m 644 lib/plugins/genequlin.cmo lib/plugins/dimacs.cmo lib/plugins/tptp.cmo lib/plugins/python.cmo lib/plugins/microc.cmo lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/python.cmxs lib/plugins/microc.cmxs /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/plugins /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/bin /usr/bin/install -c bin/why3.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/bin/why3 /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3config.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3config /usr/bin/install -c bin/why3execute.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3execute /usr/bin/install -c bin/why3extract.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3extract /usr/bin/install -c bin/why3prove.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3prove /usr/bin/install -c bin/why3realize.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3realize /usr/bin/install -c bin/why3replay.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3replay /usr/bin/install -c bin/why3wc.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3wc /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3 /usr/bin/install -c lib/why3server /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/why3server /usr/bin/install -c lib/why3cpulimit /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/why3cpulimit /usr/bin/install -c lib/why3-call-pvs /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/why3-call-pvs /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3webserver.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3webserver /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3session.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3session /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3shell.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3shell /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3pp.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3pp /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3doc.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3doc /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3 /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/vim /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/vim/ftdetect /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/vim/syntax /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/lang /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/stdlib /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/stdlib/mach /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 stdlib/*.mlw /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/stdlib /usr/bin/install -c -m 644 stdlib/mach/*.mlw /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/stdlib/mach /usr/bin/install -c -m 644 drivers/*.drv drivers/*.gen /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 LICENSE /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/ /usr/bin/install -c -m 644 share/provers-detection-data.conf /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/ /usr/bin/install -c -m 644 share/why3session.dtd /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3 /usr/bin/install -c -m 644 share/Makefile.config /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3 /usr/bin/install -c -m 644 share/vim/ftdetect/why3.vim /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/vim/ftdetect/why3.vim /usr/bin/install -c -m 644 share/vim/syntax/why3.vim /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/vim/syntax/why3.vim /usr/bin/install -c -m 644 share/lang/why3.lang /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/lang/why3.lang /usr/bin/install -c -m 644 share/lang/why3c.lang /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/lang/why3c.lang /usr/bin/install -c -m 644 share/lang/why3py.lang /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/lang/why3py.lang /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 drivers/coq-realizations.aux /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers/ /usr/bin/install -c -m 644 drivers/pvs-realizations.aux /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers/ /usr/bin/install -c -m 644 drivers/isabelle-realizations.aux /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/emacs/site-lisp/ /usr/bin/install -c -m 644 share/emacs/why3.el /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/emacs/site-lisp/why3.el /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c bin/why3ide.opt /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/commands/why3ide /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/images for i in share/images/*.rc; do \ d=`basename $i .rc`; \ /usr/bin/install -c -m 644 $i /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/images; \ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/images/$d; \ /usr/bin/install -c -m 644 share/images/$d/* /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/images/$d; \ done /usr/bin/install -c -m 644 share/images/*.png /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/images /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq /usr/bin/install -c -m 644 lib/coq/version /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/ /usr/bin/install -c -m 644 lib/coq/BuiltIn.vo lib/coq/HighOrd.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/int /usr/bin/install -c -m 644 lib/coq/int/Exponentiation.vo lib/coq/int/Abs.vo lib/coq/int/ComputerDivision.vo lib/coq/int/Div2.vo lib/coq/int/EuclideanDivision.vo lib/coq/int/Int.vo lib/coq/int/MinMax.vo lib/coq/int/Power.vo lib/coq/int/NumOf.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/int/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/bool /usr/bin/install -c -m 644 lib/coq/bool/Bool.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/bool/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/real /usr/bin/install -c -m 644 lib/coq/real/Abs.vo lib/coq/real/ExpLog.vo lib/coq/real/FromInt.vo lib/coq/real/MinMax.vo lib/coq/real/PowerInt.vo lib/coq/real/PowerReal.vo lib/coq/real/Real.vo lib/coq/real/RealInfix.vo lib/coq/real/Square.vo lib/coq/real/Trigonometry.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/real/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/number /usr/bin/install -c -m 644 lib/coq/number/Divisibility.vo lib/coq/number/Gcd.vo lib/coq/number/Parity.vo lib/coq/number/Prime.vo lib/coq/number/Coprime.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/number/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/set /usr/bin/install -c -m 644 lib/coq/set/Set.vo lib/coq/set/Cardinal.vo lib/coq/set/Fset.vo lib/coq/set/FsetInduction.vo lib/coq/set/FsetInt.vo lib/coq/set/FsetSum.vo lib/coq/set/SetApp.vo lib/coq/set/SetAppInt.vo lib/coq/set/SetImp.vo lib/coq/set/SetImpInt.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/set/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/map /usr/bin/install -c -m 644 lib/coq/map/Map.vo lib/coq/map/Const.vo lib/coq/map/Occ.vo lib/coq/map/MapPermut.vo lib/coq/map/MapInjection.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/map/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/list /usr/bin/install -c -m 644 lib/coq/list/List.vo lib/coq/list/Length.vo lib/coq/list/Mem.vo lib/coq/list/Nth.vo lib/coq/list/NthLength.vo lib/coq/list/HdTl.vo lib/coq/list/NthHdTl.vo lib/coq/list/Append.vo lib/coq/list/NthLengthAppend.vo lib/coq/list/Reverse.vo lib/coq/list/HdTlNoOpt.vo lib/coq/list/NthNoOpt.vo lib/coq/list/RevAppend.vo lib/coq/list/Combine.vo lib/coq/list/Distinct.vo lib/coq/list/NumOcc.vo lib/coq/list/Permut.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/list/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/option /usr/bin/install -c -m 644 lib/coq/option/Option.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/option/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/bv /usr/bin/install -c -m 644 lib/coq/bv/Pow2int.vo lib/coq/bv/BV_Gen.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/bv/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/for_drivers /usr/bin/install -c -m 644 lib/coq/for_drivers/ComputerOfEuclideanDivision.vo /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/lib/ocaml/why3/coq/for_drivers/ /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 drivers/coq-realizations.aux /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/share/why3/drivers/ if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then \ /usr/bin/install -c share/bash/why3 /etc/bash_completion.d; \ fi /bin/mkdir -p /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/local/lib/ocaml/4.11.1/why3 /usr/bin/install -c -m 644 lib/why3/why3.a lib/why3/why3.cma lib/why3/why3.cmx lib/why3/why3.cmi lib/why3/why3.cmxa lib/why3/why3.cmxs \ lib/why3/META /build/why3-GGVL5z/why3-1.3.3/debian/tmp/usr/local/lib/ocaml/4.11.1/why3 make[2]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_install -a -XLICENSE echo 'F:CoqABI=8.12.0+4.11.1' >> debian/why3-coq.substvars make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_ocamldoc -a dh_installdocs -a dh_installchangelogs -a debian/rules override_dh_installexamples make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' dh_installexamples if [ -d debian/why3-examples/usr/share/doc/why3-examples/examples ]; \ then \ find debian/why3-examples/usr/share/doc/why3-examples/examples \ -name why3shapes.gz \ -exec sh -c 'if [ $(zcat {} | wc -c) -eq 0 ]; then \rm {}; fi' \;;\ fi make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_installman -a dh_installemacsen -a dh_perl -a dh_link -a dh_installtex -a dh_strip_nondeterminism -a debian/rules override_dh_compress make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' dh_compress -Xmanual.pdf make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_fixperms -a dh_missing -a dh_strip -a -a dh_makeshlibs -a -a dh_shlibdeps -a -a dh_installdeb -a debian/rules override_dh_ocaml make[1]: Entering directory '/build/why3-GGVL5z/why3-1.3.3' dh_ocaml --nodefined-map=why3-coq:Why3,MenhirLib,Gzip,Zlib,Zip \ make[1]: Leaving directory '/build/why3-GGVL5z/why3-1.3.3' dh_gencontrol -a dpkg-gencontrol: warning: Depends field of package why3-coq: substitution variable ${ocaml:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package why3-coq: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libwhy3-ocaml-dev: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libwhy3-ocaml-dev: substitution variable ${shlibs:Depends} used, but is not defined dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'why3' in '../why3_1.3.3-1+b4_amd64.deb'. dpkg-deb: building package 'libwhy3-ocaml-dev-dbgsym' in '../libwhy3-ocaml-dev-dbgsym_1.3.3-1+b4_amd64.deb'. dpkg-deb: building package 'why3-coq' in '../why3-coq_1.3.3-1+b4_amd64.deb'. dpkg-deb: building package 'libwhy3-ocaml-dev' in '../libwhy3-ocaml-dev_1.3.3-1+b4_amd64.deb'. dpkg-deb: building package 'why3-dbgsym' in '../why3-dbgsym_1.3.3-1+b4_amd64.deb'. dpkg-genbuildinfo --build=any dpkg-genchanges --build=any >../why3_1.3.3-1+b4_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/why3-GGVL5z /tmp/why3-1.3.3-1+b40nz0l5bo I: cleaning package lists and apt cache... W: deleting files in /tmp: camlobj5ed3bd.cds W: deleting files in /tmp: camlobj7d8810.cds I: creating tarball... I: done I: removing tempdir /tmp/mmdebstrap.lXjGN1XehT... I: success in 1856.1432 seconds md5: libwhy3-ocaml-dev-dbgsym_1.3.3-1+b4_amd64.deb: OK md5: libwhy3-ocaml-dev_1.3.3-1+b4_amd64.deb: OK md5: why3-coq_1.3.3-1+b4_amd64.deb: OK md5: why3-dbgsym_1.3.3-1+b4_amd64.deb: OK md5: why3_1.3.3-1+b4_amd64.deb: OK sha1: libwhy3-ocaml-dev-dbgsym_1.3.3-1+b4_amd64.deb: OK sha1: libwhy3-ocaml-dev_1.3.3-1+b4_amd64.deb: OK sha1: why3-coq_1.3.3-1+b4_amd64.deb: OK sha1: why3-dbgsym_1.3.3-1+b4_amd64.deb: OK sha1: why3_1.3.3-1+b4_amd64.deb: OK sha256: libwhy3-ocaml-dev-dbgsym_1.3.3-1+b4_amd64.deb: OK sha256: libwhy3-ocaml-dev_1.3.3-1+b4_amd64.deb: OK sha256: why3-coq_1.3.3-1+b4_amd64.deb: OK sha256: why3-dbgsym_1.3.3-1+b4_amd64.deb: OK sha256: why3_1.3.3-1+b4_amd64.deb: OK Checksums: OK