Package smtml.0.14.0

[filipeom]

smtml.0.14.0

An SMT solver frontend for OCaml
Smt.ml is an SMT solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability.

---

• Homepage: https://github.com/formalsec/smtml
• Source repo: git+https://github.com/formalsec/smtml.git
• Bug tracker: https://github.com/formalsec/smtml/issues

---

Git shortlog

Filipe Marques (7):
      Remove old datasets dir
      Add new datasets directory
      Bring back collections-c benchmarking as a test
      WIP: Add a simple Smtml.Expr.t -> smt2 pretty printer
      Promote tests
      Add draft smtml logo
      Add `threads` to smtml's libraries stanza

S41d (1):
      move cache hits and misses to Solver_intf.S

github-actions[bot] (1):
      Release 0.14.0

---

🐫 Pull-request generated by opam-publish v2.7.0

[jmid]

Thanks!

There is only a minor nit causing a failure on 4.14:

[ERROR] The compilation of smtml.0.14.0 failed at "dune build -p smtml -j 255 @install".

#=== ERROR while compiling smtml.0.14.0 =======================================#
# context              2.5.0~beta1 | linux/x86_64 | ocaml-base-compiler.4.14.2 | pinned(https://github.com/formalsec/smtml/archive/refs/tags/v0.14.0.tar.gz)
# path                 ~/.opam/4.14/.opam-switch/build/smtml.0.14.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p smtml -j 255 @install
# exit-code            1
# env-file             ~/.opam/log/smtml-7-7986db.env
# output-file          ~/.opam/log/smtml-7-7986db.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/biniou -I /home/opam/.opam/4.14/lib/bos -I /home/opam/.opam/4.14/lib/cmdliner -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_model -I /home/opam/.opam/4.14/lib/dolmen_type -I /home/opam/.opam/4.14/lib/easy-format -I /home/opam/.opam/4.14/lib/farith -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/hc -I /home/opam/.opam/4.14/lib/hmap -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_intrinsics -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_hash/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/result -I /home/opam/.opam/4.14/lib/rresult -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/uchar -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 -no-alias-deps -open Smtml -o src/smtml/.smtml.objs/byte/smtml__Utils.cmo -c -impl src/smtml/utils.pp.ml)
# File "src/smtml/utils.ml", line 17, characters 2-12:
# 17 |   Mutex.lock m;
#        ^^^^^^^^^^
# Error: Unbound module Mutex

On 4.14 in order to use the Mutex module, one has to state a dependency on threads using (libraries ... threads ...) in the dune file. The module is already distributed with the compiler, so this doesn't materialize as an additional opam package dependency.

I am a unsure why this only triggers during 4.14's lower bound search 🤔

[filipeom]

There is only a minor nit causing a failure on 4.14:

Ah thanks for spotting this!

On 4.14 in order to use the Mutex module, one has to state a dependency on threads using (libraries ... threads ...) in the dune file. The module is already distributed with the compiler, so this doesn't materialize as an additional opam package dependency.

I am a unsure why this only triggers during 4.14's lower bound search 🤔

Thanks for the explanation! I also find it a bit odd why it triggers only in a lower-bounds CI. I think in a previous version of smtml I already had this change and it compiled fine back then. 😅 Nevertheless, I'll move this to draft and make the change to see if it fixes it. Once it's all green, I'll make it ready.

[filipeom]

Seems now there's an error in the centos CI saying it cannot install the gmp-devel depext.

Don't know if it's related to this error:

+ /usr/bin/sudo "yum" "install" "-y" "gmp-devel"
- CentOS Stream 10 - BaseOS                        47 kB/s |  15 kB     00:00    
- CentOS Stream 10 - BaseOS                       430  B/s | 3.9 kB     00:09    
- Errors during downloading metadata for repository 'baseos':
-   - Curl error (60): SSL peer certificate or SSH remote key was not OK for https://ftp.byfly.by/pub/centos-stream/10-stream/BaseOS/x86_64/os/repodata/repomd.xml [SSL certificate problem: certificate has expired]
-   - Downloading successful, but checksum doesn't match. Calculated: cedae4fed62772cdda4516898ca598192a64ba1df2a9b630553df82e5f7c13d0cd5c36dcf2f7d0ba5de5717cead7e77307ae5b50b1546204b9b703bf3c7caeae(sha512)  Expected: e2fca36f22b02afa772369db7b35d7d47368cdbe053eb5807ae971175ab4a9f978ea57cbc04b8998745644922317e7d09dfe1708df5fa35882bc3ffb6e666d2f(sha512) 
- Error: Failed to download metadata for repo 'baseos': Cannot download repomd.xml: Cannot download repodata/repomd.xml: All mirrors were tried
[ERROR] System package install failed with exit code 1 at command:
            sudo yum install -y gmp-devel

[redianthus]

It looks unrelated to the PR.

[jmid]

LGTM - and all green even, thanks!

(and I agree the certificate expiration is unrelated 👍 )

[avsm]

Thanks! You may want to announce this on https://discuss.ocaml.org, where we have a Community category and an announce tag for this purpose.