+ case "${usergroup_phase}" in
+ local run_cmd
+ run_cmd=run_su
+ shift
+ run_su /opt/local/bin/bmake all BATCH=1 DEPENDS_TARGET=/nonexistent WRKLOG=/tmp/bulklog/why3-1.5.1nb1/work.log
+ su pbulk -c '"$@"' make /opt/local/bin/bmake all BATCH=1 DEPENDS_TARGET=/nonexistent WRKLOG=/tmp/bulklog/why3-1.5.1nb1/work.log
=> Bootstrap dependency digest>=20211023: found digest-20220214
===> Building for why3-1.5.1nb1
cp src/util/json_base.ml src/trywhy3/json_base.ml
Menhir src/util/json_parser.mly
cp src/util/json_parser.ml src/trywhy3/json_parser.ml
Ocamllex src/util/json_lexer.mll
52 states, 495 transitions, table size 2292 bytes
cp src/util/json_lexer.ml src/trywhy3/json_lexer.ml
cp src/util/json_base.mli src/trywhy3/json_base.mli
cp src/util/json_parser.mli src/trywhy3/json_parser.mli
cp src/util/json_lexer.mli src/trywhy3/json_lexer.mli
Ocamldep src/trywhy3/worker_proto.ml
Ocamldep src/trywhy3/why3_worker.ml
Ocamldep src/trywhy3/trywhy3.ml
Ocamldep src/trywhy3/shortener.ml
Ocamldep src/trywhy3/bindings.ml
Ocamldep src/trywhy3/json_lexer.ml
Ocamldep src/trywhy3/json_parser.ml
Ocamldep src/trywhy3/json_base.ml
Ocamllex src/why3doc/doc_lexer.mll
120 states, 685 transitions, table size 3460 bytes
1763 additional bytes used for bindings
Ocamldep src/why3doc/doc_main.ml
Ocamldep src/why3doc/doc_lexer.ml
Ocamldep src/why3doc/doc_def.ml
Ocamldep src/why3doc/doc_html.ml
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
Ocamldep src/tools/why3pp.ml
Ocamldep src/tools/why3pp_sexp.ml
Ocamldep src/isabelle-client/isabelle_client_main.ml
Ocamldep src/tools/why3shell.ml
Ocamldep src/why3session/why3session_main.ml
Ocamldep src/why3session/why3session_update.ml
Ocamldep src/why3session/why3session_latex.ml
Ocamldep src/why3session/why3session_html.ml
Ocamldep src/why3session/why3session_info.ml
Ocamldep src/why3session/why3session_lib.ml
Ocamldep src/ide/why3web.ml
Ocamldep src/ide/wserver.ml
Ocamllex src/tools/why3wc.mll
307 states, 15627 transitions, table size 64350 bytes
Ocamldep src/tools/why3wc.ml
Ocamldep src/tools/why3show.ml
Ocamldep src/tools/why3replay.ml
Ocamldep src/tools/why3realize.ml
Ocamldep src/tools/why3prove.ml
Ocamldep src/tools/why3extract.ml
Ocamldep src/tools/why3execute.ml
Ocamldep src/tools/why3config.ml
Ocamldep src/tools/main.ml
Ocamllex plugins/tptp/tptp_lexer.mll
101 states, 1563 transitions, table size 6858 bytes
3126 additional bytes used for bindings
Menhir plugins/tptp/tptp_parser.mly
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
Ocamllex plugins/cfg/cfg_lexer.mll
155 states, 4342 transitions, table size 18298 bytes
7537 additional bytes used for bindings
Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly
Ocamllex plugins/parser/dimacs.mll
34 states, 434 transitions, table size 1940 bytes
1293 additional bytes used for bindings
Ocamldep plugins/cfg/cfg_ast.mli
Ocamldep plugins/microc/mc_ast.mli
Ocamldep plugins/python/py_ast.mli
Ocamldep plugins/tptp/tptp_ast.mli
Ocamldep plugins/cfg/cfg_main.ml
Ocamldep plugins/cfg/cfg_paths.ml
Ocamldep plugins/cfg/cfg_lexer.ml
Ocamldep plugins/cfg/cfg_parser.ml
Ocamldep plugins/microc/mc_main.ml
Ocamldep plugins/microc/mc_printer.ml
Ocamldep plugins/microc/mc_lexer.ml
Ocamldep plugins/microc/mc_parser.ml
Ocamldep plugins/python/py_main.ml
Ocamldep plugins/python/py_lexer.ml
Ocamldep plugins/python/py_parser.ml
Ocamldep plugins/tptp/tptp_printer.ml
Ocamldep plugins/tptp/tptp_lexer.ml
Ocamldep plugins/tptp/tptp_typing.ml
Ocamldep plugins/tptp/tptp_parser.ml
Ocamldep plugins/parser/dimacs.ml
Ocamldep plugins/parser/genequlin.ml
Generate src/util/config.ml
Ocamllex src/util/rc.mll
48 states, 1889 transitions, table size 7844 bytes
3073 additional bytes used for bindings
Ocamllex src/util/lexlib.mll
39 states, 600 transitions, table size 2634 bytes
1338 additional bytes used for bindings
cmp -s src/util/mysexplib-dummy.ml src/util/mysexplib.ml || cp src/util/mysexplib-dummy.ml src/util/mysexplib.ml
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
Ocamllex src/parser/lexer.mll
158 states, 4359 transitions, table size 18384 bytes
7555 additional bytes used for bindings
Menhir src/parser/parser_common.mly
Menhir src/parser/parser_common.mly src/parser/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
Read 3 sample input sentences and 3 error messages.
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
47 states, 678 transitions, table size 2994 bytes
2153 additional bytes used for bindings
Ocamldep src/driver/driver_ast.mli
Ocamldep src/session/unix_scheduler.ml
Ocamldep src/session/json_util.ml
Ocamldep src/session/itp_server.ml
Ocamldep src/session/itp_communication.ml
Ocamldep src/session/server_utils.ml
Ocamldep src/session/controller_itp.ml
Ocamldep src/session/strategy_parser.ml
Ocamldep src/session/strategy.ml
Ocamldep src/session/session_itp.ml
Ocamldep src/session/termcode.ml
Ocamldep src/session/xml.ml
Ocamldep src/session/compress.ml
Ocamldep src/printer/mathematica.ml
Ocamldep src/printer/yices.ml
Ocamldep src/printer/cvc3.ml
Ocamldep src/printer/gappa.ml
Ocamldep src/printer/simplify.ml
Ocamldep src/printer/isabelle.ml
Ocamldep src/printer/pvs.ml
Ocamldep src/printer/coq.ml
Ocamldep src/printer/smtv2.ml
Ocamldep src/printer/smtv1.ml
Ocamldep src/printer/why3printer.ml
Ocamldep src/printer/alt_ergo.ml
Ocamldep src/printer/cntexmp_printer.ml
Ocamldep src/transform/reflection.ml
Ocamldep src/transform/induction_pr.ml
Ocamldep src/transform/induction.ml
Ocamldep src/transform/prepare_for_counterexmp.ml
Ocamldep src/transform/intro_vc_vars_counterexmp.ml
Ocamldep src/transform/congruence.ml
Ocamldep src/transform/cut.ml
Ocamldep src/transform/destruct.ml
Ocamldep src/transform/ind_itp.ml
Ocamldep src/transform/introduction.ml
Ocamldep src/transform/subst.ml
Ocamldep src/transform/apply.ml
Ocamldep src/transform/case.ml
Ocamldep src/transform/generic_arg_trans_utils.ml
Ocamldep src/transform/eliminate_literal.ml
Ocamldep src/transform/prop_curry.ml
Ocamldep src/transform/smoke_detector.ml
Ocamldep src/transform/instantiate_predicate.ml
Ocamldep src/transform/intro_projections_counterexmp.ml
Ocamldep src/transform/eliminate_epsilon.ml
Ocamldep src/transform/lift_epsilon.ml
Ocamldep src/transform/close_epsilon.ml
Ocamldep src/transform/abstraction.ml
Ocamldep src/transform/filter_trigger.ml
Ocamldep src/transform/simplify_array.ml
Ocamldep src/transform/encoding_sort.ml
Ocamldep src/transform/encoding_twin.ml
Ocamldep src/transform/encoding_tags.ml
Ocamldep src/transform/encoding_guards.ml
Ocamldep src/transform/encoding_tags_full.ml
Ocamldep src/transform/encoding_guards_full.ml
Ocamldep src/transform/encoding_select.ml
Ocamldep src/transform/encoding.ml
Ocamldep src/transform/discriminate.ml
Ocamldep src/transform/libencoding.ml
Ocamldep src/transform/eliminate_if.ml
Ocamldep src/transform/eliminate_let.ml
Ocamldep src/transform/eliminate_inductive.ml
Ocamldep src/transform/eliminate_symbol.ml
Ocamldep src/transform/eliminate_unknown_lsymbols.ml
Ocamldep src/transform/eliminate_unknown_types.ml
Ocamldep src/transform/abstract_quantifiers.ml
Ocamldep src/transform/eliminate_algebraic.ml
Ocamldep src/transform/eliminate_definition.ml
Ocamldep src/transform/compute.ml
Ocamldep src/transform/reduction_engine.ml
Ocamldep src/transform/detect_polymorphism.ml
Ocamldep src/transform/args_wrapper.ml
Ocamldep src/transform/split_goal.ml
Ocamldep src/transform/inlining.ml
Ocamldep src/transform/simplify_formula.ml
Ocamldep src/parser/mlw_printer.ml
Ocamldep src/parser/lexer.ml
Ocamldep src/parser/report.ml
Ocamldep src/parser/typing.ml
Ocamldep src/parser/parser.ml
Ocamldep src/parser/parser_messages.ml
Ocamldep src/parser/glob.ml
Ocamldep src/parser/ptree_helpers.ml
Ocamldep src/parser/ptree.ml
Ocamldep src/extract/cakeml.ml
Ocamldep src/extract/ocaml.ml
Ocamldep src/extract/c.ml
Ocamldep src/extract/ml_printer.ml
Ocamldep src/extract/pdriver.ml
Ocamldep src/extract/mlinterp.ml
Ocamldep src/extract/compile.ml
Ocamldep src/extract/mltree.ml
Ocamldep src/mlw/check_ce.ml
Ocamldep src/mlw/pinterp.ml
Ocamldep src/mlw/rac.ml
Ocamldep src/mlw/pinterp_core.ml
Ocamldep src/mlw/big_real.ml
Ocamldep src/mlw/dexpr.ml
Ocamldep src/mlw/pmodule.ml
Ocamldep src/mlw/vc.ml
Ocamldep src/mlw/typeinv.ml
Ocamldep src/mlw/eval_match.ml
Ocamldep src/mlw/pdecl.ml
Ocamldep src/mlw/expr.ml
Ocamldep src/mlw/ity.ml
Ocamldep src/driver/smtv2_model_parser.ml
Ocamldep src/driver/sexp.ml
Ocamldep src/driver/collect_data_model.ml
Ocamldep src/driver/smtv2_model_defs.ml
Ocamldep src/driver/autodetection.ml
Ocamldep src/driver/whyconf.ml
Ocamldep src/driver/driver.ml
Ocamldep src/driver/driver_lexer.ml
Ocamldep src/driver/driver_parser.ml
Ocamldep src/driver/call_provers.ml
Ocamldep src/driver/prove_client.ml
Ocamldep src/core/model_parser.ml
Ocamldep src/core/printer.ml
Ocamldep src/core/trans.ml
Ocamldep src/core/env.ml
Ocamldep src/core/dterm.ml
Ocamldep src/core/pretty.ml
Ocamldep src/core/task.ml
Ocamldep src/core/keywords.ml
Ocamldep src/core/parser_tokens.ml
Ocamldep src/core/theory.ml
Ocamldep src/core/coercion.ml
Ocamldep src/core/decl.ml
Ocamldep src/core/pattern.ml
Ocamldep src/core/term.ml
Ocamldep src/core/ty.ml
Ocamldep src/core/ident.ml
cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml
Ocamldep src/util/re.ml
Ocamldep src/util/pqueue.ml
Ocamldep src/util/vector.ml
Ocamldep src/util/constant.ml
Ocamldep src/util/number.ml
Ocamldep src/util/bigInt.ml
Ocamldep src/util/plugin.ml
Ocamldep src/util/rc.ml
Ocamldep src/util/sysutil.ml
Ocamldep src/util/warning.ml
Ocamldep src/util/cmdline.ml
Ocamldep src/util/dynlink_wrapper.ml
Ocamldep src/util/print_tree.ml
Ocamldep src/util/lexlib.ml
Ocamldep src/util/loc.ml
Ocamldep src/util/debug.ml
Ocamldep src/util/json_lexer.ml
Ocamldep src/util/json_parser.ml
Ocamldep src/util/json_base.ml
Ocamldep src/util/getopt.ml
Ocamldep src/util/exn_printer.ml
Ocamldep src/util/wstdlib.ml
Ocamldep src/util/hashcons.ml
Ocamldep src/util/diffmap.ml
Ocamldep src/util/weakhtbl.ml
Ocamldep src/util/exthtbl.ml
Ocamldep src/util/extset.ml
Ocamldep src/util/extmap.ml
Ocamldep src/util/pp.ml
Ocamldep src/util/strings.ml
Ocamldep src/util/lists.ml
Ocamldep src/util/opt.ml
Ocamldep src/util/util.ml
Ocamldep src/util/mlmpfr_wrapper.ml
Ocamldep src/util/config.ml
Ocamldep src/util/mysexplib.ml
mkdir lib/plugins
Ocamlc src/util/mysexplib.ml
File "src/util/mysexplib.ml", line 1:
Warning 70 [missing-mli]: Cannot find interface file.
Ocamlopt src/util/mysexplib.ml
Ocamlc src/util/config.mli
Ocamlopt src/util/config.ml
Ocamlc src/util/bigInt.mli
Ocamlopt src/util/bigInt.ml
Ocamlc src/util/mlmpfr_wrapper.mli
Ocamlopt src/util/mlmpfr_wrapper.ml
Ocamlc src/util/util.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.
Ocamlopt src/util/util.ml
Ocamlc src/util/opt.mli
Ocamlopt src/util/opt.ml
Ocamlc src/util/lists.mli
Ocamlopt src/util/lists.ml
Ocamlc src/util/strings.mli
Ocamlopt src/util/strings.ml
Ocamlc src/util/pp.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
Ocamlopt src/util/pp.ml
Ocamlc src/util/extmap.mli
Ocamlopt src/util/extmap.ml
Ocamlc src/util/extset.mli
Ocamlopt src/util/extset.ml
Ocamlc src/util/exthtbl.mli
Ocamlopt src/util/exthtbl.ml
Ocamlc src/util/weakhtbl.mli
Ocamlopt src/util/weakhtbl.ml
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/diffmap.ml
Ocamlc src/util/hashcons.mli
Ocamlopt src/util/hashcons.ml
Ocamlc src/util/wstdlib.mli
Ocamlopt src/util/wstdlib.ml
Ocamlc src/util/exn_printer.mli
Ocamlopt src/util/exn_printer.ml
Ocamlc src/util/getopt.mli
Ocamlopt src/util/getopt.ml
Ocamlc src/util/json_base.mli
Ocamlopt src/util/json_base.ml
Ocamlc src/util/json_parser.mli
Ocamlopt src/util/json_parser.ml
Ocamlc src/util/json_lexer.mli
Ocamlopt src/util/json_lexer.ml
Ocamlc src/util/debug.mli
Ocamlopt src/util/debug.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/util/loc.mli
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
Ocamlc src/util/lexlib.mli
Ocamlopt src/util/lexlib.ml
Ocamlc src/util/print_tree.mli
Ocamlopt src/util/print_tree.ml
Ocamlc src/util/dynlink_wrapper.mli
Ocamlopt src/util/dynlink_wrapper.ml
Ocamlc src/util/cmdline.mli
Ocamlopt src/util/cmdline.ml
Ocamlc src/util/warning.mli
Ocamlopt src/util/warning.ml
Ocamlc src/util/sysutil.mli
Ocamlopt src/util/sysutil.ml
Ocamlc src/util/rc.mli
Ocamlopt src/util/rc.ml
Ocamlc src/util/plugin.mli
Ocamlopt src/util/plugin.ml
Ocamlc src/util/number.mli
Ocamlopt src/util/number.ml
Ocamlc src/util/constant.mli
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
Ocamlc src/util/vector.mli
Ocamlopt src/util/vector.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/util/pqueue.mli
Ocamlopt src/util/pqueue.ml
Ocamlc src/util/re.ml
File "src/util/re.ml", line 1:
Warning 70 [missing-mli]: Cannot find interface file.
Ocamlopt src/util/re.ml
Ocamlc src/core/ident.mli
Ocamlopt src/core/ident.ml
Ocamlc src/core/ty.mli
Ocamlopt src/core/ty.ml
Ocamlc src/core/term.mli
Ocamlopt src/core/term.ml
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/pattern.mli
Ocamlopt src/core/pattern.ml
Ocamlc src/core/decl.mli
Ocamlopt src/core/decl.ml
Ocamlc src/core/coercion.mli
Ocamlopt src/core/coercion.ml
Ocamlc src/core/theory.mli
Ocamlopt src/core/theory.ml
Ocamlc src/core/parser_tokens.mli
Ocamlopt src/core/parser_tokens.ml
Ocamlc src/mlw/ity.mli
Ocamlc src/mlw/expr.mli
Ocamlc src/core/dterm.mli
Ocamlc src/parser/ptree.ml
File "src/parser/ptree.ml", line 1:
Warning 70 [missing-mli]: Cannot find interface file.
Ocamlc src/mlw/pdecl.mli
Ocamlc src/core/env.mli
Ocamlc src/mlw/pmodule.mli
Ocamlc src/parser/parser.mli
Ocamlc src/core/keywords.mli
Ocamlopt src/core/keywords.ml
Ocamlc src/core/task.mli
Ocamlopt src/core/task.ml
Ocamlc src/core/pretty.mli
Ocamlopt src/core/pretty.ml
Ocamlopt src/core/dterm.ml
Ocamlopt src/core/env.ml
Ocamlc src/core/trans.mli
Ocamlopt src/core/trans.ml
Ocamlc src/core/printer.mli
Ocamlopt src/core/printer.ml
Ocamlc src/core/model_parser.mli
Ocamlopt src/core/model_parser.ml
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/driver/prove_client.mli
Ocamlopt src/driver/prove_client.ml
Ocamlc src/driver/call_provers.mli
Ocamlopt src/driver/call_provers.ml
Ocamlc src/driver/driver_ast.mli
Ocamlc src/driver/driver_parser.mli
Ocamlopt src/driver/driver_parser.ml
Ocamlc src/driver/driver_lexer.mli
Ocamlopt src/driver/driver_lexer.ml
Ocamlc src/driver/driver.mli
Ocamlopt src/driver/driver.ml
Ocamlc src/driver/whyconf.mli
Ocamlopt src/driver/whyconf.ml
Ocamlc src/driver/autodetection.mli
Ocamlopt src/driver/autodetection.ml
Ocamlc src/driver/smtv2_model_defs.mli
Ocamlopt src/driver/smtv2_model_defs.ml
Ocamlc src/driver/collect_data_model.mli
Ocamlopt src/driver/collect_data_model.ml
Ocamlc src/driver/sexp.mli
Ocamlopt src/driver/sexp.ml
Ocamlc src/driver/smtv2_model_parser.mli
Ocamlopt src/driver/smtv2_model_parser.ml
Ocamlopt src/mlw/ity.ml
Ocamlopt src/mlw/expr.ml
Ocamlopt src/mlw/pdecl.ml
Ocamlc src/mlw/eval_match.mli
Ocamlopt src/mlw/eval_match.ml
Ocamlc src/mlw/typeinv.mli
Ocamlopt src/mlw/typeinv.ml
Ocamlc src/mlw/vc.mli
Ocamlopt src/mlw/vc.ml
Ocamlopt src/mlw/pmodule.ml
Ocamlc src/mlw/dexpr.mli
Ocamlopt src/mlw/dexpr.ml
Ocamlc src/mlw/big_real.mli
Ocamlopt src/mlw/big_real.ml
Ocamlc src/mlw/pinterp_core.mli
Ocamlopt src/mlw/pinterp_core.ml
Ocamlc src/mlw/rac.mli
Ocamlopt src/mlw/rac.ml
Ocamlc src/mlw/pinterp.mli
Ocamlopt src/mlw/pinterp.ml
Ocamlc src/mlw/check_ce.mli
Ocamlopt src/mlw/check_ce.ml
Ocamlc src/extract/mltree.mli
Ocamlopt src/extract/mltree.ml
Ocamlc src/extract/compile.mli
Ocamlopt src/extract/compile.ml
Linking src/util/ppx_debug_optim
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /opt/local/lib/ocaml, /opt/local/lib/ocaml/compiler-libs
Ocamlc src/extract/mlinterp.mli
Ocamlopt src/extract/mlinterp.ml
Ocamlc src/extract/pdriver.mli
Ocamlopt src/extract/pdriver.ml
Ocamlc src/extract/ml_printer.mli
Ocamlopt src/extract/ml_printer.ml
Ocamlc src/extract/c.mli
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.)
Ocamlc src/extract/ocaml.mli
Ocamlopt src/extract/ocaml.ml
Ocamlc src/extract/cakeml.mli
Ocamlopt src/extract/cakeml.ml
Ocamlopt src/parser/ptree.ml
Ocamlc src/parser/ptree_helpers.mli
Ocamlopt src/parser/ptree_helpers.ml
Ocamlc src/parser/glob.mli
Ocamlopt src/parser/glob.ml
Ocamlc src/parser/typing.mli
Ocamlopt src/parser/typing.ml
Ocamlc src/parser/parser_messages.mli
Ocamlopt src/parser/parser_messages.ml
Ocamlopt src/parser/parser.ml
Ocamlc src/parser/report.mli
Ocamlopt src/parser/report.ml
Ocamlc src/parser/lexer.mli
Ocamlopt src/parser/lexer.ml
Ocamlc src/parser/mlw_printer.mli
Ocamlopt src/parser/mlw_printer.ml
Ocamlc src/transform/simplify_formula.mli
Ocamlopt src/transform/simplify_formula.ml
Ocamlc src/transform/inlining.mli
Ocamlopt src/transform/inlining.ml
Ocamlc src/transform/split_goal.mli
Ocamlopt src/transform/split_goal.ml
Ocamlc src/transform/args_wrapper.mli
Ocamlopt src/transform/args_wrapper.ml
Ocamlc src/transform/detect_polymorphism.mli
Ocamlopt src/transform/detect_polymorphism.ml
Ocamlc src/transform/reduction_engine.mli
Ocamlopt src/transform/reduction_engine.ml
Ocamlc src/transform/compute.mli
Ocamlopt src/transform/compute.ml
Ocamlc src/transform/eliminate_definition.mli
Ocamlopt src/transform/eliminate_definition.ml
Ocamlc src/transform/eliminate_algebraic.mli
Ocamlopt src/transform/eliminate_algebraic.ml
Ocamlc src/transform/abstract_quantifiers.mli
Ocamlopt src/transform/abstract_quantifiers.ml
Ocamlc src/transform/eliminate_unknown_types.mli
Ocamlopt src/transform/eliminate_unknown_types.ml
Ocamlc src/transform/eliminate_unknown_lsymbols.mli
Ocamlopt src/transform/eliminate_unknown_lsymbols.ml
Ocamlc src/transform/eliminate_symbol.mli
Ocamlopt src/transform/eliminate_symbol.ml
Ocamlc src/transform/eliminate_inductive.mli
Ocamlopt src/transform/eliminate_inductive.ml
Ocamlc src/transform/eliminate_let.mli
Ocamlopt src/transform/eliminate_let.ml
Ocamlc src/transform/eliminate_if.mli
Ocamlopt src/transform/eliminate_if.ml
Ocamlc src/transform/libencoding.mli
Ocamlopt src/transform/libencoding.ml
Ocamlc src/transform/discriminate.mli
Ocamlopt src/transform/discriminate.ml
Ocamlc src/transform/encoding.mli
Ocamlopt src/transform/encoding.ml
Ocamlc src/transform/encoding_select.mli
Ocamlopt src/transform/encoding_select.ml
Ocamlc src/transform/encoding_guards_full.mli
Ocamlopt src/transform/encoding_guards_full.ml
Ocamlc src/transform/encoding_tags_full.mli
Ocamlopt src/transform/encoding_tags_full.ml
Ocamlc src/transform/encoding_guards.mli
Ocamlopt src/transform/encoding_guards.ml
Ocamlc src/transform/encoding_tags.mli
Ocamlopt src/transform/encoding_tags.ml
Ocamlc src/transform/encoding_twin.mli
Ocamlopt src/transform/encoding_twin.ml
Ocamlc src/transform/encoding_sort.mli
Ocamlopt src/transform/encoding_sort.ml
Ocamlc src/transform/simplify_array.mli
Ocamlopt src/transform/simplify_array.ml
Ocamlc src/transform/filter_trigger.mli
Ocamlopt src/transform/filter_trigger.ml
Ocamlc src/transform/abstraction.mli
Ocamlopt src/transform/abstraction.ml
Ocamlc src/transform/close_epsilon.mli
Ocamlopt src/transform/close_epsilon.ml
Ocamlc src/transform/lift_epsilon.mli
Ocamlopt src/transform/lift_epsilon.ml
Ocamlc src/transform/eliminate_epsilon.mli
Ocamlopt src/transform/eliminate_epsilon.ml
Ocamlc src/transform/intro_projections_counterexmp.mli
Ocamlopt src/transform/intro_projections_counterexmp.ml
Ocamlc src/transform/instantiate_predicate.mli
Ocamlopt src/transform/instantiate_predicate.ml
Ocamlc src/transform/smoke_detector.mli
Ocamlopt src/transform/smoke_detector.ml
Ocamlc src/transform/prop_curry.mli
Ocamlopt src/transform/prop_curry.ml
Ocamlc src/transform/eliminate_literal.mli
Ocamlopt src/transform/eliminate_literal.ml
Ocamlc src/transform/generic_arg_trans_utils.mli
Ocamlopt src/transform/generic_arg_trans_utils.ml
Ocamlc src/transform/case.mli
Ocamlopt src/transform/case.ml
Ocamlc src/transform/apply.mli
Ocamlopt src/transform/apply.ml
Ocamlc src/transform/subst.mli
Ocamlopt src/transform/subst.ml
Ocamlc src/transform/introduction.mli
Ocamlopt src/transform/introduction.ml
Ocamlc src/transform/ind_itp.mli
Ocamlopt src/transform/ind_itp.ml
Ocamlc src/transform/destruct.mli
Ocamlopt src/transform/destruct.ml
Ocamlc src/transform/cut.mli
Ocamlopt src/transform/cut.ml
Ocamlc src/transform/congruence.mli
Ocamlopt src/transform/congruence.ml
Ocamlc src/transform/intro_vc_vars_counterexmp.mli
Ocamlopt src/transform/intro_vc_vars_counterexmp.ml
Ocamlc src/transform/prepare_for_counterexmp.mli
Ocamlopt src/transform/prepare_for_counterexmp.ml
Ocamlc src/transform/induction.mli
Ocamlopt src/transform/induction.ml
Ocamlc src/transform/induction_pr.mli
Ocamlopt src/transform/induction_pr.ml
Ocamlc src/transform/reflection.mli
Ocamlopt src/transform/reflection.ml
Ocamlc src/printer/cntexmp_printer.mli
Ocamlopt src/printer/cntexmp_printer.ml
Ocamlc src/printer/alt_ergo.mli
Ocamlopt src/printer/alt_ergo.ml
Ocamlc src/printer/why3printer.mli
Ocamlopt src/printer/why3printer.ml
Ocamlc src/printer/smtv1.mli
Ocamlopt src/printer/smtv1.ml
Ocamlc src/printer/smtv2.mli
Ocamlopt src/printer/smtv2.ml
Ocamlc src/printer/coq.mli
Ocamlopt src/printer/coq.ml
Ocamlc src/printer/pvs.mli
Ocamlopt src/printer/pvs.ml
Ocamlc src/printer/isabelle.mli
Ocamlopt src/printer/isabelle.ml
Ocamlc src/printer/simplify.mli
Ocamlopt src/printer/simplify.ml
Ocamlc src/printer/gappa.mli
Ocamlopt src/printer/gappa.ml
Ocamlc src/printer/cvc3.mli
Ocamlopt src/printer/cvc3.ml
Ocamlc src/printer/yices.mli
Ocamlopt src/printer/yices.ml
Ocamlc src/printer/mathematica.mli
Ocamlopt src/printer/mathematica.ml
Ocamlc src/session/compress.mli
Ocamlopt 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/xml.mli
Ocamlopt src/session/xml.ml
Ocamlc src/session/termcode.mli
Ocamlopt src/session/termcode.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/session_itp.mli
Ocamlopt src/session/session_itp.ml
Ocamlc src/session/strategy.mli
Ocamlopt src/session/strategy.ml
Ocamlc src/session/strategy_parser.mli
Ocamlopt src/session/strategy_parser.ml
Ocamlc src/session/controller_itp.mli
Ocamlopt src/session/controller_itp.ml
Ocamlc src/session/itp_communication.mli
Ocamlopt src/session/itp_communication.ml
Ocamlc src/session/server_utils.mli
Ocamlopt src/session/server_utils.ml
Ocamlc src/session/itp_server.mli
Ocamlopt src/session/itp_server.ml
Ocamlc src/session/json_util.mli
Ocamlopt src/session/json_util.ml
Ocamlc src/session/unix_scheduler.mli
Ocamlopt src/session/unix_scheduler.ml
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/extset.ml
Ocamlc src/util/exthtbl.ml
Ocamlc 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.ml
Ocamlc src/util/hashcons.ml
Ocamlc src/util/wstdlib.ml
Ocamlc src/util/exn_printer.ml
Ocamlc src/util/getopt.ml
Ocamlc src/util/json_base.ml
Ocamlc src/util/json_parser.ml
Ocamlc src/util/json_lexer.ml
Ocamlc src/util/debug.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/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
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/warning.ml
Ocamlc src/util/sysutil.ml
Ocamlc src/util/rc.ml
Ocamlc src/util/plugin.ml
Ocamlc src/util/number.ml
Ocamlc src/util/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/util/vector.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/util/pqueue.ml
Ocamlc src/core/ident.ml
Ocamlc src/core/ty.ml
Ocamlc 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/core/pattern.ml
Ocamlc src/core/decl.ml
Ocamlc src/core/coercion.ml
Ocamlc src/core/theory.ml
Ocamlc src/core/parser_tokens.ml
Ocamlc src/core/keywords.ml
Ocamlc src/core/task.ml
Ocamlc src/core/pretty.ml
Ocamlc src/core/dterm.ml
Ocamlc src/core/env.ml
Ocamlc src/core/trans.ml
Ocamlc src/core/printer.ml
Ocamlc src/core/model_parser.ml
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/driver/prove_client.ml
Ocamlc src/driver/call_provers.ml
Ocamlc src/driver/driver_parser.ml
Ocamlc src/driver/driver_lexer.ml
Ocamlc src/driver/driver.ml
Ocamlc src/driver/whyconf.ml
Ocamlc src/driver/autodetection.ml
Ocamlc src/driver/smtv2_model_defs.ml
Ocamlc src/driver/collect_data_model.ml
Ocamlc src/driver/sexp.ml
Ocamlc src/driver/smtv2_model_parser.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/mlw/pmodule.ml
Ocamlc src/mlw/dexpr.ml
Ocamlc src/mlw/big_real.ml
Ocamlc src/mlw/pinterp_core.ml
Ocamlc src/mlw/rac.ml
Ocamlc src/mlw/pinterp.ml
Ocamlc src/mlw/check_ce.ml
Ocamlc src/extract/mltree.ml
Ocamlc src/extract/compile.ml
Ocamlc src/extract/mlinterp.ml
Ocamlc src/extract/pdriver.ml
Ocamlc src/extract/ml_printer.ml
Ocamlc 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.)
Ocamlc src/extract/ocaml.ml
Ocamlc src/extract/cakeml.ml
Ocamlc src/parser/ptree_helpers.ml
Ocamlc src/parser/glob.ml
Ocamlc src/parser/typing.ml
Ocamlc src/parser/parser_messages.ml
Ocamlc src/parser/parser.ml
Ocamlc src/parser/report.ml
Ocamlc src/parser/lexer.ml
Ocamlc src/parser/mlw_printer.ml
Ocamlc src/transform/simplify_formula.ml
Ocamlc src/transform/inlining.ml
Ocamlc src/transform/split_goal.ml
Ocamlc src/transform/args_wrapper.ml
Ocamlc src/transform/detect_polymorphism.ml
Ocamlc src/transform/reduction_engine.ml
Ocamlc src/transform/compute.ml
Ocamlc src/transform/eliminate_definition.ml
Ocamlc src/transform/eliminate_algebraic.ml
Ocamlc src/transform/abstract_quantifiers.ml
Ocamlc src/transform/eliminate_unknown_types.ml
Ocamlc src/transform/eliminate_unknown_lsymbols.ml
Ocamlc src/transform/eliminate_symbol.ml
Ocamlc src/transform/eliminate_inductive.ml
Ocamlc src/transform/eliminate_let.ml
Ocamlc src/transform/eliminate_if.ml
Ocamlc src/transform/libencoding.ml
Ocamlc src/transform/discriminate.ml
Ocamlc src/transform/encoding.ml
Ocamlc src/transform/encoding_select.ml
Ocamlc src/transform/encoding_guards_full.ml
Ocamlc src/transform/encoding_tags_full.ml
Ocamlc src/transform/encoding_guards.ml
Ocamlc src/transform/encoding_tags.ml
Ocamlc src/transform/encoding_twin.ml
Ocamlc src/transform/encoding_sort.ml
Ocamlc src/transform/simplify_array.ml
Ocamlc src/transform/filter_trigger.ml
Ocamlc src/transform/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/prepare_for_counterexmp.ml
Ocamlc src/transform/induction.ml
Ocamlc src/transform/induction_pr.ml
Ocamlc src/transform/reflection.ml
Ocamlc src/printer/cntexmp_printer.ml
Ocamlc src/printer/alt_ergo.ml
Ocamlc src/printer/why3printer.ml
Ocamlc src/printer/smtv1.ml
Ocamlc src/printer/smtv2.ml
Ocamlc src/printer/coq.ml
Ocamlc src/printer/pvs.ml
Ocamlc src/printer/isabelle.ml
Ocamlc src/printer/simplify.ml
Ocamlc src/printer/gappa.ml
Ocamlc src/printer/cvc3.ml
Ocamlc src/printer/yices.ml
Ocamlc src/printer/mathematica.ml
Ocamlc src/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/xml.ml
Ocamlc src/session/termcode.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/session_itp.ml
Ocamlc src/session/strategy.ml
Ocamlc src/session/strategy_parser.ml
Ocamlc src/session/controller_itp.ml
Ocamlc src/session/server_utils.ml
Ocamlc src/session/itp_communication.ml
Ocamlc src/session/itp_server.ml
Ocamlc src/session/json_util.ml
Ocamlc src/session/unix_scheduler.ml
Linking lib/why3/why3.cmo
Linking lib/why3/why3.cmx
Ocamlc plugins/parser/genequlin.mli
Ocamlopt plugins/parser/genequlin.ml
Linking lib/plugins/genequlin.cmxs
Ocamlc plugins/parser/dimacs.mli
Ocamlopt plugins/parser/dimacs.ml
Linking lib/plugins/dimacs.cmxs
Ocamlc plugins/tptp/tptp_ast.mli
Ocamlc plugins/tptp/tptp_parser.mli
Ocamlopt plugins/tptp/tptp_parser.ml
Ocamlc plugins/tptp/tptp_typing.mli
Ocamlopt plugins/tptp/tptp_typing.ml
Ocamlc plugins/tptp/tptp_lexer.mli
Ocamlopt plugins/tptp/tptp_lexer.ml
Ocamlc plugins/tptp/tptp_printer.mli
Ocamlopt plugins/tptp/tptp_printer.ml
Linking lib/plugins/tptp.cmxs
Ocamlc plugins/python/py_ast.mli
Ocamlc plugins/python/py_parser.mli
Ocamlopt plugins/python/py_parser.ml
Ocamlc plugins/python/py_lexer.mli
Ocamlopt plugins/python/py_lexer.ml
Ocamlc plugins/python/py_main.mli
Ocamlopt plugins/python/py_main.ml
Linking lib/plugins/python.cmxs
Ocamlc plugins/microc/mc_ast.mli
Ocamlc plugins/microc/mc_parser.mli
Ocamlopt plugins/microc/mc_parser.ml
Ocamlc plugins/microc/mc_lexer.mli
Ocamlopt plugins/microc/mc_lexer.ml
Ocamlc plugins/microc/mc_printer.mli
Ocamlopt plugins/microc/mc_printer.ml
Ocamlc plugins/microc/mc_main.mli
Ocamlopt plugins/microc/mc_main.ml
Linking lib/plugins/microc.cmxs
Ocamlc plugins/cfg/cfg_ast.mli
Ocamlc plugins/cfg/cfg_parser.mli
Ocamlopt plugins/cfg/cfg_parser.ml
Ocamlc plugins/cfg/cfg_lexer.mli
Ocamlopt plugins/cfg/cfg_lexer.ml
Ocamlc plugins/cfg/cfg_paths.mli
Ocamlopt plugins/cfg/cfg_paths.ml
Ocamlc plugins/cfg/cfg_main.mli
Ocamlopt plugins/cfg/cfg_main.ml
Linking lib/plugins/cfg.cmxs
Linking lib/why3/why3.cmxa
Linking lib/why3/why3.cmxs
Ocamlc src/tools/main.mli
Ocamlopt src/tools/main.ml
Linking bin/why3.opt
Ocamlc src/tools/why3config.mli
Ocamlopt src/tools/why3config.ml
Linking bin/why3config.cmxs
Ocamlc src/tools/why3execute.mli
Ocamlopt src/tools/why3execute.ml
Linking bin/why3execute.cmxs
Ocamlc src/tools/why3extract.mli
Ocamlopt src/tools/why3extract.ml
Linking bin/why3extract.cmxs
Ocamlc src/tools/why3prove.mli
Ocamlopt src/tools/why3prove.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.
Linking bin/why3prove.cmxs
Ocamlc src/tools/why3realize.mli
Ocamlopt src/tools/why3realize.ml
Linking bin/why3realize.cmxs
Ocamlc src/tools/why3replay.mli
Ocamlopt src/tools/why3replay.ml
Linking bin/why3replay.cmxs
Ocamlc src/tools/why3show.mli
Ocamlopt src/tools/why3show.ml
Linking bin/why3show.cmxs
Ocamlc src/tools/why3wc.mli
Ocamlopt src/tools/why3wc.ml
Linking bin/why3wc.cmxs
Ocamlc src/ide/wserver.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.
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.
Ocamlc src/ide/why3web.mli
Ocamlopt src/ide/why3web.ml
Linking bin/why3webserver.cmxs
Ocamlc src/why3session/why3session_lib.mli
Ocamlopt src/why3session/why3session_lib.ml
Ocamlc src/why3session/why3session_info.mli
Ocamlopt src/why3session/why3session_info.ml
Ocamlc src/why3session/why3session_html.mli
Ocamlopt src/why3session/why3session_html.ml
Ocamlc src/why3session/why3session_latex.mli
Ocamlopt src/why3session/why3session_latex.ml
Ocamlc src/why3session/why3session_update.mli
Ocamlopt src/why3session/why3session_update.ml
Ocamlc src/why3session/why3session_main.mli
Ocamlopt src/why3session/why3session_main.ml
Linking bin/why3session.cmxs
Ocamlc src/tools/why3shell.mli
Ocamlopt src/tools/why3shell.ml
Linking bin/why3shell.cmxs
Ocamlc src/isabelle-client/isabelle_client_main.mli
Ocamlopt src/isabelle-client/isabelle_client_main.ml
Linking bin/isabelle_client.opt
Ocamlc src/tools/why3pp_sexp.mli
Ocamlopt src/tools/why3pp_sexp.ml
Ocamlc src/tools/why3pp.mli
Ocamlopt src/tools/why3pp.ml
Linking bin/why3pp.cmxs
Ocamlc src/why3doc/doc_html.mli
Ocamlopt src/why3doc/doc_html.ml
Ocamlc src/why3doc/doc_def.mli
Ocamlopt src/why3doc/doc_def.ml
Ocamlc src/why3doc/doc_lexer.mli
Ocamlopt src/why3doc/doc_lexer.ml
Ocamlc src/why3doc/doc_main.mli
Ocamlopt src/why3doc/doc_main.ml
Linking bin/why3doc.cmxs
gcc -Wall -O -g -o src/server/logging.o -c src/server/logging.c
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 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
Undefined first referenced
symbol in file
bind src/server/server-unix.o
accept src/server/server-unix.o
listen src/server/server-unix.o
socket src/server/server-unix.o
ld: fatal: symbol referencing errors. No output written to lib/why3server
collect2: error: ld returned 1 exit status
gmake: *** [Makefile:746: lib/why3server] Error 1
*** Error code 2
Stop.
bmake[1]: stopped in /data/jenkins/workspace/pkgsrc-trunk-x86_64/devel/why3
*** Error code 1
Stop.
bmake: stopped in /data/jenkins/workspace/pkgsrc-trunk-x86_64/devel/why3