sci-mathematics:why3-1.6.0:20230512-205316.log

sci-mathematics:why3-1.6.0:20230512-205316.log (text/plain), 17.80 KB, created by Toralf Förster on 2023-05-12 21:09:48 UTC

 * Package:    sci-mathematics/why3-1.6.0:0/1.6.0
 * Repository: gentoo
 * Maintainer: [e-mail] [e-mail],[e-mail]
 * 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... <none>
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'