* Package: sci-mathematics/alt-ergo-2.4.1_p20220407 * Repository: gentoo * Maintainer: ml@gentoo.org sci-mathematics@gentoo.org * Upstream: https://github.com/OCamlPro/alt-ergo/issues/ * USE: abi_x86_64 amd64 elibc_glibc kernel_linux ocamlopt userland_GNU * FEATURES: network-sandbox preserve-libs sandbox userpriv usersandbox >>> Unpacking source... >>> Unpacking alt-ergo-2.4.1_p20220407.tar.gz to /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work >>> Source unpacked in /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work >>> Preparing source in /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work/alt-ergo-4e082218efe6e0e2315331580bbd08306c1f8a2d ... >>> Source prepared. >>> Configuring source in /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work/alt-ergo-4e082218efe6e0e2315331580bbd08306c1f8a2d ... Using provided value for 'prefix' : /usr Using provided value for 'libdir' : /usr/lib64 Using default value for 'mandir' : /usr/man Generating file src/lib/util/config.ml...done. Generating file src/bin/text/flags.dune...done. Generating file Makefile.config...done. Good to go! >>> Source configured. >>> Compiling source in /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work/alt-ergo-4e082218efe6e0e2315331580bbd08306c1f8a2d ... * Building ... File "src/lib/frontend/parsed_interface.mli", line 18, characters 20-77: 18 | [@ocaml.ppwarning "TODO: add documentation for every function in this file"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add documentation for every function in this file File "src/lib/structures/ty.ml", line 200, characters 20-51: 200 | [@ocaml.ppwarning "TODO: should be implemented ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should be implemented ? File "src/lib/structures/ty.ml", line 334, characters 24-65: 334 | [@ocaml.ppwarning "TODO: detect when there are no changes "] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: detect when there are no changes File "src/lib/structures/ty.ml", line 589, characters 28-59: 589 | | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: remove fragile pattern File "src/lib/structures/ty.ml", line 639, characters 20-61: 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: detect when there are no changes File "src/lib/structures/satml_types.ml", line 852, characters 33-71: 852 | [@ocaml.ppwarning "xlit or at_lit is probably redundant"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: xlit or at_lit is probably redundant File "src/lib/frontend/cnf.ml", lines 38-40, characters 19-33: 38 | ..................."TODO: Change Symbols.Float to store FP numeral \ 39 | constants (eg, <24, -149> for single) instead of \ 40 | having terms". Warning 22 [preprocessor]: TODO: Change Symbols.Float to store FP numeral constants (eg, <24, -149> for single) instead of having terms File "src/lib/frontend/cnf.ml", line 250, characters 29-64: 250 | [@ocaml.ppwarning "TODO: should introduce fresh vars"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should introduce fresh vars File "src/lib/frontend/cnf.ml", line 475, characters 29-64: 475 | [@ocaml.ppwarning "TODO: should introduce fresh vars"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should introduce fresh vars File "src/lib/structures/expr.ml", line 1387, characters 33-66: 1387 | else acc [@ocaml.ppwarning "TODO: add some stuff from let_e"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add some stuff from let_e File "src/lib/structures/expr.ml", lines 1599-1601, characters 24-55: 1599 | ........................"TODO: should also inline form in form. But \ 1600 | not possible to detect if we are not \ 1601 | inlining a form inside a term". Warning 22 [preprocessor]: TODO: should also inline form in form. But not possible to detect if we are not inlining a form inside a term File "src/lib/structures/expr.ml", lines 2094-2097, characters 34-77: 2094 | .................................."TODO: once 'let x = term in term' \ 2095 | added, check that the resulting sbt \ 2096 | is well normalized (may be not true \ 2097 | depending on the ordering of vars in lets". Warning 22 [preprocessor]: TODO: once 'let x = term in term' added, check that the resulting sbt is well normalized (may be not true depending on the ordering of vars in lets File "src/lib/structures/expr.ml", lines 2118-2120, characters 26-49: 2118 | .........................."TODO: do it for this case once \ 2119 | free-vars issues of theories axioms \ 2120 | with hypotheses fixed". Warning 22 [preprocessor]: TODO: do it for this case once free-vars issues of theories axioms with hypotheses fixed File "src/lib/structures/expr.ml", lines 2114-2116, characters 26-56: 2114 | .........................."TODO: filter_good_triggers for this \ 2115 | case once free-vars issues of theories \ 2116 | axioms with hypotheses fixed". Warning 22 [preprocessor]: TODO: filter_good_triggers for this case once free-vars issues of theories axioms with hypotheses fixed File "src/lib/structures/expr.ml", line 2320, characters 20-57: 2320 | [@ocaml.ppwarning "TODO: add a match construct in expr"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add a match construct in expr File "src/lib/structures/expr.ml", line 2319, characters 20-50: 2319 | [@ocaml.ppwarning "TODO: add other elim schemes"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add other elim schemes File "src/lib/structures/expr.ml", line 2318, characters 20-62: 2318 | [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: introduce a let if e is a big expr File "src/lib/reasoners/adt.ml", lines 63-64, characters 21-30: 63 | ....................."XXX: IsConstr not interpreted currently. Maybe \ 64 | it's OK". Warning 22 [preprocessor]: XXX: IsConstr not interpreted currently. Maybe it's OK File "src/lib/reasoners/adt.ml", line 105, characters 24-64: 105 | [@ocaml.ppwarning "TODO: canonize Constr(list of selects)"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: canonize Constr(list of selects) File "src/lib/reasoners/adt.ml", line 227, characters 21-37: 227 | [@@ocaml.ppwarning "TODO: not sure"] ^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: not sure File "src/lib/reasoners/adt.ml", line 318, characters 24-50: 318 | [@ocaml.ppwarning "TODO: abstract Selectors"] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors File "src/lib/reasoners/adt.ml", line 305, characters 26-66: 305 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors: case to test File "src/lib/reasoners/adt.ml", line 313, characters 27-67: 313 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] then ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors: case to test File "src/lib/reasoners/adt.ml", line 328, characters 27-53: 328 | [@ocaml.ppwarning "TODO: abstract Selectors"] then ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors File "src/lib/reasoners/records.ml", line 283, characters 26-69: 283 | [@ocaml.ppwarning "TODO: should not rebuild if not changed !"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should not rebuild if not changed ! File "src/lib/reasoners/shostak.ml", lines 551-553, characters 26-39: 551 | .........................."TODO: a simple way of handling equalities \ 552 | with void and unit is to add this case is \ 553 | the solver!". Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver! File "src/lib/structures/ty.ml", line 200, characters 20-51: 200 | [@ocaml.ppwarning "TODO: should be implemented ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should be implemented ? File "src/lib/structures/ty.ml", line 334, characters 24-65: 334 | [@ocaml.ppwarning "TODO: detect when there are no changes "] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: detect when there are no changes File "src/lib/structures/ty.ml", line 589, characters 28-59: 589 | | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: remove fragile pattern File "src/lib/structures/ty.ml", line 639, characters 20-61: 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: detect when there are no changes File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51: 41 | ......................"selectors should be improved. only representatives \ 42 | in it. No true or false _is". Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is File "src/lib/reasoners/adt_rel.ml", lines 296-297, characters 19-66: 296 | ..................."XXX improve. For each selector, store its \ 297 | corresponding constructor when typechecking ?". Warning 22 [preprocessor]: XXX improve. For each selector, store its corresponding constructor when typechecking ? File "src/lib/reasoners/adt_rel.ml", line 334, characters 19-72: 334 | [@@ocaml.ppwarning "working with X.term_extract r would be sufficient ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: working with X.term_extract r would be sufficient ? File "src/lib/reasoners/adt_rel.ml", line 648, characters 31-77: 648 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ? File "src/lib/reasoners/adt_rel.ml", line 709, characters 26-72: 709 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ? File "src/lib/reasoners/ite_rel.ml", line 119, characters 35-62: 119 | [@ocaml.ppwarning "TODO: build IFF instead ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: build IFF instead ? File "src/lib/reasoners/intervalCalculus.ml", line 1838, characters 27-63: 1838 | [@ocaml.ppwarning "TODO: add other terms such as div!"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add other terms such as div! File "src/lib/reasoners/intervalCalculus.ml", line 2091, characters 28-73: 2091 | [@ocaml.ppwarning "TODO: find an example triggering this case!"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: find an example triggering this case! File "src/lib/reasoners/satml.ml", line 523, characters 26-66: 523 | [@ocaml.ppwarning "TODO: try to disable 'fill_with_dummy'"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: try to disable 'fill_with_dummy' File "src/lib/reasoners/satml.ml", lines 1576-1579, characters 28-42: 1576 | ............................"TODO: add a heavy assert that checks \ 1577 | that clauses are not redundant, watchs \ 1578 | are well set, unit and bottom are \ 1579 | detected ...". Warning 22 [preprocessor]: TODO: add a heavy assert that checks that clauses are not redundant, watchs are well set, unit and bottom are detected ... File "src/lib/reasoners/satml.ml", lines 1645-1646, characters 22-43: 1645 | ......................"Issue: BAD decision_level, in particular, \ 1646 | if minimal-bj is ON". Warning 22 [preprocessor]: Issue: BAD decision_level, in particular, if minimal-bj is ON File "src/lib/reasoners/satml_frontend.ml", line 374, characters 24-77: 374 | [@ocaml.ppwarning "TODO: modifications made in tbox are lost! improve?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: modifications made in tbox are lost! improve? File "src/lib/reasoners/satml_frontend.ml", lines 671-672, characters 6-63: 671 | ......"improve terms / atoms extraction in lazy/non-lazy \ 672 | and greedy/non-greedy mode. Separate atoms from terms !". Warning 22 [preprocessor]: improve terms / atoms extraction in lazy/non-lazy and greedy/non-greedy mode. Separate atoms from terms ! File "src/lib/reasoners/satml_frontend.ml", line 693, characters 22-75: 693 | [@ocaml.ppwarning "Issue for greedy: terms inside lemmas not extracted"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: Issue for greedy: terms inside lemmas not extracted File "src/lib/reasoners/satml_frontend.ml", lines 714-715, characters 22-73: 714 | ......................"!!! Possibles issues du to replacement of atoms \ 715 | that are facts with TRUE by mk_lit (and simplify)". Warning 22 [preprocessor]: !!! Possibles issues du to replacement of atoms that are facts with TRUE by mk_lit (and simplify) File "src/lib/reasoners/satml_frontend.ml", line 748, characters 28-61: 748 | [@ocaml.ppwarning "TODO: should be assert failure?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should be assert failure? File "src/lib/reasoners/satml_frontend.ml", line 846, characters 34-79: 846 | [@ocaml.ppwarning "TODO: should fix for unsat cores generation"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should fix for unsat cores generation File "src/lib/reasoners/satml_frontend.ml", line 985, characters 20-79: 985 | "TODO: first intantiation a la DfsSAT before searching ..."] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: first intantiation a la DfsSAT before searching ... File "src/lib/structures/expr.ml", line 1387, characters 33-66: 1387 | else acc [@ocaml.ppwarning "TODO: add some stuff from let_e"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add some stuff from let_e File "src/lib/structures/expr.ml", lines 1599-1601, characters 24-55: 1599 | ........................"TODO: should also inline form in form. But \ 1600 | not possible to detect if we are not \ 1601 | inlining a form inside a term". Warning 22 [preprocessor]: TODO: should also inline form in form. But not possible to detect if we are not inlining a form inside a term File "src/lib/structures/expr.ml", lines 2094-2097, characters 34-77: 2094 | .................................."TODO: once 'let x = term in term' \ 2095 | added, check that the resulting sbt \ 2096 | is well normalized (may be not true \ 2097 | depending on the ordering of vars in lets". Warning 22 [preprocessor]: TODO: once 'let x = term in term' added, check that the resulting sbt is well normalized (may be not true depending on the ordering of vars in lets File "src/lib/structures/expr.ml", lines 2118-2120, characters 26-49: 2118 | .........................."TODO: do it for this case once \ 2119 | free-vars issues of theories axioms \ 2120 | with hypotheses fixed". Warning 22 [preprocessor]: TODO: do it for this case once free-vars issues of theories axioms with hypotheses fixed File "src/lib/structures/expr.ml", lines 2114-2116, characters 26-56: 2114 | .........................."TODO: filter_good_triggers for this \ 2115 | case once free-vars issues of theories \ 2116 | axioms with hypotheses fixed". Warning 22 [preprocessor]: TODO: filter_good_triggers for this case once free-vars issues of theories axioms with hypotheses fixed File "src/lib/structures/expr.ml", line 2320, characters 20-57: 2320 | [@ocaml.ppwarning "TODO: add a match construct in expr"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add a match construct in expr File "src/lib/structures/expr.ml", line 2319, characters 20-50: 2319 | [@ocaml.ppwarning "TODO: add other elim schemes"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add other elim schemes File "src/lib/structures/expr.ml", line 2318, characters 20-62: 2318 | [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: introduce a let if e is a big expr File "src/lib/reasoners/adt.ml", lines 63-64, characters 21-30: 63 | ....................."XXX: IsConstr not interpreted currently. Maybe \ 64 | it's OK". Warning 22 [preprocessor]: XXX: IsConstr not interpreted currently. Maybe it's OK File "src/lib/reasoners/adt.ml", line 105, characters 24-64: 105 | [@ocaml.ppwarning "TODO: canonize Constr(list of selects)"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: canonize Constr(list of selects) File "src/lib/reasoners/adt.ml", line 227, characters 21-37: 227 | [@@ocaml.ppwarning "TODO: not sure"] ^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: not sure File "src/lib/reasoners/adt.ml", line 318, characters 24-50: 318 | [@ocaml.ppwarning "TODO: abstract Selectors"] -> ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors File "src/lib/reasoners/adt.ml", line 305, characters 26-66: 305 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors: case to test File "src/lib/reasoners/adt.ml", line 313, characters 27-67: 313 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] then ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors: case to test File "src/lib/reasoners/adt.ml", line 328, characters 27-53: 328 | [@ocaml.ppwarning "TODO: abstract Selectors"] then ^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: abstract Selectors File "src/lib/structures/satml_types.ml", line 852, characters 33-71: 852 | [@ocaml.ppwarning "xlit or at_lit is probably redundant"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: xlit or at_lit is probably redundant File "src/lib/reasoners/records.ml", line 283, characters 26-69: 283 | [@ocaml.ppwarning "TODO: should not rebuild if not changed !"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should not rebuild if not changed ! File "src/lib/frontend/cnf.ml", lines 38-40, characters 19-33: 38 | ..................."TODO: Change Symbols.Float to store FP numeral \ 39 | constants (eg, <24, -149> for single) instead of \ 40 | having terms". Warning 22 [preprocessor]: TODO: Change Symbols.Float to store FP numeral constants (eg, <24, -149> for single) instead of having terms File "src/lib/frontend/cnf.ml", line 250, characters 29-64: 250 | [@ocaml.ppwarning "TODO: should introduce fresh vars"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should introduce fresh vars File "src/lib/frontend/cnf.ml", line 475, characters 29-64: 475 | [@ocaml.ppwarning "TODO: should introduce fresh vars"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should introduce fresh vars File "src/lib/reasoners/shostak.ml", lines 551-553, characters 26-39: 551 | .........................."TODO: a simple way of handling equalities \ 552 | with void and unit is to add this case is \ 553 | the solver!". Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver! File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51: 41 | ......................"selectors should be improved. only representatives \ 42 | in it. No true or false _is". Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is File "src/lib/reasoners/adt_rel.ml", lines 296-297, characters 19-66: 296 | ..................."XXX improve. For each selector, store its \ 297 | corresponding constructor when typechecking ?". Warning 22 [preprocessor]: XXX improve. For each selector, store its corresponding constructor when typechecking ? File "src/lib/reasoners/adt_rel.ml", line 334, characters 19-72: 334 | [@@ocaml.ppwarning "working with X.term_extract r would be sufficient ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: working with X.term_extract r would be sufficient ? File "src/lib/reasoners/adt_rel.ml", line 648, characters 31-77: 648 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ? File "src/lib/reasoners/adt_rel.ml", line 709, characters 26-72: 709 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ? File "src/lib/reasoners/ite_rel.ml", line 119, characters 35-62: 119 | [@ocaml.ppwarning "TODO: build IFF instead ?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: build IFF instead ? File "src/lib/reasoners/intervalCalculus.ml", line 1838, characters 27-63: 1838 | [@ocaml.ppwarning "TODO: add other terms such as div!"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: add other terms such as div! File "src/lib/reasoners/intervalCalculus.ml", line 2091, characters 28-73: 2091 | [@ocaml.ppwarning "TODO: find an example triggering this case!"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: find an example triggering this case! File "src/lib/reasoners/satml.ml", line 523, characters 26-66: 523 | [@ocaml.ppwarning "TODO: try to disable 'fill_with_dummy'"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: try to disable 'fill_with_dummy' File "src/lib/reasoners/satml.ml", lines 1576-1579, characters 28-42: 1576 | ............................"TODO: add a heavy assert that checks \ 1577 | that clauses are not redundant, watchs \ 1578 | are well set, unit and bottom are \ 1579 | detected ...". Warning 22 [preprocessor]: TODO: add a heavy assert that checks that clauses are not redundant, watchs are well set, unit and bottom are detected ... File "src/lib/reasoners/satml.ml", lines 1645-1646, characters 22-43: 1645 | ......................"Issue: BAD decision_level, in particular, \ 1646 | if minimal-bj is ON". Warning 22 [preprocessor]: Issue: BAD decision_level, in particular, if minimal-bj is ON File "src/lib/reasoners/satml_frontend.ml", line 374, characters 24-77: 374 | [@ocaml.ppwarning "TODO: modifications made in tbox are lost! improve?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: modifications made in tbox are lost! improve? File "src/lib/reasoners/satml_frontend.ml", lines 671-672, characters 6-63: 671 | ......"improve terms / atoms extraction in lazy/non-lazy \ 672 | and greedy/non-greedy mode. Separate atoms from terms !". Warning 22 [preprocessor]: improve terms / atoms extraction in lazy/non-lazy and greedy/non-greedy mode. Separate atoms from terms ! File "src/lib/reasoners/satml_frontend.ml", line 693, characters 22-75: 693 | [@ocaml.ppwarning "Issue for greedy: terms inside lemmas not extracted"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: Issue for greedy: terms inside lemmas not extracted File "src/lib/reasoners/satml_frontend.ml", lines 714-715, characters 22-73: 714 | ......................"!!! Possibles issues du to replacement of atoms \ 715 | that are facts with TRUE by mk_lit (and simplify)". Warning 22 [preprocessor]: !!! Possibles issues du to replacement of atoms that are facts with TRUE by mk_lit (and simplify) File "src/lib/reasoners/satml_frontend.ml", line 748, characters 28-61: 748 | [@ocaml.ppwarning "TODO: should be assert failure?"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should be assert failure? File "src/lib/reasoners/satml_frontend.ml", line 846, characters 34-79: 846 | [@ocaml.ppwarning "TODO: should fix for unsat cores generation"] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: should fix for unsat cores generation File "src/lib/reasoners/satml_frontend.ml", line 985, characters 20-79: 985 | "TODO: first intantiation a la DfsSAT before searching ..."] ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 22 [preprocessor]: TODO: first intantiation a la DfsSAT before searching ... ocamlopt src/bin/text/Main_text.exe (exit 2) (cd _build/default && /usr/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -o src/bin/text/Main_text.exe /usr/lib64/ocaml/seq/seq.cmxa /usr/lib64/ocaml/unix.cmxa -I /usr/lib64/ocaml /usr/lib64/ocaml/nums.cmxa -I /usr/lib64/ocaml /usr/lib64/ocaml/str.cmxa -I /usr/lib64/ocaml /usr/lib64/ocaml/zarith/zarith.cmxa -I /usr/lib64/ocaml/zarith /usr/lib64/ocaml/dynlink.cmxa -I /usr/lib64/ocaml /usr/lib64/ocaml/ocplib-simplex/ocplibSimplex.cmxa /usr/lib64/ocaml/stdlib-shims/stdlib_shims.cmxa src/lib/AltErgoLib.cmxa /usr/lib64/ocaml/zip/zip.cmxa -I /usr/lib64/ocaml/zip /usr/lib64/ocaml/psmt2-frontend/psmt2Frontend.cmxa src/parsers/AltErgoParsers.cmxa /usr/lib64/ocaml/cmdliner/cmdliner.cmxa src/bin/common/alt_ergo_common.cmxa src/bin/text/.Main_text.eobjs/native/dune__exe__Main_text.cmx -linkall) /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build8a0210.dune/camlstartup04be27.o: in function `caml_program': :(.text+0xff5): undefined reference to `camlCmdliner__entry' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build8a0210.dune/camlstartup04be27.o: in function `caml_globals': :(.data+0xa50): undefined reference to `camlCmdliner__gc_roots' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build8a0210.dune/camlstartup04be27.o: in function `caml_data_segments': :(.data+0x5230): undefined reference to `camlCmdliner__data_begin' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0x5238): undefined reference to `camlCmdliner__data_end' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build8a0210.dune/camlstartup04be27.o: in function `caml_code_segments': :(.data+0x62b8): undefined reference to `camlCmdliner__code_begin' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.data+0x62c0): undefined reference to `camlCmdliner__code_end' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: /var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build8a0210.dune/camlstartup04be27.o: in function `caml_frametable': :(.data+0x6b48): undefined reference to `camlCmdliner__frametable' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: src/bin/common/alt_ergo_common.a(alt_ergo_common__Parse_command.o): in function `camlAlt_ergo_common__Parse_command__entry': :(.text+0x2592): undefined reference to `camlCmdliner' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.text+0x25a6): undefined reference to `camlCmdliner' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.text+0x25ef): undefined reference to `camlCmdliner' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.text+0x2603): undefined reference to `camlCmdliner' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: :(.text+0x264d): undefined reference to `camlCmdliner' /usr/lib/gcc/x86_64-pc-linux-gnu/12.0.1/../../../../x86_64-pc-linux-gnu/bin/ld: src/bin/common/alt_ergo_common.a(alt_ergo_common__Parse_command.o)::(.text+0x2661): more undefined references to `camlCmdliner' follow collect2: error: ld returned 1 exit status File "caml_startup", line 1: Error: Error during linking (exit code 1) [ !! ] * ERROR: sci-mathematics/alt-ergo-2.4.1_p20220407::gentoo failed (compile phase): * (no error message) * * Call stack: * ebuild.sh, line 127: Called src_compile * environment, line 658: Called dune_src_compile * environment, line 436: Called die * The specific snippet of code: * eend $? || die * * If you need support, post the output of `emerge --info '=sci-mathematics/alt-ergo-2.4.1_p20220407::gentoo'`, * the complete build log and the output of `emerge -pqv '=sci-mathematics/alt-ergo-2.4.1_p20220407::gentoo'`. * The complete build log is located at '/var/log/portage/sci-mathematics:alt-ergo-2.4.1_p20220407:20220503-141649.log'. * For convenience, a symlink to the build log is located at '/var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/build.log'. * The ebuild environment file is located at '/var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/temp/environment'. * Working directory: '/var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work/alt-ergo-4e082218efe6e0e2315331580bbd08306c1f8a2d' * S: '/var/tmp/portage/sci-mathematics/alt-ergo-2.4.1_p20220407/work/alt-ergo-4e082218efe6e0e2315331580bbd08306c1f8a2d'