Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/w/why3/why3_1.4.1-2_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/why3-1.4.1-2tyks87a7/why3_1.4.1-2_amd64.buildinfo Get source package info: why3=1.4.1-2 Source URL: http://snapshot.notset.fr/mr/package/why3/1.4.1-2/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=adduser=3.121 adwaita-icon-theme=42~really41.0-1 autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-4 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6 binutils=2.38-3 binutils-common=2.38-3 binutils-x86-64-linux-gnu=2.38-3 bsdextrautils=2.37.3-1+b1 bsdutils=1:2.37.3-1+b1 build-essential=12.9 bzip2=1.0.8-5 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.2.0-18 dash=0.5.11+git20210903+057cd650a4ed-8 dbus=1.14.0-1 dbus-bin=1.14.0-1 dbus-daemon=1.14.0-1 dbus-session-bus-common=1.14.0-1 dbus-system-bus-common=1.14.0-1 dbus-user-session=1.14.0-1 dconf-gsettings-backend=0.40.0-3 dconf-service=0.40.0-3 debconf=1.5.79 debhelper=13.6 debianutils=5.7-0.1 dh-autoreconf=20 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dmsetup=2:1.02.175-2.1 dpkg=1.21.2 dpkg-dev=1.21.2 dwz=0.14-1 file=1:5.41-2 findutils=4.9.0-2 fontconfig=2.13.1-4.4 fontconfig-config=2.13.1-4.4 fonts-dejavu-core=2.37-2 g++=4:11.2.0-2 g++-11=11.2.0-18 gcc=4:11.2.0-2 gcc-11=11.2.0-18 gcc-11-base=11.2.0-18 gcc-12-base=12-20220313-1 gettext=0.21-4 gettext-base=0.21-4 gir1.2-atk-1.0=2.36.0-3 gir1.2-atspi-2.0=2.42.0-2 gir1.2-freedesktop=1.72.0-1 gir1.2-gdkpixbuf-2.0=2.42.6+dfsg-2 gir1.2-glib-2.0=1.72.0-1 gir1.2-gtk-3.0=3.24.33-1 gir1.2-gtksource-3.0=3.24.11-2+b1 gir1.2-harfbuzz-0.0=2.7.4-1 gir1.2-pango-1.0=1.50.4+ds-1 grep=3.7-1 groff-base=1.22.4-8 gtk-update-icon-cache=3.24.33-1 gzip=1.10-4 hicolor-icon-theme=0.17-2 hostname=3.23 icu-devtools=67.1-7 init-system-helpers=1.62 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libapparmor1=3.0.4-2 libarchive-zip-perl=1.68-1 libargon2-1=0~20171227-0.3 libasan6=11.2.0-18 libatk-bridge2.0-0=2.38.0-3 libatk-bridge2.0-dev=2.38.0-3 libatk1.0-0=2.36.0-3 libatk1.0-data=2.36.0-3 libatk1.0-dev=2.36.0-3 libatomic1=12-20220313-1 libatspi2.0-0=2.42.0-2 libatspi2.0-dev=2.42.0-2 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libavahi-client3=0.8-5 libavahi-common-data=0.8-5 libavahi-common3=0.8-5 libbinutils=2.38-3 libblkid-dev=2.37.3-1+b1 libblkid1=2.37.3-1+b1 libbrotli-dev=1.0.9-2+b3 libbrotli1=1.0.9-2+b3 libbsd0=0.11.5-1+b1 libbz2-1.0=1.0.8-5 libc-bin=2.33-7 libc-dev-bin=2.33-7 libc6=2.33-7 libc6-dev=2.33-7 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.2+dfsg-1+b1 libcairo2-ocaml-dev=0.6.2+dfsg-1+b1 libcap-ng0=0.7.9-2.2+b1 libcap2=1:2.44-1 libcc1-0=12-20220313-1 libcolord2=1.4.6-1 libcom-err2=1.46.5-2 libcrypt-dev=1:4.4.27-1.1 libcrypt1=1:4.4.27-1.1 libcryptsetup12=2:2.4.3-1 libctf-nobfd0=2.38-3 libctf0=2.38-3 libcups2=2.4.1op1-2 libdatrie-dev=0.2.13-2 libdatrie1=0.2.13-2 libdb5.3=5.3.28+dfsg1-0.8 libdbus-1-3=1.14.0-1 libdbus-1-dev=1.14.0-1 libdconf1=0.40.0-3 libdebconfclient0=0.261 libdebhelper-perl=13.6 libdeflate-dev=1.10-2 libdeflate0=1.10-2 libdevmapper1.02.1=2:1.02.175-2.1 libdpkg-perl=1.21.2 libdrm-amdgpu1=2.4.110-1 libdrm-common=2.4.110-1 libdrm-intel1=2.4.110-1 libdrm-nouveau2=2.4.110-1 libdrm-radeon1=2.4.110-1 libdrm2=2.4.110-1 libedit2=3.1-20210910-1 libegl-dev=1.4.0-1 libegl-mesa0=21.3.7-1 libegl1=1.4.0-1 libegl1-mesa-dev=21.3.7-1 libelf1=0.186-1 libepoxy-dev=1.5.9-2 libepoxy0=1.5.9-2 libexpat1=2.4.7-1 libexpat1-dev=2.4.7-1 libfdisk1=2.37.3-1+b1 libffi-dev=3.4.2-4 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libfontconfig-dev=2.13.1-4.4 libfontconfig1=2.13.1-4.4 libfontconfig1-dev=2.13.1-4.4 libfreetype-dev=2.11.1+dfsg-1 libfreetype6=2.11.1+dfsg-1 libfreetype6-dev=2.11.1+dfsg-1 libfribidi-dev=1.0.8-2 libfribidi0=1.0.8-2 libgbm1=21.3.7-1 libgcc-11-dev=11.2.0-18 libgcc-s1=12-20220313-1 libgcrypt20=1.9.4-5 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgdk-pixbuf-2.0-0=2.42.6+dfsg-2 libgdk-pixbuf-2.0-dev=2.42.6+dfsg-2 libgdk-pixbuf2.0-bin=2.42.6+dfsg-2 libgdk-pixbuf2.0-common=2.42.6+dfsg-2 libgirepository-1.0-1=1.72.0-1 libgl-dev=1.4.0-1 libgl1=1.4.0-1 libgl1-mesa-dri=21.3.7-1 libglapi-mesa=21.3.7-1 libgles-dev=1.4.0-1 libgles1=1.4.0-1 libgles2=1.4.0-1 libglib2.0-0=2.72.0-1 libglib2.0-bin=2.72.0-1 libglib2.0-data=2.72.0-1 libglib2.0-dev=2.72.0-1 libglib2.0-dev-bin=2.72.0-1 libglvnd-core-dev=1.4.0-1 libglvnd-dev=1.4.0-1 libglvnd0=1.4.0-1 libglx-dev=1.4.0-1 libglx-mesa0=21.3.7-1 libglx0=1.4.0-1 libgmp-dev=2:6.2.1+dfsg-3 libgmp10=2:6.2.1+dfsg-3 libgmp3-dev=2:6.2.1+dfsg-3 libgmpxx4ldbl=2:6.2.1+dfsg-3 libgnutls30=3.7.3-4+b1 libgomp1=12-20220313-1 libgpg-error0=1.43-3 libgraphite2-3=1.3.14-1 libgraphite2-dev=1.3.14-1 libgssapi-krb5-2=1.19.2-2+b1 libgtk-3-0=3.24.33-1 libgtk-3-common=3.24.33-1 libgtk-3-dev=3.24.33-1 libgtksourceview-3.0-1=3.24.11-2+b1 libgtksourceview-3.0-common=3.24.11-2 libgtksourceview-3.0-dev=3.24.11-2+b1 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.7.3-1 libice-dev=2:1.0.10-1 libice6=2:1.0.10-1 libicu-dev=67.1-7 libicu67=67.1-7 libidn2-0=2.3.2-2 libip4tc2=1.8.7-1 libisl23=0.24-2 libitm1=12-20220313-1 libjbig-dev=2.1-3.1+b2 libjbig0=2.1-3.1+b2 libjpeg-dev=1:2.1.2-1 libjpeg62-turbo=1:2.1.2-1 libjpeg62-turbo-dev=1:2.1.2-1 libjson-c5=0.15-2 libk5crypto3=1.19.2-2+b1 libkeyutils1=1.6.1-3 libkmod2=29-1 libkrb5-3=1.19.2-2+b1 libkrb5support0=1.19.2-2+b1 liblablgtk3-ocaml=3.1.2-1 liblablgtk3-ocaml-dev=3.1.2-1 liblablgtksourceview3-ocaml=3.1.2-1 liblablgtksourceview3-ocaml-dev=3.1.2-1 liblcms2-2=2.12~rc1-2 libllvm13=1:13.0.1-3+b1 liblsan0=12-20220313-1 liblz4-1=1.9.3-2 liblzma-dev=5.2.5-2 liblzma5=5.2.5-2 liblzo2-2=2.10-2 libmagic-mgc=1:5.41-2 libmagic1=1:5.41-2 libmd0=1.0.4-1 libmenhir-ocaml-dev=20210929-1+b1 libmount-dev=2.37.3-1+b1 libmount1=2.37.3-1+b1 libmpc3=1.2.1-1 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3-2 libncurses5-dev=6.3-2 libncurses6=6.3-2 libncursesw6=6.3-2 libnettle8=3.7.3-1 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libnum-ocaml=1.4-2 libnum-ocaml-dev=1.4-2 libocamlgraph-ocaml-dev=2.0.0-3+b1 libopengl-dev=1.4.0-1 libopengl0=1.4.0-1 libp11-kit0=0.24.0-6 libpam-modules=1.4.0-11 libpam-modules-bin=1.4.0-11 libpam-runtime=1.4.0-11 libpam-systemd=250.4-1 libpam0g=1.4.0-11 libpango-1.0-0=1.50.4+ds-1 libpango1.0-dev=1.50.4+ds-1 libpangocairo-1.0-0=1.50.4+ds-1 libpangoft2-1.0-0=1.50.4+ds-1 libpangoxft-1.0-0=1.50.4+ds-1 libpciaccess0=0.16-3 libpcre16-3=2:8.39-13 libpcre2-16-0=10.39-3 libpcre2-32-0=10.39-3 libpcre2-8-0=10.39-3 libpcre2-dev=10.39-3 libpcre2-posix3=10.39-3 libpcre3=2:8.39-13 libpcre3-dev=2:8.39-13 libpcre32-3=2:8.39-13 libpcrecpp0v5=2:8.39-13 libperl5.34=5.34.0-3 libpipeline1=1.5.5-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 libpthread-stubs0-dev=0.4-1 libpython3-stdlib=3.9.8-1 libpython3.9-minimal=3.9.11-1 libpython3.9-stdlib=3.9.11-1 libquadmath0=12-20220313-1 libreadline8=8.1.2-1 libseccomp2=2.5.3-2 libselinux1=3.3-1+b2 libselinux1-dev=3.3-1+b2 libsemanage-common=3.3-1 libsemanage2=3.3-1+b2 libsensors-config=1:3.6.0-7 libsensors5=1:3.6.0-7 libsepol-dev=3.3-1 libsepol2=3.3-1 libsigsegv2=2.14-1 libsm-dev=2:1.2.3-1 libsm6=2:1.2.3-1 libsmartcols1=2.37.3-1+b1 libsqlite3-0=3.38.1-1 libsqlite3-dev=3.38.1-1 libsqlite3-ocaml=5.1.0-1 libsqlite3-ocaml-dev=5.1.0-1 libssl1.1=1.1.1n-1 libstdc++-11-dev=11.2.0-18 libstdc++6=12-20220313-1 libsub-override-perl=0.09-2 libsystemd0=250.4-1 libtasn1-6=4.18.0-4 libthai-data=0.1.29-1 libthai-dev=0.1.29-1 libthai0=0.1.29-1 libtiff-dev=4.3.0-6 libtiff5=4.3.0-6 libtiffxx5=4.3.0-6 libtinfo6=6.3-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.6-15 libtsan0=11.2.0-18 libubsan1=12-20220313-1 libuchardet0=0.0.7-1 libudev1=250.4-1 libunistring2=1.0-1 libuuid1=2.37.3-1+b1 libvulkan1=1.3.204.1-2 libwayland-bin=1.20.0-1 libwayland-client0=1.20.0-1 libwayland-cursor0=1.20.0-1 libwayland-dev=1.20.0-1 libwayland-egl1=1.20.0-1 libwayland-server0=1.20.0-1 libwebp7=1.2.2-2+b1 libx11-6=2:1.7.2-2+b1 libx11-data=2:1.7.2-2 libx11-dev=2:1.7.2-2+b1 libx11-xcb1=2:1.7.2-2+b1 libxau-dev=1:1.0.9-1 libxau6=1:1.0.9-1 libxcb-dri2-0=1.14-3 libxcb-dri3-0=1.14-3 libxcb-glx0=1.14-3 libxcb-present0=1.14-3 libxcb-render0=1.14-3 libxcb-render0-dev=1.14-3 libxcb-shm0=1.14-3 libxcb-shm0-dev=1.14-3 libxcb-sync1=1.14-3 libxcb-xfixes0=1.14-3 libxcb1=1.14-3 libxcb1-dev=1.14-3 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.4-1 libxext6=2:1.3.4-1 libxfixes-dev=1:6.0.0-1 libxfixes3=1:6.0.0-1 libxft-dev=2.3.2-2 libxft2=2.3.2-2 libxi-dev=2:1.8-1 libxi6=2:1.8-1 libxinerama-dev=2:1.1.4-3 libxinerama1=2:1.1.4-3 libxkbcommon-dev=1.4.0-1 libxkbcommon0=1.4.0-1 libxml2=2.9.13+dfsg-1 libxml2-dev=2.9.13+dfsg-1 libxrandr-dev=2:1.5.2-1 libxrandr2=2:1.5.2-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.12-1+b1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzip-ocaml=1.11-1+b1 libzip-ocaml-dev=1.11-1+b1 libzstd1=1.4.8+dfsg-3 linux-libc-dev=5.16.14-1 login=1:4.11.1+dfsg1-2 lsb-base=11.1.0 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3+b1 media-types=6.0.0 menhir=20210929-1+b1 mount=2.37.3-1+b1 ncurses-base=6.3-2 ncurses-bin=6.3-2 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 pango1.0-tools=1.50.4+ds-1 passwd=1:4.11.1+dfsg1-2 patch=2.7.6-7 perl=5.34.0-3 perl-base=5.34.0-3 perl-modules-5.34=5.34.0-3 pkg-config=0.29.2-1 po-debconf=1.0.21+nmu1 python3=3.9.8-1 python3-distutils=3.9.11-1 python3-lib2to3=3.9.11-1 python3-minimal=3.9.8-1 python3.9=3.9.11-1 python3.9-minimal=3.9.11-1 readline-common=8.1.2-1 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sgml-base=1.30 shared-mime-info=2.1-2 systemd=250.4-1 systemd-sysv=250.4-1 sysvinit-utils=3.01-1 tar=1.34+dfsg-1 tex-common=6.17 tzdata=2021e-1 ucf=3.0043 util-linux=2.37.3-1+b1 uuid-dev=2.37.3-1+b1 wayland-protocols=1.25-1 x11-common=1:7.7+23 x11proto-dev=2021.5-1 xkb-data=2.33-1 xml-core=0.18+nmu1 xorg-sgml-doctools=1:1.11-1.1 xtrans-dev=1.4.0-1 xz-utils=5.2.5-2 zlib1g=1:1.2.11.dfsg-3 zlib1g-dev=1:1.2.11.dfsg-3 --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/20220322T094313Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220322T094313Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220319T033210Z/ 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.4.1-2 && mkdir -p /build/why3-MFGZlp && dpkg-source --no-check -x /*.dsc /build/why3-MFGZlp/why3-1.4.1 && chown -R builduser:builduser /build/why3-MFGZlp" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/why3-MFGZlp/why3-1.4.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1647698500" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/why3-MFGZlp /tmp/why3-1.4.1-2tyks87a7 bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220319T033210Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: null I: using /tmp/mmdebstrap.OEKzH7xirO 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.OEKzH7xirO Reading package lists... Building dependency tree... util-linux is already the newest version (2.37.3-1+b1). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 135 kB of archives. After this operation, 406 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220319T033210Z unstable/main amd64 libfakeroot amd64 1.28-1 [48.2 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220319T033210Z unstable/main amd64 fakeroot amd64 1.28-1 [87.2 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 135 kB in 0s (1118 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 ... 4702 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.28-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.28-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.28-1_amd64.deb ... Unpacking fakeroot (1.28-1) ... Setting up libfakeroot:amd64 (1.28-1) ... Setting up fakeroot (1.28-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-7) ... 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/20220322T094313Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220322T094313Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220319T033210Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.OEKzH7xirO Get:1 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm InRelease [130 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20220319T033210Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main Sources [11.9 MB] Get:4 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main amd64 Packages [11.3 MB] Fetched 23.3 MB in 19s (1197 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.OEKzH7xirO I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d why3=1.4.1-2 && mkdir -p /build/why3-MFGZlp && dpkg-source --no-check -x /*.dsc /build/why3-MFGZlp/why3-1.4.1 && chown -R builduser:builduser /build/why3-MFGZlp"' exec /tmp/mmdebstrap.OEKzH7xirO 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 6328 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main why3 1.4.1-2 (dsc) [2662 B] Get:2 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main why3 1.4.1-2 (tar) [6305 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220322T094313Z bookworm/main why3 1.4.1-2 (diff) [20.4 kB] Fetched 6328 kB in 5s (1283 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'why3_1.4.1-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting why3 in /build/why3-MFGZlp/why3-1.4.1 dpkg-source: info: unpacking why3_1.4.1.orig.tar.gz dpkg-source: info: unpacking why3_1.4.1-2.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying hardening-flags dpkg-source: info: applying ocamlgraph-cma.patch I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/why3-MFGZlp/why3-1.4.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1647698500" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.OEKzH7xirO dpkg-buildpackage: info: source package why3 dpkg-buildpackage: info: source version 1.4.1-2 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Ralf Treinen dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") dh clean --with ocaml,tex dh_ocamlclean dh_clean debian/rules binary-arch Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") dh binary-arch --with ocaml,tex dh_update_autotools_config -a dh_autoreconf -a autoreconf: warning: autoconf input should be named 'configure.ac', not 'configure.in' aclocal: warning: autoconf input should be named 'configure.ac', not 'configure.in' configure.in:203: warning: The macro `AC_PROG_CC_STDC' is obsolete. configure.in:203: You should run autoupdate. ./lib/autoconf/c.m4:1666: AC_PROG_CC_STDC is expanded from... configure.in:203: the top level dh_ocamlinit -a debian/rules override_dh_auto_configure make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") autoconf configure.in:203: warning: The macro `AC_PROG_CC_STDC' is obsolete. configure.in:203: You should run autoupdate. ./lib/autoconf/c.m4:1666: AC_PROG_CC_STDC is expanded from... configure.in:203: the top level 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 the compiler supports GNU C... yes checking whether gcc accepts -g... yes checking for gcc option to enable C11 features... none needed checking for a race-free mkdir -p... /bin/mkdir -p checking for a BSD-compatible install... /usr/bin/install -c checking for ocamlc... ocamlc ocaml version is 4.13.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... no configure: WARNING: Library seq not found. ocamlfind found lablgtk3 in /usr/lib/ocaml/lablgtk3 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 found ocamlgraph in /usr/lib/ocaml/ocamlgraph checking for /usr/lib/ocaml/ocamlgraph/graph.cmi... yes ocamlfind: Package `js_of_ocaml' not found ocamlfind: Package `mlmpfr' not found ocamlfind: Package `ppx_sexp_conv' not found checking for coqc... no configure: WARNING: Cannot find coqc. 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.13.1 Library path : /usr/lib/ocaml Ocamlfind : yes Native compilation : yes Profiling : no Memory profiling : no (disabled by default) PPX : yes S-expr for why3pp : no (requires ppx_sexp_conv) Javascript support : no (js_of_ocaml not found) MPFR support : no (mlmpfr not found) Re support : no (seq not found) Components Why3 library : yes GTK IDE : yes (gtk3) Web IDE : no (Javascript support not available) GMP arithmetic : yes Compressed sessions : yes Hypothesis selection : yes Invariant inference(exp): no (disabled by default) Frama-C support : no (disabled by default) Documentation : no (sphinx-build not found) Support for interactive proof assistants Coq : no (coqc 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.13.1/why3 Relocatable : no make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' debian/rules override_dh_auto_build-arch make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") /usr/bin/make all byte make[2]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Ocamldep src/trywhy3/worker_proto.ml Ocamldep src/trywhy3/why3_worker.ml Ocamldep src/trywhy3/trywhy3.ml Ocamldep src/trywhy3/shortener.ml Ocamldep src/trywhy3/bindings.ml Ocamldep src/trywhy3/alt_ergo_worker.ml 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 cp src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.ml Ocamldep src/tools/why3pp.ml Ocamldep src/tools/why3pp_sexp.ml Ocamldep src/isabelle-client/isabelle_client_main.ml 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/cfg/cfg_lexer.mll 155 states, 4342 transitions, table size 18298 bytes 7537 additional bytes used for bindings Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings Ocamldep plugins/cfg/cfg_main.ml Ocamldep plugins/cfg/cfg_lexer.ml Ocamldep plugins/cfg/cfg_parser.ml Ocamldep plugins/cfg/cfg_tokens.ml Ocamldep plugins/cfg/cfg_ast.ml 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/transform/hypothesis_selection.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 cp src/util/mysexplib-dummy.ml src/util/mysexplib.ml 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 cp src/util/dynlink_new.ml src/util/dynlink_wrapper.ml Ocamllex src/parser/lexer.mll 158 states, 4359 transitions, table size 18384 bytes 7555 additional bytes used for bindings Menhir src/parser/parser_common.mly src/parser/parser.mly Read 3 sample input sentences and 3 error messages. menhir --explain --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \ src/parser/handcrafted.messages > src/parser/parser_messages.ml Read 3 sample input sentences and 3 error messages. Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 34 states, 1366 transitions, table size 5668 bytes Ocamllex src/driver/sexp.mll 27 states, 306 transitions, table size 1386 bytes 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 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_helpers.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/counterexample.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/smtv2_model_parser.ml Ocamldep src/driver/sexp.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/driver/smtv2_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 cp src/util/recompat.ml src/util/re.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/dynlink_wrapper.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/getopt.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 Ocamldep src/util/mysexplib.ml mkdir lib/plugins Ocamlc src/util/mysexplib.ml File "src/util/mysexplib.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/mysexplib.ml Ocamlc src/util/config.ml File "src/util/config.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/util/util.mli", line 103, characters 22-52: 103 | val ansi_color_tags : Format.formatter_tag_functions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.formatter_tag_functions Use formatter_stag_functions. 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 122, characters 33-51: 122 | ('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 125, characters 33-51: 125 | ('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/getopt.mli Ocamlopt src/util/getopt.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 File "src/util/json_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/json_lexer.ml Ocamlc src/util/debug.mli Ocamlopt src/util/debug.ml File "src/util/debug.ml", line 115, characters 21-39: 115 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ 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/loc.mli Ocamlopt src/util/loc.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | 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 70, characters 12-26: 70 | 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/dynlink_wrapper.ml File "src/util/dynlink_wrapper.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/dynlink_wrapper.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 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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 32, characters 6-24: 32 | 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 File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/util/pqueue.mli Ocamlopt src/util/pqueue.ml Ocamlc src/util/re.ml File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/driver/driver_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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/smtv2_model_defs.mli Ocamlopt src/driver/smtv2_model_defs.ml Ocamlc src/driver/collect_data_model.mli Ocamlopt src/driver/collect_data_model.ml Ocamlc src/driver/sexp.mli Ocamlopt src/driver/sexp.ml Ocamlc src/driver/smtv2_model_parser.ml File "src/driver/smtv2_model_parser.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/driver/smtv2_model_parser.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 File "src/mlw/pinterp.ml", line 60, characters 14-28: 60 | let n = Pervasives.max 0 (Array.length a - 25) 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/mlw/pinterp.ml", line 1851, characters 48-62: 1851 | let s = String.(if length s > n then sub s 0 (Pervasives.min n (length s)) ^ "..." else s) 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/mlw/counterexample.mli Ocamlopt src/mlw/counterexample.ml Ocamlc src/extract/mltree.ml File "src/extract/mltree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/extract/mlinterp.ml", line 42, characters 4-18: 42 | env : Env.env; ^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field env is never read. (However, this field is used to build or mutate values.) File "src/extract/mlinterp.ml", line 43, characters 4-33: 43 | mm : Pmodule.pmodule Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field mm is never read. (However, this field is used to build or mutate values.) 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 File "src/extract/c.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/extract/c.ml Ocamlc src/extract/ocaml.ml File "src/extract/ocaml.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/extract/ocaml.ml Ocamlc src/extract/cakeml.ml File "src/extract/cakeml.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/extract/cakeml.ml Ocamlc src/parser/ptree.ml File "src/parser/ptree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/parser/ptree.ml Ocamlc src/parser/ptree_helpers.mli Ocamlopt src/parser/ptree_helpers.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 File "src/parser/parser_messages.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/transform/inlining.ml", line 98, characters 25-38: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/transform/inlining.ml", line 98, characters 8-21: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. 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 File "src/transform/abstract_quantifiers.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/abstract_quantifiers.ml Ocamlc src/transform/eliminate_unknown_types.ml File "src/transform/eliminate_unknown_types.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlc src/transform/eliminate_unknown_lsymbols.ml File "src/transform/eliminate_unknown_lsymbols.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlc src/transform/eliminate_symbol.ml File "src/transform/eliminate_symbol.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/transform/prop_curry.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/transform/case.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/transform/cut.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/cut.ml Ocamlc src/transform/congruence.ml File "src/transform/congruence.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/congruence.ml Ocamlc src/transform/intro_vc_vars_counterexmp.mli Ocamlopt src/transform/intro_vc_vars_counterexmp.ml File "src/transform/intro_vc_vars_counterexmp.ml", line 31, characters 2-24: 31 | vc_pre_or_post : bool; ^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field vc_pre_or_post is never read. (However, this field is used to build or mutate values.) 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 File "src/transform/matching.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/printer/alt_ergo.ml", line 47, characters 2-29: 47 | mutable info_in_goal: bool; ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field info_in_goal is never mutated. File "src/printer/alt_ergo.ml", line 49, characters 2-45: 49 | mutable list_field_def: Ident.ident Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field list_field_def is never mutated. File "src/printer/alt_ergo.ml", line 51, characters 2-26: 51 | meta_record_def : Sls.t; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field meta_record_def is never read. (However, this field is used to build or mutate values.) 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 File "src/printer/pvs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/printer/pvs.ml Ocamlc src/printer/isabelle.ml File "src/printer/isabelle.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/printer/gappa.ml", line 97, characters 2-23: 97 | info_symbols : Sid.t; ^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field info_symbols is never read. (However, this field is used to build or mutate values.) Ocamlc src/printer/cvc3.mli Ocamlopt src/printer/cvc3.ml Ocamlc src/printer/yices.ml File "src/printer/yices.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/printer/yices.ml Ocamlc src/printer/mathematica.ml File "src/printer/mathematica.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 1106, characters 24-42: 1106 | 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 File "src/session/session_itp.ml", line 36, characters 2-41: 36 | mutable theory_parent_name : fileID; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field theory_parent_name is never mutated. File "src/session/session_itp.ml", line 1938, characters 2-30: 1938 | prover_ids : int PHprover.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field prover_ids is never read. (However, this field is used to build or mutate values.) 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 File "src/session/controller_itp.ml", line 570, characters 36-43: 570 | let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification = ^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/session/controller_itp.ml", line 307, characters 4-38: 307 | tp_session : Session_itp.session; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_session is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 308, characters 4-30: 308 | tp_id : proofNodeID; ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_id is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 309, characters 4-33: 309 | tp_pr : Whyconf.prover; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_pr is never read. (However, this field is used to build or mutate values.) 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/getopt.ml Ocamlc src/util/json_base.ml Ocamlc src/util/json_parser.ml Ocamlc src/util/debug.ml File "src/util/debug.ml", line 115, characters 21-39: 115 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ 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/loc.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | 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 70, characters 12-26: 70 | 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 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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 32, characters 6-24: 32 | 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 File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. 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/smtv2_model_defs.ml Ocamlc src/driver/collect_data_model.ml Ocamlc src/driver/sexp.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 File "src/mlw/pinterp.ml", line 60, characters 14-28: 60 | let n = Pervasives.max 0 (Array.length a - 25) 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/mlw/pinterp.ml", line 1851, characters 48-62: 1851 | let s = String.(if length s > n then sub s 0 (Pervasives.min n (length s)) ^ "..." else s) 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/mlw/counterexample.ml Ocamlc src/extract/compile.ml Ocamlc src/extract/mlinterp.ml File "src/extract/mlinterp.ml", line 42, characters 4-18: 42 | env : Env.env; ^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field env is never read. (However, this field is used to build or mutate values.) File "src/extract/mlinterp.ml", line 43, characters 4-33: 43 | mm : Pmodule.pmodule Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field mm is never read. (However, this field is used to build or mutate values.) Ocamlc src/extract/pdriver.ml Ocamlc src/extract/ml_printer.ml Ocamlc src/parser/ptree_helpers.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 File "src/transform/inlining.ml", line 98, characters 25-38: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/transform/inlining.ml", line 98, characters 8-21: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. 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 File "src/transform/intro_vc_vars_counterexmp.ml", line 31, characters 2-24: 31 | vc_pre_or_post : bool; ^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field vc_pre_or_post is never read. (However, this field is used to build or mutate values.) 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 File "src/printer/alt_ergo.ml", line 47, characters 2-29: 47 | mutable info_in_goal: bool; ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field info_in_goal is never mutated. File "src/printer/alt_ergo.ml", line 49, characters 2-45: 49 | mutable list_field_def: Ident.ident Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field list_field_def is never mutated. File "src/printer/alt_ergo.ml", line 51, characters 2-26: 51 | meta_record_def : Sls.t; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field meta_record_def is never read. (However, this field is used to build or mutate values.) 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 File "src/printer/gappa.ml", line 97, characters 2-23: 97 | info_symbols : Sid.t; ^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field info_symbols is never read. (However, this field is used to build or mutate values.) 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 1106, characters 24-42: 1106 | 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 File "src/session/session_itp.ml", line 36, characters 2-41: 36 | mutable theory_parent_name : fileID; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field theory_parent_name is never mutated. File "src/session/session_itp.ml", line 1938, characters 2-30: 1938 | prover_ids : int PHprover.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field prover_ids is never read. (However, this field is used to build or mutate values.) Ocamlc src/session/strategy.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.ml File "src/session/controller_itp.ml", line 570, characters 36-43: 570 | let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification = ^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/session/controller_itp.ml", line 307, characters 4-38: 307 | tp_session : Session_itp.session; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_session is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 308, characters 4-30: 308 | tp_id : proofNodeID; ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_id is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 309, characters 4-33: 309 | tp_pr : Whyconf.prover; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_pr is never read. (However, this field is used to build or mutate values.) 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 File "plugins/parser/genequlin.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlc plugins/parser/dimacs.ml File "plugins/parser/dimacs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs Ocamlc plugins/tptp/tptp_ast.ml File "plugins/tptp/tptp_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "plugins/python/py_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_ast.ml Ocamlc plugins/python/py_parser.mli Ocamlopt plugins/python/py_parser.ml Ocamlc plugins/python/py_lexer.ml File "plugins/python/py_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_lexer.ml Ocamlc plugins/python/py_main.ml File "plugins/python/py_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_main.ml Linking lib/plugins/python.cmxs Ocamlc plugins/microc/mc_ast.ml File "plugins/microc/mc_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_ast.ml Ocamlc plugins/microc/mc_parser.mli Ocamlopt plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_lexer.ml File "plugins/microc/mc_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_lexer.ml Ocamlc plugins/microc/mc_printer.mli Ocamlopt plugins/microc/mc_printer.ml Ocamlc plugins/microc/mc_main.ml File "plugins/microc/mc_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_main.ml Linking lib/plugins/microc.cmxs Ocamlc plugins/cfg/cfg_ast.ml File "plugins/cfg/cfg_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_ast.ml Ocamlc plugins/cfg/cfg_tokens.ml File "plugins/cfg/cfg_tokens.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_tokens.ml Ocamlc plugins/cfg/cfg_parser.mli Ocamlopt plugins/cfg/cfg_parser.ml Ocamlc plugins/cfg/cfg_lexer.ml File "plugins/cfg/cfg_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_lexer.ml Ocamlc plugins/cfg/cfg_main.ml File "plugins/cfg/cfg_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_main.ml Linking lib/plugins/cfg.cmxs Ocamlc plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | 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 "plugins/transform/hypothesis_selection.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | 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 Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs Ocamlc src/tools/main.ml File "src/tools/main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/main.ml Linking bin/why3.opt Ocamlc src/tools/why3config.ml File "src/tools/why3config.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3config.ml Linking bin/why3config.cmxs Ocamlc src/tools/why3execute.ml File "src/tools/why3execute.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.cmxs Ocamlc src/tools/why3extract.ml File "src/tools/why3extract.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.cmxs Ocamlc src/tools/why3prove.ml File "src/tools/why3prove.ml", line 446, characters 6-40: 446 | Format.set_formatter_tag_functions Util.ansi_color_tags; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.set_formatter_tag_functions Use Format.set_formatter_stag_functions. File "src/tools/why3prove.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3prove.ml File "src/tools/why3prove.ml", line 446, characters 6-40: 446 | Format.set_formatter_tag_functions Util.ansi_color_tags; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.set_formatter_tag_functions Use Format.set_formatter_stag_functions. Linking bin/why3prove.cmxs Ocamlc src/tools/why3realize.ml File "src/tools/why3realize.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.cmxs Ocamlc src/tools/why3replay.ml File "src/tools/why3replay.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.cmxs Ocamlc src/tools/why3wc.ml File "src/tools/why3wc.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3wc.ml Linking bin/why3wc.cmxs Ocamlc src/ide/gtkcompat.ml File "src/ide/gtkcompat.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "src/ide/why3ide.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/ide/why3ide.ml Linking bin/why3ide.cmxs Ocamlc src/ide/wserver.mli Ocamlopt src/ide/wserver.ml Ocamlc src/ide/why3web.ml File "src/ide/why3web.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/ide/why3web.ml Linking bin/why3webserver.cmxs Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 130, characters 6-30: 130 | archived : filter_three; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field archived is never read. (However, this field is used to build or mutate values.) Ocamlc src/why3session/why3session_info.ml File "src/why3session/why3session_info.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_info.ml Ocamlc src/why3session/why3session_html.ml File "src/why3session/why3session_html.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_html.ml Ocamlc src/why3session/why3session_latex.ml File "src/why3session/why3session_latex.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_latex.ml Ocamlc src/why3session/why3session_update.ml File "src/why3session/why3session_update.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_update.ml Ocamlc src/why3session/why3session_main.ml File "src/why3session/why3session_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_main.ml Linking bin/why3session.cmxs Ocamlc src/tools/why3shell.ml File "src/tools/why3shell.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3shell.ml Linking bin/why3shell.cmxs Ocamlc src/isabelle-client/isabelle_client_main.ml File "src/isabelle-client/isabelle_client_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/isabelle-client/isabelle_client_main.ml Linking bin/isabelle_client.opt Ocamlc src/tools/why3pp_sexp.ml File "src/tools/why3pp_sexp.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3pp_sexp.ml Ocamlc src/tools/why3pp.ml File "src/tools/why3pp.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3pp.ml Linking bin/why3pp.cmxs 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 File "src/why3doc/doc_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3doc/doc_lexer.ml Ocamlc src/why3doc/doc_main.ml File "src/why3doc/doc_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.cmxs gcc -Wall -O -g -g -O2 -ffile-prefix-map=/build/why3-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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-MFGZlp/why3-1.4.1=. -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 Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Linking lib/plugins/genequlin.cma Linking lib/plugins/dimacs.cma 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.cma Ocamlc plugins/python/py_parser.ml Linking lib/plugins/python.cma Ocamlc plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_printer.ml Linking lib/plugins/microc.cma Ocamlc plugins/cfg/cfg_parser.ml Linking lib/plugins/cfg.cma Linking lib/plugins/hypothesis_selection.cma Linking lib/why3/why3.cma Linking bin/why3.byte Linking bin/why3config.cma Linking bin/why3execute.cma Linking bin/why3extract.cma Linking bin/why3prove.cma Linking bin/why3realize.cma Linking bin/why3replay.cma Linking bin/why3wc.cma Ocamlc src/ide/gconfig.ml Ocamlc src/ide/ide_utils.ml Linking bin/why3ide.cma Ocamlc src/ide/wserver.ml Linking bin/why3webserver.cma Ocamlc src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 130, characters 6-30: 130 | archived : filter_three; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field archived is never read. (However, this field is used to build or mutate values.) Linking bin/why3session.cma Linking bin/why3shell.cma Linking bin/isabelle_client.byte Linking bin/why3pp.cma Ocamlc src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.ml Linking bin/why3doc.cma make[2]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a dh_installdirs -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") # do nothing make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' debian/rules override_dh_install-arch make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") 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-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") autoconf configure.in:203: warning: The macro `AC_PROG_CC_STDC' is obsolete. configure.in:203: You should run autoupdate. ./lib/autoconf/c.m4:1666: AC_PROG_CC_STDC is expanded from... configure.in:203: the top level 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 the compiler supports GNU C... yes checking whether gcc accepts -g... yes checking for gcc option to enable C11 features... none needed checking for a race-free mkdir -p... /bin/mkdir -p checking for a BSD-compatible install... /usr/bin/install -c checking for ocamlc... ocamlc ocaml version is 4.13.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... no configure: WARNING: Library seq not found. ocamlfind found lablgtk3 in /usr/lib/ocaml/lablgtk3 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 found ocamlgraph in /usr/lib/ocaml/ocamlgraph checking for /usr/lib/ocaml/ocamlgraph/graph.cmi... yes ocamlfind: Package `js_of_ocaml' not found ocamlfind: Package `mlmpfr' not found ocamlfind: Package `ppx_sexp_conv' not found checking for coqc... no configure: WARNING: Cannot find coqc. 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.13.1 Library path : /usr/lib/ocaml Ocamlfind : yes Native compilation : yes Profiling : no Memory profiling : no (disabled by default) PPX : yes S-expr for why3pp : no (requires ppx_sexp_conv) Javascript support : no (js_of_ocaml not found) MPFR support : no (mlmpfr not found) Re support : no (seq not found) Components Why3 library : yes GTK IDE : yes (gtk3) Web IDE : no (Javascript support not available) GMP arithmetic : yes Compressed sessions : yes Hypothesis selection : yes Invariant inference(exp): no (disabled by default) Frama-C support : no (disabled by default) Documentation : no (sphinx-build not found) Support for interactive proof assistants Coq : no (coqc 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.13.1/why3 Relocatable : no make[2]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' debian/rules override_dh_auto_build-arch make[2]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/commands/why3ide.cma: No such file or directory") Fatal error: exception Sys_error("debian/why3/usr/lib/ocaml/why3/plugins/hypothesis_selection.cma: No such file or directory") /usr/bin/make all byte make[3]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' cp src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.ml Ocamldep src/tools/why3pp.ml Ocamldep src/tools/why3pp_sexp.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 Generate src/util/config.ml cp src/util/mysexplib-dummy.ml src/util/mysexplib.ml cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml cp src/util/dynlink_new.ml src/util/dynlink_wrapper.ml cp src/session/compress_z.ml src/session/compress.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_helpers.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/counterexample.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/smtv2_model_parser.ml Ocamldep src/driver/sexp.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/driver/smtv2_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 cp src/util/recompat.ml src/util/re.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/dynlink_wrapper.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/getopt.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 Ocamldep src/util/mysexplib.ml Ocamlc src/util/mysexplib.ml File "src/util/mysexplib.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/mysexplib.ml Ocamlc src/util/config.ml File "src/util/config.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/config.ml Ocamlopt src/util/bigInt.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlopt src/util/loc.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | 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 70, characters 12-26: 70 | 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 Ocamlopt src/util/lexlib.ml Ocamlc src/util/dynlink_wrapper.ml File "src/util/dynlink_wrapper.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/util/dynlink_wrapper.ml Ocamlopt src/util/warning.ml Ocamlopt src/util/number.ml Ocamlopt src/util/constant.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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 32, characters 6-24: 32 | 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/re.ml File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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_ast.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/smtv2_model_defs.ml Ocamlopt src/driver/collect_data_model.ml Ocamlc src/driver/smtv2_model_parser.ml File "src/driver/smtv2_model_parser.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/driver/smtv2_model_parser.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 Ocamlc src/mlw/pinterp.mli Ocamlopt src/mlw/pinterp.ml File "src/mlw/pinterp.ml", line 60, characters 14-28: 60 | let n = Pervasives.max 0 (Array.length a - 25) 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/mlw/pinterp.ml", line 1851, characters 48-62: 1851 | let s = String.(if length s > n then sub s 0 (Pervasives.min n (length s)) ^ "..." else s) 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/mlw/counterexample.mli Ocamlopt src/mlw/counterexample.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/extract/compile.ml Ocamlopt src/extract/mlinterp.ml File "src/extract/mlinterp.ml", line 42, characters 4-18: 42 | env : Env.env; ^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field env is never read. (However, this field is used to build or mutate values.) File "src/extract/mlinterp.ml", line 43, characters 4-33: 43 | mm : Pmodule.pmodule Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field mm is never read. (However, this field is used to build or mutate values.) Ocamlopt src/extract/pdriver.ml Ocamlopt src/extract/ml_printer.ml Ocamlc src/extract/c.ml File "src/extract/c.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/extract/c.ml Ocamlopt src/extract/ocaml.ml Ocamlopt src/extract/cakeml.ml Ocamlc src/parser/ptree.ml File "src/parser/ptree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/parser/ptree.ml Ocamlc src/parser/ptree_helpers.mli Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/parser/glob.ml Ocamlc src/parser/typing.mli Ocamlopt src/parser/typing.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 Ocamlopt src/transform/simplify_formula.ml Ocamlopt src/transform/inlining.ml File "src/transform/inlining.ml", line 98, characters 25-38: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/transform/inlining.ml", line 98, characters 8-21: 98 | let t ?(use_meta=true) ?(in_goal=false) ~notls ~notdef = ^^^^^^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlopt src/transform/split_goal.ml Ocamlc src/transform/args_wrapper.mli 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 Ocamlc src/transform/case.ml File "src/transform/case.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/case.ml Ocamlopt src/transform/apply.ml Ocamlopt src/transform/subst.ml Ocamlopt src/transform/introduction.ml Ocamlc src/transform/ind_itp.mli Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/destruct.ml Ocamlc src/transform/cut.ml File "src/transform/cut.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/transform/cut.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/intro_vc_vars_counterexmp.ml File "src/transform/intro_vc_vars_counterexmp.ml", line 31, characters 2-24: 31 | vc_pre_or_post : bool; ^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field vc_pre_or_post is never read. (However, this field is used to build or mutate values.) 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 File "src/printer/alt_ergo.ml", line 47, characters 2-29: 47 | mutable info_in_goal: bool; ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field info_in_goal is never mutated. File "src/printer/alt_ergo.ml", line 49, characters 2-45: 49 | mutable list_field_def: Ident.ident Mstr.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field list_field_def is never mutated. File "src/printer/alt_ergo.ml", line 51, characters 2-26: 51 | meta_record_def : Sls.t; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field meta_record_def is never read. (However, this field is used to build or mutate values.) 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 File "src/printer/pvs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/simplify.ml Ocamlopt src/printer/gappa.ml File "src/printer/gappa.ml", line 97, characters 2-23: 97 | info_symbols : Sid.t; ^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field info_symbols is never read. (However, this field is used to build or mutate values.) 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 1106, characters 24-42: 1106 | 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 File "src/session/session_itp.ml", line 36, characters 2-41: 36 | mutable theory_parent_name : fileID; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field theory_parent_name is never mutated. File "src/session/session_itp.ml", line 1938, characters 2-30: 1938 | prover_ids : int PHprover.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field prover_ids is never read. (However, this field is used to build or mutate values.) 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 File "src/session/controller_itp.ml", line 570, characters 36-43: 570 | let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification = ^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/session/controller_itp.ml", line 307, characters 4-38: 307 | tp_session : Session_itp.session; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_session is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 308, characters 4-30: 308 | tp_id : proofNodeID; ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_id is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 309, characters 4-33: 309 | tp_pr : Whyconf.prover; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_pr is never read. (However, this field is used to build or mutate values.) 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/bigInt.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlc src/util/loc.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | 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 70, characters 12-26: 70 | 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/number.ml Ocamlc src/util/constant.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 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 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 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 32, characters 6-24: 32 | 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/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/mlw/ity.ml Ocamlc src/mlw/pinterp.ml File "src/mlw/pinterp.ml", line 60, characters 14-28: 60 | let n = Pervasives.max 0 (Array.length a - 25) 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/mlw/pinterp.ml", line 1851, characters 48-62: 1851 | let s = String.(if length s > n then sub s 0 (Pervasives.min n (length s)) ^ "..." else s) 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/mlw/counterexample.ml Ocamlc src/parser/ptree_helpers.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/args_wrapper.ml Ocamlc src/transform/compute.ml Ocamlc src/transform/eliminate_definition.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/apply.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/ind_itp.ml Ocamlc src/transform/destruct.ml Ocamlc src/transform/induction.ml Ocamlc src/transform/induction_pr.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 File "src/session/session_itp.ml", line 36, characters 2-41: 36 | mutable theory_parent_name : fileID; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: mutable record field theory_parent_name is never mutated. File "src/session/session_itp.ml", line 1938, characters 2-30: 1938 | prover_ids : int PHprover.t; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field prover_ids is never read. (However, this field is used to build or mutate values.) Ocamlc src/session/strategy.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.ml File "src/session/controller_itp.ml", line 570, characters 36-43: 570 | let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification = ^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. File "src/session/controller_itp.ml", line 307, characters 4-38: 307 | tp_session : Session_itp.session; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_session is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 308, characters 4-30: 308 | tp_id : proofNodeID; ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_id is never read. (However, this field is used to build or mutate values.) File "src/session/controller_itp.ml", line 309, characters 4-33: 309 | tp_pr : Whyconf.prover; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field tp_pr is never read. (However, this field is used to build or mutate values.) 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 File "plugins/parser/genequlin.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlc plugins/parser/dimacs.ml File "plugins/parser/dimacs.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs Ocamlc plugins/tptp/tptp_ast.ml File "plugins/tptp/tptp_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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 File "plugins/python/py_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_ast.ml Ocamlc plugins/python/py_parser.mli Ocamlopt plugins/python/py_parser.ml Ocamlc plugins/python/py_lexer.ml File "plugins/python/py_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_lexer.ml Ocamlc plugins/python/py_main.ml File "plugins/python/py_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/python/py_main.ml Linking lib/plugins/python.cmxs Ocamlc plugins/microc/mc_ast.ml File "plugins/microc/mc_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_ast.ml Ocamlc plugins/microc/mc_parser.mli Ocamlopt plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_lexer.ml File "plugins/microc/mc_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_lexer.ml Ocamlc plugins/microc/mc_printer.mli Ocamlopt plugins/microc/mc_printer.ml Ocamlc plugins/microc/mc_main.ml File "plugins/microc/mc_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/microc/mc_main.ml Linking lib/plugins/microc.cmxs Ocamlc plugins/cfg/cfg_ast.ml File "plugins/cfg/cfg_ast.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_ast.ml Ocamlc plugins/cfg/cfg_tokens.ml File "plugins/cfg/cfg_tokens.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_tokens.ml Ocamlc plugins/cfg/cfg_parser.mli Ocamlopt plugins/cfg/cfg_parser.ml Ocamlc plugins/cfg/cfg_lexer.ml File "plugins/cfg/cfg_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_lexer.ml Ocamlc plugins/cfg/cfg_main.ml File "plugins/cfg/cfg_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/cfg/cfg_main.ml Linking lib/plugins/cfg.cmxs Ocamlc plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | 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 "plugins/transform/hypothesis_selection.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | 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 Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs Ocamlc src/tools/main.ml File "src/tools/main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/main.ml Linking bin/why3.opt Ocamlc src/tools/why3config.ml File "src/tools/why3config.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3config.ml Linking bin/why3config.cmxs Ocamlc src/tools/why3execute.ml File "src/tools/why3execute.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.cmxs Ocamlc src/tools/why3extract.ml File "src/tools/why3extract.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.cmxs Ocamlc src/tools/why3prove.ml File "src/tools/why3prove.ml", line 446, characters 6-40: 446 | Format.set_formatter_tag_functions Util.ansi_color_tags; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.set_formatter_tag_functions Use Format.set_formatter_stag_functions. File "src/tools/why3prove.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3prove.ml File "src/tools/why3prove.ml", line 446, characters 6-40: 446 | Format.set_formatter_tag_functions Util.ansi_color_tags; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.set_formatter_tag_functions Use Format.set_formatter_stag_functions. Linking bin/why3prove.cmxs Ocamlc src/tools/why3realize.ml File "src/tools/why3realize.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.cmxs Ocamlc src/tools/why3replay.ml File "src/tools/why3replay.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.cmxs Ocamlc src/tools/why3wc.ml File "src/tools/why3wc.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3wc.ml Linking bin/why3wc.cmxs Ocamlc src/ide/gtkcompat.ml File "src/ide/gtkcompat.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/ide/gtkcompat.ml Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlc src/ide/why3ide.ml File "src/ide/why3ide.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/ide/why3ide.ml Linking bin/why3ide.cmxs Ocamlopt src/ide/wserver.ml Ocamlc src/ide/why3web.ml File "src/ide/why3web.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/ide/why3web.ml Linking bin/why3webserver.cmxs Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 130, characters 6-30: 130 | archived : filter_three; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field archived is never read. (However, this field is used to build or mutate values.) Ocamlc src/why3session/why3session_info.ml File "src/why3session/why3session_info.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_info.ml Ocamlc src/why3session/why3session_html.ml File "src/why3session/why3session_html.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_html.ml Ocamlc src/why3session/why3session_latex.ml File "src/why3session/why3session_latex.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_latex.ml Ocamlc src/why3session/why3session_update.ml File "src/why3session/why3session_update.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_update.ml Ocamlc src/why3session/why3session_main.ml File "src/why3session/why3session_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3session/why3session_main.ml Linking bin/why3session.cmxs Ocamlc src/tools/why3shell.ml File "src/tools/why3shell.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3shell.ml Linking bin/why3shell.cmxs Ocamlc src/isabelle-client/isabelle_client_main.ml File "src/isabelle-client/isabelle_client_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/isabelle-client/isabelle_client_main.ml Linking bin/isabelle_client.opt Ocamlc src/tools/why3pp_sexp.ml File "src/tools/why3pp_sexp.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3pp_sexp.ml Ocamlc src/tools/why3pp.ml File "src/tools/why3pp.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/tools/why3pp.ml Linking bin/why3pp.cmxs Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml Ocamlc src/why3doc/doc_lexer.ml File "src/why3doc/doc_lexer.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3doc/doc_lexer.ml Ocamlc src/why3doc/doc_main.ml File "src/why3doc/doc_main.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.cmxs Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Linking lib/plugins/genequlin.cma Linking lib/plugins/dimacs.cma 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.cma Ocamlc plugins/python/py_parser.ml Linking lib/plugins/python.cma Ocamlc plugins/microc/mc_parser.ml Ocamlc plugins/microc/mc_printer.ml Linking lib/plugins/microc.cma Ocamlc plugins/cfg/cfg_parser.ml Linking lib/plugins/cfg.cma Linking lib/plugins/hypothesis_selection.cma Linking lib/why3/why3.cma Linking bin/why3.byte Linking bin/why3config.cma Linking bin/why3execute.cma Linking bin/why3extract.cma Linking bin/why3prove.cma Linking bin/why3realize.cma Linking bin/why3replay.cma Linking bin/why3wc.cma Ocamlc src/ide/gconfig.ml Linking bin/why3ide.cma Ocamlc src/ide/wserver.ml Linking bin/why3webserver.cma Ocamlc src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 130, characters 6-30: 130 | archived : filter_three; ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 69 [unused-field]: record field archived is never read. (However, this field is used to build or mutate values.) Linking bin/why3session.cma Linking bin/why3shell.cma Linking bin/isabelle_client.byte Linking bin/why3pp.cma Ocamlc src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.ml Linking bin/why3doc.cma make[3]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' make[2]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp /usr/bin/make install install-lib DESTDIR=/build/why3-MFGZlp/why3-1.4.1/debian/tmp make[2]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/plugins /usr/bin/install -c -m 644 lib/plugins/genequlin.cma lib/plugins/dimacs.cma lib/plugins/tptp.cma lib/plugins/python.cma lib/plugins/microc.cma lib/plugins/cfg.cma lib/plugins/hypothesis_selection.cma lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/python.cmxs lib/plugins/microc.cmxs lib/plugins/cfg.cmxs lib/plugins/hypothesis_selection.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/plugins /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/bin /usr/bin/install -c bin/why3.opt /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/bin/why3 /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3config.cmxs bin/why3execute.cmxs bin/why3extract.cmxs bin/why3prove.cmxs bin/why3realize.cmxs bin/why3replay.cmxs bin/why3wc.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3 /usr/bin/install -c lib/why3server /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/why3server /usr/bin/install -c lib/why3cpulimit /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/why3cpulimit /usr/bin/install -c lib/why3-call-pvs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/why3-call-pvs /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3webserver.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3session.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3shell.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3pp.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3doc.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3 /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/vim /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/vim/ftdetect /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/vim/syntax /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/lang /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/stdlib /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/stdlib/mach /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 stdlib/*.mlw /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/stdlib /usr/bin/install -c -m 644 stdlib/mach/*.mlw /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/stdlib/mach /usr/bin/install -c -m 644 drivers/*.drv drivers/*.gen /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 LICENSE /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/ /usr/bin/install -c -m 644 share/provers-detection-data.conf /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/ /usr/bin/install -c -m 644 share/why3session.dtd /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3 /usr/bin/install -c -m 644 share/Makefile.config /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3 /usr/bin/install -c -m 644 share/vim/ftdetect/why3.vim /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/vim/ftdetect/why3.vim /usr/bin/install -c -m 644 share/vim/syntax/why3.vim /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/vim/syntax/why3.vim /usr/bin/install -c -m 644 share/lang/why3.lang /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/lang/why3.lang /usr/bin/install -c -m 644 share/lang/why3c.lang /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/lang/why3c.lang /usr/bin/install -c -m 644 share/lang/why3py.lang /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/lang/why3py.lang /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers /usr/bin/install -c -m 644 drivers/coq-realizations.aux /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers/ /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers/ /usr/bin/install -c -m 644 drivers/pvs-realizations.aux /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers/ /usr/bin/install -c -m 644 drivers/isabelle-realizations.aux /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/drivers/ /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/emacs/site-lisp/ /usr/bin/install -c -m 644 share/emacs/why3.el /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/emacs/site-lisp/why3.el /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /usr/bin/install -c -m 644 bin/why3ide.cmxs /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/lib/ocaml/why3/commands /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/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-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/images; \ /bin/mkdir -p /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/images/$d; \ /usr/bin/install -c -m 644 share/images/$d/* /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/images/$d; \ done /usr/bin/install -c -m 644 share/images/*.png /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/share/why3/images 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-MFGZlp/why3-1.4.1/debian/tmp/usr/local/lib/ocaml/4.13.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/why3.cmt \ lib/why3/META /build/why3-MFGZlp/why3-1.4.1/debian/tmp/usr/local/lib/ocaml/4.13.1/why3 make[2]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh_install -a -XLICENSE make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh_ocamldoc -a dh_installdocs -a dh_installchangelogs -a debian/rules override_dh_installexamples make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' 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-MFGZlp/why3-1.4.1' 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-MFGZlp/why3-1.4.1' dh_compress -Xmanual.pdf make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh_fixperms -a dh_missing -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a debian/rules override_dh_ocaml make[1]: Entering directory '/build/why3-MFGZlp/why3-1.4.1' dh_ocaml --nodefined-map=why3:Bigarray,Gaux,Gpointer,Gobject,PangoEnums,Gutf8,Glib,Pango,GdkEnums,Gdk,GDraw,GPango,GdkEvent,GdkPixbuf,GtkEnums,Gtk,GtkObject,GtkSignal,GtkBaseProps,GtkStock,GtkBase,GtkData,OgtkBaseProps,GObj,GtkBinProps,GData,GtkTreeProps,OgtkTreeProps,GtkTextProps,OgtkTextProps,GtkPackProps,OgtkPackProps,GtkMiscProps,OgtkMiscProps,GtkMenuProps,OgtkMenuProps,GtkFileProps,OgtkFileProps,GtkEditProps,OgtkEditProps,GtkContainersProps,OgtkContainersProps,GtkButtonProps,OgtkButtonProps,OgtkBinProps,GtkWindow,GtkTree,GtkMain,GtkText,GtkPack,GtkMisc,GtkMenu,GtkFile,GtkEdit,GtkContainers,GtkButton,GdkKeysyms,GContainer,GPack,GFile,GWindow,GTree,GBin,GButton,GMenu,GEdit,GMain,GMisc,GText,GToolbox,SourceView3Enums,GtkSourceView3Props,OgtkSourceView3Props,GtkSourceView3,GSourceView3,Gtkcompat,Gconfig,Ide_utils,Why3ide,Graph__,Graph__XDotDraw,Graph__Builder,Graph__Dot_parser,Graph__Dot_lexer,Graph__Dot,Graph__Graphviz,Graph__Util,Graph__XDot,Graph__WeakTopological,Graph__Unionfind,Graph__Traverse,Graph__Components,Graph__Heap,Graph__Path,Graph__Topological,Graph__Strat,Graph__Delaunay,Graph__Rand,Graph__Prim,Graph__PersistentQueue,Graph__Blocks,Graph__Persistent,Graph__Classic,Graph__Coloring,Graph__Flow,Graph__Gml,Graph__Bitv,Graph__Imperative,Graph__Kruskal,Graph__Oper,Graph__Pack,Graph__Nonnegative,Graph__Minsep,Graph__Mincut,Graph__Merge,Graph__Gmap,Graph__Cliquetree,Graph__Md,Graph__Mcs_m,Graph__Leaderlist,Graph__Graphml,Graph__ChaoticIteration,Graph__Clique,Graph__Contraction,Graph__DGraphModel,Graph__DGraphRandModel,Graph__DGraphSubTree,Graph__DGraphTreeLayout,Graph__DGraphTreeModel,Graph__Dominator,Graph__Fixpoint,Graph,Hypothesis_selection W: why3 doesn't resolve dependency on unit Glib W: why3 doesn't resolve dependency on unit Gpointer W: why3 doesn't resolve dependency on unit Gconfig W: why3 doesn't resolve dependency on unit GtkSignal W: why3 doesn't resolve dependency on unit Gconfig W: why3 doesn't resolve dependency on unit Ide_utils W: why3 doesn't resolve dependency on unit Gtkcompat W: why3 doesn't resolve dependency on unit GtkSignal W: why3 doesn't resolve dependency on unit Gobject W: why3 doesn't resolve dependency on unit Gobject W: why3 doesn't resolve dependency on unit Gpointer W: why3 doesn't resolve dependency on unit Ide_utils W: why3 doesn't resolve dependency on unit Gutf8 W: why3 doesn't resolve dependency on unit Glib W: why3 doesn't resolve dependency on unit Gaux W: why3 doesn't resolve dependency on unit Gutf8 W: why3 doesn't resolve dependency on unit Gaux make[1]: Leaving directory '/build/why3-MFGZlp/why3-1.4.1' dh_gencontrol -a 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.4.1-2_amd64.deb'. dpkg-deb: building package 'why3-dbgsym' in '../why3-dbgsym_1.4.1-2_amd64.deb'. dpkg-deb: building package 'libwhy3-ocaml-dev' in '../libwhy3-ocaml-dev_1.4.1-2_amd64.deb'. dpkg-deb: building package 'libwhy3-ocaml-dev-dbgsym' in '../libwhy3-ocaml-dev-dbgsym_1.4.1-2_amd64.deb'. dpkg-genbuildinfo --build=any -O../why3_1.4.1-2_amd64.buildinfo dpkg-genchanges --build=any -O../why3_1.4.1-2_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-MFGZlp /tmp/why3-1.4.1-2tyks87a7 I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.OEKzH7xirO... I: success in 960.5985 seconds md5: libwhy3-ocaml-dev-dbgsym_1.4.1-2_amd64.deb: OK md5: libwhy3-ocaml-dev_1.4.1-2_amd64.deb: OK md5: why3-dbgsym_1.4.1-2_amd64.deb: OK md5: why3_1.4.1-2_amd64.deb: OK sha1: libwhy3-ocaml-dev-dbgsym_1.4.1-2_amd64.deb: OK sha1: libwhy3-ocaml-dev_1.4.1-2_amd64.deb: OK sha1: why3-dbgsym_1.4.1-2_amd64.deb: OK sha1: why3_1.4.1-2_amd64.deb: OK sha256: libwhy3-ocaml-dev-dbgsym_1.4.1-2_amd64.deb: OK sha256: libwhy3-ocaml-dev_1.4.1-2_amd64.deb: OK sha256: why3-dbgsym_1.4.1-2_amd64.deb: OK sha256: why3_1.4.1-2_amd64.deb: OK Checksums: OK