=> 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 Generate src/util/config.ml Ocamllex src/util/lexlib.mll Menhir src/util/json_parser.mly Ocamllex src/util/rc.mll Ocamllex src/util/json_lexer.mll 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings 52 states, 495 transitions, table size 2292 bytes cmp -s src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml || cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings cmp -s src/util/dynlink_new.ml src/util/dynlink_wrapper.ml || cp src/util/dynlink_new.ml src/util/dynlink_wrapper.ml 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 Ocamllex src/session/strategy_parser.mll 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings 47 states, 678 transitions, table size 2994 bytes 2153 additional bytes used for bindings cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml Ocamllex plugins/tptp/tptp_lexer.mll Menhir plugins/tptp/tptp_parser.mly 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 Read 3 sample input sentences and 3 error messages. Ocamldep src/why3session/why3session_lib.ml 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 Ocamllex src/why3doc/doc_lexer.mll cp src/util/json_base.mli src/trywhy3/json_base.mli 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/diffmap.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/json_base.ml Ocamldep src/util/debug.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/loc.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/rc.ml Ocamldep src/util/plugin.ml Ocamldep src/util/number.ml Ocamldep src/util/constant.ml Ocamldep src/util/vector.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/re.ml Ocamldep src/core/ident.ml Ocamldep src/core/ty.ml Ocamldep src/core/term.ml Ocamldep src/core/pattern.ml Ocamldep src/core/decl.ml Ocamldep src/core/coercion.ml Ocamldep src/core/theory.ml Ocamldep src/core/parser_tokens.ml Ocamldep src/core/keywords.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/sexp.ml Ocamldep src/driver/smtv2_model_parser.ml Ocamldep src/mlw/ity.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/c.ml Ocamldep src/extract/ocaml.ml Ocamldep src/extract/cakeml.ml Ocamldep src/parser/ptree.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/report.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_let.ml Ocamldep src/transform/eliminate_if.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_twin.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/eliminate_literal.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/intro_vc_vars_counterexmp.ml Ocamldep src/transform/congruence.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/yices.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/mathematica.ml Ocamldep src/session/xml.ml Ocamldep src/session/compress.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/termcode.ml Ocamldep src/session/strategy.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/server_utils.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/microc/mc_parser.ml Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/python/py_main.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/python/py_ast.mli Ocamldep plugins/microc/mc_ast.mli Ocamldep plugins/cfg/cfg_ast.mli mkdir lib/plugins Ocamlc src/util/config.mli Ocamlc src/util/bigInt.mli Ocamlc src/util/mysexplib.ml 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/loc.mli Ocamlc src/util/lexlib.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/vector.mli Ocamlc src/util/number.mli Ocamlc src/util/pqueue.mli Ocamlc src/util/re.ml Ocamlc src/driver/prove_client.mli Ocamlc src/driver/driver_ast.mli Ocamlc src/driver/sexp.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 Linking src/util/ppx_debug_optim Ocamlc src/extract/c.mli 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/sysutil.ml Ocamlc src/util/cmdline.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/driver/sexp.ml Ocamlc src/mlw/big_real.ml Ocamlc src/parser/parser_messages.ml Ocamlc src/session/compress.ml Ocamlc src/session/unix_scheduler.ml Ocamlc plugins/parser/genequlin.mli 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 plugins/parser/dimacs.mli Ocamlc plugins/tptp/tptp_printer.mli Ocamlc plugins/python/py_main.mli Ocamlc plugins/microc/mc_main.mli Ocamlc src/tools/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/why3show.mli Ocamlc src/tools/why3wc.mli Ocamlc src/ide/wserver.mli Ocamlc src/ide/why3web.mli Ocamlc src/why3session/why3session_main.mli Ocamlc src/tools/why3shell.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/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 Ocamlc src/util/diffmap.mli Ocamlopt 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/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 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/ident.mli 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 Ocamlopt src/mlw/big_real.ml Ocamlc src/parser/glob.mli Ocamlopt src/parser/parser_messages.ml Ocamlopt src/session/compress.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/extset.ml Ocamlc src/util/diffmap.ml 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/rc.ml Ocamlc src/util/plugin.ml Ocamlc src/util/number.ml Ocamlc src/core/ident.ml Ocamlc src/util/constant.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/core/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 Ocamlc src/core/ty.mli 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/json_lexer.ml Ocamlopt src/util/wstdlib.ml Ocamlopt src/util/json_lexer.ml Ocamlc src/core/term.mli Ocamlopt src/session/xml.ml Ocamlc src/core/ty.ml Ocamlopt src/util/loc.ml Ocamlopt src/util/plugin.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/number.ml Ocamlc src/core/pattern.mli Ocamlc src/core/decl.mli Ocamlc src/core/coercion.mli Ocamlc src/mlw/ity.mli Ocamlc src/transform/close_epsilon.mli Ocamlc src/printer/cntexmp_printer.mli Ocamlc src/core/term.ml Ocamlc src/core/pattern.ml Ocamlc src/core/decl.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 Ocamlc src/printer/cntexmp_printer.ml Ocamlopt src/util/lexlib.ml Ocamlopt src/util/warning.ml Ocamlopt src/util/rc.ml Ocamlopt src/util/constant.ml File "src/util/constant.ml", line 26, characters 33-51: 26 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 29, characters 33-51: 29 | let c = if structural then Pervasives.compare k1 k2 else 0 in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims File "src/util/constant.ml", line 32, characters 6-24: 32 | Pervasives.compare c1 c2 ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlopt src/core/ident.ml Ocamlc src/core/theory.mli Ocamlopt src/core/parser_tokens.ml Ocamlc src/mlw/expr.mli Ocamlc src/core/dterm.mli Ocamlc src/core/env.mli Ocamlc src/core/task.mli Ocamlc src/transform/detect_polymorphism.mli Ocamlc src/transform/eliminate_literal.mli Ocamlc src/core/theory.ml Ocamlc src/core/env.ml Ocamlc src/parser/ptree.ml Ocamlopt src/core/ty.ml File "src/parser/ptree.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/mlw/pdecl.mli Ocamlc src/core/pretty.mli Ocamlc src/core/trans.mli Ocamlopt src/driver/driver_parser.ml Ocamlc src/mlw/typeinv.mli Ocamlc src/mlw/eval_match.mli Ocamlc src/parser/ptree_helpers.mli Ocamlc src/mlw/vc.mli Ocamlopt src/parser/glob.ml Ocamlc src/parser/mlw_printer.mli Ocamlc src/transform/simplify_formula.mli Ocamlc src/transform/inlining.mli Ocamlc src/transform/split_goal.mli Ocamlc src/transform/args_wrapper.mli Ocamlc src/transform/compute.mli Ocamlc src/transform/reduction_engine.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/libencoding.mli Ocamlc src/transform/encoding.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/intro_vc_vars_counterexmp.mli Ocamlc src/transform/cut.mli Ocamlc src/transform/prepare_for_counterexmp.mli Ocamlc src/transform/reflection.mli Ocamlc src/session/termcode.mli Ocamlc src/core/task.ml 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/reduction_engine.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/lift_epsilon.ml Ocamlc src/transform/eliminate_epsilon.ml Ocamlc src/transform/intro_projections_counterexmp.ml Ocamlc src/transform/instantiate_predicate.ml Ocamlc src/transform/smoke_detector.ml Ocamlc src/transform/prop_curry.ml Ocamlc src/transform/eliminate_literal.ml Ocamlc src/transform/generic_arg_trans_utils.ml Ocamlc src/transform/case.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/mlw/pmodule.mli Ocamlc src/session/termcode.ml Ocamlc src/core/printer.mli Ocamlopt src/core/term.ml Ocamlopt src/driver/driver_lexer.ml Ocamlc src/transform/discriminate.mli File "src/core/term.ml", line 281, characters 39-57: 281 | let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims Ocamlc src/core/printer.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/pmodule.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/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/pattern.ml Ocamlopt src/core/coercion.ml Ocamlc src/parser/parser.mli Ocamlc src/core/model_parser.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/report.mli Ocamlc src/parser/lexer.mli Ocamlc src/core/model_parser.ml Ocamlc src/mlw/dexpr.ml Ocamlc src/mlw/pinterp_core.ml Ocamlc src/extract/mltree.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/parser/typing.ml Ocamlc src/parser/parser.ml Ocamlc src/parser/report.ml Ocamlc src/transform/args_wrapper.ml Ocamlc src/transform/reflection.ml Ocamlopt src/core/decl.ml Ocamlc src/core/keywords.mli Ocamlc src/driver/call_provers.mli Ocamlc src/driver/smtv2_model_defs.mli Ocamlc src/mlw/pinterp.mli Ocamlc src/extract/compile.mli Ocamlc src/extract/pdriver.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/mlw/pinterp.ml Ocamlc src/extract/compile.ml Ocamlc src/extract/mlinterp.ml Ocamlc src/extract/pdriver.ml Ocamlc src/extract/c.ml Ocamlc src/parser/lexer.ml Ocamlc src/printer/why3printer.ml Ocamlopt src/core/theory.ml Ocamlopt src/core/keywords.ml Ocamlc src/driver/driver.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/collect_data_model.mli Ocamlc src/mlw/check_ce.mli Ocamlc src/extract/ml_printer.mli Ocamlc src/driver/driver.ml Ocamlc src/driver/collect_data_model.ml Ocamlc src/driver/smtv2_model_parser.ml Ocamlc src/extract/ml_printer.ml Ocamlc src/extract/ocaml.ml Ocamlc src/extract/cakeml.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/task.ml Ocamlopt src/core/env.ml Ocamlc src/driver/whyconf.mli Ocamlopt src/core/pretty.ml Ocamlc src/driver/autodetection.mli Ocamlc src/mlw/rac.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/driver/autodetection.ml Ocamlc src/mlw/rac.ml Ocamlc src/mlw/check_ce.ml Ocamlc src/session/session_itp.ml Ocamlc src/session/strategy.ml Ocamlopt src/core/dterm.ml Ocamlopt src/core/trans.ml Ocamlopt src/mlw/ity.ml Ocamlc src/session/strategy_parser.mli Ocamlc src/session/controller_itp.mli Ocamlopt src/core/printer.ml 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_unknown_types.ml Ocamlopt src/transform/eliminate_unknown_lsymbols.ml Ocamlopt src/transform/eliminate_symbol.ml Ocamlopt src/transform/eliminate_inductive.ml Ocamlopt src/transform/eliminate_let.ml Ocamlopt src/transform/eliminate_if.ml Ocamlopt src/transform/libencoding.ml Ocamlopt src/transform/encoding_sort.ml Ocamlopt src/transform/simplify_array.ml Ocamlopt src/transform/filter_trigger.ml Ocamlopt src/transform/abstraction.ml Ocamlopt src/transform/close_epsilon.ml Ocamlopt src/transform/eliminate_epsilon.ml Ocamlopt src/transform/intro_projections_counterexmp.ml Ocamlopt src/transform/instantiate_predicate.ml Ocamlopt src/transform/smoke_detector.ml Ocamlopt src/transform/prop_curry.ml Ocamlopt src/transform/eliminate_literal.ml Ocamlopt src/transform/generic_arg_trans_utils.ml Ocamlopt src/transform/congruence.ml Ocamlopt src/transform/intro_vc_vars_counterexmp.ml Ocamlopt src/printer/cntexmp_printer.ml Ocamlopt src/printer/coq.ml Ocamlopt src/printer/pvs.ml Ocamlopt src/printer/isabelle.ml Ocamlopt src/printer/mathematica.ml Ocamlopt src/session/termcode.ml Ocamlc src/session/itp_communication.mli Ocamlc src/session/strategy_parser.ml Ocamlc src/session/controller_itp.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/session/itp_communication.ml Ocamlopt src/core/model_parser.ml Ocamlopt src/mlw/expr.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_algebraic.ml Ocamlopt src/transform/encoding.ml Ocamlopt src/transform/lift_epsilon.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_server.ml Ocamlc src/session/json_util.ml Ocamlopt src/driver/call_provers.ml Ocamlopt src/driver/smtv2_model_defs.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/driver.ml Ocamlopt src/driver/collect_data_model.ml Ocamlopt src/mlw/pdecl.ml Ocamlopt src/parser/ptree.ml Ocamlopt src/driver/smtv2_model_parser.ml Ocamlopt src/transform/inlining.ml Ocamlopt src/driver/whyconf.ml Ocamlopt src/parser/ptree_helpers.ml Ocamlopt src/parser/mlw_printer.ml Ocamlopt src/mlw/eval_match.ml Ocamlopt src/mlw/typeinv.ml Ocamlopt src/driver/autodetection.ml Ocamlopt src/session/strategy.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/microc/mc_printer.mli Ocamlc plugins/cfg/cfg_ast.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 Ocamlc plugins/tptp/tptp_parser.mli Ocamlc plugins/tptp/tptp_typing.mli Ocamlc plugins/tptp/tptp_lexer.mli File "plugins/transform/hypothesis_selection.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. 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_parser.mli Ocamlc plugins/cfg/cfg_lexer.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 Ocamlopt src/tools/why3pp_sexp.ml Ocamlc plugins/cfg/cfg_stackify.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/pinterp.ml Ocamlopt src/mlw/rac.ml Ocamlopt src/extract/mltree.ml Ocamlopt src/parser/typing.ml Ocamlopt src/extract/pdriver.ml Ocamlopt src/extract/compile.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/case.ml Ocamlopt src/transform/compute.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/json_util.ml Ocamlopt src/session/server_utils.ml Ocamlopt src/session/itp_server.ml Linking lib/why3/why3.cmx Ocamlopt plugins/parser/genequlin.ml Ocamlopt plugins/tptp/tptp_typing.ml Ocamlopt plugins/parser/dimacs.ml Ocamlopt plugins/tptp/tptp_parser.ml Ocamlopt plugins/tptp/tptp_printer.ml Ocamlopt plugins/python/py_parser.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 Ocamlopt plugins/transform/hypothesis_selection.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'. 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