------------------------------------------------------------------------------- -- Phase: setup ------------------------------------------------------------------------------- Installing /packages/All/libXau-1.0.9.txz Installing /packages/All/libxml2-2.9.10.txz Installing /packages/All/libpthread-stubs-0.4.txz Installing /packages/All/xorgproto-2020.1.txz Installing /packages/All/libXdmcp-1.1.3.txz Installing /packages/All/libxcb-1.13.1.txz Installing /packages/All/libX11-1.6.9_1,1.txz Installing /packages/All/ocaml-4.05.0_1.txz Installing /packages/All/indexinfo-0.3.1.txz Installing /packages/All/gmp-6.2.0.txz Installing /packages/All/freetype2-2.10.1.txz ===== Message from freetype2-2.10.1: -- The 2.7.x series now uses the new subpixel hinting mode (V40 port's option) as the default, emulating a modern version of ClearType. This change inevitably leads to different rendering results, and you might change port's options to adapt it to your taste (or use the new "FREETYPE_PROPERTIES" environment variable). The environment variable "FREETYPE_PROPERTIES" can be used to control the driver properties. Example: FREETYPE_PROPERTIES=truetype:interpreter-version=35 \ cff:no-stem-darkening=1 \ autofitter:warping=1 This allows to select, say, the subpixel hinting mode at runtime for a given application. If LONG_PCF_NAMES port's option was enabled, the PCF family names may include the foundry and information whether they contain wide characters. For example, "Sony Fixed" or "Misc Fixed Wide", instead of "Fixed". This can be disabled at run time with using pcf:no-long-family-names property, if needed. Example: FREETYPE_PROPERTIES=pcf:no-long-family-names=1 How to recreate fontconfig cache with using such environment variable, if needed: # env FREETYPE_PROPERTIES=pcf:no-long-family-names=1 fc-cache -fsv The controllable properties are listed in the section "Controlling FreeType Modules" in the reference's table of contents (/usr/local/share/doc/freetype2/reference/site/index.html, if documentation was installed). Installing /packages/All/expat-2.2.8.txz Installing /packages/All/gettext-runtime-0.20.2.txz Installing /packages/All/fontconfig-2.13.92_2,1.txz Running fc-cache to build fontconfig cache... Font directories: /usr/local/share/fonts /usr/local/lib/X11/fonts /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 /packages/All/tcl86-8.6.10.txz Installing /packages/All/libXext-1.3.4,1.txz Installing /packages/All/libXrender-0.9.10_2.txz Installing /packages/All/libXft-2.3.3.txz Installing /packages/All/libXScrnSaver-1.2.3_2.txz Installing /packages/All/tk86-8.6.10_1.txz Installing /packages/All/ocaml-labltk-8.06.3.txz ===== Message from ocaml-labltk-8.06.3: -- ===> NOTICE: The ocaml-labltk 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 Installing /packages/All/ocaml-findlib-1.7.1.txz Installing /packages/All/ocaml-zarith-1.4.1.txz ===== Message from ocaml-zarith-1.4.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 Installing /packages/All/libffi-3.2.1_3.txz Installing /packages/All/wayland-1.16.0.txz Installing /packages/All/pciids-20200421.txz Installing /packages/All/libpciaccess-0.16.txz Installing /packages/All/libdrm-2.4.101.txz Installing /packages/All/libelf-0.8.13_3.txz Installing /packages/All/libXfixes-5.0.3_2.txz Installing /packages/All/libXdamage-1.1.5.txz Installing /packages/All/libXrandr-1.5.2.txz Installing /packages/All/libxshmfence-1.3.txz Installing /packages/All/libXxf86vm-1.1.4_3.txz Installing /packages/All/mesa-libs-19.0.8.txz ===== Message from mesa-libs-19.0.8: -- ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Uses Python 2.7 which is EOLed upstream. It is scheduled to be removed on or after 2020-12-31. Installing /packages/All/libGLU-9.0.1.txz Installing /packages/All/pcre-8.43_2.txz Installing /packages/All/libiconv-1.14_11.txz Installing /packages/All/ncurses-6.1.20190525.txz Installing /packages/All/readline-8.0.4.txz Installing /packages/All/openssl-1.1.1g,1.txz Installing /packages/All/python37-3.7.7.txz ===== Message from python37-3.7.7: -- Note that some standard Python modules are provided as separate ports as they require additional dependencies. They are available as: py37-gdbm databases/py-gdbm@py37 py37-sqlite3 databases/py-sqlite3@py37 py37-tkinter x11-toolkits/py-tkinter@py37 Installing /packages/All/glib-2.56.3_7,1.txz No schema files found: doing nothing. Installing /packages/All/atk-2.28.1.txz Installing /packages/All/png-1.6.37.txz Installing /packages/All/pixman-0.40.0.txz Installing /packages/All/cairo-1.16.0,2.txz Installing /packages/All/jbigkit-2.1_1.txz Installing /packages/All/jpeg-turbo-2.0.4.txz Installing /packages/All/tiff-4.1.0.txz Installing /packages/All/shared-mime-info-1.10_2.txz Installing /packages/All/gdk-pixbuf2-2.40.0.txz Installing /packages/All/libdaemon-0.14_1.txz Installing /packages/All/libICE-1.0.10,1.txz Installing /packages/All/libSM-1.2.3,1.txz Installing /packages/All/dbus-1.12.16.txz ===> Creating groups. Creating group 'messagebus' with gid '556'. ===> Creating users Creating user 'messagebus' with uid '556'. Installing /packages/All/dbus-glib-0.110.txz Installing /packages/All/gdbm-1.18.1_1.txz Installing /packages/All/gobject-introspection-1.56.1,1.txz Installing /packages/All/gnome_subr-1.0.txz Installing /packages/All/avahi-app-0.7_3.txz ===> Creating groups. Creating group 'avahi' with gid '558'. ===> Creating users Creating user 'avahi' with uid '558'. Installing /packages/All/nettle-3.5.1_1.txz Installing /packages/All/libtasn1-4.16.0.txz Installing /packages/All/libunistring-0.9.10_1.txz Installing /packages/All/libidn2-2.3.0_1.txz Installing /packages/All/ca_root_nss-3.52.txz ===== Message from ca_root_nss-3.52: -- 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. 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 Installing /packages/All/p11-kit-0.23.20.txz Installing /packages/All/tpm-emulator-0.7.4_2.txz ===> Creating groups. Creating group '_tss' with gid '601'. ===> Creating users Creating user '_tss' with uid '601'. Installing /packages/All/trousers-0.3.14_2.txz ===> Creating groups. Using existing group '_tss'. ===> Creating users Using existing user '_tss'. ===== Message from trousers-0.3.14_2: -- 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 Installing /packages/All/gnutls-3.6.13.txz Installing /packages/All/libpaper-1.1.24.4.txz Installing /packages/All/cups-2.2.13.txz ===> Creating groups. Creating group 'cups' with gid '193'. ===> Creating users Creating user 'cups' with uid '193'. Installing /packages/All/graphite2-1.3.14.txz Installing /packages/All/harfbuzz-2.6.5.txz Installing /packages/All/fribidi-0.19.7.txz Installing /packages/All/libfontenc-1.1.4.txz Installing /packages/All/mkfontscale-1.2.1.txz Installing /packages/All/font-bh-ttf-1.0.3_4.txz Installing /packages/All/font-misc-meltho-1.0.3_4.txz Installing /packages/All/font-misc-ethiopic-1.0.3_4.txz Installing /packages/All/encodings-1.0.5,1.txz Installing /packages/All/dejavu-2.37_1.txz ===== Message from dejavu-2.37_1: -- 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. Installing /packages/All/xorg-fonts-truetype-7.7_1.txz Installing /packages/All/pango-1.42.4_3.txz Installing /packages/All/hicolor-icon-theme-0.17.txz Installing /packages/All/libXinerama-1.1.4_2,1.txz Installing /packages/All/libXi-1.7.10,1.txz Installing /packages/All/libXcursor-1.2.0.txz Installing /packages/All/libXcomposite-0.4.5,1.txz Installing /packages/All/gtk-update-icon-cache-2.24.32.txz Installing /packages/All/gtk2-2.24.32.txz Installing /packages/All/gtkglarea-2.0.1_10.txz ===== Message from gtkglarea-2.0.1_10: -- ===> NOTICE: The gtkglarea 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 Installing /packages/All/perl5-5.30.2.txz ===== Message from perl5-5.30.2: -- 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. Installing /packages/All/hunspell-1.7.0_2.txz Installing /packages/All/enchant-1.6.0_9.txz Installing /packages/All/gtkspell-2.0.16_6.txz Installing /packages/All/nspr-4.25.txz Installing /packages/All/icu-67.1,1.txz Installing /packages/All/spidermonkey60-60.9.0_3.txz ===== Message from spidermonkey60-60.9.0_3: -- ===> NOTICE: This port is deprecated; you may wish to reconsider installing it: Uses Python 2.7 which is EOLed upstream. It is scheduled to be removed on or after 2020-12-31. Installing /packages/All/polkit-0.116.txz ===> Creating groups. Creating group 'polkitd' with gid '565'. ===> Creating users Creating user 'polkitd' with uid '565'. Installing /packages/All/dconf-0.28.0.txz Installing /packages/All/libIDL-0.8.14_4.txz Installing /packages/All/ORBit2-2.14.19_2.txz Installing /packages/All/gconf2-3.2.6_5.txz Installing /packages/All/gamin-0.1.10_10.txz ===== Message from gamin-0.1.10_10: -- 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). 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 Installing /packages/All/gnome-mime-data-2.18.0_5.txz Installing /packages/All/gnome-vfs-2.24.4_11.txz Installing /packages/All/gtksourceview2-2.10.5_5.txz Installing /packages/All/libart_lgpl-2.3.21_3,1.txz Installing /packages/All/popt-1.16_2.txz Installing /packages/All/libbonobo-2.32.1.txz Installing /packages/All/xmlcatmgr-2.2_2.txz + 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 ===== 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. Installing /packages/All/libglade2-2.6.4_10.txz Installing /packages/All/libogg-1.3.4,4.txz Installing /packages/All/libvorbis-1.3.6,3.txz Installing /packages/All/libltdl-2.4.6.txz Installing /packages/All/libcanberra-0.30_5.txz Installing /packages/All/libgpg-error-1.37.txz Installing /packages/All/libgcrypt-1.8.5.txz Installing /packages/All/libxslt-1.1.34_1.txz Installing /packages/All/bash-5.0.17.txz Installing /packages/All/getopt-1.1.6.txz Installing /packages/All/iso8879-1986_3.txz Installing /packages/All/docbook-sgml-4.5_1.txz Installing /packages/All/xmlcharent-0.3_2.txz Installing /packages/All/docbook-xml-5.0_3.txz Installing /packages/All/sdocbook-xml-1.1_2,2.txz Installing /packages/All/docbook-1.5.txz Installing /packages/All/docbook-xsl-1.79.1_1,1.txz Installing /packages/All/rarian-0.8.1_4.txz Installing /packages/All/libXt-1.2.0,1.txz Installing /packages/All/libXpm-3.5.13.txz Installing /packages/All/libgnome-2.32.1.txz Installing /packages/All/libgnomecanvas-2.30.3_4.txz Installing /packages/All/libbonoboui-2.24.5_1.txz Installing /packages/All/libgnome-keyring-3.12.0_2.txz Installing /packages/All/xcb-util-0.4.0_2,1.txz Installing /packages/All/startup-notification-0.12_4.txz Installing /packages/All/gnome-icon-theme-symbolic-3.12.0.txz Installing /packages/All/gnome-icon-theme-3.12.0_1.txz Installing /packages/All/sqlite3-3.31.1_1,1.txz Installing /packages/All/libproxy-0.4.15.txz Installing /packages/All/gsettings-desktop-schemas-3.28.1.txz Installing /packages/All/glib-networking-2.56.1_2.txz Installing /packages/All/libsoup-2.62.3.txz Installing /packages/All/libsoup-gnome-2.62.3.txz Installing /packages/All/libepoxy-1.5.4.txz Installing /packages/All/lcms2-2.9.txz Installing /packages/All/argyllcms-1.9.2_5.txz Installing /packages/All/colord-1.3.5.txz ===> Creating groups. Creating group 'colord' with gid '970'. ===> Creating users Creating user 'colord' with uid '970'. Installing /packages/All/xkeyboard-config-2.29.txz Installing /packages/All/libxkbcommon-0.10.0_2.txz ===== Message from libxkbcommon-0.10.0_2: -- If arrow keys don't work under X11 switch to legacy rules e.g., For sh/bash/ksh/zsh run and (optionally) add into ~/.profile: export XKB_DEFAULT_RULES=xorg For csh/tcsh run and (optionally) add into ~/.login: setenv XKB_DEFAULT_RULES xorg Installing /packages/All/libXtst-1.2.3_2.txz Installing /packages/All/at-spi2-core-2.28.0.txz Installing /packages/All/at-spi2-atk-2.26.2.txz Installing /packages/All/adwaita-icon-theme-3.28.0.txz Installing /packages/All/libcroco-0.6.13.txz Installing /packages/All/libgsf-1.14.46.txz Installing /packages/All/librsvg2-2.40.21.txz Installing /packages/All/wayland-protocols-1.20.txz Installing /packages/All/gtk3-3.24.10_1.txz Installing /packages/All/desktop-file-utils-0.24.txz Installing /packages/All/gcr-3.28.0.txz Installing /packages/All/libsecret-0.18.6_1.txz Installing /packages/All/libcddb-1.3.2_4.txz Installing /packages/All/libcdio-2.1.0.txz Installing /packages/All/json-glib-1.4.4.txz Installing /packages/All/liblz4-1.9.2_1,1.txz Installing /packages/All/lzo2-2.10_1.txz Installing /packages/All/libarchive-3.4.2,1.txz Installing /packages/All/libinotify-20180201_2.txz ===== Message from libinotify-20180201_2: -- Libinotify functionality on FreeBSD is missing support for - detecting a file being moved into or out of a directory within the same filesystem - certain modifications to a symbolic link (rather than the file it points to.) in addition to the known limitations on all platforms using kqueue(2) where various open and close notifications are unimplemented. This means the following regression tests will fail: Directory notifications: IN_MOVED_FROM IN_MOVED_TO Open/close notifications: IN_OPEN IN_CLOSE_NOWRITE IN_CLOSE_WRITE Symbolic Link notifications: IN_DONT_FOLLOW IN_ATTRIB IN_MOVE_SELF IN_DELETE_SELF Kernel patches to address the missing directory and symbolic link notifications are available from: https://github.com/libinotify-kqueue/libinotify-kqueue/tree/master/patches You might want to consider increasing the kern.maxfiles tunable if you plan to use this library for applications that need to monitor activity of a lot of files. Installing /packages/All/jansson-2.12.txz Installing /packages/All/talloc-2.3.0.txz Installing /packages/All/tevent-0.10.1.txz Installing /packages/All/tdb-1.4.2,1.txz Installing /packages/All/lmdb-0.9.24_1,1.txz Installing /packages/All/py37-setuptools-44.0.0.txz Installing /packages/All/py37-iso8601-0.1.12.txz Installing /packages/All/krb5-1.18.1.txz Installing /packages/All/samba410-4.10.15.txz ===== Message from samba410-4.10.15: -- How to start: http://wiki.samba.org/index.php/Samba4/HOWTO * Your configuration is: /usr/local/etc/smb4.conf * All the relevant databases are under: /var/db/samba4 * All the logs are under: /var/log/samba4 * Provisioning script is: /usr/local/bin/samba-tool For additional documentation check: http://wiki.samba.org/index.php/Samba4 Bug reports should go to the: https://bugzilla.samba.org/ Installing /packages/All/gvfs-1.30.4_3.txz Installing /packages/All/libgnomeui-2.24.5.txz Installing /packages/All/freeglut-3.0.0_2.txz ===== Message from freeglut-3.0.0_2: -- Joystick support is untested and it is unknown if it works. Do not hesitate to contact x11@FreeBSD.org if this causes issues. Installing /packages/All/libXmu-1.1.3,1.txz Installing /packages/All/ocaml-lablgl-1.05_3,1.txz ===== Message from ocaml-lablgl-1.05_3,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 Installing /packages/All/ocaml-lablgtk2-2.18.5.txz Installing /packages/All/ocaml-sqlite3-4.0.5.txz ===== Message from ocaml-sqlite3-4.0.5: -- ===> NOTICE: The ocaml-sqlite3 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 Installing /packages/All/ocaml-ocamlgraph-1.8.7_2.txz ===== Message from ocaml-ocamlgraph-1.8.7_2: -- ===> NOTICE: The ocaml-ocamlgraph 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 Installing /packages/All/ocaml-camlp5-7.07.txz Installing /packages/All/gmake-4.3.txz SUCCEEDED 00:01:41 ------------------------------------------------------------------------------- -- Phase: check-sanity ------------------------------------------------------------------------------- ===> 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 SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: pkg-depends ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on file: /usr/local/sbin/pkg - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: fetch-depends ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: fetch ------------------------------------------------------------------------------- ===> 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 ===> why3-0.83_2 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by why3-0.83_2 for building SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: checksum ------------------------------------------------------------------------------- ===> 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 ===> why3-0.83_2 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by why3-0.83_2 for building => SHA256 Checksum OK for why3-0.83.tar.gz. SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: extract-depends ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: extract ------------------------------------------------------------------------------- ===> 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 ===> why3-0.83_2 depends on file: /usr/local/sbin/pkg - found ===> Fetching all distfiles required by why3-0.83_2 for building ===> Extracting for why3-0.83_2 => SHA256 Checksum OK for why3-0.83.tar.gz. ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found Extracted Memory Use: 58.71M SUCCEEDED 00:00:01 ------------------------------------------------------------------------------- -- Phase: patch-depends ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: patch ------------------------------------------------------------------------------- ===> Patching for why3-0.83_2 ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found ===> Applying ports patches for why3-0.83_2 ===> Cleanly applied ports patch(es) patch-configure patch-src_tools_cpulimit.c SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: build-depends ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on package: ocaml-zarith>1.2 - found ===> why3-0.83_2 depends on executable: lablgtk2 - found ===> why3-0.83_2 depends on package: ocaml-sqlite3>2 - found ===> why3-0.83_2 depends on package: ocaml-ocamlgraph>1.8 - found ===> why3-0.83_2 depends on executable: camlp5o - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlfind - found ===> why3-0.83_2 depends on package: gmake>=4.3 - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: lib-depends ------------------------------------------------------------------------------- SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: configure ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on package: ocaml-zarith>1.2 - found ===> why3-0.83_2 depends on executable: lablgtk2 - found ===> why3-0.83_2 depends on package: ocaml-sqlite3>2 - found ===> why3-0.83_2 depends on package: ocaml-ocamlgraph>1.8 - found ===> why3-0.83_2 depends on executable: camlp5o - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlfind - found ===> why3-0.83_2 depends on package: gmake>=4.3 - found ===> Configuring for why3-0.83_2 configure: loading site script /xports/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 ocamlc... ocamlc ocaml version is 4.05.0 ocaml library path is /usr/local/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 camlp5o... camlp5o checking for ocamlfind... yes ocamlfind found zarith in /usr/local/lib/ocaml/site-lib/zarith ocamlfind found lablgtk2 in /usr/local/lib/ocaml/site-lib/lablgtk2 ocamlfind found lablgtksourceview2 in /usr/local/lib/ocaml/site-lib/lablgtk2 ocamlfind found sqlite3 in /usr/local/lib/ocaml/site-lib/sqlite3 configure: WARNING: coq support disabled configure: WARNING: PVS support disabled configure: WARNING: Isabelle support disabled ocamlfind found ocamlgraph in /usr/local/lib/ocaml/ocamlgraph 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 src/jessie/Makefile config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.05.0 Library path : /usr/local/lib/ocaml Native compilation : yes Profiling : no Zarith : yes IDE : yes Bench tool : yes Documentation : no Coq support : no (disabled by user) PVS support : no (disabled by user) Isabelle support : no (disabled by user) Frama-C support : no (disabled by default) Hypothesis selection : yes 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 SUCCEEDED 00:00:02 ------------------------------------------------------------------------------- -- Phase: build ------------------------------------------------------------------------------- ===> Building for why3-0.83_2 gmake[1]: Entering directory '/construction/math/why3/why3-0.83' Ocamllex src/why3doc/doc_lexer.mll 105 states, 991 transitions, table size 4594 bytes 1665 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.ml Ocamldep lib/ocaml/why3__Array.ml Ocamldep lib/ocaml/why3__IntAux.ml Ocamldep lib/ocaml/why3__BigInt.ml Ocamldep src/why3bench/why3bench.ml Ocamldep src/why3bench/benchdb.ml Ocamldep src/why3bench/benchrc.ml Ocamldep src/why3bench/bench.ml Ocamldep src/why3bench/db.ml Ocamldep src/why3bench/worker.ml Ocamldep src/why3session/why3session.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/why3replayer/replay.ml Ocamldep src/ide/gmain.ml Ocamldep src/ide/gconfig.ml Ocamldep src/why3config/why3config.ml Ocamldep src/main.ml Ocamllex plugins/tptp/tptp_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Ocamlyacc plugins/tptp/tptp_parser.mly 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/parser/lexer.mll 143 states, 3137 transitions, table size 13406 bytes 7548 additional bytes used for bindings Ocamlyacc src/parser/parser.mly Ocamlyacc src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 29 states, 1101 transitions, table size 4578 bytes Ocamllex src/session/xml.mll 114 states, 1396 transitions, table size 6268 bytes 3538 additional bytes used for bindings Ocamldep src/whyml/mlw_interp.ml Ocamldep src/whyml/mlw_main.ml Ocamldep src/whyml/mlw_ocaml.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/session/session_scheduler.ml Ocamldep src/session/session_tools.ml Ocamldep src/session/session.ml Ocamldep src/session/termcode.ml Ocamldep src/session/xml.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/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/eval_match.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/induction.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/simplify_formula.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/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/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/loc.ml Ocamldep src/util/debug.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 File "src/util/strings.ml", line 34, characters 12-25: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/strings.ml", line 36, characters 4-15: Warning 3: deprecated: String.fill Use Bytes.fill instead. 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 File "src/util/weakhtbl.ml", line 172, characters 4-68: Warning 50: unattached documentation comment (ignored) Ocamlc src/util/hashcons.mli File "src/util/hashcons.mli", line 45, characters 6-67: Warning 50: ambiguous documentation comment 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 File "src/util/pp.ml", line 177, characters 4-41: Warning 3: deprecated: Format.pp_get_all_formatter_output_functions Use Format.pp_get_formatter_out_functions instead. File "src/util/pp.ml", line 178, characters 2-39: Warning 3: deprecated: Format.pp_set_all_formatter_output_functions Use Format.pp_set_formatter_out_functions instead. Ocamlc src/util/debug.mli Ocamlopt src/util/debug.ml File "src/util/debug.ml", line 67, characters 2-69: Warning 50: unattached documentation comment (ignored) File "src/util/debug.ml", line 185, characters 0-37: Warning 50: ambiguous documentation comment File "src/util/debug.ml", line 187, characters 2-69: Warning 50: unattached documentation comment (ignored) File "src/util/debug.ml", line 69, characters 4-48: Warning 3: deprecated: Format.pp_get_all_formatter_output_functions Use Format.pp_get_formatter_out_functions instead. File "src/util/debug.ml", line 70, characters 2-46: Warning 3: deprecated: Format.pp_set_all_formatter_output_functions Use Format.pp_set_formatter_out_functions instead. Ocamlc src/util/loc.mli Ocamlopt src/util/loc.ml Ocamlc src/util/print_tree.mli Ocamlopt src/util/print_tree.ml Ocamlc src/util/cmdline.mli Ocamlopt src/util/cmdline.ml File "src/util/cmdline.ml", line 46, characters 16-29: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/cmdline.ml", line 48, characters 10-20: Warning 3: deprecated: String.set Use Bytes.set instead. 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 File "src/util/rc.mli", line 35, characters 0-91: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 39, characters 0-67: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 41, characters 0-68: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 43, characters 0-60: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 45, characters 0-49: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 49, characters 0-43: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 57, characters 7-28: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 58, characters 13-38: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 59, characters 38-65: Warning 50: ambiguous documentation comment File "src/util/rc.mli", line 62, characters 14-32: Warning 50: ambiguous documentation comment Ocamlopt src/util/rc.ml File "src/util/rc.mll", line 67, characters 13-26: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/rc.mll", line 73, characters 10-27: Warning 3: deprecated: String.unsafe_set File "src/util/rc.mll", line 76, characters 6-23: Warning 3: deprecated: String.unsafe_set Ocamlc src/util/plugin.mli Ocamlopt src/util/plugin.ml Ocamlc src/util/number.mli Ocamlopt src/util/number.ml File "src/util/number.ml", line 161, characters 14-25: Warning 3: deprecated: String.copy File "src/util/number.ml", line 161, characters 31-44: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlc src/util/pqueue.mli Ocamlopt src/util/pqueue.ml Ocamlc src/core/ident.mli Ocamlopt src/core/ident.ml File "src/core/ident.ml", line 186, characters 23-42: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/core/ident.ml", line 187, characters 23-40: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/core/ty.mli File "src/core/ty.mli", line 75, characters 0-38: Warning 50: unattached documentation comment (ignored) File "src/core/ty.mli", line 83, characters 0-33: Warning 50: unattached documentation comment (ignored) File "src/core/ty.mli", line 90, characters 0-31: Warning 50: unattached documentation comment (ignored) 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 File "src/core/pretty.ml", line 71, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/core/pretty.ml", line 98, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/core/pretty.ml", line 112, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. 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 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 File "src/parser/lexer.mll", line 140, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/parser/lexer.mll", line 142, characters 46-56: Warning 3: deprecated: String.set Use Bytes.set instead. 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 File "src/driver/whyconf.mli", line 223, characters 0-93: Warning 50: ambiguous documentation comment File "src/driver/whyconf.mli", line 230, characters 0-93: Warning 50: ambiguous documentation comment Ocamlopt src/driver/whyconf.ml File "src/driver/whyconf.ml", line 37, characters 30-60: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 270, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 275, characters 2-39: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 278, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 586, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 595, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 609, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 626, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 636, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 502, characters 4-18: Warning 3: deprecated: Format.bprintf Ocamlc src/driver/autodetection.mli Ocamlopt src/driver/autodetection.ml File "src/driver/autodetection.ml", line 149, characters 4-97: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 286, characters 4-142: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 292, characters 2-38: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 331, characters 2-109: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 365, characters 6-25: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 366, characters 32-63: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 375, characters 11-46: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 378, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 421, characters 6-214: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 496, characters 4-40: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 185, characters 14-22: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "src/driver/autodetection.ml", line 203, characters 14-22: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) Ocamlc src/transform/simplify_formula.mli Ocamlopt src/transform/simplify_formula.ml File "src/transform/simplify_formula.ml", line 61, characters 6-85: Warning 57: Ambiguous or-pattern variables under guard; variables t,tv,vs may match different arguments. (See manual section 8.5) 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/eliminate_definition.mli Ocamlopt src/transform/eliminate_definition.ml File "src/transform/eliminate_definition.ml", line 281, characters 10-22: Warning 3: deprecated: Array.create Use Array.make instead. Ocamlc src/transform/eliminate_algebraic.mli Ocamlopt src/transform/eliminate_algebraic.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 File "src/transform/encoding_select.ml", line 32, characters 0-682: Warning 60: unused module Kept. File "src/transform/encoding_select.ml", line 55, characters 0-1270: Warning 60: unused module Lskept. File "src/transform/encoding_select.ml", line 89, characters 0-674: Warning 60: unused module Lsinst. Ocamlc src/transform/encoding_guards_full.mli Ocamlopt src/transform/encoding_guards_full.ml File "src/transform/encoding_guards_full.ml", line 62, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 71, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 145, characters 2-28: Warning 50: unattached documentation comment (ignored) 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/eval_match.mli Ocamlopt src/transform/eval_match.ml File "src/transform/eval_match.ml", line 99, characters 6-69: Warning 57: Ambiguous or-pattern variables under guard; variable cs may match different arguments. (See manual section 8.5) 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/printer/alt_ergo.mli Ocamlopt src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.mli Ocamlopt src/printer/why3printer.ml File "src/printer/why3printer.ml", line 51, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/printer/why3printer.ml", line 58, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/printer/why3printer.ml", line 68, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/printer/smtv1.mli Ocamlopt src/printer/smtv1.ml Ocamlc src/printer/smtv2.mli Ocamlopt src/printer/smtv2.ml File "src/printer/smtv2.ml", line 31, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 32, characters 5-31: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 39, characters 6-30: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 45, characters 6-23: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 47, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 58, characters 6-48: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/coq.mli Ocamlopt src/printer/coq.ml File "src/printer/coq.ml", line 454, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 466, characters 4-34: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 839, characters 2-154: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 154, characters 22-30: Warning 48: implicit elimination of optional argument ?whytypes File "src/printer/coq.ml", line 417, characters 38-46: Warning 48: implicit elimination of optional argument ?whytypes File "src/printer/coq.ml", line 507, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml File "src/printer/isabelle.ml", line 322, characters 2-159: Warning 50: unattached documentation comment (ignored) 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 File "src/printer/cvc3.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlopt src/printer/yices.ml File "src/printer/yices.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlopt src/printer/mathematica.ml 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 111, characters 2-16: Warning 3: deprecated: Format.bprintf File "src/session/termcode.ml", line 282, characters 4-18: Warning 3: deprecated: Format.bprintf Ocamlc src/session/session.mli Ocamlopt src/session/session.ml File "src/session/session.ml", line 93, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 580, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 960, characters 4-31: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1110, characters 8-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1152, characters 12-34: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1230, characters 2-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1266, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1290, characters 6-51: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1304, characters 2-73: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1364, characters 8-76: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1532, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1605, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1610, characters 22-66: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1614, characters 8-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1625, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1727, characters 13-43: Warning 50: ambiguous documentation comment File "src/session/session.ml", line 1736, characters 15-45: Warning 50: ambiguous documentation comment File "src/session/session.ml", line 1792, characters 2-55: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1793, characters 2-91: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1796, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1802, characters 2-70: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1859, characters 2-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1936, characters 2-164: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1954, characters 6-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1955, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2251, characters 2-28: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2258, characters 51-72: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 75, characters 0-36: Warning 60: unused module Spos. File "src/session/session.ml", line 76, characters 0-31: Warning 60: unused module Hpos. Ocamlc src/session/session_tools.mli Ocamlopt src/session/session_tools.ml File "src/session/session_tools.ml", line 36, characters 4-76: Warning 50: unattached documentation comment (ignored) File "src/session/session_tools.ml", line 42, characters 8-61: Warning 50: unattached documentation comment (ignored) Ocamlc src/session/session_scheduler.mli File "src/session/session_scheduler.mli", line 269, characters 21-78: Warning 50: unattached documentation comment (ignored) Ocamlopt src/session/session_scheduler.ml File "src/session/session_scheduler.ml", line 128, characters 6-45: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 150, characters 1-63: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 171, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 186, characters 2-50: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 200, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 955, characters 4-64: Warning 50: unattached documentation comment (ignored) Ocamlc src/whyml/mlw_ty.mli File "src/whyml/mlw_ty.mli", line 147, characters 23-57: Warning 50: ambiguous documentation comment File "src/whyml/mlw_ty.mli", line 243, characters 25-54: Warning 50: ambiguous documentation comment File "src/whyml/mlw_ty.mli", line 244, characters 25-69: Warning 50: ambiguous documentation comment 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_ocaml.mli Ocamlopt src/whyml/mlw_ocaml.ml File "src/whyml/mlw_ocaml.ml", line 111, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 139, characters 14-31: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 145, characters 43-62: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 146, characters 43-60: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/whyml/mlw_main.mli Ocamlopt src/whyml/mlw_main.ml Ocamlc src/whyml/mlw_interp.mli Ocamlopt src/whyml/mlw_interp.ml Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml File "plugins/parser/genequlin.ml", line 63, characters 2-53: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 76, characters 2-50: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 86, characters 2-36: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 94, characters 2-28: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 103, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 107, characters 2-47: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 112, characters 8-106: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 123, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 125, characters 2-39: Warning 50: unattached documentation comment (ignored) Linking lib/plugins/genequlin.cmxs Ocamlopt plugins/parser/dimacs.ml File "plugins/parser/dimacs.mll", line 46, characters 10-22: Warning 3: deprecated: Array.create Use Array.make instead. 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 File "plugins/tptp/tptp_printer.ml", line 31, characters 12-31: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "plugins/tptp/tptp_printer.ml", line 35, characters 12-29: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "plugins/tptp/tptp_printer.ml", line 39, characters 12-29: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Linking lib/plugins/tptp.cmxs Ocamlopt plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 413, characters 4-32: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 419, characters 4-46: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 422, characters 6-91: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 445, characters 4-59: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 52, characters 4-18: Warning 3: deprecated: Format.bprintf File "plugins/transform/hypothesis_selection.ml", line 365, characters 22-35: Warning 48: implicit elimination of optional argument ?pos Linking lib/plugins/hypothesis_selection.cmxs Linking lib/why3/why3.cmxa Ocamlopt src/main.ml File "src/main.ml", line 242, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/main.ml", line 250, characters 2-16: Warning 50: unattached documentation comment (ignored) File "src/main.ml", line 465, characters 10-108: Warning 50: unattached documentation comment (ignored) Linking bin/why3.opt Ocamlopt src/why3config/why3config.ml File "src/why3config/why3config.ml", line 124, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/why3config/why3config.ml", line 133, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3config/why3config.ml", line 146, characters 2-13: Warning 50: unattached documentation comment (ignored) Linking bin/why3config.opt ocamlc.opt -c -ccopt "-Wall -o src/ide/resetgc.o" src/ide/resetgc.c Ocamlc src/ide/gconfig.mli Ocamlopt src/ide/gconfig.ml File "src/ide/gconfig.ml", line 27, characters 4-77: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 341, characters 0-18: Warning 50: ambiguous documentation comment File "src/ide/gconfig.ml", line 964, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 968, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 972, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 986, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 623, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 633, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 645, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 657, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 681, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 736, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 747, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 753, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 759, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 771, characters 24-48: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 783, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 787, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 791, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 795, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 821, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 852, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 878, characters 24-48: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 888, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 891, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 895, characters 48-57: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 906, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 920, characters 52-60: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 922, characters 15-48: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 924, characters 36-43: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 1060, characters 21-56: Warning 48: implicit elimination of optional arguments ?from, ?padding Ocamlopt src/ide/gmain.ml File "src/ide/gmain.ml", line 772, characters 2-60: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 790, characters 34-64: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 794, characters 10-95: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1017, characters 6-67: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1052, characters 10-73: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1058, characters 4-106: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1061, characters 4-53: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1919, characters 4-92: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1922, characters 4-29: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 167, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/ide/gmain.ml", line 214, characters 38-47: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gmain.ml", line 225, characters 15-38: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 237, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 268, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 279, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 287, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 295, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 303, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 411, characters 35-64: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 598, characters 14-21: Warning 3: deprecated: Format.bprintf File "src/ide/gmain.ml", line 614, characters 14-21: Warning 3: deprecated: Format.bprintf File "src/ide/gmain.ml", line 838, characters 11-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?padding File "src/ide/gmain.ml", line 1985, characters 14-27: Warning 48: implicit elimination of optional argument ?destroy Linking bin/why3ide.opt Ocamlopt src/why3replayer/replay.ml Linking bin/why3replayer.opt Ocamlc src/why3session/why3session_lib.mli Ocamlopt src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 75, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 204, characters 2-16: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 208, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 214, characters 18-45: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 216, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 218, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 220, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 223, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 225, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 264, characters 14-29: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 257, characters 10-23: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlopt src/why3session/why3session_copy.ml File "src/why3session/why3session_copy.ml", line 99, characters 14-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 133, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 154, characters 20-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 155, characters 20-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 174, characters 2-61: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 180, characters 2-24: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_info.ml File "src/why3session/why3session_info.ml", line 407, characters 6-136: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_latex.ml File "src/why3session/why3session_latex.ml", line 300, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 303, characters 2-44: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 309, characters 2-43: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 312, characters 2-28: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_html.ml File "src/why3session/why3session_html.ml", line 371, characters 6-28: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 512, characters 6-24: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 522, characters 6-28: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_rm.ml Ocamlopt src/why3session/why3session_output.ml File "src/why3session/why3session_output.ml", line 69, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 74, characters 12-73: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 76, characters 12-35: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 92, characters 2-61: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_run.ml File "src/why3session/why3session_run.ml", line 184, characters 24-52: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_run.ml", line 311, characters 31-43: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session_csv.ml File "src/why3session/why3session_csv.ml", line 114, characters 23-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 198, characters 4-26: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 203, characters 32-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 205, characters 6-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 211, characters 6-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 254, characters 52-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 274, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 277, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 293, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 310, characters 2-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 331, characters 2-33: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3session/why3session.ml Linking bin/why3session.opt Ocamlopt src/why3bench/worker.ml File "src/why3bench/worker.ml", line 137, characters 4-61: Warning 50: ambiguous documentation comment Ocamlc src/why3bench/db.mli File "src/why3bench/db.mli", line 86, characters 35-50: Warning 50: ambiguous documentation comment Ocamlopt src/why3bench/db.ml Ocamlc src/why3bench/bench.mli File "src/why3bench/bench.mli", line 139, characters 2-18: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3bench/bench.ml File "src/why3bench/bench.ml", line 146, characters 4-72: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 229, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 276, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 286, characters 2-14: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 293, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 294, characters 2-18: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 346, characters 2-18: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3bench/benchrc.mli Ocamlopt src/why3bench/benchrc.ml Ocamlc src/why3bench/benchdb.mli Ocamlopt src/why3bench/benchdb.ml File "src/why3bench/benchdb.ml", line 41, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/why3bench/benchdb.ml", line 87, characters 2-29: Warning 50: unattached documentation comment (ignored) Ocamlopt src/why3bench/why3bench.ml File "src/why3bench/why3bench.ml", line 200, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3bench/why3bench.ml", line 212, characters 2-16: Warning 50: unattached documentation comment (ignored) Linking bin/why3bench.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.ml File "_none_", line 1: Warning 58: no cmx file was found in path for module Big_int_Z, and its interface was not compiled with -opaque Ocamlopt lib/ocaml/why3__IntAux.ml Ocamlopt lib/ocaml/why3__Array.ml Linking lib/why3/why3extract.cmx Linking lib/why3/why3extract.cmxa cc -Wall -o lib/why3-cpulimit src/tools/cpulimit.c Ocamlc src/why3doc/doc_html.mli Ocamlopt src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.mli Ocamlopt src/why3doc/doc_def.ml File "src/why3doc/doc_def.ml", line 79, characters 12-25: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/why3doc/doc_def.ml", line 84, characters 8-19: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 88, characters 8-21: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 89, characters 8-34: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 90, characters 8-36: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlopt src/why3doc/doc_lexer.ml File "src/why3doc/doc_lexer.mll", line 65, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/why3doc/doc_lexer.mll", line 76, characters 15-26: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlopt src/why3doc/doc_main.ml Linking bin/why3doc.opt Ocamlc plugins/parser/genequlin.ml File "plugins/parser/genequlin.ml", line 63, characters 2-53: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 76, characters 2-50: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 86, characters 2-36: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 94, characters 2-28: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 103, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 107, characters 2-47: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 112, characters 8-106: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 123, characters 2-26: Warning 50: unattached documentation comment (ignored) File "plugins/parser/genequlin.ml", line 125, characters 2-39: Warning 50: unattached documentation comment (ignored) Linking lib/plugins/genequlin.cmo Ocamlc plugins/parser/dimacs.ml File "plugins/parser/dimacs.mll", line 46, characters 10-22: Warning 3: deprecated: Array.create Use Array.make instead. Linking lib/plugins/dimacs.cmo Ocamlc plugins/tptp/tptp_ast.ml Ocamlc plugins/tptp/tptp_parser.ml Ocamlc plugins/tptp/tptp_typing.ml Ocamlc plugins/tptp/tptp_lexer.ml Ocamlc plugins/tptp/tptp_printer.ml File "plugins/tptp/tptp_printer.ml", line 31, characters 12-31: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "plugins/tptp/tptp_printer.ml", line 35, characters 12-29: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "plugins/tptp/tptp_printer.ml", line 39, characters 12-29: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Linking lib/plugins/tptp.cmo Ocamlc plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 413, characters 4-32: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 419, characters 4-46: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 422, characters 6-91: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 445, characters 4-59: Warning 50: unattached documentation comment (ignored) File "plugins/transform/hypothesis_selection.ml", line 52, characters 4-18: Warning 3: deprecated: Format.bprintf File "plugins/transform/hypothesis_selection.ml", line 365, characters 22-35: Warning 48: implicit elimination of optional argument ?pos Linking lib/plugins/hypothesis_selection.cmo 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 File "src/util/strings.ml", line 34, characters 12-25: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/strings.ml", line 36, characters 4-15: Warning 3: deprecated: String.fill Use Bytes.fill instead. Ocamlc src/util/extmap.ml Ocamlc src/util/extset.ml Ocamlc src/util/exthtbl.ml Ocamlc src/util/weakhtbl.ml File "src/util/weakhtbl.ml", line 172, characters 4-68: Warning 50: unattached documentation comment (ignored) Ocamlc src/util/hashcons.ml Ocamlc src/util/stdlib.ml Ocamlc src/util/exn_printer.ml Ocamlc src/util/pp.ml File "src/util/pp.ml", line 177, characters 4-41: Warning 3: deprecated: Format.pp_get_all_formatter_output_functions Use Format.pp_get_formatter_out_functions instead. File "src/util/pp.ml", line 178, characters 2-39: Warning 3: deprecated: Format.pp_set_all_formatter_output_functions Use Format.pp_set_formatter_out_functions instead. Ocamlc src/util/debug.ml File "src/util/debug.ml", line 67, characters 2-69: Warning 50: unattached documentation comment (ignored) File "src/util/debug.ml", line 185, characters 0-37: Warning 50: ambiguous documentation comment File "src/util/debug.ml", line 187, characters 2-69: Warning 50: unattached documentation comment (ignored) File "src/util/debug.ml", line 69, characters 4-48: Warning 3: deprecated: Format.pp_get_all_formatter_output_functions Use Format.pp_get_formatter_out_functions instead. File "src/util/debug.ml", line 70, characters 2-46: Warning 3: deprecated: Format.pp_set_all_formatter_output_functions Use Format.pp_set_formatter_out_functions instead. Ocamlc src/util/loc.ml Ocamlc src/util/print_tree.ml Ocamlc src/util/cmdline.ml File "src/util/cmdline.ml", line 46, characters 16-29: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/cmdline.ml", line 48, characters 10-20: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlc src/util/warning.ml Ocamlc src/util/sysutil.ml Ocamlc src/util/rc.ml File "src/util/rc.mll", line 67, characters 13-26: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/util/rc.mll", line 73, characters 10-27: Warning 3: deprecated: String.unsafe_set File "src/util/rc.mll", line 76, characters 6-23: Warning 3: deprecated: String.unsafe_set Ocamlc src/util/plugin.ml Ocamlc src/util/number.ml File "src/util/number.ml", line 161, characters 14-25: Warning 3: deprecated: String.copy File "src/util/number.ml", line 161, characters 31-44: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlc src/util/pqueue.ml Ocamlc src/core/ident.ml File "src/core/ident.ml", line 186, characters 23-42: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/core/ident.ml", line 187, characters 23-40: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. 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 File "src/core/pretty.ml", line 71, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/core/pretty.ml", line 98, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/core/pretty.ml", line 112, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/core/dterm.ml Ocamlc src/core/env.ml Ocamlc src/core/trans.ml Ocamlc src/core/printer.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 File "src/parser/lexer.mll", line 140, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/parser/lexer.mll", line 142, characters 46-56: Warning 3: deprecated: String.set Use Bytes.set instead. 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 File "src/driver/whyconf.ml", line 37, characters 30-60: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 270, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 275, characters 2-39: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 278, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 586, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 595, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 609, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 626, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 636, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/driver/whyconf.ml", line 502, characters 4-18: Warning 3: deprecated: Format.bprintf Ocamlc src/driver/autodetection.ml File "src/driver/autodetection.ml", line 149, characters 4-97: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 286, characters 4-142: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 292, characters 2-38: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 331, characters 2-109: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 365, characters 6-25: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 366, characters 32-63: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 375, characters 11-46: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 378, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 421, characters 6-214: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 496, characters 4-40: Warning 50: unattached documentation comment (ignored) File "src/driver/autodetection.ml", line 185, characters 14-22: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) File "src/driver/autodetection.ml", line 203, characters 14-22: Warning 52: Code should not depend on the actual values of this constructor's arguments. They are only for information and may change in future versions. (See manual section 8.5) Ocamlc src/transform/simplify_formula.ml File "src/transform/simplify_formula.ml", line 61, characters 6-85: Warning 57: Ambiguous or-pattern variables under guard; variables t,tv,vs may match different arguments. (See manual section 8.5) Ocamlc src/transform/inlining.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/induction.ml Ocamlc src/transform/eliminate_definition.ml File "src/transform/eliminate_definition.ml", line 281, characters 10-22: Warning 3: deprecated: Array.create Use Array.make instead. 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 File "src/transform/encoding_select.ml", line 32, characters 0-682: Warning 60: unused module Kept. File "src/transform/encoding_select.ml", line 55, characters 0-1270: Warning 60: unused module Lskept. File "src/transform/encoding_select.ml", line 89, characters 0-674: Warning 60: unused module Lsinst. Ocamlc src/transform/encoding_guards_full.ml File "src/transform/encoding_guards_full.ml", line 62, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 71, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/transform/encoding_guards_full.ml", line 145, characters 2-28: Warning 50: unattached documentation comment (ignored) 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/eval_match.ml File "src/transform/eval_match.ml", line 99, characters 6-69: Warning 57: Ambiguous or-pattern variables under guard; variable cs may match different arguments. (See manual section 8.5) Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/printer/why3printer.ml File "src/printer/why3printer.ml", line 51, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/printer/why3printer.ml", line 58, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/printer/why3printer.ml", line 68, characters 18-35: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/printer/smtv1.ml Ocamlc src/printer/smtv2.ml File "src/printer/smtv2.ml", line 31, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 32, characters 5-31: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 39, characters 6-30: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 45, characters 6-23: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 47, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/printer/smtv2.ml", line 58, characters 6-48: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/coq.ml File "src/printer/coq.ml", line 454, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 466, characters 4-34: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 839, characters 2-154: Warning 50: unattached documentation comment (ignored) File "src/printer/coq.ml", line 154, characters 22-30: Warning 48: implicit elimination of optional argument ?whytypes File "src/printer/coq.ml", line 417, characters 38-46: Warning 48: implicit elimination of optional argument ?whytypes File "src/printer/coq.ml", line 507, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlc src/printer/pvs.ml Ocamlc src/printer/isabelle.ml File "src/printer/isabelle.ml", line 322, characters 2-159: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/simplify.ml Ocamlc src/printer/gappa.ml Ocamlc src/printer/cvc3.ml File "src/printer/cvc3.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/cvc3.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/yices.ml File "src/printer/yices.ml", line 30, characters 4-25: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 31, characters 5-20: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 34, characters 7-26: Warning 50: unattached documentation comment (ignored) File "src/printer/yices.ml", line 39, characters 7-26: Warning 50: unattached documentation comment (ignored) Ocamlc src/printer/mathematica.ml Ocamlc src/session/xml.ml Ocamlc src/session/termcode.ml File "src/session/termcode.ml", line 111, characters 2-16: Warning 3: deprecated: Format.bprintf File "src/session/termcode.ml", line 282, characters 4-18: Warning 3: deprecated: Format.bprintf Ocamlc src/session/session.ml File "src/session/session.ml", line 93, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 580, characters 4-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 960, characters 4-31: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1110, characters 8-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1152, characters 12-34: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1230, characters 2-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1266, characters 6-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1290, characters 6-51: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1304, characters 2-73: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1364, characters 8-76: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1532, characters 4-30: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1605, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1610, characters 22-66: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1614, characters 8-35: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1625, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1727, characters 13-43: Warning 50: ambiguous documentation comment File "src/session/session.ml", line 1736, characters 15-45: Warning 50: ambiguous documentation comment File "src/session/session.ml", line 1792, characters 2-55: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1793, characters 2-91: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1796, characters 2-49: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1802, characters 2-70: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1859, characters 2-48: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1936, characters 2-164: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1954, characters 6-62: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 1955, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2251, characters 2-28: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 2258, characters 51-72: Warning 50: unattached documentation comment (ignored) File "src/session/session.ml", line 75, characters 0-36: Warning 60: unused module Spos. File "src/session/session.ml", line 76, characters 0-31: Warning 60: unused module Hpos. Ocamlc src/session/session_tools.ml File "src/session/session_tools.ml", line 36, characters 4-76: Warning 50: unattached documentation comment (ignored) File "src/session/session_tools.ml", line 42, characters 8-61: Warning 50: unattached documentation comment (ignored) Ocamlc src/session/session_scheduler.ml File "src/session/session_scheduler.ml", line 128, characters 6-45: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 150, characters 1-63: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 171, characters 2-35: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 186, characters 2-50: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 200, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/session/session_scheduler.ml", line 955, characters 4-64: Warning 50: unattached documentation comment (ignored) 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_ocaml.ml File "src/whyml/mlw_ocaml.ml", line 111, characters 18-37: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 139, characters 14-31: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 145, characters 43-62: Warning 3: deprecated: String.uncapitalize Use String.uncapitalize_ascii instead. File "src/whyml/mlw_ocaml.ml", line 146, characters 43-60: Warning 3: deprecated: String.capitalize Use String.capitalize_ascii instead. Ocamlc src/whyml/mlw_main.ml Ocamlc src/whyml/mlw_interp.ml Linking lib/why3/why3.cmo Linking lib/why3/why3.cma Ocamlc src/main.ml File "src/main.ml", line 242, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/main.ml", line 250, characters 2-16: Warning 50: unattached documentation comment (ignored) File "src/main.ml", line 465, characters 10-108: Warning 50: unattached documentation comment (ignored) Linking bin/why3.byte Ocamlc src/why3config/why3config.ml File "src/why3config/why3config.ml", line 124, characters 2-31: Warning 50: unattached documentation comment (ignored) File "src/why3config/why3config.ml", line 133, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3config/why3config.ml", line 146, characters 2-13: Warning 50: unattached documentation comment (ignored) Linking bin/why3config.byte Ocamlc src/ide/gconfig.ml File "src/ide/gconfig.ml", line 27, characters 4-77: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 341, characters 0-18: Warning 50: ambiguous documentation comment File "src/ide/gconfig.ml", line 964, characters 2-33: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 968, characters 2-24: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 972, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 986, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/ide/gconfig.ml", line 623, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 633, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 645, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 657, characters 13-36: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 681, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 736, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 747, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 753, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 759, characters 15-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 771, characters 24-48: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 783, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 787, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 791, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 795, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 821, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 852, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 878, characters 24-48: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gconfig.ml", line 888, characters 33-68: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 891, characters 15-50: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 895, characters 48-57: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 906, characters 15-24: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 920, characters 52-60: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 922, characters 15-48: Warning 48: implicit elimination of optional arguments ?from, ?padding File "src/ide/gconfig.ml", line 924, characters 36-43: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gconfig.ml", line 1060, characters 21-56: Warning 48: implicit elimination of optional arguments ?from, ?padding Ocamlc src/ide/gmain.ml File "src/ide/gmain.ml", line 772, characters 2-60: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 790, characters 34-64: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 794, characters 10-95: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1017, characters 6-67: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1052, characters 10-73: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1058, characters 4-106: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1061, characters 4-53: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1919, characters 4-92: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 1922, characters 4-29: Warning 50: unattached documentation comment (ignored) File "src/ide/gmain.ml", line 167, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/ide/gmain.ml", line 214, characters 38-47: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?fill, ?padding File "src/ide/gmain.ml", line 225, characters 15-38: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 237, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 268, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 279, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 287, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 295, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 303, characters 13-51: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 411, characters 35-64: Warning 48: implicit elimination of optional arguments ?from, ?fill, ?padding File "src/ide/gmain.ml", line 598, characters 14-21: Warning 3: deprecated: Format.bprintf File "src/ide/gmain.ml", line 614, characters 14-21: Warning 3: deprecated: Format.bprintf File "src/ide/gmain.ml", line 838, characters 11-37: Warning 48: implicit elimination of optional arguments ?from, ?expand, ?padding File "src/ide/gmain.ml", line 1985, characters 14-27: Warning 48: implicit elimination of optional argument ?destroy Linking bin/why3ide.byte Ocamlc src/why3replayer/replay.ml Linking bin/why3replayer.byte Ocamlc src/why3session/why3session_lib.ml File "src/why3session/why3session_lib.ml", line 75, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 204, characters 2-16: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 208, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 214, characters 18-45: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 216, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 218, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 220, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 223, characters 2-17: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 225, characters 2-15: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 264, characters 14-29: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_lib.ml", line 257, characters 10-23: Warning 3: deprecated: String.create Use Bytes.create instead. Ocamlc src/why3session/why3session_copy.ml File "src/why3session/why3session_copy.ml", line 99, characters 14-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 133, characters 6-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 154, characters 20-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 155, characters 20-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 174, characters 2-61: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_copy.ml", line 180, characters 2-24: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_info.ml File "src/why3session/why3session_info.ml", line 407, characters 6-136: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_latex.ml File "src/why3session/why3session_latex.ml", line 300, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 303, characters 2-44: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 309, characters 2-43: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_latex.ml", line 312, characters 2-28: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_html.ml File "src/why3session/why3session_html.ml", line 371, characters 6-28: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 512, characters 6-24: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_html.ml", line 522, characters 6-28: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_rm.ml Ocamlc src/why3session/why3session_output.ml File "src/why3session/why3session_output.ml", line 69, characters 12-74: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 74, characters 12-73: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 76, characters 12-35: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_output.ml", line 92, characters 2-61: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_run.ml File "src/why3session/why3session_run.ml", line 184, characters 24-52: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_run.ml", line 311, characters 31-43: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session_csv.ml File "src/why3session/why3session_csv.ml", line 114, characters 23-56: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 198, characters 4-26: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 203, characters 32-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 205, characters 6-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 211, characters 6-47: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 254, characters 52-65: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 274, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 277, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 293, characters 2-32: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 310, characters 2-57: Warning 50: unattached documentation comment (ignored) File "src/why3session/why3session_csv.ml", line 331, characters 2-33: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3session/why3session.ml Linking bin/why3session.byte Ocamlc src/why3bench/worker.ml File "src/why3bench/worker.ml", line 137, characters 4-61: Warning 50: ambiguous documentation comment Ocamlc src/why3bench/db.ml Ocamlc src/why3bench/bench.ml File "src/why3bench/bench.ml", line 146, characters 4-72: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 229, characters 2-19: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 276, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 286, characters 2-14: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 293, characters 2-20: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 294, characters 2-18: Warning 50: unattached documentation comment (ignored) File "src/why3bench/bench.ml", line 346, characters 2-18: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3bench/benchrc.ml Ocamlc src/why3bench/benchdb.ml File "src/why3bench/benchdb.ml", line 41, characters 2-23: Warning 50: unattached documentation comment (ignored) File "src/why3bench/benchdb.ml", line 87, characters 2-29: Warning 50: unattached documentation comment (ignored) Ocamlc src/why3bench/why3bench.ml File "src/why3bench/why3bench.ml", line 200, characters 2-22: Warning 50: unattached documentation comment (ignored) File "src/why3bench/why3bench.ml", line 212, characters 2-16: Warning 50: unattached documentation comment (ignored) Linking bin/why3bench.byte Ocamlc lib/ocaml/why3__BigInt.ml Ocamlc lib/ocaml/why3__IntAux.ml Ocamlc lib/ocaml/why3__Array.ml Linking lib/why3/why3extract.cmo Linking lib/why3/why3extract.cma Ocamlc src/why3doc/doc_html.ml Ocamlc src/why3doc/doc_def.ml File "src/why3doc/doc_def.ml", line 79, characters 12-25: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/why3doc/doc_def.ml", line 84, characters 8-19: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 88, characters 8-21: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 89, characters 8-34: Warning 3: deprecated: String.set Use Bytes.set instead. File "src/why3doc/doc_def.ml", line 90, characters 8-36: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlc src/why3doc/doc_lexer.ml File "src/why3doc/doc_lexer.mll", line 65, characters 14-27: Warning 3: deprecated: String.create Use Bytes.create instead. File "src/why3doc/doc_lexer.mll", line 76, characters 15-26: Warning 3: deprecated: String.set Use Bytes.set instead. Ocamlc src/why3doc/doc_main.ml Linking bin/why3doc.byte gmake[1]: Leaving directory '/construction/math/why3/why3-0.83' SUCCEEDED 00:01:20 ------------------------------------------------------------------------------- -- Phase: run-depends ------------------------------------------------------------------------------- ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlfind - found SUCCEEDED 00:00:00 ------------------------------------------------------------------------------- -- Phase: stage ------------------------------------------------------------------------------- ===> Staging for why3-0.83_2 ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlc - found ===> why3-0.83_2 depends on file: /usr/local/bin/ocamlfind - found ===> Generating temporary packing list gmake[1]: Entering directory '/construction/math/why3/why3-0.83' rm -f /construction/math/why3/stage/usr/local/bin/why3* rm -rf /construction/math/why3/stage/usr/local/share/why3 rm -rf /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3 mkdir -p /construction/math/why3/stage/usr/local/bin mkdir -p /construction/math/why3/stage/usr/local/share/why3 mkdir -p /construction/math/why3/stage/usr/local/share/why3/images mkdir -p /construction/math/why3/stage/usr/local/share/why3/images/boomy mkdir -p /construction/math/why3/stage/usr/local/share/why3/images/fatcow mkdir -p /construction/math/why3/stage/usr/local/share/why3/emacs mkdir -p /construction/math/why3/stage/usr/local/share/why3/vim mkdir -p /construction/math/why3/stage/usr/local/share/why3/lang mkdir -p /construction/math/why3/stage/usr/local/share/why3/theories mkdir -p /construction/math/why3/stage/usr/local/share/why3/modules/mach mkdir -p /construction/math/why3/stage/usr/local/share/why3/drivers cp -f theories/*.why /construction/math/why3/stage/usr/local/share/why3/theories cp -f modules/*.mlw /construction/math/why3/stage/usr/local/share/why3/modules cp -f modules/mach/*.mlw /construction/math/why3/stage/usr/local/share/why3/modules/mach cp -f drivers/*.drv drivers/*.gen /construction/math/why3/stage/usr/local/share/why3/drivers cp -f share/provers-detection-data.conf /construction/math/why3/stage/usr/local/share/why3/ cp -f share/images/icons.rc /construction/math/why3/stage/usr/local/share/why3/images cp -f share/images/*.png /construction/math/why3/stage/usr/local/share/why3/images cp -f share/images/boomy/*.png /construction/math/why3/stage/usr/local/share/why3/images/boomy cp -f share/images/fatcow/*.png /construction/math/why3/stage/usr/local/share/why3/images/fatcow cp -f share/why3session.dtd /construction/math/why3/stage/usr/local/share/why3 cp -rf share/javascript /construction/math/why3/stage/usr/local/share/why3/javascript cp -f share/emacs/why3.el /construction/math/why3/stage/usr/local/share/why3/emacs/why3.el cp -f share/vim/why3.vim /construction/math/why3/stage/usr/local/share/why3/vim/why3.vim cp -f share/lang/why3.lang /construction/math/why3/stage/usr/local/share/why3/lang/why3.lang rm -rf /construction/math/why3/stage/usr/local/lib/why3/plugins mkdir -p /construction/math/why3/stage/usr/local/lib/why3/plugins cp -f lib/plugins/genequlin.cmo lib/plugins/dimacs.cmo lib/plugins/tptp.cmo lib/plugins/hypothesis_selection.cmo lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs lib/plugins/hypothesis_selection.cmxs /construction/math/why3/stage/usr/local/lib/why3/plugins cp -f bin/why3.opt /construction/math/why3/stage/usr/local/bin/why3 cp -f bin/why3config.opt /construction/math/why3/stage/usr/local/bin/why3config cp -f bin/why3ide.opt /construction/math/why3/stage/usr/local/bin/why3ide cp -f bin/why3replayer.opt /construction/math/why3/stage/usr/local/bin/why3replayer cp -f bin/why3session.opt /construction/math/why3/stage/usr/local/bin/why3session cp -f bin/why3bench.opt /construction/math/why3/stage/usr/local/bin/why3bench cp drivers/coq-realizations.aux /construction/math/why3/stage/usr/local/share/why3/drivers/ cp drivers/pvs-realizations.aux /construction/math/why3/stage/usr/local/share/why3/drivers/ cp drivers/isabelle-realizations.aux /construction/math/why3/stage/usr/local/share/why3/drivers/ mkdir -p /construction/math/why3/stage/usr/local/lib/why3 cp -f lib/why3-cpulimit /construction/math/why3/stage/usr/local/lib/why3/why3-cpulimit cp -f lib/why3-call-pvs /construction/math/why3/stage/usr/local/lib/why3/why3-call-pvs cp -f bin/why3doc.opt /construction/math/why3/stage/usr/local/bin/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 /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3 cp -f lib/why3/why3.cm* lib/why3/why3.[ao] \ lib/why3/META /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3 mkdir -p /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3 cp -f lib/why3/why3extract.cm* lib/why3/why3extract.[ao] \ /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3 gmake[1]: Leaving directory '/construction/math/why3/why3-0.83' /usr/bin/strip /construction/math/why3/stage/usr/local/bin/why3* /construction/math/why3/stage/usr/local/lib/ocaml/site-lib/why3/*.o /construction/math/why3/stage/usr/local/lib/why3/plugins/*.cmxs /construction/math/why3/stage/usr/local/lib/why3/why3-cpulimit /bin/mkdir -p /construction/math/why3/stage/usr/local/share/doc/why3 install -m 0644 /construction/math/why3/why3-0.83/doc/manual.pdf /construction/math/why3/stage/usr/local/share/doc/why3 ====> Compressing man pages (compress-man) ====> Running Q/A tests (stage-qa) Error: /usr/local/bin/why3bench is linked to /usr/local/lib/libsqlite3.so.0 from databases/sqlite3 but it is not declared as a dependency Warning: you need USES+=sqlite Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgtksourceview-2.0.so.0 from x11-toolkits/gtksourceview2 but it is not declared as a dependency Warning: you need USE_GNOME+=gtksourceview2 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgtk-x11-2.0.so.0 from x11-toolkits/gtk20 but it is not declared as a dependency Warning: you need USE_GNOME+=gtk20 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgdk-x11-2.0.so.0 from x11-toolkits/gtk20 but it is not declared as a dependency Warning: you need USE_GNOME+=gtk20 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libpangocairo-1.0.so.0 from x11-toolkits/pango but it is not declared as a dependency Warning: you need USE_GNOME+=pango Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libatk-1.0.so.0 from accessibility/atk but it is not declared as a dependency Warning: you need USE_GNOME+=atk Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libcairo.so.2 from graphics/cairo but it is not declared as a dependency Warning: you need USE_GNOME+=cairo Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgdk_pixbuf-2.0.so.0 from graphics/gdk-pixbuf2 but it is not declared as a dependency Warning: you need USE_GNOME+=gdkpixbuf2 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgio-2.0.so.0 from devel/glib20 but it is not declared as a dependency Warning: you need USE_GNOME+=glib20 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libpangoft2-1.0.so.0 from x11-toolkits/pango but it is not declared as a dependency Warning: you need USE_GNOME+=pango Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libpango-1.0.so.0 from x11-toolkits/pango but it is not declared as a dependency Warning: you need USE_GNOME+=pango Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libgobject-2.0.so.0 from devel/glib20 but it is not declared as a dependency Warning: you need USE_GNOME+=glib20 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libglib-2.0.so.0 from devel/glib20 but it is not declared as a dependency Warning: you need USE_GNOME+=glib20 Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libintl.so.8 from devel/gettext-runtime but it is not declared as a dependency Warning: you need USES+=gettext-runtime Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libfontconfig.so.1 from x11-fonts/fontconfig but it is not declared as a dependency Warning: you need LIB_DEPENDS+=libfontconfig.so:x11-fonts/fontconfig Error: /usr/local/bin/why3ide is linked to /usr/local/lib/libfreetype.so.6 from print/freetype2 but it is not declared as a dependency Warning: you need LIB_DEPENDS+=libfreetype.so:print/freetype2 Warning: You have disabled the licenses framework with DISABLE_LICENSES, unable to run checks SUCCEEDED 00:00:03 ------------------------------------------------------------------------------- -- Phase: package ------------------------------------------------------------------------------- ===> Building package for why3-0.83_2 file sizes/checksums [188]: 0% file sizes/checksums [188]: 53% file sizes/checksums [188]: 100% packing files [188]: 0% packing files [188]: 53% packing files [188]: 100% packing directories [0]: 0% packing directories [0]: 100% SUCCEEDED 00:01:07 TOTAL TIME 00:04:14