opam-health-check log - why3-base.0.85 on 4.04

Home|Differences with the last checks|Previous runs

Building on m1-b.ocamllabs.io

(from ocurrent/opam:debian-unstable)
WARNING: Error loading config file: .dockercfg: $HOME is not defined
2021-07-05 06:34.23 ---> using "ec5d5faa8619574bfe663422158251f52f4b465bd9d157e348e692194b4f4a2a" from cache

/: (user (uid 1000) (gid 1000))

/: (env OPAMPRECISETRACKING 1)

/: (env OPAMDEPEXTYES 1)

/: (env OPAMUTF8 never)

/: (run (network host)
        (shell  "\
               \n        set -e\
               \n        git clone -q git://github.com/kit-ty-kate/opam.git /tmp/opam\
               \n        git -C /tmp/opam checkout -q '72695bfac80dbcd1d2f10287b2626d18d4acc9f2'\
               \n        opam remote set-url default git://github.com/ocaml/opam-repository.git\
               \n        opam pin add -yn /tmp/opam > /dev/null\
               \n        opam install -y opam-devel opam-0install-cudf 'ocamlfind>=1.9'\
               \n        sudo mv \"$(opam var opam-devel:lib)/opam\" /usr/bin/opam\
               \n        rm -rf /tmp/opam /tmp/depext.txt ~/.opam\
               \n        if ! test -d ~/opam-repository; then\
               \n          git clone -q git://github.com/ocaml/opam-repository.git ~/opam-repository\
               \n        else\
               \n          git -C ~/opam-repository pull -q origin master\
               \n        fi\
               \n        git -C ~/opam-repository checkout -q '9c3fe9d253394788e95360e5c2bcb22722fae6f5'\
               \n      "))
[default] Initialised

<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[opam-devel.2.1.0~beta4] no changes from git+file:///tmp/opam#HEAD

The following actions will be performed:
  - install ocamlfind          1.9.1
  - install seq                base         [required by re]
  - install cmdliner           1.0.4        [required by opam-devel]
  - install dune               2.9.0        [required by opam-0install-cudf, opam-devel]
  - install ocamlbuild         0.14.0       [required by cudf]
  - install base-bytes         base         [required by extlib]
  - install stdlib-shims       0.3.0        [required by ocamlgraph]
  - install re                 1.9.0        [required by opam-client]
  - install opam-file-format   2.1.3        [required by opam-format]
  - install cppo               1.6.7        [required by extlib]
  - install 0install-solver    2.17         [required by opam-0install-cudf]
  - install ocamlgraph         2.0.0        [required by dose3]
  - install extlib             1.7.7-1      [required by cudf, opam-client]
  - install opam-core          2.1.0~beta4* [required by opam-format]
  - install cudf               0.9-1        [required by opam-0install-cudf]
  - install opam-format        2.1.0~beta4* [required by opam-repository, opam-solver]
  - install opam-0install-cudf 0.4.2
  - install mccs               1.1+13       [required by opam-solver]
  - install dose3              5.0.1-1      [required by opam-solver]
  - install opam-repository    2.1.0~beta4* [required by opam-client]
  - install opam-solver        2.1.0~beta4* [required by opam-client]
  - install opam-state         2.1.0~beta4* [required by opam-client]
  - install opam-client        2.1.0~beta4* [required by opam-devel]
  - install opam-devel         2.1.0~beta4*
===== 24 to install =====

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[cppo.1.6.7] downloaded from https://github.com/ocaml-community/cppo/releases/download/v1.6.7/cppo-v1.6.7.tbz
[0install-solver.2.17] downloaded from https://github.com/0install/0install/releases/download/v2.17/0install-v2.17.tbz
[cmdliner.1.0.4] downloaded from http://erratique.ch/software/cmdliner/releases/cmdliner-1.0.4.tbz
[dose3.5.0.1-1] downloaded from https://gforge.inria.fr/frs/download.php/file/36063/dose3-5.0.1.tar.gz
[dune.2.9.0] downloaded from https://github.com/ocaml/dune/releases/download/2.9.0/dune-2.9.0.tbz
[cudf.0.9-1] downloaded from https://gforge.inria.fr/frs/download.php/36602/cudf-0.9.tar.gz
[extlib.1.7.7-1] downloaded from https://ygrek.org/p/release/ocaml-extlib/extlib-1.7.7.tar.gz
[mccs.1.1+13] downloaded from https://github.com/AltGr/ocaml-mccs/archive/1.1+13.tar.gz
[ocamlbuild.0.14.0] downloaded from https://github.com/ocaml/ocamlbuild/archive/0.14.0.tar.gz
[ocamlfind.1.9.1] downloaded from http://download.camlcity.org/download/findlib-1.9.1.tar.gz
[ocamlgraph.2.0.0] downloaded from https://github.com/backtracking/ocamlgraph/releases/download/2.0.0/ocamlgraph-2.0.0.tbz
[opam-0install-cudf.0.4.2] downloaded from https://github.com/ocaml-opam/opam-0install-solver/releases/download/v0.4.2/opam-0install-cudf-v0.4.2.tbz
[opam-file-format.2.1.3] downloaded from https://github.com/ocaml/opam-file-format/archive/2.1.3.tar.gz
[stdlib-shims.0.3.0] downloaded from https://github.com/ocaml/stdlib-shims/releases/download/0.3.0/stdlib-shims-0.3.0.tbz
[re.1.9.0] downloaded from https://github.com/ocaml/ocaml-re/releases/download/1.9.0/re-1.9.0.tbz

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed seq.base
-> installed cmdliner.1.0.4
-> installed ocamlfind.1.9.1
-> installed base-bytes.base
-> installed ocamlbuild.0.14.0
-> installed dune.2.9.0
-> installed stdlib-shims.0.3.0
-> installed opam-file-format.2.1.3
-> installed 0install-solver.2.17
-> installed cppo.1.6.7
-> installed re.1.9.0
-> installed ocamlgraph.2.0.0
-> installed extlib.1.7.7-1
-> installed opam-core.2.1.0~beta4
-> installed cudf.0.9-1
-> installed opam-0install-cudf.0.4.2
-> installed mccs.1.1+13
-> installed opam-format.2.1.0~beta4
-> installed opam-repository.2.1.0~beta4
-> installed dose3.5.0.1-1
-> installed opam-state.2.1.0~beta4
-> installed opam-solver.2.1.0~beta4
-> installed opam-client.2.1.0~beta4
-> installed opam-devel.2.1.0~beta4
Done.

<><> opam-devel.2.1.0~beta4 installed successfully ><><><><><><><><><><><><><><>
=> The development version of opam has been successfully compiled into /home/opam/.opam/4.11/lib/opam-devel. You should not run it from there, please install the binaries to your PATH, e.g. with
       sudo cp /home/opam/.opam/4.11/lib/opam-devel/opam /usr/local/bin

   If you just want to give it a try without altering your current installation, you could use instead:
       alias opam2="OPAMROOT=~/.opam2 /home/opam/.opam/4.11/lib/opam-devel/opam"
# Run eval $(opam env) to update the current shell environment
Updating files:  96% (11734/12211)
Updating files:  97% (11845/12211)
Updating files:  98% (11967/12211)
Updating files:  99% (12089/12211)
Updating files: 100% (12211/12211)
Updating files: 100% (12211/12211), done.
2021-07-05 06:34.23 ---> using "307be9aa5cdafafceded4bdc6f1d2d6cc6421661c3851f395cf39dd0065265a9" from cache

/: (env OPAMEXTERNALSOLVER builtin-0install)

/: (env OPAMCRITERIA +removed)

/: (run (shell "rm -rf ~/.opam && opam init -ya --bare --config ~/.opamrc-sandbox ~/opam-repository"))
Configuring from /home/opam/.opamrc-sandbox, then /home/opam/.opamrc, and finally from built-in defaults.
Checking for available remotes: rsync and local, git.
  - you won't be able to use mercurial repositories unless you install the hg command on your system.
  - you won't be able to use darcs repositories unless you install the darcs command on your system.


<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[default] Initialised

User configuration:
  ~/.profile is already up-to-date.
[NOTE] Make sure that ~/.profile is well sourced in your ~/.bashrc.

2021-07-05 06:34.23 ---> using "f9d18559158c26cb0236b11f8c3f1aca1927d54f77b8b978800f7461ab605d60" from cache

/: (run (network host)
        (shell "git clone -q 'git://github.com/ocaml/ocaml-beta-repository.git' ~/'beta' && git -C ~/'beta' checkout -q 79aeeadd813bdae424ab53f882f08bee0a4e0b89"))
2021-07-05 06:34.23 ---> using "0123e084a7b7841fc01d674ea3cc62b640a19885601c401c0149be13108a5da4" from cache

/: (run (shell "opam repository add --dont-select 'beta' ~/'beta'"))
[beta] Initialised
2021-07-05 06:34.23 ---> using "4382217c65ee8c899c1e38e76fe879b949ffb708f73e6e0a95f0a3814d01dd54" from cache

/: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
        (network host)
        (shell "opam switch create --repositories=beta,default 4.04.2"))

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.04.2"} | "ocaml-system" {= "4.04.2"}]

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed base-bigarray.base
-> installed base-threads.base
-> installed base-unix.base
-> retrieved ocaml-base-compiler.4.04.2  (cached)
-> installed ocaml-base-compiler.4.04.2
-> installed ocaml-config.1
-> installed ocaml.4.04.2
Done.
# Run eval $(opam env --switch=4.04.2) to update the current shell environment
2021-07-05 06:34.23 ---> using "8703de1c7b99ec1bccd0c06b261b0e55052b497436a26880a990dbff476827ed" from cache

/: (run (network host)
        (shell "opam update --depexts"))
+ /usr/bin/sudo "apt-get" "update"
- Get:1 http://deb.debian.org/debian unstable InRelease [161 kB]
- Get:2 http://deb.debian.org/debian unstable/main amd64 Packages.diff/Index [63.6 kB]
- Ign:2 http://deb.debian.org/debian unstable/main amd64 Packages.diff/Index
- Get:3 http://deb.debian.org/debian unstable/main amd64 Packages [8640 kB]
- Fetched 8865 kB in 2s (5495 kB/s)
- Reading package lists...
- 
2021-07-05 06:34.23 ---> using "cba8f6aafb248dedbca3e4d941c0dbf98f1fc89381534119d0455baef974cead" from cache

/: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
        (network host)
        (shell "opam install -y ocaml-secondary-compiler"))
The following actions will be performed:
  - install ocaml-secondary-compiler 4.08.1-1

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> retrieved ocaml-secondary-compiler.4.08.1-1  (cached)
-> installed ocaml-secondary-compiler.4.08.1-1
Done.
# Run eval $(opam env) to update the current shell environment
2021-07-05 06:34.23 ---> using "eed16c76ab0084d118e148007233264ec504a4684379a9da8e6e68fa8fb87e4a" from cache

/: (run (cache (opam-archives (target /home/opam/.opam/download-cache)))
        (network host)
        (shell  "\
               \nopam remove -y \"why3-base.0.85\"\
               \nopam install -vy \"why3-base.0.85\"\
               \nres=$?\
               \nif [ $res = 31 ]; then\
               \n    if opam show -f x-ci-accept-failures: \"why3-base.0.85\" | grep -q '\"debian-unstable\"'; then\
               \n        echo \"This package failed and has been disabled for CI using the 'x-ci-accept-failures' field.\"\
               \n        exit 69\
               \n    fi\
               \nfi\
               \n\
               \n\
               \nexit $res\
               \n"))
Nothing to do.
[NOTE] why3-base.0.85 is not installed.

The following actions will be performed:
  - remove  ocaml-secondary-compiler 4.08.1-1
  - install base-num                 base     [required by num]
  - install ocamlfind                1.9.1    [required by why3-base]
  - install num                      0        [required by why3-base]
  - install why3-base                0.85
===== 4 to install | 1 to remove =====

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> removed   ocaml-secondary-compiler.4.08.1-1
Processing  4/13:
Processing  5/13: [why3-base.0.85: http]
Processing  6/13: [why3-base.0.85: http]
-> installed base-num.base
Processing  7/13: [why3-base.0.85: http]
Processing  8/13: [why3-base.0.85: http]
-> installed num.0
Processing  9/13: [why3-base.0.85: http]
-> retrieved ocamlfind.1.9.1  (cached)
Processing 10/13: [why3-base.0.85: http] [ocamlfind: ./configure]
Processing 10/13: [ocamlfind: ./configure]
-> retrieved why3-base.0.85  (https://gforge.inria.fr/frs/download.php/file/34074/why3-0.85.tar.gz)
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "-bindir" "/home/opam/.opam/4.04.2/bin" "-sitelib" "/home/opam/.opam/4.04.2/lib" "-mandir" "/home/opam/.opam/4.04.2/man" "-config" "/home/opam/.opam/4.04.2/lib/findlib.conf" "-no-custom" "-no-camlp4" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1)
- Welcome to findlib version 1.9.1
- Configuring core...
- Checking for #remove_directory...
- Testing threading model...
- systhread_supported: true
- Testing DLLs...
- Testing whether ppxopt can be supported...
- Checking for ocamlc -opaque...
- Querying installation: META list not found
- make install will double-check installed META files
- Configuring libraries...
- unix: found
- bigarray: found
- compiler-libs: found
- dbm: not present (normal since 4.00)
- graphics: found
- num: found
- ocamlbuild: not present (normal since 4.03)
- ocamldoc: found
- raw_spacetime: found
- threads: found
- str: found
- labltk: not present (normal since 4.02)
- native dynlink: found
- camlp4: disabled
- bytes: found, installing fake library
- Configuration for dynlink written to site-lib-src/dynlink/META
- Configuration for stdlib written to site-lib-src/stdlib/META
- Configuration for unix written to site-lib-src/unix/META
- Configuration for bigarray written to site-lib-src/bigarray/META
- Configuration for compiler-libs written to site-lib-src/compiler-libs/META
- Configuration for graphics written to site-lib-src/graphics/META
- Configuration for num written to site-lib-src/num/META
- Configuration for num-top written to site-lib-src/num-top/META
- Configuration for ocamldoc written to site-lib-src/ocamldoc/META
- Configuration for raw_spacetime written to site-lib-src/raw_spacetime/META
- Configuration for threads written to site-lib-src/threads/META
- Configuration for str written to site-lib-src/str/META
- Configuration for bytes written to site-lib-src/bytes/META
- Detecting compiler arguments: (extractor built) ok
- 
- About the OCAML core installation:
-     Standard library:      /home/opam/.opam/4.04.2/lib/ocaml
-     Binaries:              /home/opam/.opam/4.04.2/bin
-     Manual pages:          /home/opam/.opam/4.04.2/man
-     Multi-threading type:  posix
- The directory of site-specific packages will be
-     site-lib:              /home/opam/.opam/4.04.2/lib
- The configuration file is written to:
-     findlib config file:   /home/opam/.opam/4.04.2/lib/findlib.conf
- Software will be installed:
-     Libraries:             in <site-lib>/findlib
-     Binaries:              /home/opam/.opam/4.04.2/bin
-     Manual pages:          /home/opam/.opam/4.04.2/man
-     topfind script:        /home/opam/.opam/4.04.2/lib/ocaml
- Topfind ppxopt support:    yes
- Toolbox:                   no
- Link custom runtime:       no
- Need bytes compatibility:  no
- 
- Configuration has been written to Makefile.config
- 
- You can now do 'make all', and optionally 'make opt', to build ocamlfind.
Processing 10/13: [ocamlfind: make all]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "make" "all" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1)
- for p in findlib; do ( cd src/$p; make all ) || exit; done
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- ocamllex fl_meta.mll
- 22 states, 392 transitions, table size 1700 bytes
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib_config.mlp | \
-          ../../tools/patch '@CONFIGFILE@' '/home/opam/.opam/4.04.2/lib/findlib.conf' | \
-          ../../tools/patch '@STDLIB@' '/home/opam/.opam/4.04.2/lib/ocaml' | \
- 	sed -e 's;@AUTOLINK@;true;g' \
- 	    -e 's;@SYSTEM@;linux;g' \
- 	     >findlib_config.ml
- if [ "true" = "true" ]; then                 \
- 	cp topfind.ml.in topfind.ml;                             \
- else                                                             \
- 	sed -e '/PPXOPT_BEGIN/,/PPXOPT_END/ d' topfind.ml.in     \
- 		> topfind.ml ;                                   \
- fi
- ocamldep *.ml *.mli >depend
- ocamlc -I +compiler-libs -opaque -g -c findlib_config.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_split.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_metatoken.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_meta.ml
- ocamlc -I +compiler-libs -opaque -c fl_metascanner.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_metascanner.ml
- ocamlc -I +compiler-libs -opaque -c fl_topo.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_topo.ml
- ocamlc -I +compiler-libs -opaque -c fl_package_base.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_package_base.ml
- ocamlc -I +compiler-libs -opaque -c findlib.mli
- ocamlc -I +compiler-libs -opaque -g -c findlib.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_args.ml
- ocamlc -I +compiler-libs -opaque -g -c fl_lint.ml
- ocamlc -I +compiler-libs -a -o findlib.cma findlib_config.cmo fl_split.cmo fl_metatoken.cmo fl_meta.cmo fl_metascanner.cmo fl_topo.cmo fl_package_base.cmo findlib.cmo fl_args.cmo fl_lint.cmo
- ocamlc -I +compiler-libs -opaque -g -c ocaml_args.ml
- ocamlc -I +compiler-libs -opaque -g -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- ocamlc -I +compiler-libs  -o ocamlfind -g findlib.cma unix.cma \
-            ocaml_args.cmo frontend.cmo
- ocamlc -I +compiler-libs -opaque -c topfind.mli
- ocamlc -I +compiler-libs -opaque -g -c topfind.ml
- ocamlc -I +compiler-libs -a -o findlib_top.cma topfind.cmo
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat topfind_rd1.p | \
-          ../../tools/patch '@SITELIB@' '/home/opam/.opam/4.04.2/lib' \
-     	    >topfind
- ocamlc -I +compiler-libs -opaque -c num_top_printers.mli
- ocamlc -I +compiler-libs -opaque -g -c num_top_printers.ml
- ocamlc -I +compiler-libs -opaque -c num_top.mli
- ocamlc -I +compiler-libs -opaque -g -c num_top.ml
- ocamlc -I +compiler-libs -a -o num_top.cma num_top_printers.cmo num_top.cmo
- ocamlc -I +compiler-libs -opaque -c fl_dynload.mli
- ocamlc -I +compiler-libs -opaque -g -c fl_dynload.ml
- ocamlc -I +compiler-libs -a -o findlib_dynload.cma fl_dynload.cmo
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- make all-config
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- USE_CYGPATH="0"; \
- export USE_CYGPATH; \
- cat findlib.conf.in | \
-      tools/patch '@SITELIB@' '/home/opam/.opam/4.04.2/lib' >findlib.conf
- if ./tools/cmd_from_same_dir ocamlc; then \
- 	echo 'ocamlc="ocamlc.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamlopt; then \
- 	echo 'ocamlopt="ocamlopt.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldep; then \
- 	echo 'ocamldep="ocamldep.opt"' >>findlib.conf; \
- fi
- if ./tools/cmd_from_same_dir ocamldoc; then \
- 	echo 'ocamldoc="ocamldoc.opt"' >>findlib.conf; \
- fi
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
Processing 10/13: [ocamlfind: make opt]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "make" "opt" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1)
- for p in findlib; do ( cd src/$p; make opt ) || exit; done
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- ocamlopt -I +compiler-libs -g -opaque -c findlib_config.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_split.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metatoken.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_meta.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_metascanner.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_topo.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_package_base.ml
- ocamlopt -I +compiler-libs -g -opaque -c findlib.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c fl_lint.ml
- ocamlopt -I +compiler-libs -g -a -o findlib.cmxa findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx
- if [ 1 -gt 0 ]; then \
-     ocamlopt -I +compiler-libs -g -shared -o findlib.cmxs findlib_config.cmx fl_split.cmx fl_metatoken.cmx fl_meta.cmx fl_metascanner.cmx fl_topo.cmx fl_package_base.cmx findlib.cmx fl_args.cmx fl_lint.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c ocaml_args.ml
- ocamlopt -I +compiler-libs -g -opaque -c frontend.ml
- File "frontend.ml", line 1826, characters 16-29:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- ocamlopt -I +compiler-libs -g -o ocamlfind_opt findlib.cmxa unix.cmxa \
- 	   ocaml_args.cmx frontend.cmx
- ocamlopt -I +compiler-libs -g -opaque -c topfind.ml
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Topdirs, and its interface was not compiled with -opaque
- File "_none_", line 1:
- Warning 58: no cmx file was found in path for module Toploop, and its interface was not compiled with -opaque
- ocamlopt -I +compiler-libs -g -a -o findlib_top.cmxa topfind.cmx
- if [ 1 -gt 0 ]; then \
-     ocamlopt -I +compiler-libs -g -shared -o findlib_top.cmxs topfind.cmx; \
- fi
- ocamlopt -I +compiler-libs -g -opaque -c fl_dynload.ml
- ocamlopt -I +compiler-libs -g -a -o findlib_dynload.cmxa fl_dynload.cmx
- if [ 1 -gt 0 ]; then \
-     ocamlopt -I +compiler-libs -g -shared -o findlib_dynload.cmxs fl_dynload.cmx; \
- fi
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
-> compiled  ocamlfind.1.9.1
Processing 11/13: [ocamlfind: make install]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1)
- if [ "1" -eq 1 ]; then \
-     for x in camlp4 dbm graphics labltk num ocamlbuild; do \
-       if [ -f "/home/opam/.opam/4.04.2/lib/$x/META" ]; then \
-         if ! grep -Fq '[distributed with Ocaml]' "//home/opam/.opam/4.04.2/lib/$x/META"; then \
-           rm -f site-lib-src/$x/META; \
-         fi \
-       fi \
-     done; \
-     test -f "site-lib-src/num/META" || rm -f "site-lib-src/num-top/META"; \
-   fi
- echo 'SITELIB_META =' > Makefile.packages.in
- for x in `ls site-lib-src`; do test ! -f "site-lib-src/$x/META" || echo $x >> Makefile.packages.in; done
- tr '\n' ' ' < Makefile.packages.in > Makefile.packages
- rm Makefile.packages.in
- mkdir -p "/home/opam/.opam/4.04.2/bin"
- mkdir -p "/home/opam/.opam/4.04.2/man"
- make install-config
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- mkdir -p "`dirname \"/home/opam/.opam/4.04.2/lib/findlib.conf\"`"
- test -f "/home/opam/.opam/4.04.2/lib/findlib.conf" || cp findlib.conf "/home/opam/.opam/4.04.2/lib/findlib.conf"
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- for p in findlib; do ( cd src/$p; make install ); done
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- mkdir -p "/home/opam/.opam/4.04.2/lib/findlib"
- mkdir -p "/home/opam/.opam/4.04.2/bin"
- test 1 -eq 0 || cp topfind "/home/opam/.opam/4.04.2/lib/ocaml"
- files=` ../../tools/collect_files ../../Makefile.config findlib.cmi findlib.mli findlib.cma findlib.cmxa findlib.a findlib.cmxs topfind.cmi topfind.mli fl_package_base.mli fl_package_base.cmi fl_metascanner.mli fl_metascanner.cmi fl_metatoken.cmi findlib_top.cma findlib_top.cmxa findlib_top.a findlib_top.cmxs findlib_dynload.cma findlib_dynload.cmxa findlib_dynload.a findlib_dynload.cmxs fl_dynload.mli fl_dynload.cmi META` && \
- cp $files "/home/opam/.opam/4.04.2/lib/findlib"
- f="ocamlfind"; { test -f ocamlfind_opt && f="ocamlfind_opt"; }; \
- cp $f "/home/opam/.opam/4.04.2/bin/ocamlfind"
- # the following "if" block is only needed for 4.00beta2
- if [ 1 -eq 0 -a -f "/home/opam/.opam/4.04.2/lib/ocaml/compiler-libs/topdirs.cmi" ]; then \
-     cd "/home/opam/.opam/4.04.2/lib/ocaml/compiler-libs/"; \
-     cp topdirs.cmi toploop.cmi "/home/opam/.opam/4.04.2/lib/findlib/"; \
- fi
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- make install-meta
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- for x in bigarray bytes compiler-libs dynlink graphics num num-top ocamldoc raw_spacetime stdlib str threads unix ; do mkdir -p "/home/opam/.opam/4.04.2/lib/$x"; cp site-lib-src/$x/META "/home/opam/.opam/4.04.2/lib/$x"; done
- mkdir -p "/home/opam/.opam/4.04.2/lib/findlib"; cp Makefile.packages "/home/opam/.opam/4.04.2/lib/findlib/Makefile.packages"
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- test ! -f 'site-lib-src/num-top/META' || { cd src/findlib; make install-num-top; }
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- mkdir -p "/home/opam/.opam/4.04.2/lib/num-top"
- cp num_top.cma num_top.cmi num_top_printers.cmi \
- 	"/home/opam/.opam/4.04.2/lib/num-top"
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1/src/findlib'
- test ! -f 'site-lib-src/camlp4/META' ||	cp tools/safe_camlp4 "/home/opam/.opam/4.04.2/bin"
- make install-doc
- make[1]: Entering directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
- mkdir -p "/home/opam/.opam/4.04.2/man/man1" "/home/opam/.opam/4.04.2/man/man3" "/home/opam/.opam/4.04.2/man/man5"
- cp doc/ref-man/ocamlfind.1 "/home/opam/.opam/4.04.2/man/man1"
- cp doc/ref-man/META.5 doc/ref-man/site-lib.5 doc/ref-man/findlib.conf.5 "/home/opam/.opam/4.04.2/man/man5"
- make[1]: Leaving directory '/home/opam/.opam/4.04.2/.opam-switch/build/ocamlfind.1.9.1'
-> installed ocamlfind.1.9.1
Processing 12/13: [why3-base: ./configure]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "./configure" "--prefix" "/home/opam/.opam/4.04.2" "--disable-bench" "--disable-frama-c" "--disable-ide" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/why3-base.0.85)
- configure: WARNING: unrecognized options: --disable-bench
- checking executable suffix... <none>
- checking for gcc... gcc
- checking whether the C compiler works... yes
- checking for C compiler default output file name... a.out
- checking for suffix of executables... 
- checking whether we are cross compiling... no
- checking for suffix of object files... o
- checking whether we are using the GNU C compiler... yes
- checking whether gcc accepts -g... yes
- checking for gcc option to accept ISO C89... none needed
- checking for ocamlc... ocamlc
- ocaml version is 4.04.2
- ocaml library path is /home/opam/.opam/4.04.2/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... no
- checking for ocamlfind... yes
- checking for rubber... no
- configure: WARNING: Cannot find rubber, documentation disabled.
- checking for emacs... no
- ocamlfind: Package `zarith' not found
- checking for /home/opam/.opam/4.04.2/lib/ocaml/zarith/zarith.cma... no
- configure: WARNING: Lib Zarith not found, using Nums instead.
- ocamlfind: Package `zip' not found
- checking for /home/opam/.opam/4.04.2/lib/ocaml/zip/zip.cma... no
- configure: WARNING: Lib camlzip not found, sessions files will not be compressed.
- checking for coqc... no
- configure: WARNING: Cannot find coqc.
- checking for pvs... no
- configure: WARNING: Cannot find pvs.
- checking for isabelle... no
- configure: WARNING: Cannot find isabelle.
- ocamlfind: Package `ocamlgraph' not found
- checking for /home/opam/.opam/4.04.2/lib/ocaml/ocamlgraph/... no
- configure: WARNING: Lib ocamlgraph not found, hypothesis selection disabled.
- configure: creating ./config.status
- config.status: creating Makefile
- config.status: creating src/config.sh
- config.status: creating doc/version.tex
- config.status: creating lib/why3/META
- config.status: creating .merlin
- config.status: creating src/jessie/Makefile
- config.status: executing chmod commands
- configure: WARNING: unrecognized options: --disable-bench
- 
-                  Summary
- -----------------------------------------
- Verbose make                : no
- OCaml compiler              : yes
-     Version                 : 4.04.2
-     Library path            : /home/opam/.opam/4.04.2/lib/ocaml
-     Native compilation      : yes
-     Profiling               : no
- Components
-     IDE command             : no
-     GMP arithmetic          : no (zarith not found)
-     Compressed sessions     : no (camlzip not found)
-     Hypothesis selection    : no (ocamlgraph not found)
-     Frama-C support         : no
- Documentation               : no (rubber not found)
- Support for interactive proof assistants
-     Coq                     : no (coqc not found)
-     PVS                     : no (pvs not found)
-     Isabelle                : no (isabelle not found)
- Installable                 : yes
-     Binary path             : ${exec_prefix}/bin
-     Lib path                : ${exec_prefix}/lib/why3
-     Data path               : ${prefix}/share/why3
-     Ocaml Library           : /home/opam/.opam/4.04.2/lib/why3
-     Relocatable             : no
Processing 12/13: [why3-base: make opt]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "build" "make" "opt" "byte" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/why3-base.0.85)
- Ocamllex src/why3doc/doc_lexer.mll
- 108 states, 991 transitions, table size 4612 bytes
- 1683 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_num.ml lib/ocaml/why3__BigInt_compat.ml
- Ocamldep lib/ocaml/why3__Array.ml
- Ocamldep lib/ocaml/why3__IntAux.ml
- Ocamldep lib/ocaml/why3__BigInt.ml
- Ocamldep lib/ocaml/why3__BigInt_compat.ml
- Ocamldep src/why3session/why3session_main.ml
- Ocamldep src/why3session/why3session_csv.ml
- Ocamldep src/why3session/why3session_run.ml
- Ocamldep src/why3session/why3session_output.ml
- Ocamldep src/why3session/why3session_rm.ml
- Ocamldep src/why3session/why3session_html.ml
- Ocamldep src/why3session/why3session_latex.ml
- Ocamldep src/why3session/why3session_info.ml
- Ocamldep src/why3session/why3session_copy.ml
- Ocamldep src/why3session/why3session_lib.ml
- Ocamllex src/tools/why3wc.mll
- 298 states, 15365 transitions, table size 63248 bytes
- Ocamldep src/tools/why3wc.ml
- Ocamldep src/tools/why3replay.ml
- Ocamldep src/tools/why3realize.ml
- Ocamldep src/tools/why3prove.ml
- Ocamldep src/tools/why3extract.ml
- Ocamldep src/tools/why3execute.ml
- Ocamldep src/tools/why3config.ml
- Ocamldep src/tools/main.ml
- Ocamllex plugins/tptp/tptp_lexer.mll
- 101 states, 1563 transitions, table size 6858 bytes
- 3126 additional bytes used for bindings
- 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/parser/dimacs.ml
- Ocamldep plugins/parser/genequlin.ml
- Generate src/util/config.ml
- Ocamllex src/util/rc.mll
- 48 states, 1889 transitions, table size 7844 bytes
- 3073 additional bytes used for bindings
- Ocamllex src/util/lexlib.mll
- 16 states, 260 transitions, table size 1136 bytes
- Ocamllex src/parser/lexer.mll
- 127 states, 3137 transitions, table size 13310 bytes
- 7452 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
- cp src/session/compress_none.ml src/session/compress.ml
- Ocamllex src/session/xml.mll
- 114 states, 1396 transitions, table size 6268 bytes
- 3538 additional bytes used for bindings
- Ocamllex src/session/strategy_parser.mll
- 39 states, 619 transitions, table size 2710 bytes
- 1755 additional bytes used for bindings
- Ocamldep src/session/session_scheduler.ml
- Ocamldep src/session/strategy_parser.ml
- Ocamldep src/session/strategy.ml
- Ocamldep src/session/session_tools.ml
- Ocamldep src/session/session.ml
- Ocamldep src/session/termcode.ml
- Ocamldep src/session/xml.ml
- Ocamldep src/session/compress.ml
- Ocamldep src/whyml/mlw_interp.ml
- Ocamldep src/whyml/mlw_main.ml
- Ocamldep src/whyml/mlw_ocaml.ml
- Ocamldep src/whyml/mlw_driver.ml
- Ocamldep src/whyml/mlw_typing.ml
- Ocamldep src/whyml/mlw_dexpr.ml
- Ocamldep src/whyml/mlw_module.ml
- Ocamldep src/whyml/mlw_wp.ml
- Ocamldep src/whyml/mlw_pretty.ml
- Ocamldep src/whyml/mlw_decl.ml
- Ocamldep src/whyml/mlw_expr.ml
- Ocamldep src/whyml/mlw_ty.ml
- Ocamldep src/printer/mathematica.ml
- Ocamldep src/printer/yices.ml
- Ocamldep src/printer/cvc3.ml
- Ocamldep src/printer/gappa.ml
- Ocamldep src/printer/simplify.ml
- Ocamldep src/printer/isabelle.ml
- Ocamldep src/printer/pvs.ml
- Ocamldep src/printer/coq.ml
- Ocamldep src/printer/smtv2.ml
- Ocamldep src/printer/smtv1.ml
- Ocamldep src/printer/why3printer.ml
- Ocamldep src/printer/alt_ergo.ml
- Ocamldep src/transform/compute.ml
- Ocamldep src/transform/reduction_engine.ml
- Ocamldep src/transform/smoke_detector.ml
- Ocamldep src/transform/instantiate_predicate.ml
- Ocamldep src/transform/eval_match.ml
- Ocamldep src/transform/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/parser/lexer.ml
- Ocamldep src/parser/typing.ml
- Ocamldep src/parser/parser.ml
- Ocamldep src/parser/glob.ml
- Ocamldep src/parser/ptree.ml
- Ocamldep src/mlw/ity.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/core/printer.ml
- Ocamldep src/core/trans.ml
- Ocamldep src/core/env.ml
- Ocamldep src/core/dterm.ml
- Ocamldep src/core/pretty.ml
- Ocamldep src/core/task.ml
- Ocamldep src/core/theory.ml
- Ocamldep src/core/decl.ml
- Ocamldep src/core/pattern.ml
- Ocamldep src/core/term.ml
- Ocamldep src/core/ty.ml
- Ocamldep src/core/ident.ml
- Ocamldep src/util/pqueue.ml
- Ocamldep src/util/number.ml
- Ocamldep src/util/bigInt.ml
- Ocamldep src/util/plugin.ml
- Ocamldep src/util/rc.ml
- Ocamldep src/util/sysutil.ml
- Ocamldep src/util/warning.ml
- Ocamldep src/util/cmdline.ml
- Ocamldep src/util/print_tree.ml
- Ocamldep src/util/lexlib.ml
- Ocamldep src/util/loc.ml
- Ocamldep src/util/debug.ml
- Ocamldep src/util/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 36, characters 12-25:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/util/strings.ml", line 38, 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
- 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 180, 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 181, 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/lexlib.mli
- Ocamlopt src/util/lexlib.ml
- File "src/util/lexlib.mll", line 101, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/util/lexlib.mll", line 103, characters 46-56:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- 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
- Ocamlopt src/core/ty.ml
- Ocamlc   src/core/term.mli
- File "src/core/term.mli", line 391, characters 0-72:
- Warning 50: ambiguous documentation comment
- 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
- 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 233, characters 0-93:
- Warning 50: ambiguous documentation comment
- File "src/driver/whyconf.mli", line 240, 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 304, characters 2-33:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 309, characters 2-39:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 312, characters 2-24:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 644, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 653, characters 2-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 658, characters 2-23:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 672, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 689, characters 2-23:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 699, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 559, 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/mlw/ity.mli
- File "src/mlw/ity.mli", line 161, characters 23-57:
- Warning 50: ambiguous documentation comment
- Ocamlopt src/mlw/ity.ml
- Ocamlopt src/parser/ptree.ml
- Ocamlc   src/parser/glob.mli
- Ocamlopt src/parser/glob.ml
- Ocamlc   src/parser/parser.mli
- Ocamlopt src/parser/parser.ml
- Ocamlc   src/parser/typing.mli
- Ocamlopt src/parser/typing.ml
- Ocamlc   src/parser/lexer.mli
- Ocamlopt src/parser/lexer.ml
- Ocamlc   src/transform/simplify_formula.mli
- Ocamlopt src/transform/simplify_formula.ml
- 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/transform/reduction_engine.mli
- Ocamlopt src/transform/reduction_engine.ml
- Ocamlc   src/transform/compute.mli
- Ocamlopt src/transform/compute.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 408, characters 4-30:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 420, characters 4-34:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 794, characters 2-154:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 136, characters 22-30:
- Warning 48: implicit elimination of optional argument ?whytypes
- File "src/printer/coq.ml", line 371, characters 38-46:
- Warning 48: implicit elimination of optional argument ?whytypes
- File "src/printer/coq.ml", line 467, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/printer/coq.ml", line 674, characters 42-57:
- Warning 48: implicit elimination of optional arguments ?whytypes, ?implicit
- File "src/printer/coq.ml", line 687, characters 31-46:
- Warning 48: implicit elimination of optional arguments ?whytypes, ?implicit
- Ocamlopt src/printer/pvs.ml
- Ocamlopt src/printer/isabelle.ml
- File "src/printer/isabelle.ml", line 329, 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/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
- Ocamlc   src/session/compress.mli
- Ocamlopt src/session/compress.ml
- Ocamlc   src/session/xml.mli
- Ocamlopt src/session/xml.ml
- Ocamlc   src/session/termcode.mli
- Ocamlopt src/session/termcode.ml
- File "src/session/termcode.ml", line 259, characters 2-16:
- Warning 3: deprecated: Format.bprintf
- File "src/session/termcode.ml", line 437, characters 6-20:
- Warning 3: deprecated: Format.bprintf
- Ocamlc   src/session/session.mli
- File "src/session/session.mli", line 528, characters 2-72:
- Warning 50: ambiguous documentation comment
- Ocamlopt src/session/session.ml
- File "src/session/session.ml", line 92, characters 2-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 402, characters 6-191:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 665, characters 4-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1132, characters 4-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1306, characters 8-62:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1348, characters 12-34:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1426, characters 2-56:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1464, characters 6-48:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1499, characters 6-51:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1622, characters 2-73:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1683, characters 8-76:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1852, characters 4-30:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1925, characters 2-49:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1930, characters 22-66:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1934, characters 8-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1945, characters 12-74:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2049, characters 13-43:
- Warning 50: ambiguous documentation comment
- File "src/session/session.ml", line 2058, characters 15-45:
- Warning 50: ambiguous documentation comment
- File "src/session/session.ml", line 2121, characters 2-55:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2122, characters 2-91:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2125, characters 2-49:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2180, characters 2-48:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2264, characters 2-164:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2284, characters 6-62:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2285, characters 6-56:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2628, characters 2-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2635, characters 51-72:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1517, characters 10-23:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/session/session.ml", line 1546, characters 16-27:
- Warning 3: deprecated: String.copy
- File "src/session/session.ml", line 74, characters 0-36:
- Warning 60: unused module Spos.
- File "src/session/session.ml", line 75, 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/strategy.mli
- Ocamlopt src/session/strategy.ml
- Ocamlc   src/session/strategy_parser.mli
- Ocamlopt src/session/strategy_parser.ml
- File "src/session/strategy_parser.mll", line 146, characters 16-28:
- Warning 3: deprecated: Array.create
- Use Array.make instead.
- Ocamlc   src/session/session_scheduler.mli
- File "src/session/session_scheduler.mli", line 266, characters 21-80:
- Warning 50: unattached documentation comment (ignored)
- Ocamlopt src/session/session_scheduler.ml
- File "src/session/session_scheduler.ml", line 91, characters 6-45:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 141, characters 2-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 156, characters 2-50:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 170, characters 2-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 894, characters 4-64:
- Warning 50: unattached documentation comment (ignored)
- 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
- 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
- Linking  lib/why3/why3.cmxa
- Ocamlopt src/tools/main.ml
- File "src/tools/main.ml", line 99, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- Linking  bin/why3.opt
- Ocamlopt src/tools/why3config.ml
- File "src/tools/why3config.ml", line 117, characters 2-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/tools/why3config.ml", line 122, characters 2-19:
- Warning 50: unattached documentation comment (ignored)
- File "src/tools/why3config.ml", line 135, characters 2-13:
- Warning 50: unattached documentation comment (ignored)
- Linking  bin/why3config.opt
- Ocamlopt src/tools/why3execute.ml
- Linking  bin/why3execute.opt
- Ocamlopt src/tools/why3extract.ml
- Linking  bin/why3extract.opt
- Ocamlopt src/tools/why3prove.ml
- Linking  bin/why3prove.opt
- Ocamlopt src/tools/why3realize.ml
- Linking  bin/why3realize.opt
- Ocamlopt src/tools/why3replay.ml
- Linking  bin/why3replay.opt
- Ocamlopt src/tools/why3wc.ml
- Linking  bin/why3wc.opt
- Ocamlc   src/why3session/why3session_lib.mli
- Ocamlopt src/why3session/why3session_lib.ml
- File "src/why3session/why3session_lib.ml", line 64, characters 2-22:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 199, characters 2-16:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 203, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 209, characters 18-45:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 211, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 213, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 215, characters 2-22:
- 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 221, characters 2-15:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 260, characters 14-29:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 253, 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 156, characters 20-74:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 157, characters 20-65:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 176, characters 2-61:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 182, 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 383, characters 6-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_html.ml", line 530, characters 6-24:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_html.ml", line 540, 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_main.ml
- Linking  bin/why3session.opt
- echo "(* generated automatically at compilation time *)" > drivers/coq-realizations.aux
- echo "(* generated automatically at compilation time *)" > drivers/pvs-realizations.aux
- echo "(* generated automatically at compilation time *)" > drivers/isabelle-realizations.aux
- Ocamlopt lib/ocaml/why3__BigInt_compat.ml
- Ocamlopt lib/ocaml/why3__BigInt.ml
- Ocamlopt lib/ocaml/why3__IntAux.ml
- Ocamlopt lib/ocaml/why3__Array.ml
- Linking  lib/why3/why3extract.cmx
- Linking  lib/why3/why3extract.cmxa
- gcc -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 54, characters 12-25:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/why3doc/doc_def.ml", line 59, characters 8-19:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 63, characters 8-21:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 64, characters 8-34:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 65, 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 64, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/why3doc/doc_lexer.mll", line 75, 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
- 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   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 36, characters 12-25:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/util/strings.ml", line 38, 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 180, 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 181, 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/lexlib.ml
- File "src/util/lexlib.mll", line 101, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/util/lexlib.mll", line 103, characters 46-56:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- 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/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 304, characters 2-33:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 309, characters 2-39:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 312, characters 2-24:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 644, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 653, characters 2-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 658, characters 2-23:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 672, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 689, characters 2-23:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 699, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/driver/whyconf.ml", line 559, 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/mlw/ity.ml
- Ocamlc   src/parser/ptree.ml
- Ocamlc   src/parser/glob.ml
- Ocamlc   src/parser/parser.ml
- Ocamlc   src/parser/typing.ml
- Ocamlc   src/parser/lexer.ml
- Ocamlc   src/transform/simplify_formula.ml
- 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/transform/reduction_engine.ml
- Ocamlc   src/transform/compute.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 408, characters 4-30:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 420, characters 4-34:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 794, characters 2-154:
- Warning 50: unattached documentation comment (ignored)
- File "src/printer/coq.ml", line 136, characters 22-30:
- Warning 48: implicit elimination of optional argument ?whytypes
- File "src/printer/coq.ml", line 371, characters 38-46:
- Warning 48: implicit elimination of optional argument ?whytypes
- File "src/printer/coq.ml", line 467, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/printer/coq.ml", line 674, characters 42-57:
- Warning 48: implicit elimination of optional arguments ?whytypes, ?implicit
- File "src/printer/coq.ml", line 687, characters 31-46:
- Warning 48: implicit elimination of optional arguments ?whytypes, ?implicit
- Ocamlc   src/printer/pvs.ml
- Ocamlc   src/printer/isabelle.ml
- File "src/printer/isabelle.ml", line 329, 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/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
- Ocamlc   src/session/compress.ml
- Ocamlc   src/session/xml.ml
- Ocamlc   src/session/termcode.ml
- File "src/session/termcode.ml", line 259, characters 2-16:
- Warning 3: deprecated: Format.bprintf
- File "src/session/termcode.ml", line 437, characters 6-20:
- Warning 3: deprecated: Format.bprintf
- Ocamlc   src/session/session.ml
- File "src/session/session.ml", line 92, characters 2-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 402, characters 6-191:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 665, characters 4-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1132, characters 4-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1306, characters 8-62:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1348, characters 12-34:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1426, characters 2-56:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1464, characters 6-48:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1499, characters 6-51:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1622, characters 2-73:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1683, characters 8-76:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1852, characters 4-30:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1925, characters 2-49:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1930, characters 22-66:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1934, characters 8-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1945, characters 12-74:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2049, characters 13-43:
- Warning 50: ambiguous documentation comment
- File "src/session/session.ml", line 2058, characters 15-45:
- Warning 50: ambiguous documentation comment
- File "src/session/session.ml", line 2121, characters 2-55:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2122, characters 2-91:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2125, characters 2-49:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2180, characters 2-48:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2264, characters 2-164:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2284, characters 6-62:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2285, characters 6-56:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2628, characters 2-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 2635, characters 51-72:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session.ml", line 1517, characters 10-23:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/session/session.ml", line 1546, characters 16-27:
- Warning 3: deprecated: String.copy
- File "src/session/session.ml", line 74, characters 0-36:
- Warning 60: unused module Spos.
- File "src/session/session.ml", line 75, 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/strategy.ml
- Ocamlc   src/session/strategy_parser.ml
- File "src/session/strategy_parser.mll", line 146, characters 16-28:
- Warning 3: deprecated: Array.create
- Use Array.make instead.
- Ocamlc   src/session/session_scheduler.ml
- File "src/session/session_scheduler.ml", line 91, characters 6-45:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 141, characters 2-35:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 156, characters 2-50:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 170, characters 2-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/session/session_scheduler.ml", line 894, characters 4-64:
- Warning 50: unattached documentation comment (ignored)
- Linking  lib/why3/why3.cmo
- Linking  lib/why3/why3.cma
- Ocamlc   src/tools/main.ml
- File "src/tools/main.ml", line 99, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- Linking  bin/why3.byte
- Ocamlc   src/tools/why3config.ml
- File "src/tools/why3config.ml", line 117, characters 2-31:
- Warning 50: unattached documentation comment (ignored)
- File "src/tools/why3config.ml", line 122, characters 2-19:
- Warning 50: unattached documentation comment (ignored)
- File "src/tools/why3config.ml", line 135, characters 2-13:
- Warning 50: unattached documentation comment (ignored)
- Linking  bin/why3config.byte
- Ocamlc   src/tools/why3execute.ml
- Linking  bin/why3execute.byte
- Ocamlc   src/tools/why3extract.ml
- Linking  bin/why3extract.byte
- Ocamlc   src/tools/why3prove.ml
- Linking  bin/why3prove.byte
- Ocamlc   src/tools/why3realize.ml
- Linking  bin/why3realize.byte
- Ocamlc   src/tools/why3replay.ml
- Linking  bin/why3replay.byte
- Ocamlc   src/tools/why3wc.ml
- Linking  bin/why3wc.byte
- Ocamlc   src/why3session/why3session_lib.ml
- File "src/why3session/why3session_lib.ml", line 64, characters 2-22:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 199, characters 2-16:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 203, characters 2-20:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 209, characters 18-45:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 211, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 213, characters 2-17:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 215, characters 2-22:
- 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 221, characters 2-15:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 260, characters 14-29:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_lib.ml", line 253, 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 156, characters 20-74:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 157, characters 20-65:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 176, characters 2-61:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_copy.ml", line 182, 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 383, characters 6-28:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_html.ml", line 530, characters 6-24:
- Warning 50: unattached documentation comment (ignored)
- File "src/why3session/why3session_html.ml", line 540, 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_main.ml
- Linking  bin/why3session.byte
- Ocamlc   lib/ocaml/why3__BigInt_compat.ml
- 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 54, characters 12-25:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/why3doc/doc_def.ml", line 59, characters 8-19:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 63, characters 8-21:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 64, characters 8-34:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- File "src/why3doc/doc_def.ml", line 65, 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 64, characters 14-27:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "src/why3doc/doc_lexer.mll", line 75, characters 15-26:
- Warning 3: deprecated: String.set
- Use Bytes.set instead.
- Ocamlc   src/why3doc/doc_main.ml
- Linking  bin/why3doc.byte
-> compiled  why3-base.0.85
Processing 13/13: [why3-base: make install]
+ /home/opam/.opam/opam-init/hooks/sandbox.sh "install" "make" "install" "install-lib" (CWD=/home/opam/.opam/4.04.2/.opam-switch/build/why3-base.0.85)
- rm -rf /home/opam/.opam/4.04.2/lib/why3
- rm -rf /home/opam/.opam/4.04.2/share/why3
- rm -rf /home/opam/.opam/4.04.2/lib/why3
- rm -f /home/opam/.opam/4.04.2/share/emacs/site-lisp/why3.el
- rm -f /home/opam/.opam/4.04.2/lib/why3/commands/why3config /home/opam/.opam/4.04.2/lib/why3/commands/why3execute /home/opam/.opam/4.04.2/lib/why3/commands/why3extract /home/opam/.opam/4.04.2/lib/why3/commands/why3prove /home/opam/.opam/4.04.2/lib/why3/commands/why3realize /home/opam/.opam/4.04.2/lib/why3/commands/why3replay /home/opam/.opam/4.04.2/lib/why3/commands/why3wc /home/opam/.opam/4.04.2/bin/why3
- rm -f /home/opam/.opam/4.04.2/bin/why3bench /home/opam/.opam/4.04.2/bin/why3replayer
- rm -f /home/opam/.opam/4.04.2/bin/why3session
- rm -f /home/opam/.opam/4.04.2/bin/why3doc
- if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then rm -f /etc/bash_completion.d/why3; fi
- mkdir -p /home/opam/.opam/4.04.2/bin
- mkdir -p /home/opam/.opam/4.04.2/lib/why3
- mkdir -p /home/opam/.opam/4.04.2/lib/why3/commands
- mkdir -p /home/opam/.opam/4.04.2/share/why3
- mkdir -p /home/opam/.opam/4.04.2/share/why3/images
- mkdir -p /home/opam/.opam/4.04.2/share/why3/images/boomy
- mkdir -p /home/opam/.opam/4.04.2/share/why3/images/fatcow
- mkdir -p /home/opam/.opam/4.04.2/share/why3/vim
- mkdir -p /home/opam/.opam/4.04.2/share/why3/lang
- mkdir -p /home/opam/.opam/4.04.2/share/why3/theories
- mkdir -p /home/opam/.opam/4.04.2/share/why3/modules/mach
- mkdir -p /home/opam/.opam/4.04.2/share/why3/drivers
- mkdir -p /home/opam/.opam/4.04.2/share/emacs/site-lisp/
- cp -f theories/*.why /home/opam/.opam/4.04.2/share/why3/theories
- cp -f modules/*.mlw /home/opam/.opam/4.04.2/share/why3/modules
- cp -f modules/mach/*.mlw /home/opam/.opam/4.04.2/share/why3/modules/mach
- cp -f drivers/*.drv drivers/*.gen /home/opam/.opam/4.04.2/share/why3/drivers
- cp -f share/provers-detection-data.conf /home/opam/.opam/4.04.2/share/why3/
- cp -f share/images/icons.rc /home/opam/.opam/4.04.2/share/why3/images
- cp -f share/images/*.png /home/opam/.opam/4.04.2/share/why3/images
- cp -f share/images/boomy/*.png /home/opam/.opam/4.04.2/share/why3/images/boomy
- cp -f share/images/fatcow/*.png /home/opam/.opam/4.04.2/share/why3/images/fatcow
- cp -f share/why3session.dtd /home/opam/.opam/4.04.2/share/why3
- cp -rf share/javascript /home/opam/.opam/4.04.2/share/why3/javascript
- cp -f share/vim/why3.vim /home/opam/.opam/4.04.2/share/why3/vim/why3.vim
- cp -f share/lang/why3.lang /home/opam/.opam/4.04.2/share/why3/lang/why3.lang
- cp -f share/emacs/why3.el /home/opam/.opam/4.04.2/share/emacs/site-lisp/why3.el
- mkdir -p /home/opam/.opam/4.04.2/lib/why3/plugins
- cp -f lib/plugins/genequlin.cmo lib/plugins/dimacs.cmo lib/plugins/tptp.cmo lib/plugins/genequlin.cmxs lib/plugins/dimacs.cmxs lib/plugins/tptp.cmxs /home/opam/.opam/4.04.2/lib/why3/plugins
- cp -f bin/why3.opt /home/opam/.opam/4.04.2/bin/why3
- cp -f bin/why3config.opt  /home/opam/.opam/4.04.2/lib/why3/commands/why3config
- cp -f bin/why3execute.opt /home/opam/.opam/4.04.2/lib/why3/commands/why3execute
- cp -f bin/why3extract.opt /home/opam/.opam/4.04.2/lib/why3/commands/why3extract
- cp -f bin/why3prove.opt   /home/opam/.opam/4.04.2/lib/why3/commands/why3prove
- cp -f bin/why3realize.opt /home/opam/.opam/4.04.2/lib/why3/commands/why3realize
- cp -f bin/why3replay.opt  /home/opam/.opam/4.04.2/lib/why3/commands/why3replay
- cp -f bin/why3wc.opt      /home/opam/.opam/4.04.2/lib/why3/commands/why3wc
- cp -f bin/why3session.opt /home/opam/.opam/4.04.2/lib/why3/commands/why3session
- cp drivers/coq-realizations.aux /home/opam/.opam/4.04.2/share/why3/drivers/
- cp drivers/pvs-realizations.aux /home/opam/.opam/4.04.2/share/why3/drivers/
- cp drivers/isabelle-realizations.aux /home/opam/.opam/4.04.2/share/why3/drivers/
- cp -f lib/why3-cpulimit /home/opam/.opam/4.04.2/lib/why3/why3-cpulimit
- cp -f lib/why3-call-pvs /home/opam/.opam/4.04.2/lib/why3/why3-call-pvs
- cp -f bin/why3doc.opt /home/opam/.opam/4.04.2/lib/why3/commands/why3doc
- if test -d /etc/bash_completion.d -a -w /etc/bash_completion.d; then cp -f share/bash/why3 /etc/bash_completion.d; fi
- mkdir -p /home/opam/.opam/4.04.2/lib/why3
- cp -f lib/why3/why3.a lib/why3/why3.cma lib/why3/why3.cmx lib/why3/why3.cmi lib/why3/why3.cmxa \
- 	lib/why3/META /home/opam/.opam/4.04.2/lib/why3
- mkdir -p /home/opam/.opam/4.04.2/lib/why3
- cp -f lib/why3/why3extract.a lib/why3/why3extract.cma lib/why3/why3extract.cmx lib/why3/why3extract.cmi lib/why3/why3extract.cmxa \
-   /home/opam/.opam/4.04.2/lib/why3
-> installed why3-base.0.85
Done.
# Run eval $(opam env) to update the current shell environment
2021-07-05 06:36.54 ---> saved as "8ddddafd2edf148b726d11709bda7e24e9e5ccd6c170f13e8187f8eb9aa8b266"
Job succeeded