+ case "${usergroup_phase}" in + local run_cmd + run_cmd=run_su + shift + run_su /opt/pkg/bin/bmake all BATCH=1 DEPENDS_TARGET=/nonexistent WRKLOG=/tmp/bulklog/why3-1.8.0nb2/work.log + su pbulk -c '"$@"' make /opt/pkg/bin/bmake all BATCH=1 DEPENDS_TARGET=/nonexistent WRKLOG=/tmp/bulklog/why3-1.8.0nb2/work.log ===> Building for why3-1.8.0nb2 Ocamllex src/util/rc.mll Ocamllex src/util/lexlib.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Generate src/util/config.ml 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings Menhir src/util/json_parser.mly Ocamllex src/util/json_lexer.mll 52 states, 495 transitions, table size 2292 bytes Ocamllex src/parser/lexer.mll Menhir src/parser/parser_common.mly src/parser/parser.mly Menhir src/parser/parser_common.mly 174 states, 4831 transitions, table size 20368 bytes 9859 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 33 states, 370 transitions, table size 1678 bytes Ocamllex src/session/xml.mll 117 states, 1396 transitions, table size 6286 bytes 3556 additional bytes used for bindings Ocamllex src/session/strategy_parser.mll cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml 59 states, 799 transitions, table size 3550 bytes 2611 additional bytes used for bindings 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 Read 3 sample input sentences and 3 error messages. Ocamllex plugins/coma/coma_lexer.mll 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 Menhir src/parser/parser_common.mly plugins/coma/coma_parser.mly 251 states, 6731 transitions, table size 28430 bytes 16559 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 Ocamllex plugins/cfg/cfg_lexer.mll Read 3 sample input sentences and 3 error messages. Menhir src/parser/parser_common.mly plugins/cfg/cfg_parser.mly 173 states, 4796 transitions, table size 20222 bytes 9853 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/gconfig.ml Ocamldep src/ide/ide_utils.ml Ocamldep src/ide/why3ide.ml Ocamldep src/ide/wserver.ml Ocamldep src/ide/why3web.ml 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_output.ml Ocamldep src/why3session/why3session_create.ml Ocamldep src/why3session/why3session_main.ml Ocamldep src/tools/why3shell.ml Coqdep lib/coq/BuiltIn.v Coqdep lib/coq/HighOrd.v Coqdep lib/coq/WellFounded.v Coqdep lib/coq/int/Exponentiation.v Coqdep lib/coq/int/Abs.v Coqdep lib/coq/int/ComputerDivision.v Coqdep lib/coq/int/Div2.v Coqdep lib/coq/int/EuclideanDivision.v Coqdep lib/coq/int/Int.v Coqdep lib/coq/int/MinMax.v Coqdep lib/coq/int/Power.v Coqdep lib/coq/int/NumOf.v Coqdep lib/coq/bool/Bool.v Coqdep lib/coq/real/Abs.v Coqdep lib/coq/real/ExpLog.v Coqdep lib/coq/real/FromInt.v Coqdep lib/coq/real/MinMax.v Coqdep lib/coq/real/PowerInt.v Coqdep lib/coq/real/PowerReal.v Coqdep lib/coq/real/Real.v Coqdep lib/coq/real/RealInfix.v Coqdep lib/coq/real/Square.v Coqdep lib/coq/real/Trigonometry.v Coqdep lib/coq/number/Divisibility.v Coqdep lib/coq/number/Gcd.v Coqdep lib/coq/number/Parity.v Coqdep lib/coq/number/Prime.v Coqdep lib/coq/number/Coprime.v Coqdep lib/coq/set/Set.v Coqdep lib/coq/set/Cardinal.v Coqdep lib/coq/set/Fset.v Coqdep lib/coq/set/FsetInduction.v Coqdep lib/coq/set/FsetInt.v Coqdep lib/coq/set/FsetSum.v Coqdep lib/coq/set/SetApp.v Coqdep lib/coq/set/SetAppInt.v Coqdep lib/coq/set/SetImp.v Coqdep lib/coq/set/SetImpInt.v Coqdep lib/coq/map/Map.v Coqdep lib/coq/map/Const.v Coqdep lib/coq/map/MapExt.v Coqdep lib/coq/map/Occ.v Coqdep lib/coq/map/MapInjection.v Coqdep lib/coq/map/MapPermut.v Coqdep lib/coq/list/List.v Coqdep lib/coq/list/Length.v Coqdep lib/coq/list/Mem.v Coqdep lib/coq/list/Nth.v Coqdep lib/coq/list/NthLength.v Coqdep lib/coq/list/HdTl.v Coqdep lib/coq/list/NthHdTl.v Coqdep lib/coq/list/Append.v Coqdep lib/coq/list/NthLengthAppend.v Coqdep lib/coq/list/Reverse.v Coqdep lib/coq/list/HdTlNoOpt.v Coqdep lib/coq/list/NthNoOpt.v Coqdep lib/coq/list/RevAppend.v Coqdep lib/coq/list/Combine.v Coqdep lib/coq/list/Distinct.v Coqdep lib/coq/list/NumOcc.v Coqdep lib/coq/list/Permut.v Coqdep lib/coq/option/Option.v Coqdep lib/coq/bv/Pow2int.v Coqdep lib/coq/bv/BV_Gen.v Coqdep lib/coq/for_drivers/ComputerOfEuclideanDivision.v Ocamldep src/isabelle-client/isabelle_client_main.ml Ocamldep src/tools/why3pp.ml Ocamllex src/why3doc/doc_lexer.mll 120 states, 706 transitions, table size 3544 bytes 1763 additional bytes used for bindings cp src/util/json_base.ml src/trywhy3/json_base.ml 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 Ocamldep src/util/exn_printer.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/hcpt.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_base.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/debug.ml Ocamldep src/util/loc.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/rc.ml Ocamldep src/util/plugin.ml Ocamldep src/util/constant.ml Ocamldep src/util/vector.ml Ocamldep src/util/number.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/whyconf.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/autodetection.ml Ocamldep src/driver/smtv2_model_defs.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/extract/java.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/parser/ptree.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/parser/sexp_parser.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/reduction_engine.ml Ocamldep src/transform/compute.ml Ocamldep src/transform/remove_unused.ml Ocamldep src/transform/detect_polymorphism.ml Ocamldep src/transform/eliminate_definition.ml Ocamldep src/transform/extensional.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_let.ml Ocamldep src/transform/eliminate_inductive.ml Ocamldep src/transform/eliminate_if.ml Ocamldep src/transform/libencoding.ml Ocamldep src/transform/eliminate_algebraic.ml Ocamldep src/transform/discriminate.ml Ocamldep src/transform/encoding.ml Ocamldep src/transform/encoding_select.ml Ocamldep src/transform/encoding_guards_full.ml Ocamldep src/transform/encoding_tags_full.ml Ocamldep src/transform/encoding_guards.ml Ocamldep src/transform/encoding_tags.ml Ocamldep src/transform/encoding_twin.ml Ocamldep src/transform/encoding_sort.ml Ocamldep src/transform/simplify_array.ml Ocamldep src/transform/filter_trigger.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/smoke_detector.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/congruence.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/reflection.ml Ocamldep src/transform/keep_only_arithmetic.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/pvs.ml Ocamldep src/printer/coq.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/mathematica.ml Ocamldep src/session/compress.ml Ocamldep src/session/xml.ml Ocamldep src/session/termcode.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/strategy.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/json_util.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/parser/genequlin.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/transform/hypothesis_selection.ml Ocamldep plugins/strategies/forward_propagation.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/coma/coma_logic.ml Ocamldep plugins/coma/coma_syntax.ml Ocamldep plugins/coma/coma_parser.ml Ocamldep plugins/coma/coma_lexer.ml Ocamldep plugins/coma/coma_typing.ml Ocamldep plugins/coma/coma_main.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/python/py_lexer.ml Ocamldep plugins/python/py_main.ml Ocamldep plugins/microc/mc_parser.ml Ocamldep plugins/microc/mc_lexer.ml Ocamldep plugins/microc/mc_printer.ml Ocamldep plugins/microc/mc_main.ml Ocamldep plugins/cfg/cfg_parser.ml Ocamldep plugins/cfg/cfg_lexer.ml Ocamldep plugins/cfg/cfg_paths.ml Ocamldep plugins/cfg/subregion_analysis.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 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/why3bench.ml Ocamldep src/why3doc/doc_html.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 mkdir lib/plugins Ocamlc src/util/exn_printer.mli Ocamlc src/util/config.mli Ocamlc src/util/bigInt.mli Ocamlc src/util/mlmpfr_wrapper.mli Ocamlc src/util/util.mli Ocamlc src/util/opt.mli Ocamlc src/util/lists.mli Ocamlc src/util/strings.mli Ocamlc src/util/pp.mli Ocamlc src/util/extmap.mli Ocamlc src/util/exthtbl.mli Ocamlc src/util/weakhtbl.mli Ocamlc src/util/hcpt.mli Ocamlc src/util/json_base.mli Ocamlc src/util/getopt.mli Ocamlc src/util/print_tree.mli Ocamlc src/util/hashcons.mli Ocamlc src/util/cmdline.mli Ocamlc src/util/sysutil.mli Ocamlc src/util/lexlib.mli Ocamlc src/util/number.mli Ocamlc src/util/vector.mli Ocamlc src/util/pqueue.mli Ocamlc src/util/re.ml Ocamlc src/driver/prove_client.mli Ocamlc src/driver/smtv2_model_defs.mli File "src/util/re.ml", line 1: Warning 70 [missing-mli]: Cannot find interface file. Ocamlc src/driver/sexp.mli Ocamlc src/driver/smtv2_model_parser.mli Ocamlc src/mlw/big_real.mli Linking src/util/ppx_debug_optim findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /opt/pkg/lib/ocaml, /opt/pkg/lib/ocaml/compiler-libs Ocamlc src/extract/c.mli Ocamlc src/extract/ocaml.mli Ocamlc src/extract/cakeml.mli Ocamlc src/extract/java.mli Ocamlc src/parser/parser_messages.mli Ocamlc src/transform/remove_unused.mli Ocamlc src/transform/abstract_quantifiers.mli Ocamlc src/transform/extensional.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/transform/prepare_for_counterexmp.mli Ocamlc src/transform/keep_only_arithmetic.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/isabelle.mli Ocamlc src/printer/pvs.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/exn_printer.ml Ocamlc src/util/config.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/hcpt.ml Ocamlc src/util/hashcons.ml Ocamlc src/util/getopt.ml Ocamlc src/util/json_base.ml Ocamlc src/util/print_tree.ml Ocamlc src/util/cmdline.ml Ocamlc src/util/sysutil.ml Ocamlc src/util/vector.ml Ocamlc src/util/pqueue.ml File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/driver/prove_client.ml Ocamlc src/driver/smtv2_model_defs.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 Ocamlc plugins/parser/dimacs.mli Ocamlc plugins/tptp/tptp_printer.mli Ocamlc plugins/python/py_main.mli Ocamlc plugins/microc/mc_main.mli Ocamlc plugins/coma/coma_main.mli Ocamlc plugins/cfg/cfg_stackify.mli Ocamlc plugins/strategies/forward_propagation.mli Ocamlc plugins/transform/hypothesis_selection.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/tools/why3bench.mli Ocamlc src/ide/ide_utils.mli Ocamlc src/ide/why3ide.mli Ocamlc src/ide/wserver.mli Ocamlc src/ide/why3web.mli Ocamlc src/why3session/why3session_main.mli Ocamlc src/tools/why3shell.mli Ocamlc src/isabelle-client/isabelle_client_main.mli Ocamlc src/tools/why3pp.mli Ocamlc src/why3doc/doc_html.mli Ocamlc src/why3doc/doc_lexer.mli Ocamlc src/why3doc/doc_main.mli 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 -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 Coqc lib/coq/BuiltIn.v Generate drivers/coq-realizations.aux Generate drivers/pvs-realizations.aux Generate drivers/isabelle-realizations.aux Ocamlopt src/util/exn_printer.ml Ocamlc 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/hcpt.ml Ocamlopt src/util/hashcons.ml Ocamlc src/util/wstdlib.mli Ocamlopt src/util/getopt.ml Ocamlopt src/util/json_base.ml Ocamlc src/util/json_parser.mli Ocamlc src/util/debug.mli Ocamlc src/util/loc.mli Ocamlopt src/util/print_tree.ml Ocamlopt src/util/cmdline.ml Ocamlopt src/util/sysutil.ml Ocamlc src/util/rc.mli Ocamlc src/util/plugin.mli Ocamlc src/util/constant.mli Ocamlopt src/util/vector.ml Ocamlopt src/util/re.ml Ocamlc src/core/ident.mli File "src/util/vector.ml", line 22, characters 22-30: 22 | let create ?capacity:(capacity: (int) option) ~dummy:(dummy: 'a) : 'a t = ^^^^^^^^ Warning 16 [unerasable-optional-argument]: this optional argument cannot be erased. Ocamlc src/core/parser_tokens.mli Ocamlopt src/driver/prove_client.ml Ocamlc src/driver/driver_ast.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 Ocamlc src/util/extset.ml Ocamlc src/util/bigInt.ml Ocamlc src/util/diffmap.ml Ocamlc src/util/wstdlib.ml Ocamlc src/util/json_parser.ml Ocamlc src/util/debug.ml Ocamlc src/util/loc.ml Ocamlc src/util/lexlib.ml Ocamlc src/util/rc.ml Ocamlc src/util/plugin.ml Ocamlc src/util/number.ml Ocamlc src/util/constant.ml Ocamlc src/core/ident.ml Ocamlc src/core/parser_tokens.ml Ocamlc src/parser/glob.ml Ocamlc src/session/xml.ml Ocamlopt src/ide/ide_utils.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 gcc -Wall -o lib/why3cpulimit src/server/cpulimit-unix.o src/server/cpulimit-win.o Coqc lib/coq/HighOrd.v 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 Coqc lib/coq/WellFounded.v collect2: error: ld returned 1 exit status gmake: *** [Makefile:799: lib/why3server] Error 1 gmake: *** Waiting for unfinished jobs.... *** Error code 2 Stop. bmake[1]: stopped making "all" in /data/jenkins/workspace/pkgsrc-upstream-trunk/devel/why3 *** Error code 1 Stop. bmake: stopped making "all" in /data/jenkins/workspace/pkgsrc-upstream-trunk/devel/why3