Build:
- 0
2026-06-23 16:53.53: New job: build alt-ergo-lib.2.4.0 (e95bbfd33497)
2026-06-23 16:53.53: Waiting for resource in pool day11-builds
2026-06-23 18:23.57: Got resource from pool day11-builds
2026-06-23 18:23.57: [profile full] build alt-ergo-lib.2.4.0
2026-06-23 18:23.57: build alt-ergo-lib.2.4.0 (e95bbfd33497)
=== DEPENDENCIES (18 transitive) ===
base-threads.base b7164ff76afe
base-unix.base 839dc585f12d
conf-autoconf.0.2 b3cd190cf0b5
conf-gmp.5 61e3c79e0ddf
conf-pkg-config.5 4b60827fc174
csexp.1.5.1 e3f0f167b110
dune.2.9.3 36797f878ec2
dune-configurator.2.9.3 d180a2638840
num.1.6 480227ca99db
ocaml.4.14.4 cb826ea44eb2
ocaml-base-compiler.4.14.4 d2f775f983d7
ocaml-config.2 669e0fcf9e4d
ocamlfind.1.9.8 6025f4a8e98e
ocplib-simplex.0.4.1 e8755ec4bafa
result.1.5 33a2387f4b32
seq.base 063828a3d698
stdlib-shims.0.3.0 d11064be4664
zarith.1.14 da8b932acb94
=== STDOUT ===
Processing: [default: loading data]
[alt-ergo-lib.2.4.0: dl]
[alt-ergo-lib.2.4.0: extract]
-> retrieved alt-ergo-lib.2.4.0 (https://opam.ocaml.org/cache)
[alt-ergo-lib: ocaml unix.cma]
+ /home/opam/.opam/default/bin/ocaml "unix.cma" "configure.ml" "alt-ergo-lib" "--libdir" "/home/opam/.opam/default/lib" "--mandir" "/home/opam/.opam/default/man" (CWD=/home/opam/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.0)
- Found opam in path.
- Using default value for 'prefix' : /home/opam/.opam/default
- Using provided value for 'libdir' : /home/opam/.opam/default/lib
- Using provided value for 'mandir' : /home/opam/.opam/default/man
- Generating file src/lib/util/config.ml...done.
- Generating file src/bin/text/flags.dune...done.
- Generating file Makefile.config...done.
- Found dune in path.
- All deps are installed.
- Good to go!
[alt-ergo-lib: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "alt-ergo-lib" "-j" "39" (CWD=/home/opam/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.0)
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Parsed_interface.{cmi,cmti}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Ty.{cmo,cmt}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt.{cmo,cmt}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Records.{cmo,cmt}
- 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 !
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Cnf.{cmo,cmt}
- 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 231, characters 29-64:
- 231 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- File "src/lib/frontend/cnf.ml", line 445, characters 29-64:
- 445 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_types.{cmo,cmt}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Ite_rel.{cmo,cmt}
- 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 ?
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Shostak.{cmo,cmt}
- File "src/lib/reasoners/shostak.ml", lines 549-551, characters 26-39:
- 549 | .........................."TODO: a simple way of handling equalities \
- 550 | with void and unit is to add this case is \
- 551 | the solver!".
- Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver!
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt_rel.{cmo,cmt}
- 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 ?
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Ty.{cmx,o}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_frontend.{cmo,cmt}
- 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 ...
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml.{cmo,cmt}
- 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
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__IntervalCalculus.{cmo,cmt}
- File "src/lib/reasoners/intervalCalculus.ml", line 1809, characters 27-63:
- 1809 | [@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 2058, characters 28-73:
- 2058 | [@ocaml.ppwarning "TODO: find an example triggering this case!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: find an example triggering this case!
- ocamlc src/lib/.AltErgoLib.objs/byte/altErgoLib__Expr.{cmo,cmt}
- 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 1595-1597, characters 24-55:
- 1595 | ........................"TODO: should also inline form in form. But \
- 1596 | not possible to detect if we are not \
- 1597 | 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 2074-2077, characters 34-77:
- 2074 | .................................."TODO: once 'let x = term in term' \
- 2075 | added, check that the resulting sbt \
- 2076 | is well normalized (may be not true \
- 2077 | 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 2098-2100, characters 26-49:
- 2098 | .........................."TODO: do it for this case once \
- 2099 | free-vars issues of theories axioms \
- 2100 | 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 2094-2096, characters 26-56:
- 2094 | .........................."TODO: filter_good_triggers for this \
- 2095 | case once free-vars issues of theories \
- 2096 | 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 2300, characters 20-57:
- 2300 | [@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 2299, characters 20-50:
- 2299 | [@ocaml.ppwarning "TODO: add other elim schemes"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other elim schemes
- File "src/lib/structures/expr.ml", line 2298, characters 20-62:
- 2298 | [@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
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Expr.{cmx,o}
- 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 1595-1597, characters 24-55:
- 1595 | ........................"TODO: should also inline form in form. But \
- 1596 | not possible to detect if we are not \
- 1597 | 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 2074-2077, characters 34-77:
- 2074 | .................................."TODO: once 'let x = term in term' \
- 2075 | added, check that the resulting sbt \
- 2076 | is well normalized (may be not true \
- 2077 | 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 2098-2100, characters 26-49:
- 2098 | .........................."TODO: do it for this case once \
- 2099 | free-vars issues of theories axioms \
- 2100 | 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 2094-2096, characters 26-56:
- 2094 | .........................."TODO: filter_good_triggers for this \
- 2095 | case once free-vars issues of theories \
- 2096 | 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 2300, characters 20-57:
- 2300 | [@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 2299, characters 20-50:
- 2299 | [@ocaml.ppwarning "TODO: add other elim schemes"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other elim schemes
- File "src/lib/structures/expr.ml", line 2298, characters 20-62:
- 2298 | [@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
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Cnf.{cmx,o}
- 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 231, characters 29-64:
- 231 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- File "src/lib/frontend/cnf.ml", line 445, characters 29-64:
- 445 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Adt.{cmx,o}
- 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
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Records.{cmx,o}
- 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 !
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Satml_types.{cmx,o}
- 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
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Shostak.{cmx,o}
- File "src/lib/reasoners/shostak.ml", lines 549-551, characters 26-39:
- 549 | .........................."TODO: a simple way of handling equalities \
- 550 | with void and unit is to add this case is \
- 551 | the solver!".
- Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver!
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Ite_rel.{cmx,o}
- 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 ?
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Adt_rel.{cmx,o}
- 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 ?
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__IntervalCalculus.{cmx,o}
- File "src/lib/reasoners/intervalCalculus.ml", line 1809, characters 27-63:
- 1809 | [@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 2058, characters 28-73:
- 2058 | [@ocaml.ppwarning "TODO: find an example triggering this case!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: find an example triggering this case!
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Satml.{cmx,o}
- 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
- ocamlopt src/lib/.AltErgoLib.objs/native/altErgoLib__Satml_frontend.{cmx,o}
- 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 ...
-> compiled alt-ergo-lib.2.4.0
-> installed alt-ergo-lib.2.4.0
[WARNING] Opam packages conf-gmp.5 and conf-pkg-config.5 depend on the following system packages that are no longer installed: libgmp-dev pkg-config
- conf-gmp.5: depends on libgmp-dev
- conf-pkg-config.5: depends on pkg-config
=== STDERR ===
2026-06-23 18:28.16: OK: build alt-ergo-lib.2.4.0 (runc: 32.1s, disk: 37KB)
2026-06-23 18:28.16: Job succeeded