+ 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.0nb1/work.log + su pbulk -c '"$@"' make /opt/pkg/bin/bmake all BATCH=1 DEPENDS_TARGET=/nonexistent WRKLOG=/tmp/bulklog/why3-1.8.0nb1/work.log ===> Building for why3-1.8.0nb1 Generate src/util/config.ml Ocamllex src/util/rc.mll Ocamllex src/util/lexlib.mll 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings Menhir src/util/json_parser.mly Ocamllex src/util/json_lexer.mll Ocamllex src/parser/lexer.mll 52 states, 495 transitions, table size 2292 bytes Menhir src/parser/parser_common.mly Menhir src/parser/parser_common.mly src/parser/parser.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 Ocamllex plugins/coma/coma_lexer.mll Read 3 sample input sentences and 3 error messages. 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 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/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. Ocamllex plugins/cfg/cfg_lexer.mll 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/HighOrd.v Coqdep lib/coq/BuiltIn.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/MapPermut.v Coqdep lib/coq/map/MapInjection.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/NthHdTl.v Coqdep lib/coq/list/HdTl.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/number.ml Ocamldep src/util/pqueue.ml Ocamldep src/util/vector.ml Ocamldep src/util/constant.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/model_parser.ml Ocamldep src/driver/whyconf.ml Ocamldep src/driver/prove_client.ml Ocamldep src/core/printer.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/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/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_inductive.ml Ocamldep src/transform/eliminate_let.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/lift_epsilon.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/abstraction.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/prop_curry.ml Ocamldep src/transform/smoke_detector.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/coq.ml Ocamldep src/printer/pvs.ml Ocamldep src/printer/isabelle.ml Ocamldep src/printer/simplify.ml Ocamldep src/printer/gappa.ml Ocamldep src/printer/cvc3.ml Ocamldep src/printer/yices.ml Ocamldep src/printer/mathematica.ml Ocamldep src/session/compress.ml Ocamldep src/session/xml.ml Ocamldep src/session/termcode.ml Ocamldep src/session/session_itp.ml Ocamldep src/session/strategy.ml Ocamldep src/session/strategy_parser.ml Ocamldep src/session/controller_itp.ml Ocamldep src/session/server_utils.ml Ocamldep src/session/itp_communication.ml Ocamldep src/session/itp_server.ml Ocamldep src/session/json_util.ml Ocamldep src/session/unix_scheduler.ml Ocamldep src/driver/driver_ast.mli Ocamldep plugins/parser/genequlin.ml Ocamldep plugins/parser/dimacs.ml Ocamldep plugins/transform/hypothesis_selection.ml Ocamldep plugins/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/why3realize.ml Ocamldep src/tools/why3prove.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/extmap.mli Ocamlc src/util/exthtbl.mli Ocamlc src/util/pp.mli Ocamlc src/util/weakhtbl.mli Ocamlc src/util/hcpt.mli Ocamlc src/util/hashcons.mli Ocamlc src/util/getopt.mli Ocamlc src/util/json_base.mli Ocamlc src/util/print_tree.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/extensional.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/case.mli Ocamlc src/transform/congruence.mli Ocamlc src/transform/prop_curry.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/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/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/hashcons.ml Ocamlc src/util/hcpt.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/why3realize.mli Ocamlc src/tools/why3prove.mli Ocamlc src/tools/why3replay.mli Ocamlc src/tools/why3show.mli Ocamlc src/tools/why3bench.mli Ocamlc src/tools/why3wc.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/re.ml Ocamlopt src/util/vector.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/bigInt.ml Ocamlc src/util/extset.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 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