Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 776522 Details for
Bug 842471
sci-mathematics/alt-ergo-2.4.1_p20220407 - :(.text+<snip>): undefined reference to camlCmdliner_entry
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
sci-mathematics:alt-ergo-2.4.1_p20220407:20220503-141649.log
sci-mathematics:alt-ergo-2.4.1_p20220407:20220503-141649.log (text/plain), 32.14 KB, created by
Toralf Förster
on 2022-05-03 17:04:05 UTC
(
hide
)
Description:
sci-mathematics:alt-ergo-2.4.1_p20220407:20220503-141649.log
Filename:
MIME Type:
Creator:
Toralf Förster
Created:
2022-05-03 17:04:05 UTC
Size:
32.14 KB
patch
obsolete
> * 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' >
You cannot view the attachment while viewing its details because your browser does not support IFRAMEs.
View the attachment on a separate page
.
View Attachment As Raw
Actions:
View
Attachments on
bug 842471
:
776510
|
776513
|
776516
|
776519
| 776522 |
776525