sci-mathematics:why3-1.6.0:20240810-112458.log

sci-mathematics:why3-1.6.0:20240810-112458.log (text/plain), 20.56 KB, created by Toralf Förster on 2024-08-10 13:48:26 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 coq elibc_glibc kernel_linux ocamlopt sexp stackify 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.guess with /usr/share/gnuconfig/config.guess
 * econf: updating why3-1.6.0/config.sub with /usr/share/gnuconfig/config.sub
./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 --enable-coq-libs --disable-doc --disable-emacs-compilation --disable-ide --enable-native-code --disable-re --enable-pp-sexp --enable-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.12/ebuild-helpers/xattr/install -c
checking for ocamlc... ocamlc
configure: ocaml version is 4.14.2
configure: ocaml library path is /usr/lib64/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version... ok
checking for ocamlc.opt... ocamlc.opt
checking ocamlc.opt version... ok
checking for ocamlopt.opt... ocamlopt.opt
checking ocamlc.opt version... ok
checking for ocamldep... ocamldep
checking for ocamldep.opt... ocamldep.opt
checking for ocamllex... ocamllex
checking for ocamllex.opt... ocamllex.opt
checking for ocamlyacc... ocamlyacc
checking for ocamldoc... ocamldoc
checking for ocamldoc.opt... ocamldoc.opt
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 ocamlgraph using ocamlfind... yes
checking for /usr/lib64/ocaml/ocamlgraph/graph.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
checking for coqc... coqc
checking Coq version... 8.19.2
configure: WARNING: You need Coq 8.7 or later; Coq discarded.
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.2
    Library path            : /usr/lib64/ocaml
    Ocamlfind               : yes
    Native compilation      : yes
    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              : no (disabled by user)
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                : yes
    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 (need version >= 8.7)
    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/lexlib.mll
Ocamllex src/util/rc.mll
Menhir src/util/json_parser.mly
48 states, 1889 transitions, table size 7844 bytes
3073 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
52 states, 495 transitions, table size 2292 bytes
39 states, 600 transitions, table size 2634 bytes
1338 additional bytes used for bindings
Ocamllex src/parser/lexer.mll
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
Ocamllex src/driver/sexp.mll
34 states, 1366 transitions, table size 5668 bytes
cmp -s src/session/compress_z.ml src/session/compress.ml || cp src/session/compress_z.ml src/session/compress.ml
27 states, 306 transitions, table size 1386 bytes
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
cmp -s src/util/recompat.ml src/util/re.ml || cp src/util/recompat.ml src/util/re.ml
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
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
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
Read 3 sample input sentences and 3 error messages.
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_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
cp src/util/json_base.ml src/trywhy3/json_base.ml
cp src/util/json_base.mli src/trywhy3/json_base.mli
120 states, 685 transitions, table size 3460 bytes
1763 additional bytes used for bindings
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/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/exthtbl.ml
Ocamldep src/util/extset.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/constant.ml
Ocamldep src/util/vector.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/cakeml.ml
Ocamldep src/extract/ocaml.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/discriminate.ml
Ocamldep src/transform/eliminate_algebraic.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_tags.ml
Ocamldep src/transform/encoding_guards.ml
Ocamldep src/transform/encoding_twin.ml
Ocamldep src/transform/encoding_sort.ml
Ocamldep src/transform/filter_trigger.ml
Ocamldep src/transform/simplify_array.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/driver/driver_ast.mli
Ocamldep src/session/unix_scheduler.ml
Ocamldep plugins/parser/genequlin.ml
Ocamldep plugins/tptp/tptp_parser.ml
Ocamldep plugins/parser/dimacs.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/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/why3pp_sexp.ml
Ocamldep src/tools/why3pp.ml
Ocamldep src/why3doc/doc_def.ml
Ocamldep src/why3doc/doc_html.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/mysexplib.ml
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/exn_printer.mli
Ocamlc   src/util/hashcons.mli
Ocamlc   src/util/getopt.mli
Ocamlc   src/util/json_base.mli
Ocamlc   src/util/loc.mli
Ocamlc   src/util/lexlib.mli
Ocamlc   src/util/print_tree.mli
Ocamlc   src/util/cmdline.mli
Ocamlc   src/util/sysutil.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/driver_ast.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/smtv2_model_parser.mli
Ocamlc   src/driver/sexp.mli
Ocamlc   src/mlw/big_real.mli
Linking src/util/ppx_debug_optim
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/lib64/ocaml, /usr/lib64/ocaml/compiler-libs
Ocamlc   src/extract/c.mli
Ocamlc   src/extract/ocaml.mli
Ocamlc   src/extract/cakeml.mli
Ocamlc   src/parser/parser_messages.mli
Ocamlc   src/transform/remove_unused.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/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/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/config.ml
Ocamlc   src/util/bigInt.ml
Ocamlc   src/util/mlmpfr_wrapper.ml
Ocamlc   src/util/util.ml
Ocamlc   src/util/opt.ml
File "src/util/bigInt.ml", line 1:
Error: The files src/util/mysexplib.cmi and /usr/lib64/ocaml/big_int.cmi
       make inconsistent assumptions over interface Nat
make: *** [Makefile:2052: src/util/bigInt.cmo] Error 2
make: *** Waiting for unfinished jobs....
 * 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:20240810-112458.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'