=> Bootstrap dependency digest>=20211023: found digest-20220214 ===> Skipping vulnerability checks. WARNING: No /usr/pkg/pkgdb/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /usr/pkg/pkgdb fetch-pkg-vulnerabilities'. ===> Building for why3-1.5.1nb1 cmp -s src/util/mysexplib-dummy.ml src/util/mysexplib.ml || cp src/util/mysexplib-dummy.ml src/util/mysexplib.ml Ocamllex src/util/rc.mll Generate src/util/config.ml Menhir src/util/json_parser.mly Ocamllex src/util/lexlib.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings Ocamllex src/util/json_lexer.mll cmp -s src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml || cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml cmp -s src/util/dynlink_new.ml src/util/dynlink_wrapper.ml || cp src/util/dynlink_new.ml src/util/dynlink_wrapper.ml 52 states, 495 transitions, table size 2292 bytes Ocamllex src/parser/lexer.mll Menhir src/parser/parser_common.mly Menhir src/parser/parser_common.mly src/parser/parser.mly 158 states, 4359 transitions, table size 18384 bytes 7555 additional bytes used for bindings Menhir src/driver/driver_parser.mly Ocamllex src/driver/driver_lexer.mll 34 states, 1366 transitions, table size 5668 bytes Ocamllex src/driver/sexp.mll 27 states, 306 transitions, table size 1386 bytes cmp -s src/session/compress_none.ml src/session/compress.ml || cp src/session/compress_none.ml src/session/compress.ml Ocamllex src/session/xml.mll 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings Ocamllex src/session/strategy_parser.mll cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml 47 states, 678 transitions, table size 2994 bytes 2153 additional bytes used for bindings Menhir plugins/tptp/tptp_parser.mly Ocamllex plugins/tptp/tptp_lexer.mll 101 states, 1563 transitions, table size 6858 bytes 3126 additional bytes used for bindings Ocamllex plugins/python/py_lexer.mll 69 states, 1256 transitions, table size 5438 bytes 1453 additional bytes used for bindings Menhir plugins/python/py_parser.mly Ocamllex plugins/microc/mc_lexer.mll 77 states, 473 transitions, table size 2354 bytes 1504 additional bytes used for bindings Menhir plugins/microc/mc_parser.mly Read 3 sample input sentences and 3 error messages. menhir --explain --strict src/parser/parser_common.mly src/parser/parser.mly --base src/parser/parser --compile-errors \ src/parser/handcrafted.messages > src/parser/parser_messages.ml Ocamllex plugins/cfg/cfg_lexer.mll Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly 155 states, 4342 transitions, table size 18298 bytes 7537 additional bytes used for bindings Ocamllex plugins/parser/dimacs.mll 34 states, 434 transitions, table size 1940 bytes 1293 additional bytes used for bindings Ocamllex src/tools/why3wc.mll 307 states, 15627 transitions, table size 64350 bytes Ocamldep src/ide/wserver.ml Ocamldep src/ide/why3web.ml Ocamldep src/why3session/why3session_lib.ml Read 3 sample input sentences and 3 error messages. Ocamldep src/why3session/why3session_info.ml Ocamldep src/why3session/why3session_html.ml Ocamldep src/why3session/why3session_latex.ml Ocamldep src/why3session/why3session_update.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/tools/why3shell.ml Ocamldep src/isabelle-client/isabelle_client_main.ml cmp -s src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.ml || cp src/tools/why3pp_sexp-dummy.ml src/tools/why3pp_sexp.ml cp src/util/json_base.ml src/trywhy3/json_base.ml cp src/util/json_base.mli src/trywhy3/json_base.mli Ocamllex src/why3doc/doc_lexer.mll cp src/util/json_parser.ml src/trywhy3/json_parser.ml cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml cp src/util/json_parser.mli src/trywhy3/json_parser.mli cp src/util/json_lexer.mli src/trywhy3/json_lexer.mli 120 states, 685 transitions, table size 3460 bytes 1763 additional bytes used for bindings Ocamldep src/tools/main.ml Ocamldep src/tools/why3config.ml Ocamldep src/tools/why3execute.ml Ocamldep src/tools/why3extract.ml Ocamldep src/tools/why3prove.ml Ocamldep src/tools/why3realize.ml Ocamldep src/tools/why3replay.ml Ocamldep src/tools/why3show.ml Ocamldep src/tools/why3wc.ml Ocamldep src/tools/why3pp_sexp.ml Ocamldep src/why3doc/doc_html.ml Ocamldep src/tools/why3pp.ml Ocamldep src/why3doc/doc_def.ml Ocamldep src/why3doc/doc_lexer.ml Ocamldep src/why3doc/doc_main.ml Ocamldep src/trywhy3/json_base.ml Ocamldep src/trywhy3/json_parser.ml Ocamldep src/trywhy3/json_lexer.ml Ocamldep src/trywhy3/bindings.ml Ocamldep src/trywhy3/shortener.ml Ocamldep src/trywhy3/trywhy3.ml Ocamldep src/trywhy3/why3_worker.ml Ocamldep src/trywhy3/worker_proto.ml Ocamldep src/util/mysexplib.ml Ocamldep src/util/config.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/util.ml Ocamldep src/util/opt.ml Ocamldep src/util/lists.ml Ocamldep src/util/strings.ml Ocamldep src/util/pp.ml Ocamldep src/util/extmap.ml Ocamldep src/util/extset.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_base.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/debug.ml Ocamldep src/util/loc.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/dynlink_wrapper.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/warning.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/plugin.ml Ocamldep src/util/rc.ml Ocamldep src/util/vector.ml Ocamldep src/util/number.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/constant.ml Ocamldep src/core/ident.ml Ocamldep src/util/re.ml Ocamldep src/core/term.ml Ocamldep src/core/ty.ml Ocamldep src/core/pattern.ml Ocamldep src/core/decl.ml Ocamldep src/core/coercion.ml Ocamldep src/core/theory.ml Ocamldep src/core/keywords.ml Ocamldep src/core/parser_tokens.ml Ocamldep src/core/task.ml Ocamldep src/core/pretty.ml Ocamldep src/core/dterm.ml Ocamldep src/core/env.ml Ocamldep src/core/trans.ml Ocamldep src/core/printer.ml Ocamldep src/core/model_parser.ml Ocamldep src/driver/prove_client.ml Ocamldep src/driver/call_provers.ml Ocamldep src/driver/driver_parser.ml Ocamldep src/driver/driver_lexer.ml Ocamldep src/driver/driver.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/autodetection.ml Ocamldep src/driver/smtv2_model_defs.ml Ocamldep src/driver/collect_data_model.ml Ocamldep src/driver/smtv2_model_parser.ml Ocamldep src/mlw/ity.ml Ocamldep src/driver/sexp.ml Ocamldep src/mlw/expr.ml Ocamldep src/mlw/pdecl.ml Ocamldep src/mlw/eval_match.ml Ocamldep src/mlw/typeinv.ml Ocamldep src/mlw/vc.ml Ocamldep src/mlw/pmodule.ml Ocamldep src/mlw/dexpr.ml Ocamldep src/mlw/big_real.ml Ocamldep src/mlw/pinterp_core.ml Ocamldep src/mlw/rac.ml Ocamldep src/mlw/pinterp.ml Ocamldep src/mlw/check_ce.ml Ocamldep src/extract/mltree.ml Ocamldep src/extract/compile.ml Ocamldep src/extract/mlinterp.ml Ocamldep src/extract/pdriver.ml Ocamldep src/extract/ml_printer.ml Ocamldep src/extract/ocaml.ml Ocamldep src/extract/c.ml Ocamldep src/extract/cakeml.ml Ocamldep src/parser/ptree.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/report.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/reduction_engine.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/abstract_quantifiers.ml Ocamldep src/transform/eliminate_unknown_types.ml Ocamldep src/transform/eliminate_unknown_lsymbols.ml Ocamldep src/transform/eliminate_symbol.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/eliminate_let.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/eliminate_literal.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/generic_arg_trans_utils.ml Ocamldep src/transform/case.ml Ocamldep src/transform/apply.ml Ocamldep src/transform/subst.ml Ocamldep src/transform/introduction.ml Ocamldep src/transform/ind_itp.ml Ocamldep src/transform/destruct.ml Ocamldep src/transform/cut.ml Ocamldep src/transform/congruence.ml Ocamldep src/transform/intro_vc_vars_counterexmp.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/reflection.ml Ocamldep src/printer/cntexmp_printer.ml Ocamldep src/printer/alt_ergo.ml Ocamldep src/printer/why3printer.ml Ocamldep src/printer/smtv1.ml Ocamldep src/printer/smtv2.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/mathematica.ml Ocamldep src/session/compress.ml Ocamldep src/session/xml.ml Ocamldep src/session/termcode.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/strategy.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/json_util.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/parser/genequlin.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/transform/hypothesis_selection.ml Ocamldep plugins/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/python/py_main.ml Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/microc/mc_parser.ml Ocamldep plugins/microc/mc_lexer.ml Ocamldep plugins/microc/mc_printer.ml Ocamldep plugins/microc/mc_main.ml Ocamldep plugins/cfg/cfg_parser.ml Ocamldep plugins/cfg/cfg_lexer.ml Ocamldep plugins/cfg/cfg_paths.ml Ocamldep plugins/cfg/cfg_main.ml Ocamldep plugins/cfg/stackify.ml Ocamldep plugins/cfg/cfg_stackify.ml Ocamldep plugins/tptp/tptp_ast.mli Ocamldep plugins/microc/mc_ast.mli Ocamldep plugins/cfg/cfg_ast.mli Ocamldep plugins/python/py_ast.mli mkdir lib/plugins Ocamlc src/util/mysexplib.ml Ocamlc src/util/bigInt.mli Ocamlc src/util/config.mli Ocamlc src/util/mlmpfr_wrapper.mli File "src/util/mysexplib.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/util/util.mli Ocamlc src/util/opt.mli Ocamlc src/util/lists.mli Ocamlc src/util/strings.mli File "src/util/util.mli", line 110, characters 22-52: 110 | val ansi_color_tags : Format.formatter_tag_functions ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.formatter_tag_functions Use formatter_stag_functions. Ocamlc src/util/pp.mli Ocamlc src/util/extmap.mli Ocamlc src/util/exthtbl.mli Ocamlc src/util/weakhtbl.mli File "src/util/pp.mli", line 122, characters 33-51: 122 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/pp.mli", line 125, characters 33-51: 125 | ('b, formatter, unit, string) Pervasives.format4 -> 'b ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/util/hashcons.mli Ocamlc src/util/exn_printer.mli Ocamlc src/util/getopt.mli Ocamlc src/util/json_base.mli Ocamlc src/util/lexlib.mli Ocamlc src/util/loc.mli Ocamlc src/util/print_tree.mli Ocamlc src/util/dynlink_wrapper.mli Ocamlc src/util/cmdline.mli Ocamlc src/util/sysutil.mli Ocamlc src/util/number.mli Ocamlc src/util/vector.mli Ocamlc src/util/pqueue.mli Ocamlc src/util/re.ml Ocamlc src/driver/sexp.mli Ocamlc src/driver/driver_ast.mli Ocamlc src/driver/prove_client.mli File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/driver/smtv2_model_parser.mli Ocamlc src/mlw/big_real.mli Ocamlc src/extract/c.mli Linking src/util/ppx_debug_optim findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/pkg/lib/ocaml, /usr/pkg/lib/ocaml/compiler-libs Ocamlc src/extract/ocaml.mli Ocamlc src/extract/cakeml.mli Ocamlc src/parser/parser_messages.mli Ocamlc src/transform/abstract_quantifiers.mli Ocamlc src/transform/eliminate_unknown_types.mli Ocamlc src/transform/eliminate_unknown_lsymbols.mli Ocamlc src/transform/eliminate_symbol.mli Ocamlc src/transform/encoding_select.mli Ocamlc src/transform/encoding_guards_full.mli Ocamlc src/transform/encoding_tags_full.mli Ocamlc src/transform/encoding_guards.mli Ocamlc src/transform/encoding_tags.mli Ocamlc src/transform/encoding_twin.mli Ocamlc src/transform/encoding_sort.mli Ocamlc src/transform/simplify_array.mli Ocamlc src/transform/filter_trigger.mli Ocamlc src/transform/lift_epsilon.mli Ocamlc src/transform/instantiate_predicate.mli Ocamlc src/transform/prop_curry.mli Ocamlc src/transform/case.mli Ocamlc src/transform/congruence.mli Ocamlc src/transform/induction.mli Ocamlc src/transform/induction_pr.mli Ocamlc src/printer/alt_ergo.mli Ocamlc src/printer/why3printer.mli Ocamlc src/printer/smtv1.mli Ocamlc src/printer/smtv2.mli Ocamlc src/printer/coq.mli Ocamlc src/printer/pvs.mli Ocamlc src/printer/isabelle.mli Ocamlc src/printer/simplify.mli Ocamlc src/printer/gappa.mli Ocamlc src/printer/cvc3.mli Ocamlc src/printer/yices.mli Ocamlc src/printer/mathematica.mli Ocamlc src/session/compress.mli Ocamlc src/session/xml.mli Ocamlc src/session/unix_scheduler.mli Ocamlc src/util/config.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/mlmpfr_wrapper.ml Ocamlc src/util/util.ml Ocamlc src/util/opt.ml Ocamlc src/util/lists.ml Ocamlc src/util/strings.ml Ocamlc src/util/pp.ml Ocamlc src/util/extmap.ml Ocamlc src/util/exthtbl.ml Ocamlc src/util/weakhtbl.ml Ocamlc src/util/hashcons.ml File "src/util/weakhtbl.ml", line 98, characters 13-19: 98 | let iter = H.iter ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 99, characters 13-19: 99 | let fold = H.fold ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 101, characters 19-25: 101 | let iterk fn t = H.iter (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 102, characters 19-25: 102 | let foldk fn t = H.fold (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 Ocamlc src/util/exn_printer.ml Ocamlc src/util/getopt.ml Ocamlc src/util/json_base.ml Ocamlc src/util/lexlib.ml Ocamlc src/util/print_tree.ml Ocamlc src/util/dynlink_wrapper.ml Ocamlc src/util/cmdline.ml Ocamlc src/util/sysutil.ml Ocamlc src/util/vector.ml Ocamlc src/util/pqueue.ml File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/driver/prove_client.ml Ocamlc src/mlw/big_real.ml Ocamlc src/parser/parser_messages.ml Ocamlc src/driver/sexp.ml Ocamlc src/session/compress.ml File "src/session/compress_none.ml", line 43, characters 23-33: Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/session/compress_none.ml", line 45, characters 20-30: Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/session/unix_scheduler.ml Ocamlc plugins/tptp/tptp_printer.mli Ocamlc plugins/parser/dimacs.mli Ocamlc plugins/parser/genequlin.mli Ocamlc plugins/python/py_main.mli Ocamlc src/tools/main.mli Ocamlc plugins/microc/mc_main.mli Ocamlc src/tools/why3config.mli Ocamlc src/tools/why3execute.mli Ocamlc src/tools/why3extract.mli Ocamlc src/tools/why3prove.mli Ocamlc src/tools/why3realize.mli Ocamlc src/tools/why3replay.mli Ocamlc src/tools/why3wc.mli Ocamlc src/tools/why3show.mli Ocamlc src/ide/wserver.mli Ocamlc src/ide/why3web.mli File "src/ide/wserver.mli", line 71, characters 35-43: 71 | val get_request_and_content : char Stream.t -> string list * string ^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. Ocamlc src/why3session/why3session_main.mli Ocamlc src/tools/why3shell.mli Ocamlc src/isabelle-client/isabelle_client_main.mli Ocamlc src/tools/why3pp.mli Ocamlc src/why3doc/doc_html.mli Ocamlc src/why3doc/doc_lexer.mli gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c Ocamlc src/why3doc/doc_main.mli gcc -Wall -O -g -o src/server/arraylist.o -c src/server/arraylist.c gcc -Wall -O -g -o src/server/options.o -c src/server/options.c gcc -Wall -O -g -o src/server/queue.o -c src/server/queue.c gcc -Wall -O -g -o src/server/readbuf.o -c src/server/readbuf.c gcc -Wall -O -g -o src/server/request.o -c src/server/request.c gcc -Wall -O -g -o src/server/proc.o -c src/server/proc.c gcc -Wall -O -g -o src/server/writebuf.o -c src/server/writebuf.c gcc -Wall -O -g -o src/server/server-unix.o -c src/server/server-unix.c gcc -Wall -O -g -o src/server/server-win.o -c src/server/server-win.c gcc -Wall -O -g -o src/server/cpulimit-unix.o -c src/server/cpulimit-unix.c gcc -Wall -O -g -o src/server/cpulimit-win.o -c src/server/cpulimit-win.c Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Ocamlopt src/util/mysexplib.ml Ocamlopt src/util/config.ml Ocamlopt src/util/mlmpfr_wrapper.ml Ocamlopt src/util/util.ml Ocamlopt src/util/opt.ml Ocamlopt src/util/lists.ml Ocamlopt src/util/strings.ml Ocamlopt src/util/pp.ml Ocamlopt src/util/extmap.ml Ocamlc src/util/extset.mli Ocamlopt src/util/exthtbl.ml Ocamlopt src/util/weakhtbl.ml File "src/util/weakhtbl.ml", line 98, characters 13-19: 98 | let iter = H.iter ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 99, characters 13-19: 99 | let fold = H.fold ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 101, characters 19-25: 101 | let iterk fn t = H.iter (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.iter This function won't be available in 5.0 File "src/util/weakhtbl.ml", line 102, characters 19-25: 102 | let foldk fn t = H.fold (fun k _ -> fn k) t ^^^^^^ Alert old_ephemeron_api: H.fold This function won't be available in 5.0 Ocamlc src/util/diffmap.mli Ocamlopt src/util/hashcons.ml Ocamlc src/util/wstdlib.mli Ocamlopt src/util/exn_printer.ml Ocamlopt src/util/getopt.ml Ocamlopt src/util/json_base.ml Ocamlc src/util/json_parser.mli Ocamlc src/util/debug.mli Ocamlopt src/util/print_tree.ml Ocamlopt src/util/dynlink_wrapper.ml Ocamlopt src/util/cmdline.ml Ocamlc src/util/warning.mli Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli Ocamlc src/util/plugin.mli Ocamlc src/util/constant.mli Ocamlopt src/util/vector.ml Ocamlopt src/util/re.ml Ocamlc src/core/ident.mli File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/core/parser_tokens.mli Ocamlopt src/driver/prove_client.ml Ocamlc src/driver/driver_parser.mli Ocamlc src/driver/driver_lexer.mli Ocamlopt src/driver/sexp.ml Ocamlc src/parser/glob.mli Ocamlopt src/mlw/big_real.ml Ocamlopt src/parser/parser_messages.ml Ocamlopt src/session/compress.ml Ocamlc src/util/extset.ml Ocamlc src/util/diffmap.ml Ocamlopt src/session/unix_scheduler.ml File "src/session/compress_none.ml", line 43, characters 23-33: Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/session/compress_none.ml", line 45, characters 20-30: Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/util/wstdlib.ml Ocamlc src/util/json_parser.ml Ocamlc src/util/loc.ml Ocamlc src/util/debug.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | let compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/loc.ml", line 70, characters 12-26: 70 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/debug.ml", line 114, characters 21-39: 114 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/util/warning.ml Ocamlc src/util/plugin.ml Ocamlc src/util/number.ml Ocamlc src/util/rc.ml Ocamlc src/util/constant.ml Ocamlc src/core/ident.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/core/parser_tokens.ml Ocamlc src/driver/driver_parser.ml Ocamlc src/driver/driver_lexer.ml Ocamlc src/parser/glob.ml gcc -Wall -o lib/why3server src/server/logging.o src/server/arraylist.o src/server/options.o src/server/queue.o src/server/readbuf.o src/server/request.o src/server/proc.o src/server/writebuf.o src/server/server-unix.o src/server/server-win.o Ocamlc src/session/xml.ml gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Ocamlopt src/util/bigInt.ml Ocamlopt src/util/extset.ml Ocamlopt src/util/diffmap.ml Ocamlopt src/util/json_parser.ml Ocamlc src/util/json_lexer.mli Ocamlopt src/util/debug.ml Ocamlopt src/util/pqueue.ml File "src/util/debug.ml", line 114, characters 21-39: 114 | (List.sort Pervasives.compare list); ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/core/ty.mli Ocamlc src/util/json_lexer.ml Ocamlopt src/util/wstdlib.ml Ocamlopt src/util/json_lexer.ml Ocamlopt src/util/loc.ml File "src/util/loc.ml", line 69, characters 14-32: 69 | let compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/loc.ml", line 70, characters 12-26: 70 | let equal = Pervasives.(=) ^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt src/util/plugin.ml Ocamlopt src/util/number.ml Ocamlc src/core/term.mli Ocamlopt src/session/xml.ml Ocamlc src/core/ty.ml Ocamlopt src/util/lexlib.ml Ocamlopt src/util/warning.ml Ocamlopt src/util/rc.ml Ocamlopt src/core/ident.ml Ocamlc src/core/pattern.mli Ocamlc src/core/coercion.mli Ocamlc src/core/decl.mli Ocamlopt src/core/parser_tokens.ml Ocamlc src/mlw/ity.mli Ocamlc src/core/dterm.mli Ocamlc src/transform/close_epsilon.mli Ocamlc src/printer/cntexmp_printer.mli Ocamlc src/core/term.ml Ocamlc src/core/decl.ml Ocamlc src/core/pattern.ml Ocamlc src/core/coercion.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt src/util/constant.ml Ocamlc src/printer/cntexmp_printer.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt src/core/ty.ml Ocamlc src/core/theory.mli Ocamlc src/mlw/expr.mli Ocamlc src/core/env.mli Ocamlc src/core/task.mli Ocamlopt src/driver/driver_parser.ml Ocamlopt src/parser/glob.ml Ocamlc src/transform/detect_polymorphism.mli Ocamlc src/transform/reduction_engine.mli Ocamlc src/transform/eliminate_literal.mli Ocamlc src/session/termcode.mli Ocamlc src/core/theory.ml Ocamlc src/core/task.ml Ocamlc src/core/env.ml Ocamlc src/transform/reduction_engine.ml Ocamlopt src/core/term.ml File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/parser/ptree.ml Ocamlc src/mlw/pdecl.mli File "src/parser/ptree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/core/trans.mli Ocamlc src/core/pretty.mli Ocamlopt src/driver/driver_lexer.ml Ocamlc src/mlw/eval_match.mli Ocamlc src/mlw/typeinv.mli Ocamlc src/mlw/vc.mli Ocamlc src/parser/ptree_helpers.mli Ocamlc src/parser/mlw_printer.mli Ocamlc src/transform/simplify_formula.mli Ocamlc src/transform/split_goal.mli Ocamlc src/transform/inlining.mli Ocamlc src/transform/args_wrapper.mli Ocamlc src/transform/compute.mli Ocamlc src/transform/eliminate_definition.mli Ocamlc src/transform/eliminate_algebraic.mli Ocamlc src/transform/eliminate_inductive.mli Ocamlc src/transform/eliminate_let.mli Ocamlc src/transform/eliminate_if.mli Ocamlc src/transform/encoding.mli Ocamlc src/transform/libencoding.mli Ocamlc src/transform/abstraction.mli Ocamlc src/transform/eliminate_epsilon.mli Ocamlc src/transform/intro_projections_counterexmp.mli Ocamlc src/transform/smoke_detector.mli Ocamlc src/transform/generic_arg_trans_utils.mli Ocamlc src/transform/apply.mli Ocamlc src/transform/subst.mli Ocamlc src/transform/introduction.mli Ocamlc src/transform/ind_itp.mli Ocamlc src/transform/destruct.mli Ocamlc src/transform/cut.mli Ocamlc src/transform/intro_vc_vars_counterexmp.mli Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlc src/transform/reflection.mli Ocamlc src/core/dterm.ml Ocamlc src/core/trans.ml Ocamlc src/mlw/ity.ml Ocamlc src/mlw/expr.ml Ocamlc src/mlw/pdecl.ml Ocamlc src/mlw/eval_match.ml Ocamlc src/mlw/typeinv.ml Ocamlc src/mlw/vc.ml Ocamlc src/parser/ptree_helpers.ml Ocamlc src/parser/mlw_printer.ml Ocamlc src/transform/simplify_formula.ml Ocamlc src/transform/split_goal.ml Ocamlc src/transform/detect_polymorphism.ml Ocamlc src/transform/compute.ml Ocamlc src/transform/abstract_quantifiers.ml Ocamlc src/transform/eliminate_symbol.ml Ocamlc src/transform/eliminate_inductive.ml Ocamlc src/transform/eliminate_let.ml Ocamlc src/transform/encoding.ml Ocamlc src/transform/simplify_array.ml Ocamlc src/transform/abstraction.ml Ocamlc src/transform/close_epsilon.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/transform/lift_epsilon.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/case.ml Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/apply.ml Ocamlc src/transform/subst.ml Ocamlc src/transform/introduction.ml Ocamlc src/transform/ind_itp.ml Ocamlc src/transform/destruct.ml Ocamlc src/transform/cut.ml Ocamlc src/transform/congruence.ml Ocamlc src/transform/intro_vc_vars_counterexmp.ml Ocamlc src/transform/induction.ml Ocamlc src/transform/induction_pr.ml Ocamlc src/session/termcode.ml Ocamlopt src/core/pattern.ml Ocamlopt src/core/coercion.ml Ocamlc src/mlw/pmodule.mli File "src/session/termcode.ml", line 1108, characters 24-42: 1108 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/core/printer.mli Ocamlc src/mlw/dexpr.mli Ocamlc src/mlw/pinterp_core.mli Ocamlc src/extract/mltree.mli Ocamlc src/extract/mlinterp.mli Ocamlc src/parser/typing.mli Ocamlc src/parser/lexer.mli Ocamlc src/transform/discriminate.mli Ocamlc src/core/printer.ml Ocamlc src/mlw/pmodule.ml Ocamlc src/mlw/dexpr.ml Ocamlc src/mlw/pinterp_core.ml Ocamlc src/extract/mltree.ml Ocamlc src/parser/typing.ml Ocamlc src/transform/args_wrapper.ml Ocamlc src/transform/eliminate_algebraic.ml Ocamlc src/transform/eliminate_unknown_types.ml Ocamlc src/transform/eliminate_unknown_lsymbols.ml Ocamlc src/transform/eliminate_if.ml Ocamlc src/transform/libencoding.ml Ocamlc src/transform/discriminate.ml Ocamlc src/transform/encoding_select.ml Ocamlc src/transform/encoding_guards_full.ml Ocamlc src/transform/encoding_tags_full.ml Ocamlc src/transform/encoding_guards.ml Ocamlc src/transform/encoding_tags.ml Ocamlc src/transform/encoding_twin.ml Ocamlc src/transform/encoding_sort.ml Ocamlc src/transform/filter_trigger.ml Ocamlc src/transform/reflection.ml Ocamlc src/printer/smtv1.ml Ocamlc src/printer/coq.ml Ocamlc src/printer/pvs.ml Ocamlc src/printer/isabelle.ml Ocamlc src/printer/simplify.ml Ocamlc src/printer/gappa.ml Ocamlc src/printer/cvc3.ml Ocamlc src/printer/yices.ml Ocamlc src/printer/mathematica.ml Ocamlopt src/core/decl.ml Ocamlc src/parser/parser.mli Ocamlc src/core/model_parser.mli Ocamlc src/mlw/pinterp.mli Ocamlc src/extract/pdriver.mli Ocamlc src/extract/compile.mli Ocamlc src/parser/report.mli Ocamlc src/core/model_parser.ml Ocamlc src/mlw/pinterp.ml Ocamlc src/extract/compile.ml File "src/core/model_parser.ml", line 824, characters 17-23: 824 | "loc", String (string_of_int i); ^^^^^^ Warning 40 [name-out-of-scope]: String was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 824, characters 17-23: 824 | "loc", String (string_of_int i); ^^^^^^ Warning 42 [disambiguated-name]: this use of String relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. File "src/core/model_parser.ml", line 825, characters 24-28: 825 | "is_vc_line", Bool is_vc_line; ^^^^ Warning 40 [name-out-of-scope]: Bool was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 825, characters 24-28: 825 | "is_vc_line", Bool is_vc_line; ^^^^ Warning 42 [disambiguated-name]: this use of Bool relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. File "src/core/model_parser.ml", line 835, characters 22-28: 835 | "filename", String file_name; ^^^^^^ Warning 40 [name-out-of-scope]: String was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 835, characters 22-28: 835 | "filename", String file_name; ^^^^^^ Warning 42 [disambiguated-name]: this use of String relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. Ocamlc src/extract/mlinterp.ml Ocamlc src/extract/pdriver.ml Ocamlc src/extract/c.ml Ocamlc src/parser/parser.ml Ocamlc src/parser/report.ml Ocamlopt src/core/theory.ml Ocamlc src/core/keywords.mli Ocamlc src/driver/call_provers.mli File "src/extract/c.ml", line 68, characters 4-22: 68 | | Cfloat of string ^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cfloat is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 69, characters 4-21: 69 | | Cchar of string ^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cchar is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 45-56: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostincr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 68-79: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostdecr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 41, characters 59-64: 41 | and binop = Band | Bor | Beq | Bne | Bassign | Blt | Ble | Bgt | Bge ^^^^^ Warning 37 [unused-constructor]: constructor Bgt is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 29, characters 4-41: 29 | | Tunion of ident * (ident * ty) list ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Tunion is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 92, characters 4-28: 92 | | Dtypedef of ty * ident ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Dtypedef is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 83, characters 21-24: 83 | and include_kind = Sys | Proj (* include <...> vs. include "..." *) ^^^ Warning 37 [unused-constructor]: constructor Sys is never used to build values. (However, this constructor appears in patterns.) Ocamlc src/driver/smtv2_model_defs.mli Ocamlc src/mlw/check_ce.mli Ocamlc src/extract/ml_printer.mli Ocamlc src/core/keywords.ml Ocamlc src/core/pretty.ml Ocamlc src/driver/call_provers.ml Ocamlc src/driver/smtv2_model_defs.ml Ocamlc src/extract/ml_printer.ml Ocamlc src/extract/ocaml.ml Ocamlc src/extract/cakeml.ml Ocamlc src/parser/lexer.ml Ocamlc src/printer/why3printer.ml Ocamlopt src/core/keywords.ml Ocamlopt src/core/task.ml Ocamlopt src/core/env.ml Ocamlc src/driver/driver.mli Ocamlc src/driver/collect_data_model.mli Ocamlc src/driver/driver.ml Ocamlc src/driver/collect_data_model.ml Ocamlc src/driver/smtv2_model_parser.ml Ocamlc src/transform/inlining.ml Ocamlc src/transform/eliminate_definition.ml Ocamlc src/transform/prepare_for_counterexmp.ml Ocamlc src/printer/alt_ergo.ml Ocamlc src/printer/smtv2.ml Ocamlopt src/core/pretty.ml Ocamlc src/driver/whyconf.mli Ocamlopt src/transform/reduction_engine.ml Ocamlc src/session/session_itp.mli Ocamlc src/session/strategy.mli Ocamlc src/driver/whyconf.ml Ocamlc src/session/session_itp.ml Ocamlc src/session/strategy.ml Ocamlopt src/core/dterm.ml Ocamlopt src/core/trans.ml Ocamlc src/driver/autodetection.mli Ocamlopt src/mlw/ity.ml Ocamlc src/mlw/rac.mli Ocamlopt src/transform/simplify_formula.ml Ocamlopt src/transform/split_goal.ml Ocamlopt src/transform/detect_polymorphism.ml Ocamlopt src/transform/abstract_quantifiers.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlopt src/transform/eliminate_inductive.ml Ocamlopt src/transform/eliminate_let.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlopt src/printer/cntexmp_printer.ml Ocamlopt src/session/termcode.ml Ocamlc src/session/strategy_parser.mli Ocamlc src/session/controller_itp.mli Ocamlc src/driver/autodetection.ml Ocamlc src/mlw/rac.ml File "src/session/termcode.ml", line 1108, characters 24-42: 1108 | let compare e1 e2 = Pervasives.compare e1.shape e2.shape in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/mlw/check_ce.ml Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.ml Ocamlopt src/core/printer.ml Ocamlopt src/mlw/expr.ml Ocamlopt src/transform/lift_epsilon.ml Ocamlc src/session/itp_communication.mli Ocamlopt src/core/model_parser.ml Ocamlopt src/transform/eliminate_algebraic.ml File "src/core/model_parser.ml", line 824, characters 17-23: 824 | "loc", String (string_of_int i); ^^^^^^ Warning 40 [name-out-of-scope]: String was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 824, characters 17-23: 824 | "loc", String (string_of_int i); ^^^^^^ Warning 42 [disambiguated-name]: this use of String relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. File "src/core/model_parser.ml", line 825, characters 24-28: 825 | "is_vc_line", Bool is_vc_line; ^^^^ Warning 40 [name-out-of-scope]: Bool was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 825, characters 24-28: 825 | "is_vc_line", Bool is_vc_line; ^^^^ Warning 42 [disambiguated-name]: this use of Bool relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. File "src/core/model_parser.ml", line 835, characters 22-28: 835 | "filename", String file_name; ^^^^^^ Warning 40 [name-out-of-scope]: String was selected from type Json_base.json. It is not visible in the current scope, and will not be selected if the type becomes unknown. File "src/core/model_parser.ml", line 835, characters 22-28: 835 | "filename", String file_name; ^^^^^^ Warning 42 [disambiguated-name]: this use of String relies on type-directed disambiguation, it will not compile with OCaml 4.00 or earlier. Ocamlopt src/transform/eliminate_unknown_types.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/transform/encoding_sort.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/printer/coq.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/mathematica.ml Ocamlc src/session/server_utils.mli Ocamlc src/session/itp_server.mli Ocamlc src/session/json_util.mli Ocamlc src/session/server_utils.ml Ocamlc src/session/itp_communication.ml Ocamlc src/session/itp_server.ml Ocamlc src/session/json_util.ml Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/smtv2_model_defs.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/parser/ptree.ml Ocamlopt src/transform/encoding.ml Ocamlopt src/transform/eliminate_literal.ml Ocamlopt src/driver/driver.ml Ocamlopt src/driver/collect_data_model.ml Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/parser/mlw_printer.ml Ocamlopt src/transform/encoding_guards_full.ml Ocamlopt src/transform/encoding_tags_full.ml Ocamlopt src/transform/encoding_guards.ml Ocamlopt src/transform/encoding_tags.ml Ocamlopt src/transform/encoding_twin.ml Linking lib/why3/why3.cmo Ocamlopt src/driver/whyconf.ml Ocamlopt src/driver/smtv2_model_parser.ml Ocamlopt src/mlw/eval_match.ml Ocamlopt src/transform/inlining.ml Ocamlopt src/mlw/typeinv.ml Ocamlopt src/session/strategy.ml Ocamlopt src/driver/autodetection.ml Ocamlopt src/session/strategy_parser.ml Ocamlc plugins/tptp/tptp_ast.mli Ocamlc plugins/python/py_ast.mli Ocamlc plugins/microc/mc_ast.mli Ocamlc plugins/cfg/cfg_ast.mli Ocamlc plugins/microc/mc_printer.mli Ocamlc plugins/transform/hypothesis_selection.ml Ocamlc src/why3session/why3session_lib.mli Ocamlc src/tools/why3pp_sexp.mli Ocamlc src/why3doc/doc_def.mli File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | let compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt src/mlw/vc.ml File "plugins/transform/hypothesis_selection.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc plugins/tptp/tptp_parser.mli Ocamlc plugins/tptp/tptp_typing.mli Ocamlc plugins/tptp/tptp_lexer.mli Ocamlc plugins/python/py_parser.mli Ocamlc plugins/python/py_lexer.mli Ocamlc plugins/microc/mc_parser.mli Ocamlc plugins/microc/mc_lexer.mli Ocamlc plugins/cfg/cfg_lexer.mli Ocamlc plugins/cfg/cfg_parser.mli Ocamlc plugins/cfg/cfg_paths.mli Ocamlc plugins/cfg/cfg_main.mli Ocamlc plugins/cfg/stackify.mli Ocamlc src/why3session/why3session_info.mli Ocamlc src/why3session/why3session_html.mli Ocamlc src/why3session/why3session_latex.mli Ocamlc src/why3session/why3session_update.mli Ocamlc plugins/cfg/cfg_stackify.ml Ocamlopt src/tools/why3pp_sexp.ml File "plugins/cfg/cfg_stackify.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlopt src/mlw/pmodule.ml Ocamlopt src/mlw/dexpr.ml Ocamlopt src/mlw/pinterp_core.ml Ocamlopt src/mlw/rac.ml Ocamlopt src/mlw/pinterp.ml Ocamlopt src/parser/typing.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/extract/compile.ml Ocamlopt src/extract/pdriver.ml Ocamlopt src/extract/ml_printer.ml Ocamlopt src/mlw/check_ce.ml Ocamlopt src/extract/ocaml.ml Ocamlopt src/extract/cakeml.ml Ocamlopt src/extract/mlinterp.ml Ocamlopt src/extract/c.ml File "src/extract/c.ml", line 68, characters 4-22: 68 | | Cfloat of string ^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cfloat is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 69, characters 4-21: 69 | | Cchar of string ^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Cchar is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 45-56: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostincr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 44, characters 68-79: 44 | and unop = Unot | Ustar | Uaddr | Upreincr | Upostincr | Upredecr | Upostdecr ^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Upostdecr is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 41, characters 59-64: 41 | and binop = Band | Bor | Beq | Bne | Bassign | Blt | Ble | Bgt | Bge ^^^^^ Warning 37 [unused-constructor]: constructor Bgt is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 29, characters 4-41: 29 | | Tunion of ident * (ident * ty) list ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Tunion is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 92, characters 4-28: 92 | | Dtypedef of ty * ident ^^^^^^^^^^^^^^^^^^^^^^^^ Warning 37 [unused-constructor]: constructor Dtypedef is never used to build values. (However, this constructor appears in patterns.) File "src/extract/c.ml", line 83, characters 21-24: 83 | and include_kind = Sys | Proj (* include <...> vs. include "..." *) ^^^ Warning 37 [unused-constructor]: constructor Sys is never used to build values. (However, this constructor appears in patterns.) Ocamlopt src/parser/parser.ml Ocamlopt src/parser/report.ml Ocamlopt src/parser/lexer.ml Ocamlopt src/transform/args_wrapper.ml Ocamlopt src/transform/apply.ml Ocamlopt src/transform/subst.ml Ocamlopt src/transform/compute.ml Ocamlopt src/transform/case.ml Ocamlopt src/transform/ind_itp.ml Ocamlopt src/transform/cut.ml Ocamlopt src/printer/gappa.ml Ocamlopt src/transform/eliminate_definition.ml Ocamlopt src/transform/discriminate.ml Ocamlopt src/transform/introduction.ml Ocamlopt src/transform/destruct.ml Ocamlopt src/transform/induction.ml Ocamlopt src/transform/induction_pr.ml Ocamlopt src/transform/reflection.ml Ocamlopt src/printer/alt_ergo.ml Ocamlopt src/printer/why3printer.ml Ocamlopt src/printer/smtv1.ml Ocamlopt src/printer/smtv2.ml Ocamlopt src/printer/simplify.ml Ocamlopt src/printer/cvc3.ml Ocamlopt src/printer/yices.ml Ocamlopt src/transform/encoding_select.ml Ocamlopt src/transform/prepare_for_counterexmp.ml Ocamlopt src/session/session_itp.ml Ocamlopt src/session/controller_itp.ml Ocamlopt src/session/itp_communication.ml Ocamlopt src/session/server_utils.ml Ocamlopt src/session/json_util.ml Ocamlopt src/session/itp_server.ml Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml Ocamlopt plugins/tptp/tptp_parser.ml Ocamlopt plugins/tptp/tptp_typing.ml Ocamlopt plugins/parser/dimacs.ml Ocamlopt plugins/python/py_parser.ml Ocamlopt plugins/tptp/tptp_printer.ml Ocamlopt plugins/microc/mc_parser.ml Ocamlopt plugins/microc/mc_printer.ml Ocamlopt plugins/cfg/cfg_parser.ml Ocamlopt plugins/cfg/cfg_paths.ml Ocamlopt plugins/cfg/stackify.ml File "plugins/cfg/stackify.ml", line 43, characters 8-28: 43 | let rec print_exp_structure' exp = match exp with ^^^^^^^^^^^^^^^^^^^^ Warning 32 [unused-value-declaration]: unused value print_exp_structure'. Ocamlopt plugins/transform/hypothesis_selection.ml File "plugins/transform/hypothesis_selection.ml", line 25, characters 16-34: 25 | let compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Linking lib/why3/why3.cmxa Linking lib/why3/why3.cmxs Ocamlopt src/tools/main.ml Ocamlopt src/tools/why3config.ml Ocamlopt src/tools/why3execute.ml Ocamlopt src/tools/why3extract.ml Ocamlopt src/tools/why3prove.ml Ocamlopt src/tools/why3realize.ml File "src/tools/why3prove.ml", line 517, characters 6-40: 517 | Format.set_formatter_tag_functions Util.ansi_color_tags; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Stdlib.Format.set_formatter_tag_functions Use Format.set_formatter_stag_functions. Ocamlopt src/tools/why3replay.ml Ocamlopt src/tools/why3show.ml Ocamlopt src/tools/why3wc.ml Ocamlopt src/ide/wserver.ml File "src/ide/wserver.ml", line 198, characters 27-35: 198 | let rec loop (strm__ : _ Stream.t) = ^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 199, characters 10-21: 199 | match Stream.peek strm__ with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 201, characters 6-17: 201 | Stream.junk strm__; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 207, characters 21-32: 207 | | Some '\013' -> Stream.junk strm__; loop strm__ ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 209, characters 6-17: 209 | Stream.junk strm__; ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 223, characters 24-32: 223 | let (strm__ : _ Stream.t) = strm in ^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 224, characters 14-25: 224 | match Stream.peek strm__ with ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 225, characters 20-31: 225 | | Some x -> Stream.junk strm__; x ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. File "src/ide/wserver.ml", line 240, characters 6-17: 240 | Stream.from ^^^^^^^^^^^ Alert deprecated: module Stdlib.Stream Use the camlp-streams library instead. Ocamlopt src/why3session/why3session_lib.ml Ocamlopt src/tools/why3shell.ml Ocamlopt src/isabelle-client/isabelle_client_main.ml Ocamlopt src/tools/why3pp.ml Ocamlopt src/why3doc/doc_html.ml Ocamlopt src/why3doc/doc_def.ml Linking lib/plugins/genequlin.cmxs Linking lib/plugins/dimacs.cmxs Ocamlopt plugins/tptp/tptp_lexer.ml Ocamlopt plugins/python/py_lexer.ml Ocamlopt plugins/microc/mc_lexer.ml Linking lib/plugins/hypothesis_selection.cmxs Linking bin/why3.opt Linking bin/why3config.cmxs Linking bin/why3execute.cmxs Linking bin/why3extract.cmxs Linking bin/why3prove.cmxs Linking bin/why3realize.cmxs Linking bin/why3replay.cmxs Linking bin/why3show.cmxs Linking bin/why3wc.cmxs Ocamlopt src/ide/why3web.ml Ocamlopt src/why3session/why3session_info.ml Ocamlopt src/why3session/why3session_html.ml Ocamlopt src/why3session/why3session_latex.ml Ocamlopt src/why3session/why3session_update.ml Linking bin/why3shell.cmxs Linking bin/isabelle_client.opt Linking bin/why3pp.cmxs Ocamlopt src/why3doc/doc_lexer.ml Linking lib/plugins/tptp.cmxs Ocamlopt plugins/python/py_main.ml Ocamlopt plugins/microc/mc_main.ml Linking bin/why3webserver.cmxs Ocamlopt src/why3session/why3session_main.ml Ocamlopt src/why3doc/doc_main.ml Linking bin/why3session.cmxs Linking bin/why3doc.cmxs Linking lib/plugins/microc.cmxs Linking lib/plugins/python.cmxs Ocamlopt plugins/cfg/cfg_lexer.ml Ocamlopt plugins/cfg/cfg_main.ml Ocamlopt plugins/cfg/cfg_stackify.ml Linking lib/plugins/cfg.cmxs