Skip to content

[new release] colibri2 (4 packages) (0.6)#30097

Open
bobot wants to merge 1 commit into
ocaml:masterfrom
bobot:release-colibri2-0.6
Open

[new release] colibri2 (4 packages) (0.6)#30097
bobot wants to merge 1 commit into
ocaml:masterfrom
bobot:release-colibri2-0.6

Conversation

@bobot

@bobot bobot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

A CP solver for smtlib

CHANGES:
  • Add bv2int, bv2nat, nat2bv, int2bv,
  • produce models that why3 can parse
  • tentatively produce "proof trace" as smtlib2 files
  • --try-disprove-forall-using-domain use domain to disprove universal quantification on floating-points
  • Soundness fix on floating-point linearization
  • Soundness fix on instantiation of real for integer variable

@bobot

bobot commented Jun 22, 2026

Copy link
Copy Markdown
Contributor Author

I hope it will be more succesful than 0.5 release, thanks again to the maintainers.

@bobot bobot force-pushed the release-colibri2-0.6 branch from b3c1195 to f0d6769 Compare June 22, 2026 14:14
CHANGES:

  - Add bv2int, bv2nat, nat2bv, int2bv,
  - produce models that why3 can parse
  - tentatively produce "proof trace" as smtlib2 files
  - --try-disprove-forall-using-domain use domain to disprove universal quantification on floating-points
  - Soundness fix on floating-point linearization
  - Soundness fix on instantiation of real for integer variable
@bobot bobot force-pushed the release-colibri2-0.6 branch from f0d6769 to 5f2a7a2 Compare June 22, 2026 14:16
@mseri

mseri commented Jun 22, 2026

Copy link
Copy Markdown
Member

There is a common failure in the revdeps:

#=== ERROR while compiling smtml.0.9.0 ========================================#
# context              2.5.1 | linux/x86_64 | ocaml-base-compiler.4.14.3 | file:///home/opam/opam-repository
# path                 ~/.opam/4.14/.opam-switch/build/smtml.0.9.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p smtml -j 71 @install
# exit-code            1
# env-file             ~/.opam/log/smtml-7-92d5fa.env
# output-file          ~/.opam/log/smtml-7-92d5fa.out
### output ###
# (cd _build/default && /home/opam/.opam/4.14/bin/ocamlc.opt -w -40 -open Smtml_prelude -g -bin-annot -I src/smtml/.smtml.objs/byte -I src/smtml/.smtml.objs/public_cmi -I /home/opam/.opam/4.14/lib/astring -I /home/opam/.opam/4.14/lib/base -I /home/opam/.opam/4.14/lib/base/base_internalhash_types -I /home/opam/.opam/4.14/lib/base/caml -I /home/opam/.opam/4.14/lib/base/shadow_stdlib -I /home/opam/.opam/4.14/lib/bos -I /home/opam/.opam/4.14/lib/cmdliner -I /home/opam/.opam/4.14/lib/colibri2/core -I /home/opam/.opam/4.14/lib/colibri2/popop_lib -I /home/opam/.opam/4.14/lib/colibri2/solver -I /home/opam/.opam/4.14/lib/colibri2/stdlib -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/congruence -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/def -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage0/sign_domain -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage2 -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage2/union_domain -I /home/opam/.opam/4.14/lib/colibri2/theories/bool -I /home/opam/.opam/4.14/lib/colibri2/theories/fp -I /home/opam/.opam/4.14/lib/colibri2/theories/quantifiers -I /home/opam/.opam/4.14/lib/colibrilib -I /home/opam/.opam/4.14/lib/containers -I /home/opam/.opam/4.14/lib/containers/domain -I /home/opam/.opam/4.14/lib/containers/monomorphic -I /home/opam/.opam/4.14/lib/ctypes -I /home/opam/.opam/4.14/lib/ctypes/stubs -I /home/opam/.opam/4.14/lib/cudd -I /home/opam/.opam/4.14/lib/dolmen -I /home/opam/.opam/4.14/lib/dolmen/ae -I /home/opam/.opam/4.14/lib/dolmen/class -I /home/opam/.opam/4.14/lib/dolmen/dimacs -I /home/opam/.opam/4.14/lib/dolmen/icnf -I /home/opam/.opam/4.14/lib/dolmen/intf -I /home/opam/.opam/4.14/lib/dolmen/line -I /home/opam/.opam/4.14/lib/dolmen/smtlib2 -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/poly -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6 -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6_response -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6_script -I /home/opam/.opam/4.14/lib/dolmen/std -I /home/opam/.opam/4.14/lib/dolmen/tptp -I /home/opam/.opam/4.14/lib/dolmen/tptp/v6_3_0 -I /home/opam/.opam/4.14/lib/dolmen/zf -I /home/opam/.opam/4.14/lib/dolmen_loop -I /home/opam/.opam/4.14/lib/dolmen_type -I /home/opam/.opam/4.14/lib/either -I /home/opam/.opam/4.14/lib/farith -I /home/opam/.opam/4.14/lib/flint -I /home/opam/.opam/4.14/lib/fmt -I /home/opam/.opam/4.14/lib/fpath -I /home/opam/.opam/4.14/lib/gen -I /home/opam/.opam/4.14/lib/gmap -I /home/opam/.opam/4.14/lib/hc -I /home/opam/.opam/4.14/lib/hmap -I /home/opam/.opam/4.14/lib/integers -I /home/opam/.opam/4.14/lib/jane-street-headers -I /home/opam/.opam/4.14/lib/logs -I /home/opam/.opam/4.14/lib/menhirLib -I /home/opam/.opam/4.14/lib/mtime -I /home/opam/.opam/4.14/lib/mtime/clock -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/ocaml_intrinsics -I /home/opam/.opam/4.14/lib/ocamlgraph -I /home/opam/.opam/4.14/lib/ocplib-simplex -I /home/opam/.opam/4.14/lib/patricia-tree -I /home/opam/.opam/4.14/lib/pp_loc -I /home/opam/.opam/4.14/lib/ppx_compare/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_deriving/runtime -I /home/opam/.opam/4.14/lib/ppx_enumerate/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_hash/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_here/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_inline_test/config -I /home/opam/.opam/4.14/lib/ppx_inline_test/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_sexp_conv/runtime-lib -I /home/opam/.opam/4.14/lib/prelude -I /home/opam/.opam/4.14/lib/qcheck-core -I /home/opam/.opam/4.14/lib/re -I /home/opam/.opam/4.14/lib/scfg -I /home/opam/.opam/4.14/lib/sedlex -I /home/opam/.opam/4.14/lib/seq -I /home/opam/.opam/4.14/lib/sexplib0 -I /home/opam/.opam/4.14/lib/spelll -I /home/opam/.opam/4.14/lib/stdlib-shims -I /home/opam/.opam/4.14/lib/time_now -I /home/opam/.opam/4.14/lib/trace-tef -I /home/opam/.opam/4.14/lib/trace/core -I /home/opam/.opam/4.14/lib/trace/debug -I /home/opam/.opam/4.14/lib/trace/util -I /home/opam/.opam/4.14/lib/uutf -I /home/opam/.opam/4.14/lib/yojson -I /home/opam/.opam/4.14/lib/zarith -I src/smtml_prelude/.smtml_prelude.objs/byte -intf-suffix .ml -no-alias-deps -open Smtml -o src/smtml/.smtml.objs/byte/smtml__Colibri2_mappings.cmo -c -impl src/smtml/colibri2_mappings.ml)
# File "src/smtml/colibri2_mappings.default.ml", line 119, characters 15-59:
# Error: Unbound value Colibri2_core.ForSchedulers.default_theories
# (cd _build/default && /home/opam/.opam/4.14/bin/ocamlopt.opt -w -40 -open Smtml_prelude -g -I src/smtml/.smtml.objs/byte -I src/smtml/.smtml.objs/native -I src/smtml/.smtml.objs/public_cmi -I /home/opam/.opam/4.14/lib/astring -I /home/opam/.opam/4.14/lib/base -I /home/opam/.opam/4.14/lib/base/base_internalhash_types -I /home/opam/.opam/4.14/lib/base/caml -I /home/opam/.opam/4.14/lib/base/shadow_stdlib -I /home/opam/.opam/4.14/lib/bos -I /home/opam/.opam/4.14/lib/cmdliner -I /home/opam/.opam/4.14/lib/colibri2/core -I /home/opam/.opam/4.14/lib/colibri2/popop_lib -I /home/opam/.opam/4.14/lib/colibri2/solver -I /home/opam/.opam/4.14/lib/colibri2/stdlib -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/congruence -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/def -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage0/sign_domain -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage2 -I /home/opam/.opam/4.14/lib/colibri2/theories/LRA/stages/stage2/union_domain -I /home/opam/.opam/4.14/lib/colibri2/theories/bool -I /home/opam/.opam/4.14/lib/colibri2/theories/fp -I /home/opam/.opam/4.14/lib/colibri2/theories/quantifiers -I /home/opam/.opam/4.14/lib/colibrilib -I /home/opam/.opam/4.14/lib/containers -I /home/opam/.opam/4.14/lib/containers/domain -I /home/opam/.opam/4.14/lib/containers/monomorphic -I /home/opam/.opam/4.14/lib/ctypes -I /home/opam/.opam/4.14/lib/ctypes/stubs -I /home/opam/.opam/4.14/lib/cudd -I /home/opam/.opam/4.14/lib/dolmen -I /home/opam/.opam/4.14/lib/dolmen/ae -I /home/opam/.opam/4.14/lib/dolmen/class -I /home/opam/.opam/4.14/lib/dolmen/dimacs -I /home/opam/.opam/4.14/lib/dolmen/icnf -I /home/opam/.opam/4.14/lib/dolmen/intf -I /home/opam/.opam/4.14/lib/dolmen/line -I /home/opam/.opam/4.14/lib/dolmen/smtlib2 -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/poly -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6 -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6_response -I /home/opam/.opam/4.14/lib/dolmen/smtlib2/v6_script -I /home/opam/.opam/4.14/lib/dolmen/std -I /home/opam/.opam/4.14/lib/dolmen/tptp -I /home/opam/.opam/4.14/lib/dolmen/tptp/v6_3_0 -I /home/opam/.opam/4.14/lib/dolmen/zf -I /home/opam/.opam/4.14/lib/dolmen_loop -I /home/opam/.opam/4.14/lib/dolmen_type -I /home/opam/.opam/4.14/lib/either -I /home/opam/.opam/4.14/lib/farith -I /home/opam/.opam/4.14/lib/flint -I /home/opam/.opam/4.14/lib/fmt -I /home/opam/.opam/4.14/lib/fpath -I /home/opam/.opam/4.14/lib/gen -I /home/opam/.opam/4.14/lib/gmap -I /home/opam/.opam/4.14/lib/hc -I /home/opam/.opam/4.14/lib/hmap -I /home/opam/.opam/4.14/lib/integers -I /home/opam/.opam/4.14/lib/jane-street-headers -I /home/opam/.opam/4.14/lib/logs -I /home/opam/.opam/4.14/lib/menhirLib -I /home/opam/.opam/4.14/lib/mtime -I /home/opam/.opam/4.14/lib/mtime/clock -I /home/opam/.opam/4.14/lib/ocaml/threads -I /home/opam/.opam/4.14/lib/ocaml_intrinsics -I /home/opam/.opam/4.14/lib/ocamlgraph -I /home/opam/.opam/4.14/lib/ocplib-simplex -I /home/opam/.opam/4.14/lib/patricia-tree -I /home/opam/.opam/4.14/lib/pp_loc -I /home/opam/.opam/4.14/lib/ppx_compare/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_deriving/runtime -I /home/opam/.opam/4.14/lib/ppx_enumerate/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_hash/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_here/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_inline_test/config -I /home/opam/.opam/4.14/lib/ppx_inline_test/runtime-lib -I /home/opam/.opam/4.14/lib/ppx_sexp_conv/runtime-lib -I /home/opam/.opam/4.14/lib/prelude -I /home/opam/.opam/4.14/lib/qcheck-core -I /home/opam/.opam/4.14/lib/re -I /home/opam/.opam/4.14/lib/scfg -I /home/opam/.opam/4.14/lib/sedlex -I /home/opam/.opam/4.14/lib/seq -I /home/opam/.opam/4.14/lib/sexplib0 -I /home/opam/.opam/4.14/lib/spelll -I /home/opam/.opam/4.14/lib/stdlib-shims -I /home/opam/.opam/4.14/lib/time_now -I /home/opam/.opam/4.14/lib/trace-tef -I /home/opam/.opam/4.14/lib/trace/core -I /home/opam/.opam/4.14/lib/trace/debug -I /home/opam/.opam/4.14/lib/trace/util -I /home/opam/.opam/4.14/lib/uutf -I /home/opam/.opam/4.14/lib/yojson -I /home/opam/.opam/4.14/lib/zarith -I src/smtml_prelude/.smtml_prelude.objs/byte -I src/smtml_prelude/.smtml_prelude.objs/native -intf-suffix .ml -no-alias-deps -open Smtml -o src/smtml/.smtml.objs/native/smtml__Colibri2_mappings.cmx -c -impl src/smtml/colibri2_mappings.ml)
# File "src/smtml/colibri2_mappings.default.ml", line 119, characters 15-59:
# Error: Unbound value Colibri2_core.ForSchedulers.default_theories

Shoudl we add an upper bound to the affected packages (in a separate pr)?

@jmid jmid added the question label Jun 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants