=> Building math/why3-spark build started at Wed Oct 5 16:11:03 PDT 2016 port directory: /usr/ports/math/why3-spark building for: DragonFly pkgbox64.dragonflybsd.org 4.7-DEVELOPMENT DragonFly v4.7.0.78.g7d868-DEVELOPMENT #7: Mon Aug 1 22:25:32 PDT 2016 root@pkgbox64.dragonflybsd.org:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64 maintained by: ports@FreeBSD.org ident warning: no id keywords in /build/boomdata/data/.m/bleeding-edge-default/ref/../07//usr/ports/math/why3-spark/Makefile Makefile ident: Poudriere version: 3.1-pre Host OSVERSION: 400700 Jail OSVERSION: 400702 !!! Jail is newer than host. (Jail: 400702, Host: 400700) !!! !!! This is not supported. !!! !!! Host kernel must be same or newer than jail. !!! !!! Expect build failures. !!! ---Begin Environment--- STATUS=1 SAVED_TERM=screen MASTERMNT=/build/boomdata/data/.m/bleeding-edge-default/ref PATH=/usr/local/libexec/poudriere:/sbin:/bin:/usr/sbin:/usr/bin:/usr/pkg/bin:/usr/pkg/sbin:/usr/games:/usr/local/sbin:/usr/local/bin:/usr/pkg/xorg/bin:/usr/X11R6/bin:/root/bin:/sbin:/usr/sbin POUDRIERE_BUILD_TYPE=bulk PKGNAME=why3-spark-2016 OLDPWD=/root/boom PWD=/build/boomdata/data/.m/bleeding-edge-default/ref/.p/pool MASTERNAME=bleeding-edge-default TERM=cons25 USER=root HOME=/root POUDRIERE_VERSION=3.1-pre LOCALBASE=/usr/local PACKAGE_BUILDING=yes ---End Environment--- ---Begin OPTIONS List--- ---End OPTIONS List--- --CONFIGURE_ARGS-- --enable-relocation --disable-doc --disable-pvs-libs --disable-profiling --disable-coq-tactic --disable-coq-libs --disable-isabelle-libs --prefix=/usr/local ${_LATE_CONFIGURE_ARGS} --End CONFIGURE_ARGS-- --CONFIGURE_ENV-- MAKE=gmake XDG_DATA_HOME=/wrkdirs/math/why3-spark XDG_CONFIG_HOME=/wrkdirs/math/why3-spark HOME=/wrkdirs/math/why3-spark TMPDIR="/tmp" SHELL=/bin/sh CONFIG_SHELL=/bin/sh CCVER=gcc50 CONFIG_SITE=/usr/ports/Templates/config.site lt_cv_sys_max_cmd_len=262144 --End CONFIGURE_ENV-- --MAKE_ENV-- XDG_DATA_HOME=/wrkdirs/math/why3-spark XDG_CONFIG_HOME=/wrkdirs/math/why3-spark HOME=/wrkdirs/math/why3-spark TMPDIR="/tmp" NO_PIE=yes MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES CCVER=gcc50 PREFIX=/usr/local LOCALBASE=/usr/local LIBDIR="/usr/lib" NOPROFILE=1 CC="cc" CFLAGS="-pipe -O2 -fno-strict-aliasing" CPP="cpp" CPPFLAGS="" LDFLAGS="" LIBS="" CXX="c++" CXXFLAGS=" -pipe -O2 -fno-strict-aliasing" MANPREFIX="/usr/local" BSD_INSTALL_PROGRAM="install -s -m 555" BSD_INSTALL_LIB="install -s -m 444" BSD_INSTALL_SCRIPT="install -m 555" BSD_INSTALL_DATA="install -m 0644" BSD_INSTALL_MAN="install -m 444" --End MAKE_ENV-- --PLIST_SUB-- OCAML_SITELIBDIR="lib/ocaml/site-lib" GTK2_VERSION="2.10.0" GTK3_VERSION="3.0.0" OSREL=4.7 PREFIX=%D LOCALBASE=/usr/local RESETPREFIX=/usr/local PORTDOCS="" PORTEXAMPLES="" LIB32DIR=lib PROFILE="@comment " DOCSDIR="share/doc/why3" EXAMPLESDIR="share/examples/why3" DATADIR="share/why3" WWWDIR="www/why3" ETCDIR="etc/why3" --End PLIST_SUB-- --SUB_LIST-- PREFIX=/usr/local LOCALBASE=/usr/local DATADIR=/usr/local/share/why3 DOCSDIR=/usr/local/share/doc/why3 EXAMPLESDIR=/usr/local/share/examples/why3 WWWDIR=/usr/local/www/why3 ETCDIR=/usr/local/etc/why3 --End SUB_LIST-- ---Begin make.conf--- USE_PACKAGE_DEPENDS=yes BATCH=yes WRKDIRPREFIX=/wrkdirs NO_BACKUP=yes USE_PACKAGE_DEPENDS=yes PKG_CREATE_VERBOSE=yes BATCH=yes WRKDIRPREFIX=/wrkdirs PORT_DBDIR=/options PORTSDIR=/usr/ports PACKAGES=/packages DISTDIR=/distfiles MAKE_JOBS_NUMBER=5 ---End make.conf--- =================================================== ===> NOTICE: The why3 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Only useful for deprecated lang/spark. It is scheduled to be removed on or after 2016-09-30. ===> License LGPL21 GPLv3 accepted by the user =========================================================================== =================================================== ===> why3-spark-2016 depends on file: /usr/local/sbin/pkg - not found ===> Installing existing package /packages/All/pkg-1.8.7_3.txz Installing pkg-1.8.7_3... Extracting pkg-1.8.7_3: .......... done ===> why3-spark-2016 depends on file: /usr/local/sbin/pkg - found ===> Returning to build of why3-spark-2016 =========================================================================== =================================================== =========================================================================== =================================================== ===> NOTICE: The why3 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Only useful for deprecated lang/spark. It is scheduled to be removed on or after 2016-09-30. ===> License LGPL21 GPLv3 accepted by the user ===> Fetching all distfiles required by why3-spark-2016 for building =========================================================================== =================================================== ===> NOTICE: The why3 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Only useful for deprecated lang/spark. It is scheduled to be removed on or after 2016-09-30. ===> License LGPL21 GPLv3 accepted by the user ===> Fetching all distfiles required by why3-spark-2016 for building => SHA256 Checksum OK for why3-for-spark-gpl-2016-src.tar.gz. =========================================================================== =================================================== ===> why3-spark-2016 depends on file: /usr/local/bin/ocamlc - not found ===> Installing existing package /packages/All/ocaml-4.02.3.txz Installing ocaml-4.02.3... `-- Installing libX11-1.6.3,1... | `-- Installing xproto-7.0.28... | `-- Extracting xproto-7.0.28: .......... done | `-- Installing kbproto-1.0.7... | `-- Extracting kbproto-1.0.7: .......... done | `-- Installing libXdmcp-1.1.2... | `-- Extracting libXdmcp-1.1.2: ......... done | `-- Installing libxcb-1.11.1... | | `-- Installing libxml2-2.9.4... | | `-- Extracting libxml2-2.9.4: .......... done | | `-- Installing libpthread-stubs-0.3_6... | | `-- Extracting libpthread-stubs-0.3_6: ..... done | | `-- Installing libXau-1.0.8_3... | | `-- Extracting libXau-1.0.8_3: .......... done | `-- Extracting libxcb-1.11.1: .......... done `-- Extracting libX11-1.6.3,1: .......... done Extracting ocaml-4.02.3: .......... done ===> why3-spark-2016 depends on file: /usr/local/bin/ocamlc - found ===> Returning to build of why3-spark-2016 =========================================================================== =================================================== ===> NOTICE: The why3 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Only useful for deprecated lang/spark. It is scheduled to be removed on or after 2016-09-30. ===> License LGPL21 GPLv3 accepted by the user ===> Fetching all distfiles required by why3-spark-2016 for building ===> Extracting for why3-spark-2016 => SHA256 Checksum OK for why3-for-spark-gpl-2016-src.tar.gz. =========================================================================== =================================================== ===> why3-spark-2016 depends on file: /usr/local/bin/ocamlc - found =========================================================================== =================================================== ===> Patching for why3-spark-2016 =========================================================================== =================================================== ===> why3-spark-2016 depends on executable: menhir - not found ===> Installing existing package /packages/All/menhir-20160303.txz Installing menhir-20160303... `-- Installing ocaml-findlib-1.6.2... | `-- Installing ocaml-labltk-8.06.0... | | `-- Installing tk85-8.5.19... | | `-- Installing libXft-2.3.2_1... | | | `-- Installing fontconfig-2.12.1,1... | | | `-- Installing expat-2.2.0... | | | `-- Extracting expat-2.2.0: .......... done | | | `-- Installing freetype2-2.6.3... | | | `-- Extracting freetype2-2.6.3: .......... done | | | `-- Extracting fontconfig-2.12.1,1: .......... done Running fc-cache to build fontconfig cache... /usr/local/share/fonts: skipping, no such directory /usr/local/lib/X11/fonts: skipping, no such directory /var/db/fontconfig: cleaning cache directory fc-cache: succeeded | | | `-- Installing libXrender-0.9.9... | | | `-- Installing renderproto-0.11.1... | | | `-- Extracting renderproto-0.11.1: .... done | | | `-- Extracting libXrender-0.9.9: .......... done | | `-- Extracting libXft-2.3.2_1: ......... done | | `-- Installing tcl85-8.5.19... | | `-- Extracting tcl85-8.5.19: .......... done | | `-- Installing libXScrnSaver-1.2.2_3... | | | `-- Installing libXext-1.3.3_1,1... | | | `-- Installing xextproto-7.3.0... | | | `-- Extracting xextproto-7.3.0: .......... done | | | `-- Extracting libXext-1.3.3_1,1: .......... done | | | `-- Installing scrnsaverproto-1.2.2... | | | `-- Extracting scrnsaverproto-1.2.2: ... done | | `-- Extracting libXScrnSaver-1.2.2_3: .......... done | | `-- Extracting tk85-8.5.19: .......... done | `-- Extracting ocaml-labltk-8.06.0: .......... done `-- Extracting ocaml-findlib-1.6.2: .......... done Extracting menhir-20160303: .......... done Message from menhir-20160303: ===> NOTICE: The menhir port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> why3-spark-2016 depends on executable: menhir - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on package: ocaml-zip>1 - not found ===> Installing existing package /packages/All/ocaml-zip-1.05.txz Installing ocaml-zip-1.05... Extracting ocaml-zip-1.05: .......... done Message from ocaml-zip-1.05: ===> NOTICE: The ocaml-zip port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> why3-spark-2016 depends on package: ocaml-zip>1 - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on package: ocaml-zarith>1.2 - not found ===> Installing existing package /packages/All/ocaml-zarith-1.2.1.txz Installing ocaml-zarith-1.2.1... `-- Installing gmp-5.1.3_3... | `-- Installing indexinfo-0.2.5... | `-- Extracting indexinfo-0.2.5: .... done `-- Extracting gmp-5.1.3_3: .......... done Extracting ocaml-zarith-1.2.1: .......... done Message from ocaml-zarith-1.2.1: ===> NOTICE: The ocaml-zarith port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> why3-spark-2016 depends on package: ocaml-zarith>1.2 - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on executable: lablgtk2 - not found ===> Installing existing package /packages/All/ocaml-lablgtk2-2.18.3.txz Installing ocaml-lablgtk2-2.18.3... `-- Installing pango-1.38.0_1... | `-- Installing encodings-1.0.4_3,1... | | `-- Installing font-util-1.3.1... | | `-- Extracting font-util-1.3.1: .......... done | `-- Extracting encodings-1.0.4_3,1: .......... done | `-- Installing harfbuzz-1.3.2... | | `-- Installing cairo-1.14.6_1,2... | | `-- Installing glproto-1.4.17... | | `-- Extracting glproto-1.4.17: ...... done | | `-- Installing libEGL-11.2.2... | | | `-- Installing libdevq-0.0.2_1... | | | `-- Extracting libdevq-0.0.2_1: ....... done | | | `-- Installing libXdamage-1.1.4_3... | | | `-- Installing libXfixes-5.0.1_3... | | | | `-- Installing fixesproto-5.0... | | | | `-- Extracting fixesproto-5.0: .... done | | | `-- Extracting libXfixes-5.0.1_3: .......... done | | | `-- Installing damageproto-1.2.1... | | | `-- Extracting damageproto-1.2.1: .... done | | | `-- Extracting libXdamage-1.1.4_3: ...... done | | | `-- Installing libxshmfence-1.2... | | | `-- Extracting libxshmfence-1.2: ......... done | | | `-- Installing gbm-11.2.2... | | | `-- Installing libglapi-11.2.2... | | | | `-- Installing libXvMC-1.0.9... | | | | `-- Installing libXv-1.0.10_3,1... | | | | | `-- Installing videoproto-2.3.2... | | | | | `-- Extracting videoproto-2.3.2: ...... done | | | | `-- Extracting libXv-1.0.10_3,1: .......... done | | | | `-- Extracting libXvMC-1.0.9: .......... done | | | | `-- Installing libdrm-2.4.66,1... | | | | `-- Installing libpciaccess-0.13.4... | | | | | `-- Installing pciids-20160621... | | | | | `-- Extracting pciids-20160621: ..... done | | | | `-- Extracting libpciaccess-0.13.4: ...... done | | | | `-- Extracting libdrm-2.4.66,1: .......... done | | | | `-- Installing libelf-0.8.13_1... | | | | `-- Installing gettext-runtime-0.19.8.1... | | | | `-- Extracting gettext-runtime-0.19.8.1: .......... done | | | | `-- Extracting libelf-0.8.13_1: .......... done | | | `-- Extracting libglapi-11.2.2: ... done | | | `-- Extracting gbm-11.2.2: ..... done | | | `-- Installing llvm37-3.7.1_3... | | | `-- Installing python27-2.7.12... | | | | `-- Installing readline-6.3.8... | | | | `-- Installing ncurses-6.0_5... | | | | `-- Extracting ncurses-6.0_5: .......... done | | | | `-- Extracting readline-6.3.8: .......... done | | | | `-- Installing libffi-3.2.1... | | | | `-- Extracting libffi-3.2.1: .......... done | | | | `-- Installing libressl-2.4.3... | | | | `-- Extracting libressl-2.4.3: .......... done | | | `-- Extracting python27-2.7.12: .......... done | | | `-- Installing perl5-5.20.3_15... | | | `-- Extracting perl5-5.20.3_15: .......... done | | | `-- Installing libedit-3.1.20150325_2,1... | | | `-- Extracting libedit-3.1.20150325_2,1: .......... done | | | `-- Extracting llvm37-3.7.1_3: .......... done | | `-- Extracting libEGL-11.2.2: .......... done | | `-- Installing libGL-11.2.2... | | | `-- Installing dri2proto-2.8... | | | `-- Extracting dri2proto-2.8: .... done | | | `-- Installing libXxf86vm-1.1.4_1... | | | `-- Installing xf86vidmodeproto-2.3.1... | | | `-- Extracting xf86vidmodeproto-2.3.1: .... done | | | `-- Extracting libXxf86vm-1.1.4_1: .......... done | | `-- Extracting libGL-11.2.2: .......... done | | `-- Installing xcb-util-renderutil-0.3.9_1... | | | `-- Installing xcb-util-0.4.0_1,1... | | | `-- Extracting xcb-util-0.4.0_1,1: .......... done | | `-- Extracting xcb-util-renderutil-0.3.9_1: ...... done | | `-- Installing png-1.6.23... | | `-- Extracting png-1.6.23: .......... done | | `-- Installing pixman-0.34.0... | | `-- Extracting pixman-0.34.0: .......... done | | `-- Installing glib-2.46.2_3... | | | `-- Installing libiconv-1.14_9... | | | `-- Extracting libiconv-1.14_9: .......... done | | | `-- Installing pcre-8.39... | | | `-- Extracting pcre-8.39: .......... done | | `-- Extracting glib-2.46.2_3: .......... done No schema files found: doing nothing. | | `-- Extracting cairo-1.14.6_1,2: .......... done | | `-- Installing icu-57.1,1... | | `-- Extracting icu-57.1,1: .......... done | | `-- Installing graphite2-1.3.8... | | `-- Extracting graphite2-1.3.8: .......... done | `-- Extracting harfbuzz-1.3.2: .......... done | `-- Installing xorg-fonts-truetype-7.7_1... | | `-- Installing font-misc-meltho-1.0.3_3... | | `-- Installing mkfontdir-1.0.7... | | | `-- Installing mkfontscale-1.1.2... | | | `-- Installing libfontenc-1.1.3... | | | `-- Extracting libfontenc-1.1.3: ...... done | | | `-- Extracting mkfontscale-1.1.2: .. done | | `-- Extracting mkfontdir-1.0.7: .. done | | `-- Extracting font-misc-meltho-1.0.3_3: .......... done | | `-- Installing font-bh-ttf-1.0.3_3... | | `-- Extracting font-bh-ttf-1.0.3_3: .......... done | | `-- Installing font-misc-ethiopic-1.0.3_3... | | `-- Extracting font-misc-ethiopic-1.0.3_3: ... done | | `-- Installing dejavu-2.35... | | `-- Extracting dejavu-2.35: .......... done `-- Extracting pango-1.38.0_1: .......... done `-- Installing gconf2-3.2.6_4... | `-- Installing gtk2-2.24.29_2... | | `-- Installing hicolor-icon-theme-0.15... | | `-- Extracting hicolor-icon-theme-0.15: . done | | `-- Installing gtk-update-icon-cache-2.24.29... | | `-- Installing libXcursor-1.1.14_3... | | `-- Extracting libXcursor-1.1.14_3: .......... done | | `-- Installing libXinerama-1.1.3_3,1... | | | `-- Installing xineramaproto-1.2.1... | | | `-- Extracting xineramaproto-1.2.1: .. done | | `-- Extracting libXinerama-1.1.3_3,1: .......... done | | `-- Installing libXcomposite-0.4.4_3,1... | | | `-- Installing compositeproto-0.4.2... | | | `-- Extracting compositeproto-0.4.2: .... done | | `-- Extracting libXcomposite-0.4.4_3,1: .......... done | | `-- Installing libXi-1.7.6,1... | | | `-- Installing inputproto-2.3.1... | | | `-- Extracting inputproto-2.3.1: ..... done | | `-- Extracting libXi-1.7.6,1: .......... done | | `-- Installing atk-2.18.0... | | `-- Extracting atk-2.18.0: .......... done | | `-- Installing libXrandr-1.5.0... | | | `-- Installing randrproto-1.5.0... | | | `-- Extracting randrproto-1.5.0: .... done | | `-- Extracting libXrandr-1.5.0: .......... done | | `-- Installing gdk-pixbuf2-2.32.3_1... | | | `-- Installing jasper-1.900.1_16... | | | `-- Installing jpeg-turbo-1.4.2... | | | `-- Extracting jpeg-turbo-1.4.2: .......... done | | | `-- Extracting jasper-1.900.1_16: .......... done | | | `-- Installing libXt-1.1.5,1... | | | `-- Installing libSM-1.2.2_3,1... | | | | `-- Installing libICE-1.0.9_1,1... | | | | `-- Extracting libICE-1.0.9_1,1: .......... done | | | `-- Extracting libSM-1.2.2_3,1: .......... done | | | `-- Extracting libXt-1.1.5,1: .......... done | | | `-- Installing tiff-4.0.6_2... | | | `-- Installing jbigkit-2.1_1... | | | `-- Extracting jbigkit-2.1_1: .......... done | | | `-- Extracting tiff-4.0.6_2: .......... done | | `-- Extracting gdk-pixbuf2-2.32.3_1: .......... done | | `-- Installing shared-mime-info-1.5... | | `-- Extracting shared-mime-info-1.5: .......... done | | `-- Extracting gtk-update-icon-cache-2.24.29: .... done | | `-- Installing cups-2.1.4... | | `-- Installing avahi-app-0.6.31_5... | | | `-- Installing gnome_subr-1.0... | | | `-- Extracting gnome_subr-1.0: . done | | | `-- Installing gobject-introspection-1.46.0... | | | `-- Installing python2-2_3... | | | `-- Extracting python2-2_3: ...... done | | | `-- Extracting gobject-introspection-1.46.0: .......... done | | | `-- Installing gdbm-1.12... | | | `-- Extracting gdbm-1.12: .......... done | | | `-- Installing libdaemon-0.14_1... | | | `-- Extracting libdaemon-0.14_1: .......... done | | | `-- Installing dbus-glib-0.104... | | | `-- Installing dbus-1.8.20... ===> Creating groups. Creating group 'messagebus' with gid '556'. ===> Creating users Creating user 'messagebus' with uid '556'. | | | `-- Extracting dbus-1.8.20: ......... done | | | `-- Extracting dbus-glib-0.104: .......... done ===> Creating groups. Creating group 'avahi' with gid '558'. ===> Creating users Creating user 'avahi' with uid '558'. | | `-- Extracting avahi-app-0.6.31_5: .......... done | | `-- Installing gnutls-3.4.15... | | | `-- Installing nettle-3.2... | | | `-- Extracting nettle-3.2: .......... done | | | `-- Installing ca_root_nss-3.27... | | | `-- Extracting ca_root_nss-3.27: ....... done | | | `-- Installing libtasn1-4.9... | | | `-- Extracting libtasn1-4.9: .......... done | | | `-- Installing trousers-0.3.13_1... | | | `-- Installing tpm-emulator-0.7.4_1... ===> Creating groups. Creating group '_tss' with gid '601'. ===> Creating users Creating user '_tss' with uid '601'. | | | `-- Extracting tpm-emulator-0.7.4_1: ......... done ===> Creating groups. Using existing group '_tss'. ===> Creating users Using existing user '_tss'. | | | `-- Extracting trousers-0.3.13_1: .......... done | | | `-- Installing p11-kit-0.23.2... | | | `-- Extracting p11-kit-0.23.2: .......... done | | | `-- Installing libidn-1.33_1... | | | `-- Extracting libidn-1.33_1: .......... done | | `-- Extracting gnutls-3.4.15: .......... done | | `-- Installing libpaper-1.1.24.4... | | `-- Extracting libpaper-1.1.24.4: .......... done ===> Creating groups. Creating group 'cups' with gid '193'. ===> Creating users Creating user 'cups' with uid '193'. | | `-- Extracting cups-2.1.4: .......... done | | `-- Installing python-2.7_2,2... | | `-- Extracting python-2.7_2,2: ..... done | `-- Extracting gtk2-2.24.29_2: .......... done | `-- Installing ORBit2-2.14.19_1... | | `-- Installing libIDL-0.8.14_2... | | `-- Extracting libIDL-0.8.14_2: ......... done | `-- Extracting ORBit2-2.14.19_1: .......... done | `-- Installing polkit-0.113_1... | | `-- Installing spidermonkey170-17.0.0_1... | | `-- Installing nspr-4.13... | | `-- Extracting nspr-4.13: .......... done | | `-- Extracting spidermonkey170-17.0.0_1: .......... done ===> Creating groups. Creating group 'polkitd' with gid '565'. ===> Creating users Creating user 'polkitd' with uid '565'. | `-- Extracting polkit-0.113_1: ........ done | `-- Installing dconf-0.24.0_1... | `-- Extracting dconf-0.24.0_1: .......... done `-- Extracting gconf2-3.2.6_4: .......... done `-- Installing esound-0.2.41_3... | `-- Installing pkgconf-1.0.1... | `-- Extracting pkgconf-1.0.1: .......... done | `-- Installing libaudiofile-0.3.6_3... | | `-- Installing flac-1.3.1_2... | | `-- Installing libogg-1.3.2_1,4... | | `-- Extracting libogg-1.3.2_1,4: .......... done | | `-- Extracting flac-1.3.1_2: .......... done | `-- Extracting libaudiofile-0.3.6_3: .......... done `-- Extracting esound-0.2.41_3: .......... done `-- Installing gtkspell-2.0.16_5... | `-- Installing enchant-1.6.0_5... | | `-- Installing hunspell-1.3.3... | | `-- Extracting hunspell-1.3.3: .......... done | `-- Extracting enchant-1.6.0_5: .......... done `-- Extracting gtkspell-2.0.16_5: .......... done `-- Installing gtkglarea-2.0.1_6... | `-- Installing libGLU-9.0.0_2... | `-- Extracting libGLU-9.0.0_2: ...... done `-- Extracting gtkglarea-2.0.1_6: ........ done `-- Installing gtksourceview2-2.10.5_4... `-- Extracting gtksourceview2-2.10.5_4: .......... done `-- Installing libgsf-1.14.36... `-- Extracting libgsf-1.14.36: .......... done `-- Installing gnome-mime-data-2.18.0_5... `-- Extracting gnome-mime-data-2.18.0_5: .......... done `-- Installing libart_lgpl-2.3.21_2,1... `-- Extracting libart_lgpl-2.3.21_2,1: .......... done `-- Installing librsvg2-2.40.16... | `-- Installing libcroco-0.6.11... | `-- Extracting libcroco-0.6.11: .......... done `-- Extracting librsvg2-2.40.16: .......... done `-- Installing libgnome-2.32.0_3... | `-- Installing libbonobo-2.32.0_2... | | `-- Installing popt-1.16_1... | | `-- Extracting popt-1.16_1: .......... done | `-- Extracting libbonobo-2.32.0_2: .......... done | `-- Installing libXpm-3.5.11_4... | `-- Extracting libXpm-3.5.11_4: .......... done | `-- Installing libcanberra-0.30_3... | | `-- Installing libvorbis-1.3.5,3... | | `-- Extracting libvorbis-1.3.5,3: .......... done | | `-- Installing libltdl-2.4.6... | | `-- Extracting libltdl-2.4.6: .......... done | `-- Extracting libcanberra-0.30_3: .......... done | `-- Installing gnome-vfs-2.24.4_4... | | `-- Installing gamin-0.1.10_8... | | `-- Extracting gamin-0.1.10_8: .......... done | | `-- Installing samba36-libsmbclient-3.6.25_2... | | `-- Installing talloc-2.1.6... | | `-- Extracting talloc-2.1.6: .......... done | | `-- Installing tdb-1.3.9,1... | | `-- Extracting tdb-1.3.9,1: .......... done | | `-- Installing tevent-0.9.28... | | `-- Extracting tevent-0.9.28: .......... done | | `-- Extracting samba36-libsmbclient-3.6.25_2: .......... done | `-- Extracting gnome-vfs-2.24.4_4: .......... done | `-- Installing rarian-0.8.1_4... | | `-- Installing bash-4.3.46_1... | | `-- Extracting bash-4.3.46_1: .......... done | | `-- Installing docbook-xsl-1.76.1_3... | | `-- Installing docbook-1.5... | | | `-- Installing sdocbook-xml-1.1_2,2... | | | `-- Installing xmlcatmgr-2.2_2... | | | `-- Extracting xmlcatmgr-2.2_2: ......... done + Creating /usr/local/share/sgml/catalog + Registering CATALOG catalog.ports (SGML) + Creating /usr/local/share/sgml/catalog.ports + Creating /usr/local/share/xml/catalog + Registering nextCatalog catalog.ports (XML) + Creating /usr/local/share/xml/catalog.ports | | | `-- Extracting sdocbook-xml-1.1_2,2: .......... done | | | `-- Installing docbook-sgml-4.5_1... | | | `-- Installing iso8879-1986_3... | | | `-- Extracting iso8879-1986_3: .......... done | | | `-- Extracting docbook-sgml-4.5_1: .......... done | | | `-- Installing docbook-xml-5.0_3... | | | `-- Installing xmlcharent-0.3_2... | | | `-- Extracting xmlcharent-0.3_2: .......... done | | | `-- Extracting docbook-xml-5.0_3: .......... done | | `-- Extracting docbook-xsl-1.76.1_3: .......... done | | `-- Installing libxslt-1.1.29... | | `-- Installing libgcrypt-1.7.3... | | | `-- Installing libgpg-error-1.24... | | | `-- Extracting libgpg-error-1.24: .......... done | | `-- Extracting libgcrypt-1.7.3: .......... done | | `-- Extracting libxslt-1.1.29: .......... done | | `-- Installing getopt-1.1.6... | | `-- Extracting getopt-1.1.6: .......... done | `-- Extracting rarian-0.8.1_4: .......... done `-- Extracting libgnome-2.32.0_3: .......... done `-- Installing ocaml-lablgl-1.05,1... | `-- Installing freeglut-3.0.0... | `-- Extracting freeglut-3.0.0: .......... done | `-- Installing libXmu-1.1.2_3,1... | `-- Extracting libXmu-1.1.2_3,1: .......... done `-- Extracting ocaml-lablgl-1.05,1: .......... done `-- Installing libgnomeui-2.24.4_5... | `-- Installing gnome-icon-theme-3.12.0_1... | | `-- Installing gnome-icon-theme-symbolic-3.12.0... | | `-- Extracting gnome-icon-theme-symbolic-3.12.0: .......... done | `-- Extracting gnome-icon-theme-3.12.0_1: .......... done | `-- Installing libgnomecanvas-2.30.3_3... | | `-- Installing libglade2-2.6.4_8... | | `-- Extracting libglade2-2.6.4_8: .......... done | `-- Extracting libgnomecanvas-2.30.3_3: .......... done | `-- Installing libbonoboui-2.24.4_3... | `-- Extracting libbonoboui-2.24.4_3: .......... done | `-- Installing startup-notification-0.12_4... | `-- Extracting startup-notification-0.12_4: .......... done | `-- Installing gvfs-1.26.3_2... | | `-- Installing libsecret-0.18.4... | | `-- Extracting libsecret-0.18.4: .......... done | | `-- Installing gcr-3.18.0... | | `-- Installing desktop-file-utils-0.22_3... | | `-- Extracting desktop-file-utils-0.22_3: .......... done | | `-- Installing gtk3-3.18.8_3... | | | `-- Installing colord-1.2.11_1... | | | `-- Installing lcms2-2.7_2... | | | `-- Extracting lcms2-2.7_2: .......... done | | | `-- Installing argyllcms-1.7.0_1... | | | `-- Extracting argyllcms-1.7.0_1: .......... done | | | `-- Installing sqlite3-3.14.1_1... | | | `-- Extracting sqlite3-3.14.1_1: .......... done ===> Creating groups. Creating group 'colord' with gid '970'. ===> Creating users Creating user 'colord' with uid '970'. | | | `-- Extracting colord-1.2.11_1: .......... done | | | `-- Installing libepoxy-1.3.1... | | | `-- Installing libglesv2-11.2.2... | | | `-- Extracting libglesv2-11.2.2: .......... done | | | `-- Extracting libepoxy-1.3.1: .......... done | | | `-- Installing at-spi2-atk-2.18.1... | | | `-- Installing at-spi2-core-2.18.3... | | | | `-- Installing libXtst-1.2.2_3... | | | | `-- Installing recordproto-1.14.2... | | | | `-- Extracting recordproto-1.14.2: .... done | | | | `-- Extracting libXtst-1.2.2_3: .......... done | | | `-- Extracting at-spi2-core-2.18.3: .......... done | | | `-- Extracting at-spi2-atk-2.18.1: .......... done | | | `-- Installing adwaita-icon-theme-3.18.0... | | | `-- Extracting adwaita-icon-theme-3.18.0: .......... done | | `-- Extracting gtk3-3.18.8_3: .......... done | | `-- Extracting gcr-3.18.0: .......... done | | `-- Installing libarchive-3.2.1,1... | | `-- Installing liblz4-131... | | `-- Extracting liblz4-131: .......... done | | `-- Installing lzo2-2.09... | | `-- Extracting lzo2-2.09: .......... done | | `-- Extracting libarchive-3.2.1,1: .......... done | | `-- Installing libsoup-gnome-2.52.2... | | `-- Installing glib-networking-2.46.1_1... | | | `-- Installing libproxy-0.4.12... | | | `-- Extracting libproxy-0.4.12: ........ done | | | `-- Installing gsettings-desktop-schemas-3.18.1... | | | `-- Installing cantarell-fonts-0.0.24... | | | `-- Extracting cantarell-fonts-0.0.24: ...... done | | | `-- Extracting gsettings-desktop-schemas-3.18.1: .......... done | | `-- Extracting glib-networking-2.46.1_1: .......... done | | `-- Installing libsoup-2.52.2... | | `-- Extracting libsoup-2.52.2: .......... done | | `-- Extracting libsoup-gnome-2.52.2: ......... done | `-- Extracting gvfs-1.26.3_2: .......... done | `-- Installing libgnome-keyring-3.12.0_2... | `-- Extracting libgnome-keyring-3.12.0_2: .......... done `-- Extracting libgnomeui-2.24.4_5: .......... done Extracting ocaml-lablgtk2-2.18.3: .......... done Message from ncurses-6.0_5: ===> NOTICE: The ncurses port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port Message from python27-2.7.12: =========================================================================== Note that some standard Python modules are provided as separate ports as they require additional dependencies. They are available as: bsddb databases/py-bsddb gdbm databases/py-gdbm sqlite3 databases/py-sqlite3 tkinter x11-toolkits/py-tkinter =========================================================================== Message from perl5-5.20.3_15: The /usr/bin/perl symlink has been removed starting with Perl 5.20. For shebangs, you should either use: #!/usr/local/bin/perl or #!/usr/bin/env perl The first one will only work if you have a /usr/local/bin/perl, the second will work as long as perl is in PATH. Message from dejavu-2.35: Make sure that the freetype module is loaded. If it is not, add the following line to the "Modules" section of your X Windows configuration file: Load "freetype" Add the following line to the "Files" section of X Windows configuration file: FontPath "/usr/local/share/fonts/dejavu/" Note: your X Windows configuration file is typically /etc/X11/XF86Config if you are using XFree86, and /etc/X11/xorg.conf if you are using X.Org. Message from ca_root_nss-3.27: ********************************* WARNING ********************************* FreeBSD does not, and can not warrant that the certification authorities whose certificates are included in this package have in any way been audited for trustworthiness or RFC 3647 compliance. Assessment and verification of trust is the complete responsibility of the system administrator. *********************************** NOTE ********************************** This package installs symlinks to support root certificates discovery by default for software that uses OpenSSL. This enables SSL Certificate Verification by client software without manual intervention. If you prefer to do this manually, replace the following symlinks with either an empty file or your site-local certificate bundle. * /etc/ssl/cert.pem * /usr/local/etc/ssl/cert.pem * /usr/local/openssl/cert.pem *************************************************************************** Message from trousers-0.3.13_1: To run tcsd automatically, add the following line to /etc/rc.conf: tcsd_enable="YES" You might want to edit /usr/local/etc/tcsd.conf to reflect your setup. If you want to use tcsd with software TPM emulator, use the following configuration in /etc/rc.conf: tcsd_enable="YES" tcsd_mode="emulator" tpmd_enable="YES" To use TPM, add your_account to '_tss' group like following: # pw groupmod _tss -m your_account Message from esound-0.2.41_3: The ESounD daemon (esd) must be started on a per-user basis. This is typically done by the Session Manager in GNOME. However, if you are not using the GNOME Desktop, you will need to add something like the following to your X Windows initialization script: esd -terminate -nobeeps -as 2 Message from gamin-0.1.10_8: =============================================================================== Gamin will only provide realtime notification of changes for at most n files, where n is the minimum value between (kern.maxfiles * 0.7) and (kern.maxfilesperproc - 200). Beyond that limit, files will be polled. If you often open several large folders with Nautilus, you might want to increase the kern.maxfiles tunable (you do not need to set kern.maxfilesperproc, since it is computed at boot time from kern.maxfiles). For a typical desktop, add the following line to /boot/loader.conf, then reboot the system: kern.maxfiles="25000" The behavior of gamin can be controlled via the various gaminrc files. See http://www.gnome.org/~veillard/gamin/config.html on how to create these files. In particular, if you find gam_server is taking up too much CPU time polling for changes, something like the following may help in one of the gaminrc files: # reduce polling frequency to once per 10 seconds # for UFS file systems in order to lower CPU load fsset ufs poll 10 =============================================================================== ===> NOTICE: The gamin port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port Message from samba36-libsmbclient-3.6.25_2: ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: not supported by the upstream. It is scheduled to be removed on or after 2016-04-01. Message from xmlcatmgr-2.2_2: The following catalogs are installed: 1) /usr/local/share/sgml/catalog The top level catalog for SGML stuff. It is not changed by any ports/packages except textproc/xmlcatmgr. 2) /usr/local/share/sgml/catalog.ports This catalog is for handling SGML stuff installed under /usr/local/share/sgml. It is changed by ports/packages. 3) /usr/local/share/xml/catalog The top level catalog for XML stuff. It is not changed by any ports/packages except textproc/xmlcatmgr. 4) /usr/local/share/xml/catalog.ports This catalog is for handling XML stuff installed under /usr/local/share/xml. It is changed by ports/packages. Message from freeglut-3.0.0: Joystick support is untested and it is unknown if it works. Do not hesitate to contact x11@FreeBSD.org if this causes issues. Message from ocaml-lablgl-1.05,1: ===> NOTICE: The ocaml-lablgl port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port Message from ocaml-lablgtk2-2.18.3: ===> NOTICE: The ocaml-lablgtk2 port currently does not have a maintainer. As a result, it is more likely to have unresolved issues, not be up-to-date, or even be removed in the future. To volunteer to maintain this port, please create an issue at: https://bugs.freebsd.org/bugzilla More information about port maintainership is available at: https://www.freebsd.org/doc/en/articles/contributing/ports-contributing.html#maintain-port ===> why3-spark-2016 depends on executable: lablgtk2 - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on package: ocaml-sqlite3>2 - not found ===> Installing existing package /packages/All/ocaml-sqlite3-4.0.5.txz Installing ocaml-sqlite3-4.0.5... Extracting ocaml-sqlite3-4.0.5: .......... done ===> why3-spark-2016 depends on package: ocaml-sqlite3>2 - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on package: ocaml-ocamlgraph>1.8 - not found ===> Installing existing package /packages/All/ocaml-ocamlgraph-1.8.7.txz Installing ocaml-ocamlgraph-1.8.7... Extracting ocaml-ocamlgraph-1.8.7: .......... done ===> why3-spark-2016 depends on package: ocaml-ocamlgraph>1.8 - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on executable: camlp5o - not found ===> Installing existing package /packages/All/ocaml-camlp5-6.16.txz Installing ocaml-camlp5-6.16... Extracting ocaml-camlp5-6.16: .......... done ===> why3-spark-2016 depends on executable: camlp5o - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on file: /usr/local/bin/ocamlc - found ===> why3-spark-2016 depends on executable: gmake - not found ===> Installing existing package /packages/All/gmake-4.2.1_1.txz Installing gmake-4.2.1_1... Extracting gmake-4.2.1_1: .......... done ===> why3-spark-2016 depends on executable: gmake - found ===> Returning to build of why3-spark-2016 ===> why3-spark-2016 depends on executable: msgfmt - not found ===> Installing existing package /packages/All/gettext-tools-0.19.8.1.txz Installing gettext-tools-0.19.8.1... Extracting gettext-tools-0.19.8.1: .......... done ===> why3-spark-2016 depends on executable: msgfmt - found ===> Returning to build of why3-spark-2016 =========================================================================== =================================================== ===> why3-spark-2016 depends on shared library: libfontconfig.so - found (/usr/local/lib/libfontconfig.so) ===> why3-spark-2016 depends on shared library: libfreetype.so - found (/usr/local/lib/libfreetype.so) ===> why3-spark-2016 depends on shared library: libintl.so - found (/usr/local/lib/libintl.so) ===> why3-spark-2016 depends on shared library: libatk-1.0.so - found (/usr/local/lib/libatk-1.0.so) ===> why3-spark-2016 depends on shared library: libcairo.so - found (/usr/local/lib/libcairo.so) ===> why3-spark-2016 depends on shared library: libgdk_pixbuf-2.0.so - found (/usr/local/lib/libgdk_pixbuf-2.0.so) ===> why3-spark-2016 depends on shared library: libglib-2.0.so - found (/usr/local/lib/libglib-2.0.so) ===> why3-spark-2016 depends on shared library: libgtk-x11-2.0.so - found (/usr/local/lib/libgtk-x11-2.0.so) ===> why3-spark-2016 depends on shared library: libgtksourceview-2.0.so - found (/usr/local/lib/libgtksourceview-2.0.so) ===> why3-spark-2016 depends on shared library: libxml2.so - found (/usr/local/lib/libxml2.so) ===> why3-spark-2016 depends on shared library: libpango-1.0.so - found (/usr/local/lib/libpango-1.0.so) =========================================================================== =================================================== ===> Configuring for why3-spark-2016 configure: loading site script /usr/ports/Templates/config.site checking executable suffix... checking for gcc... cc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether we are using the GNU C compiler... yes checking whether cc accepts -g... yes checking for cc option to accept ISO C89... none needed checking for ocp-ocamlc... no checking for ocamlc... ocamlc ocaml version is 4.02.3 ocaml library path is /usr/local/lib/ocaml checking for ocp-ocamlopt... no checking for ocamlopt... ocamlopt checking ocamlopt version... ok checking for ocp-ocamlc.opt... no checking for ocamlc.opt... ocamlc.opt checking ocamlc.opt version... ok checking for ocp-ocamlopt.opt... no 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... yes checking for emacs... no ocamlfind found zarith in /usr/local/lib/ocaml/site-lib/zarith ocamlfind found camlzip in /usr/local/lib/ocaml/site-lib/zip ocamlfind found menhirLib in /usr/local/lib/ocaml/site-lib/menhirLib ocamlfind found lablgtk2 in /usr/local/lib/ocaml/site-lib/lablgtk2 ocamlfind found lablgtksourceview2 in /usr/local/lib/ocaml/site-lib/lablgtk2 configure: WARNING: coq support disabled configure: WARNING: PVS support disabled configure: WARNING: Isabelle support disabled ocamlfind: Package `ocamlgraph' not found checking for /usr/local/lib/ocaml/ocamlgraph/... yes configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating doc/version.tex config.status: creating lib/why3/META config.status: creating .merlin config.status: creating src/jessie/Makefile config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.02.3 Library path : /usr/local/lib/ocaml Native compilation : yes Profiling : no Components IDE command : yes GMP arithmetic : yes Compressed sessions : yes MenhirLib support : yes Hypothesis selection : yes Frama-C support : no (disabled by default) Documentation : no Support for interactive proof assistants Coq : no (disabled by user) PVS : no (disabled by user) Isabelle : no (disabled by user) Installable : yes Binary path : ${exec_prefix}/bin Lib path : ${exec_prefix}/lib/why3 Data path : ${prefix}/share/why3 Ocaml Library : /usr/local/lib/ocaml/site-lib/why3 Relocatable : yes =========================================================================== =================================================== ===> Building for why3-spark-2016 gmake[1]: Entering directory '/wrkdirs/math/why3-spark/why3-for-spark-gpl-2016-src' Ocamllex src/why3doc/doc_lexer.mll 112 states, 1119 transitions, table size 5148 bytes 1707 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 lib/ocaml/why3__BigInt_zarith.ml lib/ocaml/why3__BigInt_compat.ml Ocamldep lib/ocaml/why3__Matrix.ml Ocamldep lib/ocaml/why3__Array.ml Ocamldep lib/ocaml/why3__IntAux.ml Ocamldep lib/ocaml/why3__BigInt.ml Ocamldep lib/ocaml/why3__BigInt_compat.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/why3session/why3session_csv.ml Ocamldep src/why3session/why3session_run.ml Ocamldep src/why3session/why3session_output.ml Ocamldep src/why3session/why3session_rm.ml Ocamldep src/why3session/why3session_html.ml Ocamldep src/why3session/why3session_latex.ml Ocamldep src/why3session/why3session_info.ml Ocamldep src/why3session/why3session_copy.ml Ocamldep src/why3session/why3session_lib.ml Ocamldep src/ide/gmain.ml Ocamldep src/ide/gconfig.ml ocamldep.opt -slash -I lib/why3 -I src -I src/util -I src/gnat src/gnat/gnat_util.ml src/gnat/gnat_loc.ml src/gnat/gnat_expl.ml src/gnat/gnat_config.ml src/gnat/gnat_sched.ml src/gnat/gnat_manual.ml src/gnat/gnat_objectives.ml src/gnat/gnat_report.ml src/gnat/gnat_main.ml src/gnat/gnat_util.mli src/gnat/gnat_loc.mli src/gnat/gnat_expl.mli src/gnat/gnat_config.mli src/gnat/gnat_sched.mli src/gnat/gnat_manual.mli src/gnat/gnat_objectives.mli src/gnat/gnat_report.mli src/gnat/gnat_main.mli > .depend.gnat Ocamllex src/tools/why3wc.mll 298 states, 15365 transitions, table size 63248 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 Warning: you are using the standard library and/or the %inline keyword. We recommend switching on --infer in order to avoid obscure type error messages. Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings 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 16 states, 260 transitions, table size 1136 bytes Ocamllex src/parser/lexer.mll 128 states, 3284 transitions, table size 13904 bytes 7458 additional bytes used for bindings Menhir src/parser/parser.mly Warning: you are using the standard library and/or the %inline keyword. We recommend switching on --infer in order to avoid obscure type error messages. Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 29 states, 1101 transitions, table size 4578 bytes Menhir src/driver/parse_smtv2_model_parser.mly Ocamllex src/driver/parse_smtv2_model_lexer.mll 47 states, 833 transitions, table size 3614 bytes 1740 additional bytes used for bindings cp src/session/compress_z.ml src/session/compress.ml Ocamllex src/session/xml.mll 114 states, 1396 transitions, table size 6268 bytes 3538 additional bytes used for bindings Ocamllex src/session/strategy_parser.mll 39 states, 619 transitions, table size 2710 bytes 1755 additional bytes used for bindings Ocamldep src/session/session_scheduler.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/strategy.ml Ocamldep src/session/session_tools.ml Ocamldep src/session/session.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.ml Ocamldep src/session/compress.ml Ocamldep src/whyml/mlw_interp.ml Ocamldep src/whyml/mlw_main.ml Ocamldep src/whyml/mlw_ocaml.ml Ocamldep src/whyml/mlw_exec.ml Ocamldep src/whyml/mlw_driver.ml Ocamldep src/whyml/mlw_typing.ml Ocamldep src/whyml/mlw_dexpr.ml Ocamldep src/whyml/mlw_module.ml Ocamldep src/whyml/mlw_wp.ml Ocamldep src/whyml/mlw_pretty.ml Ocamldep src/whyml/mlw_decl.ml Ocamldep src/whyml/mlw_expr.ml Ocamldep src/whyml/mlw_ty.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/transform/eliminate_unused_hypo.ml Ocamldep src/transform/gnat_split_disj.ml Ocamldep src/transform/gnat_split_conj.ml Ocamldep src/transform/eliminate_bounded_types.ml Ocamldep src/transform/rec_logic.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/eval_match.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/intro_vc_vars_counterexmp.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/introduction.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_algebraic.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/ity.ml Ocamldep src/driver/parse_smtv2_model.ml Ocamldep src/driver/parse_smtv2_model_lexer.ml Ocamldep src/driver/parse_smtv2_model_parser.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/decl.ml Ocamldep src/core/pattern.ml Ocamldep src/core/term.ml Ocamldep src/core/ty.ml Ocamldep src/core/ident.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/number.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/plugin.ml Ocamldep src/util/rc.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/warning.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/loc.ml Ocamldep src/util/debug.ml Ocamldep src/util/json.ml Ocamldep src/util/pp.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/stdlib.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/extset.ml Ocamldep src/util/extmap.ml Ocamldep src/util/strings.ml Ocamldep src/util/lists.ml Ocamldep src/util/opt.ml Ocamldep src/util/util.ml Ocamldep src/util/config.ml Ocamlopt src/util/config.ml Ocamlc src/util/bigInt.mli Ocamlopt src/util/bigInt.ml Ocamlc src/util/util.mli Ocamlopt src/util/util.ml Ocamlc src/util/opt.mli Ocamlopt src/util/opt.ml Ocamlc src/util/lists.mli Ocamlopt src/util/lists.ml Ocamlc src/util/strings.mli Ocamlopt src/util/strings.ml Ocamlc src/util/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/hashcons.mli Ocamlopt src/util/hashcons.ml Ocamlc src/util/stdlib.mli Ocamlopt src/util/stdlib.ml Ocamlc src/util/exn_printer.mli Ocamlopt src/util/exn_printer.ml Ocamlc src/util/pp.mli Ocamlopt src/util/pp.ml Ocamlc src/util/json.mli Ocamlopt src/util/json.ml Ocamlc src/util/debug.mli Ocamlopt src/util/debug.ml Ocamlc src/util/loc.mli Ocamlopt src/util/loc.ml Ocamlc src/util/lexlib.mli Ocamlopt src/util/lexlib.ml Ocamlc src/util/print_tree.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/cmdline.mli Ocamlopt src/util/cmdline.ml Ocamlc src/util/warning.mli Ocamlopt src/util/warning.ml Ocamlc src/util/sysutil.mli Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli Ocamlopt src/util/rc.ml Ocamlc src/util/plugin.mli Ocamlopt src/util/plugin.ml Ocamlc src/util/number.mli Ocamlopt src/util/number.ml Ocamlc src/util/pqueue.mli Ocamlopt src/util/pqueue.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 Ocamlc src/core/pattern.mli Ocamlopt src/core/pattern.ml Ocamlc src/core/decl.mli Ocamlopt src/core/decl.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 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/parse_smtv2_model_parser.mli Ocamlopt src/driver/parse_smtv2_model_parser.ml Ocamlopt src/driver/parse_smtv2_model_lexer.ml Ocamlopt src/driver/parse_smtv2_model.ml Ocamlc src/mlw/ity.mli Ocamlopt src/mlw/ity.ml Ocamlc src/mlw/expr.mli Ocamlopt src/mlw/expr.ml Ocamlc src/mlw/dexpr.mli Ocamlopt src/mlw/dexpr.ml Ocamlc src/mlw/pdecl.mli Ocamlopt src/mlw/pdecl.ml Ocamlc src/mlw/pmodule.mli Ocamlopt src/mlw/pmodule.ml Ocamlopt src/parser/ptree.ml Ocamlc src/parser/glob.mli Ocamlopt src/parser/glob.ml Ocamlc src/parser/parser.mli Ocamlopt src/parser/parser.ml Ocamlc src/parser/typing.mli Ocamlopt src/parser/typing.ml Ocamlc src/parser/lexer.mli Ocamlopt src/parser/lexer.ml Ocamlc src/transform/simplify_formula.mli Ocamlopt src/transform/simplify_formula.ml Ocamlc src/transform/inlining.mli Ocamlopt src/transform/inlining.ml Ocamlc src/transform/split_goal.mli Ocamlopt src/transform/split_goal.ml Ocamlc src/transform/induction.mli Ocamlopt src/transform/induction.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 File "src/transform/eliminate_algebraic.ml", line 307, characters 18-20: Warning 3: deprecated: Pervasives.or Use (||) instead. 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/introduction.mli Ocamlopt src/transform/introduction.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/intro_vc_vars_counterexmp.mli Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlc src/transform/eval_match.mli Ocamlopt src/transform/eval_match.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/induction_pr.mli Ocamlopt src/transform/induction_pr.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/rec_logic.ml Ocamlc src/transform/eliminate_bounded_types.mli Ocamlopt src/transform/eliminate_bounded_types.ml Ocamlc src/transform/gnat_split_conj.mli Ocamlopt src/transform/gnat_split_conj.ml Ocamlc src/transform/gnat_split_disj.mli Ocamlopt src/transform/gnat_split_disj.ml Ocamlopt src/transform/eliminate_unused_hypo.ml Ocamlc src/printer/alt_ergo.mli Ocamlopt src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.mli Ocamlopt src/printer/why3printer.ml Ocamlc src/printer/smtv1.mli Ocamlopt src/printer/smtv1.ml Ocamlc src/printer/smtv2.mli Ocamlopt src/printer/smtv2.ml Ocamlc src/printer/coq.mli Ocamlopt src/printer/coq.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlc src/printer/simplify.mli Ocamlopt src/printer/simplify.ml Ocamlc src/printer/gappa.mli Ocamlopt src/printer/gappa.ml Ocamlc src/printer/cvc3.mli Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/printer/mathematica.ml Ocamlc src/whyml/mlw_ty.mli Ocamlopt src/whyml/mlw_ty.ml Ocamlc src/whyml/mlw_expr.mli Ocamlopt src/whyml/mlw_expr.ml Ocamlc src/whyml/mlw_decl.mli Ocamlopt src/whyml/mlw_decl.ml Ocamlc src/whyml/mlw_pretty.mli Ocamlopt src/whyml/mlw_pretty.ml Ocamlc src/whyml/mlw_wp.mli Ocamlopt src/whyml/mlw_wp.ml Ocamlc src/whyml/mlw_module.mli Ocamlopt src/whyml/mlw_module.ml Ocamlc src/whyml/mlw_dexpr.mli Ocamlopt src/whyml/mlw_dexpr.ml Ocamlc src/whyml/mlw_typing.mli Ocamlopt src/whyml/mlw_typing.ml Ocamlc src/whyml/mlw_driver.mli Ocamlopt src/whyml/mlw_driver.ml Ocamlc src/whyml/mlw_exec.mli Ocamlopt src/whyml/mlw_exec.ml Ocamlc src/whyml/mlw_ocaml.mli Ocamlopt src/whyml/mlw_ocaml.ml Ocamlc src/whyml/mlw_main.mli Ocamlopt src/whyml/mlw_main.ml Ocamlc src/whyml/mlw_interp.mli Ocamlopt src/whyml/mlw_interp.ml Ocamlc src/session/compress.mli Ocamlopt src/session/compress.ml Ocamlc src/session/xml.mli Ocamlopt src/session/xml.ml Ocamlc src/session/termcode.mli Ocamlopt src/session/termcode.ml Ocamlc src/session/session.mli Ocamlopt src/session/session.ml Ocamlc src/session/session_tools.mli Ocamlopt src/session/session_tools.ml Ocamlc src/session/strategy.mli Ocamlopt src/session/strategy.ml Ocamlc src/session/strategy_parser.mli Ocamlopt src/session/strategy_parser.ml Ocamlc src/session/session_scheduler.mli Ocamlopt src/session/session_scheduler.ml Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml Linking lib/plugins/genequlin.cmxs Ocamlopt plugins/parser/dimacs.ml Linking lib/plugins/dimacs.cmxs 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 Ocamlopt plugins/transform/hypothesis_selection.ml Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Ocamlopt src/tools/main.ml Linking bin/why3.opt Ocamlopt src/tools/why3config.ml Linking bin/why3config.opt Ocamlopt src/tools/why3execute.ml Linking bin/why3execute.opt Ocamlopt src/tools/why3extract.ml Linking bin/why3extract.opt Ocamlopt src/tools/why3prove.ml Linking bin/why3prove.opt Ocamlopt src/tools/why3realize.ml Linking bin/why3realize.opt Ocamlopt src/tools/why3replay.ml Linking bin/why3replay.opt Ocamlopt src/tools/why3wc.ml Linking bin/why3wc.opt Ocamlc src/gnat/gnat_util.mli Ocamlopt src/gnat/gnat_util.ml Ocamlc src/gnat/gnat_loc.mli Ocamlopt src/gnat/gnat_loc.ml Ocamlc src/util/config.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/util.ml Ocamlc src/util/opt.ml Ocamlc src/util/lists.ml Ocamlc src/util/strings.ml Ocamlc src/util/extmap.ml Ocamlc src/util/extset.ml Ocamlc src/util/exthtbl.ml Ocamlc src/util/weakhtbl.ml Ocamlc src/util/hashcons.ml Ocamlc src/util/stdlib.ml Ocamlc src/util/exn_printer.ml Ocamlc src/util/pp.ml Ocamlc src/util/json.ml Ocamlc src/util/debug.ml Ocamlc src/util/loc.ml 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/pqueue.ml Ocamlc src/core/ident.ml Ocamlc src/core/ty.ml Ocamlc src/core/term.ml Ocamlc src/core/pattern.ml Ocamlc src/core/decl.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_ast.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/parse_smtv2_model_parser.ml Ocamlc src/driver/parse_smtv2_model_lexer.ml Ocamlc src/driver/parse_smtv2_model.ml Ocamlc src/mlw/ity.ml Ocamlc src/mlw/expr.ml Ocamlc src/mlw/dexpr.ml Ocamlc src/mlw/pdecl.ml Ocamlc src/mlw/pmodule.ml Ocamlc src/parser/ptree.ml Ocamlc src/parser/glob.ml Ocamlc src/parser/parser.ml Ocamlc src/parser/typing.ml Ocamlc src/parser/lexer.ml Ocamlc src/transform/simplify_formula.ml Ocamlc src/transform/inlining.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/induction.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 File "src/transform/eliminate_algebraic.ml", line 307, characters 18-20: Warning 3: deprecated: Pervasives.or Use (||) instead. 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/introduction.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/intro_vc_vars_counterexmp.ml Ocamlc src/transform/prepare_for_counterexmp.ml Ocamlc src/transform/eval_match.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/rec_logic.ml Ocamlc src/transform/eliminate_bounded_types.ml Ocamlc src/transform/gnat_split_conj.ml Ocamlc src/transform/gnat_split_disj.ml Ocamlc src/transform/eliminate_unused_hypo.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.ml Ocamlc src/printer/smtv1.ml Ocamlc src/printer/smtv2.ml Ocamlc src/printer/coq.ml Ocamlc src/printer/pvs.ml Ocamlc src/printer/isabelle.ml Ocamlc src/printer/simplify.ml Ocamlc src/printer/gappa.ml Ocamlc src/printer/cvc3.ml Ocamlc src/printer/yices.ml Ocamlc src/printer/mathematica.ml Ocamlc src/whyml/mlw_ty.ml Ocamlc src/whyml/mlw_expr.ml Ocamlc src/whyml/mlw_decl.ml Ocamlc src/whyml/mlw_pretty.ml Ocamlc src/whyml/mlw_wp.ml Ocamlc src/whyml/mlw_module.ml Ocamlc src/whyml/mlw_dexpr.ml Ocamlc src/whyml/mlw_typing.ml Ocamlc src/whyml/mlw_driver.ml Ocamlc src/whyml/mlw_exec.ml Ocamlc src/whyml/mlw_ocaml.ml Ocamlc src/whyml/mlw_main.ml Ocamlc src/whyml/mlw_interp.ml Ocamlc src/session/compress.ml Ocamlc src/session/xml.ml Ocamlc src/session/termcode.ml Ocamlc src/session/session.ml Ocamlc src/session/session_tools.ml Ocamlc src/session/strategy.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/session_scheduler.ml Linking lib/why3/why3.cmo Ocamlc src/gnat/gnat_expl.mli Ocamlopt src/gnat/gnat_expl.ml Ocamlc src/gnat/gnat_config.mli Ocamlopt src/gnat/gnat_config.ml Ocamlc src/gnat/gnat_sched.mli Ocamlopt src/gnat/gnat_sched.ml Ocamlc src/gnat/gnat_manual.mli Ocamlopt src/gnat/gnat_manual.ml Ocamlc src/gnat/gnat_objectives.mli Ocamlopt src/gnat/gnat_objectives.ml Ocamlc src/gnat/gnat_report.mli Ocamlopt src/gnat/gnat_report.ml Ocamlopt src/gnat/gnat_main.ml Linking bin/gnatwhy3.opt cc -c -Wall -g -o src/server/logging.o src/server/logging.c cc -c -Wall -g -o src/server/arraylist.o src/server/arraylist.c cc -c -Wall -g -o src/server/options.o src/server/options.c cc -c -Wall -g -o src/server/queue.o src/server/queue.c cc -c -Wall -g -o src/server/readbuf.o src/server/readbuf.c cc -c -Wall -g -o src/server/request.o src/server/request.c cc -c -Wall -g -o src/server/writebuf.o src/server/writebuf.c cc -c -Wall -g -o src/server/server-unix.o src/server/server-unix.c cc -c -Wall -g -o src/server/server-win.o src/server/server-win.c cc -Wall -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/writebuf.o src/server/server-unix.o src/server/server-win.o cc -c -Wall -g -o src/server/cpulimit-unix.o src/server/cpulimit-unix.c cc -c -Wall -g -o src/server/cpulimit-win.o src/server/cpulimit-win.c cc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Ocamlc src/ide/resetgc.c Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml Ocamlopt src/ide/gmain.ml Linking bin/why3ide.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml Ocamlopt src/why3session/why3session_copy.ml Ocamlopt src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_rm.ml Ocamlopt src/why3session/why3session_output.ml Ocamlopt src/why3session/why3session_run.ml Ocamlopt src/why3session/why3session_csv.ml Ocamlopt src/why3session/why3session_main.ml Linking bin/why3session.opt echo "(* generated automatically at compilation time *)" > drivers/coq-realizations.aux echo "(* generated automatically at compilation time *)" > drivers/pvs-realizations.aux echo "(* generated automatically at compilation time *)" > drivers/isabelle-realizations.aux Ocamlopt lib/ocaml/why3__BigInt_compat.ml Ocamlopt lib/ocaml/why3__BigInt.ml Ocamlopt lib/ocaml/why3__IntAux.ml Ocamlopt lib/ocaml/why3__Array.ml Ocamlopt lib/ocaml/why3__Matrix.ml Linking lib/why3/why3extract.cmx Linking lib/why3/why3extract.cmxa Ocamlc src/why3doc/doc_html.mli Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml Ocamlopt src/why3doc/doc_lexer.ml Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.opt gmake[1]: Leaving directory '/wrkdirs/math/why3-spark/why3-for-spark-gpl-2016-src' =========================================================================== =================================================== ===> why3-spark-2016 depends on file: /usr/local/bin/ocamlc - found =========================================================================== =================================================== ===> Staging for why3-spark-2016 ===> Generating temporary packing list gmake[1]: Entering directory '/wrkdirs/math/why3-spark/why3-for-spark-gpl-2016-src' rm -rf /wrkdirs/math/why3-spark/stage/usr/local/lib/why3 rm -rf /wrkdirs/math/why3-spark/stage/usr/local/share/why3 rm -rf /wrkdirs/math/why3-spark/stage/usr/local/lib/ocaml/site-lib/why3 rm -f /wrkdirs/math/why3-spark/stage/usr/local/share/emacs/site-lisp/why3.el rm -f /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3config /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3execute /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3extract /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3prove /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3realize /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3replay /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3wc /wrkdirs/math/why3-spark/stage/usr/local/bin/why3 rm -f /wrkdirs/math/why3-spark/stage/usr/local/bin/why3bench /wrkdirs/math/why3-spark/stage/usr/local/bin/why3replayer rm -f /wrkdirs/math/why3-spark/stage/usr/local/bin/why3ide rm -f /wrkdirs/math/why3-spark/stage/usr/local/bin/why3session rm -f /wrkdirs/math/why3-spark/stage/usr/local/bin/why3doc if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/bin mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/lib/why3 mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3 mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/images mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/vim mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/lang mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/theories mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/modules/mach mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/why3/drivers mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/share/emacs/site-lisp/ cp -f theories/*.why /wrkdirs/math/why3-spark/stage/usr/local/share/why3/theories cp -f modules/*.mlw /wrkdirs/math/why3-spark/stage/usr/local/share/why3/modules cp -f modules/mach/*.mlw /wrkdirs/math/why3-spark/stage/usr/local/share/why3/modules/mach cp -f drivers/*.drv drivers/*.gen /wrkdirs/math/why3-spark/stage/usr/local/share/why3/drivers cp -f LICENSE /wrkdirs/math/why3-spark/stage/usr/local/share/why3/ cp -f share/provers-detection-data.conf /wrkdirs/math/why3-spark/stage/usr/local/share/why3/ for i in share/images/*.rc; do \ d=`basename $i .rc`; \ cp -f $i /wrkdirs/math/why3-spark/stage/usr/local/share/why3/images; \ mkdir /wrkdirs/math/why3-spark/stage/usr/local/share/why3/images/$d; \ cp -f share/images/$d/* /wrkdirs/math/why3-spark/stage/usr/local/share/why3/images/$d; \ done cp -f share/images/*.png /wrkdirs/math/why3-spark/stage/usr/local/share/why3/images cp -f share/why3session.dtd /wrkdirs/math/why3-spark/stage/usr/local/share/why3 cp -f share/vim/why3.vim /wrkdirs/math/why3-spark/stage/usr/local/share/why3/vim/why3.vim cp -f share/lang/why3.lang /wrkdirs/math/why3-spark/stage/usr/local/share/why3/lang/why3.lang cp -f share/emacs/why3.el /wrkdirs/math/why3-spark/stage/usr/local/share/emacs/site-lisp/why3.el mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/plugins cp -f lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/hypothesis_selection.cmxs /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/plugins cp -f bin/why3.opt /wrkdirs/math/why3-spark/stage/usr/local/bin/why3 cp -f bin/why3config.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3config cp -f bin/why3execute.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3execute cp -f bin/why3extract.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3extract cp -f bin/why3prove.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3prove cp -f bin/why3realize.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3realize cp -f bin/why3replay.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3replay cp -f bin/why3wc.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3wc cp -f bin/gnatwhy3.opt /wrkdirs/math/why3-spark/stage/usr/local/bin/gnatwhy3 cp -f lib/why3server /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/why3server cp -f lib/why3cpulimit /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/why3cpulimit cp -f lib/why3-call-pvs /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/why3-call-pvs cp -f bin/why3ide.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3ide cp -f bin/why3session.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3session cp drivers/coq-realizations.aux /wrkdirs/math/why3-spark/stage/usr/local/share/why3/drivers/ cp drivers/pvs-realizations.aux /wrkdirs/math/why3-spark/stage/usr/local/share/why3/drivers/ cp drivers/isabelle-realizations.aux /wrkdirs/math/why3-spark/stage/usr/local/share/why3/drivers/ cp -f bin/why3doc.opt /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3doc # if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then cp -f share/bash/why3 /etc/bash_completion.d; fi mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/lib/ocaml/site-lib/why3 cp -f lib/why3/why3.a lib/why3/why3.cmx lib/why3/why3.cmi lib/why3/why3.cmxa \ lib/why3/META /wrkdirs/math/why3-spark/stage/usr/local/lib/ocaml/site-lib/why3 mkdir -p /wrkdirs/math/why3-spark/stage/usr/local/lib/ocaml/site-lib/why3 cp -f lib/why3/why3extract.a lib/why3/why3extract.cmx lib/why3/why3extract.cmi lib/why3/why3extract.cmxa \ /wrkdirs/math/why3-spark/stage/usr/local/lib/ocaml/site-lib/why3 gmake[1]: Leaving directory '/wrkdirs/math/why3-spark/why3-for-spark-gpl-2016-src' /usr/bin/strip /wrkdirs/math/why3-spark/stage/usr/local/bin/*why3 /usr/bin/strip /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/why3server /usr/bin/strip /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/why3cpulimit /usr/bin/strip /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/commands/why3* /usr/bin/strip /wrkdirs/math/why3-spark/stage/usr/local/lib/why3/plugins/*.cmxs ====> Compressing man pages (compress-man) =========================================================================== =================================================== ===> Building package for why3-spark-2016 file sizes/checksums [178]: .. done packing files [178]: .. done packing directories [0]: . done =========================================================================== => Cleaning up wrkdir ===> Cleaning for why3-spark-2016 build of math/why3-spark ended at Wed Oct 5 16:16:23 PDT 2016 build time: 00:05:20