* Package: sci-mathematics/why3-1.6.0:0/1.6.0 * Repository: gentoo * Maintainer: fx.carton91@gmail.com ml@gentoo.org,sci-mathematics@gentoo.org * USE: abi_x86_64 amd64 elibc_glibc kernel_linux re sexp userland_GNU zarith zip * FEATURES: network-sandbox preserve-libs sandbox userpriv usersandbox >>> Unpacking source... >>> Unpacking why3-1.6.0.tar.gz to /var/tmp/portage/sci-mathematics/why3-1.6.0/work >>> Source unpacked in /var/tmp/portage/sci-mathematics/why3-1.6.0/work >>> Preparing source in /var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0 ... * Running eautoreconf in '/var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0' ... * Running 'aclocal --system-acdir=/var/tmp/portage/sci-mathematics/why3-1.6.0/temp/aclocal' ... [ ok ] * Running 'autoconf --force' ... [ ok ] * Running elibtoolize in: why3-1.6.0/ >>> Source prepared. >>> Configuring source in /var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0 ... * econf: updating why3-1.6.0/config.sub with /usr/share/gnuconfig/config.sub * econf: updating why3-1.6.0/config.guess with /usr/share/gnuconfig/config.guess ./configure --prefix=/usr --build=x86_64-pc-linux-gnu --host=x86_64-pc-linux-gnu --mandir=/usr/share/man --infodir=/usr/share/info --datadir=/usr/share --sysconfdir=/etc --localstatedir=/var/lib --datarootdir=/usr/share --docdir=/usr/share/doc/why3-1.6.0 --htmldir=/usr/share/doc/why3-1.6.0/html --libdir=/usr/lib64 --disable-frama-c --disable-hypothesis-selection --disable-infer --disable-isabelle-libs --disable-pvs-libs --disable-web-ide --disable-coq-libs --disable-doc --disable-emacs-compilation --disable-ide --disable-native-code --enable-re --enable-pp-sexp --disable-stackify --enable-zarith --enable-zip checking executable suffix... checking for x86_64-pc-linux-gnu-gcc... x86_64-pc-linux-gnu-gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether the compiler supports GNU C... yes checking whether x86_64-pc-linux-gnu-gcc accepts -g... yes checking for x86_64-pc-linux-gnu-gcc option to enable C11 features... none needed checking for a race-free mkdir -p... /usr/bin/mkdir -p checking for a BSD-compatible install... /usr/lib/portage/python3.11/ebuild-helpers/xattr/install -c checking for ocamlc... ocamlc configure: ocaml version is 4.14.1 configure: ocaml library path is /usr/lib64/ocaml checking for ocamlopt... no configure: WARNING: cannot find ocamlopt; bytecode compilation only. checking for ocamlc.opt... no checking for ocamldep... ocamldep checking for ocamldep.opt... no checking for ocamllex... ocamllex checking for ocamllex.opt... no checking for ocamlyacc... ocamlyacc checking for ocamldoc... ocamldoc checking for ocamldoc.opt... no checking for menhir... menhir checking for ocamlfind... ocamlfind checking for compiler-libs using ocamlfind... yes checking for num using ocamlfind... yes checking for /usr/lib64/ocaml/num/nums.cma... no checking for /usr/lib64/ocaml/num/num.cmi... no checking for /usr/lib64/ocaml/nums.cma... yes checking for /usr/lib64/ocaml/num.cmi... yes checking for zarith using ocamlfind... yes checking for /usr/lib64/ocaml/zarith/z.cmi... yes checking for camlzip using ocamlfind... yes checking for /usr/lib64/ocaml/zip/zip.cmi... yes checking for menhirLib using ocamlfind... yes checking for /usr/lib64/ocaml/menhirLib/menhirLib.cmi... yes checking for re using ocamlfind... yes checking for /usr/lib64/ocaml/re/re.cmi... yes checking for mlmpfr... no checking for js_of_ocaml... no checking for ppx_sexp_conv using ocamlfind... yes checking for sexplib using ocamlfind... yes checking for ppx_deriving using ocamlfind... yes configure: creating ./config.status config.status: creating Makefile config.status: creating src/config.sh config.status: creating lib/why3/META config.status: creating .merlin config.status: creating src/jessie/Makefile config.status: creating src/jessie/.merlin config.status: creating lib/coq/version config.status: creating lib/pvs/version config.status: executing chmod commands Summary ----------------------------------------- Verbose make : no OCaml compiler : yes Version : 4.14.1 Library path : /usr/lib64/ocaml Ocamlfind : yes Native compilation : no Memory profiling : no (disabled by default) PPX : yes S-expr for why3pp : yes Javascript support : no (js_of_ocaml not found) MPFR support : no (mlmpfr not found) Re support : yes Components Why3 library : yes GTK IDE : no (disabled by user) Web IDE : no (disabled by user) GMP arithmetic : yes Compressed sessions : yes Hypothesis selection : no (disabled by user) Stackify : no (disabled by user) Invariant inference(exp): no (disabled by default) Inference with BDDs(exp): no (disabled by default) Frama-C support : no Documentation : no Support for interactive proof assistants Coq : no (disabled by user) PVS : no (disabled by user) Isabelle : no (disabled by user) Installable : yes Binary path : ${exec_prefix}/bin Library path : /usr/lib64/why3 Data path : /usr/share/why3 OCaml library path : /usr/lib64/ocaml/why3 Relocatable : no >>> Source configured. >>> Compiling source in /var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0 ... make -j4 cmp -s src/util/mysexplib-real.ml src/util/mysexplib.ml || cp src/util/mysexplib-real.ml src/util/mysexplib.ml Generate src/util/config.ml Ocamllex src/util/rc.mll Ocamllex src/util/lexlib.mll Menhir src/util/json_parser.mly 39 states, 600 transitions, table size 2634 bytes 1338 additional bytes used for bindings Ocamllex src/util/json_lexer.mll cmp -s src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml || cp src/util/mlmpfr_dummy.ml src/util/mlmpfr_wrapper.ml Ocamllex src/parser/lexer.mll 48 states, 1889 transitions, table size 7844 bytes 3073 additional bytes used for bindings 52 states, 495 transitions, table size 2292 bytes Menhir src/parser/parser_common.mly Menhir src/parser/parser_common.mly src/parser/parser.mly Menhir src/driver/driver_parser.mly 174 states, 4831 transitions, table size 20368 bytes 9859 additional bytes used for bindings 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_z.ml src/session/compress.ml || cp src/session/compress_z.ml src/session/compress.ml Ocamllex src/session/xml.mll Ocamllex src/session/strategy_parser.mll 53 states, 796 transitions, table size 3502 bytes 2509 additional bytes used for bindings 117 states, 1396 transitions, table size 6286 bytes 3556 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/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 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/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 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 Ocamldep src/why3session/why3session_main.ml Ocamldep src/tools/why3shell.ml Ocamldep src/isabelle-client/isabelle_client_main.ml cmp -s src/tools/why3pp_sexp-real.ml src/tools/why3pp_sexp.ml || cp src/tools/why3pp_sexp-real.ml src/tools/why3pp_sexp.ml Ocamllex src/why3doc/doc_lexer.mll 120 states, 685 transitions, table size 3460 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/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 Read 3 sample input sentences and 3 error messages. Ocamldep src/tools/why3pp_sexp.ml Ocamldep src/tools/why3pp.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 Ocamldep src/util/mysexplib.ml Ocamldep src/util/config.ml Ocamldep src/util/bigInt.ml Ocamldep src/util/mlmpfr_wrapper.ml Ocamldep src/util/util.ml Ocamldep src/util/opt.ml Ocamldep src/util/lists.ml Ocamldep src/util/strings.ml Ocamldep src/util/pp.ml Ocamldep src/util/extmap.ml Ocamldep src/util/extset.ml Ocamldep src/util/exthtbl.ml Ocamldep src/util/weakhtbl.ml Ocamldep src/util/diffmap.ml Ocamldep src/util/hashcons.ml Ocamldep src/util/wstdlib.ml Ocamldep src/util/exn_printer.ml Ocamldep src/util/getopt.ml Ocamldep src/util/json_base.ml Ocamldep src/util/json_parser.ml Ocamldep src/util/json_lexer.ml Ocamldep src/util/debug.ml Ocamldep src/util/loc.ml Ocamldep src/util/lexlib.ml Ocamldep src/util/print_tree.ml Ocamldep src/util/cmdline.ml Ocamldep src/util/sysutil.ml Ocamldep src/util/rc.ml Ocamldep src/util/plugin.ml Ocamldep src/util/number.ml Ocamldep src/util/vector.ml Ocamldep src/util/constant.ml Ocamldep src/util/pqueue.ml Ocamldep src/core/ident.ml Ocamldep src/core/ty.ml Ocamldep src/core/term.ml Ocamldep src/core/pattern.ml Ocamldep src/core/coercion.ml Ocamldep src/core/decl.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/parser/ptree.ml Ocamldep src/parser/ptree_helpers.ml Ocamldep src/parser/glob.ml Ocamldep src/parser/typing.ml Ocamldep src/parser/parser_messages.ml Ocamldep src/parser/parser.ml Ocamldep src/parser/report.ml Ocamldep src/parser/lexer.ml Ocamldep src/parser/mlw_printer.ml Ocamldep src/transform/simplify_formula.ml Ocamldep src/transform/inlining.ml Ocamldep src/transform/split_goal.ml Ocamldep src/transform/args_wrapper.ml Ocamldep src/transform/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/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/abstraction.ml Ocamldep src/transform/close_epsilon.ml Ocamldep src/transform/lift_epsilon.ml Ocamldep src/transform/eliminate_epsilon.ml Ocamldep src/transform/intro_projections_counterexmp.ml Ocamldep src/transform/instantiate_predicate.ml Ocamldep src/transform/smoke_detector.ml Ocamldep src/transform/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/intro_vc_vars_counterexmp.ml Ocamldep src/transform/prepare_for_counterexmp.ml Ocamldep src/transform/induction.ml Ocamldep src/transform/induction_pr.ml Ocamldep src/transform/reflection.ml Ocamldep src/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/tptp/tptp_parser.ml Ocamldep plugins/tptp/tptp_typing.ml Ocamldep plugins/tptp/tptp_lexer.ml Ocamldep plugins/tptp/tptp_printer.ml Ocamldep plugins/python/py_parser.ml Ocamldep plugins/python/py_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/tptp/tptp_ast.mli Ocamldep plugins/python/py_ast.mli Ocamldep plugins/microc/mc_ast.mli Ocamldep plugins/cfg/cfg_ast.mli mkdir lib/plugins Ocamlc src/util/mysexplib.ml Ocamlc src/util/config.mli Ocamlc src/util/bigInt.mli Ocamlc src/util/mlmpfr_wrapper.mli File "_none_", line 1: Error: Cannot load ppx_sexp_conv: this object file uses unsafe features File "_none_", line 1: Error: Cannot load ppx_sexp_conv: this object file uses unsafe features make: *** [Makefile:2052: src/util/mysexplib.cmo] Error 2 make: *** Waiting for unfinished jobs.... make: *** [Makefile:2038: src/util/mlmpfr_wrapper.cmi] Error 2 File "_none_", line 1: Error: Cannot load ppx_sexp_conv: this object file uses unsafe features make: *** [Makefile:2038: src/util/bigInt.cmi] Error 2 File "_none_", line 1: Error: Cannot load ppx_sexp_conv: this object file uses unsafe features make: *** [Makefile:2038: src/util/config.cmi] Error 2 * ERROR: sci-mathematics/why3-1.6.0::gentoo failed (compile phase): * emake failed * * If you need support, post the output of `emerge --info '=sci-mathematics/why3-1.6.0::gentoo'`, * the complete build log and the output of `emerge -pqv '=sci-mathematics/why3-1.6.0::gentoo'`. * The complete build log is located at '/var/log/portage/sci-mathematics:why3-1.6.0:20230512-205316.log'. * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/why3-1.6.0/temp/build.log'. * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/why3-1.6.0/temp/environment'. * Working directory: '/var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0' * S: '/var/tmp/portage/sci-mathematics/why3-1.6.0/work/why3-1.6.0'