Add ls command to quickly list installed solvers and versions - #672
Open
filipeom wants to merge 1 commit into
Open
Add ls command to quickly list installed solvers and versions#672filipeom wants to merge 1 commit into
ls command to quickly list installed solvers and versions#672filipeom wants to merge 1 commit into
Conversation
📝 WalkthroughSummary by CodeRabbit
WalkthroughThe CLI adds an ChangesSolver listing command
Estimated code review effort: 3 (Moderate) | ~20 minutes Suggested reviewers: 🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 inconclusive)
✅ Passed checks (4 passed)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Member
Author
|
@coderabbitai full review |
✅ Action performedFull review finished. |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@src/bin/cmd_ls.ml`:
- Line 1: Add the repository-required SPDX, copyright, and author header,
followed by a top-level OCaml module documentation comment, before the existing
open Smtml declaration in the new module. Preserve the current module code after
these additions.
In `@src/smtml/solver_type.ml`:
- Around line 36-42: The package_name mapping must remain aligned with
statically linked library names: keep Colibri2_solver mapped to colibrilib and
update the package_name interface in src/smtml/solver_type.ml lines 36-42 and
src/smtml/solver_type.mli lines 42-43 to describe a statically linked-library
name, documenting that None means no linked library and Some contains the name
passed to Build_info.V1.Statically_linked_libraries.find.
In `@src/smtml/solver_type.mli`:
- Around line 42-43: The public package_name declaration needs complete contract
documentation. Update the package_name documentation in solver_type.mli with an
`@param` entry for the solver, an `@return` entry describing Some as the
Smtml.Statically_linked_library identifier used by Build_info and None for
solvers without one, while preserving the existing signature.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Path: .coderabbit.yaml
Review profile: CHILL
Plan: Pro Plus
Run ID: e5212bd7-584a-4220-9731-b1d44e953ca2
📒 Files selected for processing (4)
src/bin/cli.mlsrc/bin/cmd_ls.mlsrc/smtml/solver_type.mlsrc/smtml/solver_type.mli
| @@ -0,0 +1,35 @@ | |||
| open Smtml | |||
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick win
Add the required file header and module documentation.
This new OCaml module starts with open Smtml and has no required header or top-level (** ... *) comment. Add both before the code.
Suggested header
+(* SPDX-License-Identifier: MIT *)
+(* Copyright (C) 2023-2026 formalsec *)
+(* Written by the Smtml programmers *)
+
+(** List solver availability and linked-library version information. *)
open SmtmlAs per path instructions, every new .ml file must include the SPDX, copyright, author header, and a top-level module documentation comment. Based on learnings, new OCaml modules in this repository follow the same documentation convention.
📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| open Smtml | |
| (* SPDX-License-Identifier: MIT *) | |
| (* Copyright (C) 2023-2026 formalsec *) | |
| (* Written by the Smtml programmers *) | |
| (** List solver availability and linked-library version information. *) | |
| open Smtml |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/bin/cmd_ls.ml` at line 1, Add the repository-required SPDX, copyright,
and author header, followed by a top-level OCaml module documentation comment,
before the existing open Smtml declaration in the new module. Preserve the
current module code after these additions.
Sources: Path instructions, Learnings
Comment on lines
+36
to
+42
| let package_name = function | ||
| | Z3_solver -> Some "z3" | ||
| | Bitwuzla_solver -> Some "bitwuzla-cxx" | ||
| | Colibri2_solver -> Some "colibrilib" | ||
| | Cvc5_solver -> Some "cvc5" | ||
| | Altergo_solver -> Some "alt-ergo-lib" | ||
| | Smtzilla_solver -> None |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== files =="
git ls-files | rg '(^|/)solver_type\.(ml|mli)$|(^|/)dune$|cmd_ls\.ml|build_info|lib'
echo
echo "== solver_type excerpts =="
for f in src/smtml/solver_type.ml src/smtml/solver_type.mli; do
echo "--- $f ---"
nl -ba "$f" | sed -n '1,120p'
done
echo
echo "== searches for package_name / Colibri2 / linked libraries =="
rg -n "package_name|Colibri2|colibri2|colibrilib|Statically_linked_libraries|dune-build-info|Build_info|Cmd_ls|cmd_ls|install" -S .
echo
echo "== relevant dune files candidates =="
git ls-files | rg '(^|/)dune$' | while read -r f; do
if rg -n "colibri2|Colibri2|Package|solver|Smtml|Build_info" "$f" >/dev/null; then
echo "--- $f ---"
nl -ba "$f" | sed -n '1,220p'
fi
doneRepository: formalsec/smtml
Length of output: 821
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== repo root dune-build-info refs =="
rg -n "dune-build-info|Build_info" -S .
echo
echo "== opam package refs =="
git ls-files | rg '(^|/)smtml\.opam$|\.opam$' | while read -r f; do
if rg -n "colibri2|Colibri2|colibrilib|bitwuzla|z3|cvc5|alt-ergo|smtzilla" "$f" >/dev/null; then
echo "--- $f ---"
rg -n "colibri2|Colibri2|colibrilib|bitwuzla|z3|cvc5|alt-ergo|smtzilla" "$f"
fi
done
echo
echo "== source identifiers around cmd_ls for availability =="
for f in src/bin/cmd_ls.ml; do
if [ -f "$f" ]; then
echo "--- $f ---"
nl -ba "$f" | sed -n '1,140p'
fi
doneRepository: formalsec/smtml
Length of output: 1830
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== candidate file sizes =="
wc -l src/smtml/solver_type.ml src/smtml/solver_type.mli src/bin/cmd_ls.ml src/smtml/dune dune-project smtml.opam 2>/dev/null || true
echo
echo "== solver_type.ml with cat =="
cat -n src/smtml/solver_type.ml | sed -n '1,140p'
echo
echo "== solver_type.mli with cat =="
cat -n src/smtml/solver_type.mli | sed -n '1,140p'
echo
echo "== src/smtml/dune with cat =="
cat -n src/smtml/dune | sed -n '1,240p'
echo
echo "== src/bin/cmd_ls.ml with cat =="
cat -n src/bin/cmd_ls.ml | sed -n '1,100p'
echo
echo "== dune-project build-info refs with cat =="
cat -n dune-project | sed -n '55,75p'
echo
echo "== smtml.opam deps refs with cat =="
cat -n smtml.opam | sed -n '55,105p'Repository: formalsec/smtml
Length of output: 13353
Keep package_name on the linked-library side.
package_name is used as the argument to Build_info.V1.Statically_linked_libraries.find, and dune-project declares the colibrilib static library dependency, so return colibrilib consistently. Change the interface to describe it as a statically linked-library name and document the None/Some contract.
📍 Affects 2 files
src/smtml/solver_type.ml#L36-L42(this comment)src/smtml/solver_type.mli#L42-L43
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/smtml/solver_type.ml` around lines 36 - 42, The package_name mapping must
remain aligned with statically linked library names: keep Colibri2_solver mapped
to colibrilib and update the package_name interface in src/smtml/solver_type.ml
lines 36-42 and src/smtml/solver_type.mli lines 42-43 to describe a statically
linked-library name, documenting that None means no linked library and Some
contains the name passed to Build_info.V1.Statically_linked_libraries.find.
Comment on lines
+42
to
+43
| (** [package_name solver] opam repo package name of the solver *) | ||
| val package_name : t -> string option |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== files =="
git ls-files | rg '(^|/)solver_type\.(ml|mli)$|src/smtml' | head -100
echo "== target file excerpt =="
if [ -f src/smtml/solver_type.mli ]; then
wc -l src/smtml/solver_type.mli
cat -n src/smtml/solver_type.mli | sed -n '1,90p'
fi
echo "== implementation and usages =="
if [ -f src/smtml/solver_type.ml ]; then
wc -l src/smtml/solver_type.ml
cat -n src/smtml/solver_type.ml | sed -n '1,180p'
fi
rg -n "package_name|Build_info|opam|linked-library|linked-library" -S .
echo "== local odoc compliance patterns in mli headers =="
fd -e mli . src | head -100 | while read f; do
echo "--- $f"
head -80 "$f"
doneRepository: formalsec/smtml
Length of output: 50371
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== cmd_ls excerpt =="
if [ -f src/bin/cmd_ls.ml ]; then
wc -l src/bin/cmd_ls.ml
cat -n src/bin/cmd_ls.ml | sed -n '1,80p'
fi
echo "== package_name returns / option handling =="
python3 - <<'PY'
from pathlib import Path
import re
ml = Path("src/smtml/solver_type.ml").read_text()
mli = Path("src/smtml/solver_type.mli").read_text()
cm = Path("src/bin/cmd_ls.ml").read_text()
print("module_comment_has_odoc_tags = {}".format("(`@param` solver" in mri if (mri := re.search(r'\(\*\* \[package_name solver\] (.*)\nval package_name', mli, re.S)) else False))
print("returns_documented = {}".format(bool(re.search(r'\breturns\b|Returns\b', mri.group(1)) if (mri := re.search(r'\(\*\* \[package_name solver\] (.*)\nval package_name', mli, re.S)) else False)))
print("param_documented = {}".format("(`@param` solver" in mli))
print("return_documented = {}".format("(`@return`" in mli))
print("none_case_documented = {}".format,bool(re.search(r'None\b|no linked-library|linked-library|package', mri.group(1)) if (mri := re.search(r'\(\*\* \[package_name solver\] (.*)\nval package_name', mli, re.S)) else False))
impl = re.search(r'let package_name = function?\n(.*)\n[^ ]', ml, re.S).group(1)
print("implementation_smtzilla_returns_none = {}".format("(Smtzilla_solver) -> None" in impl))
print("implementation_all_others_some_literal_identifiers = {}".format(re.search(r'Z3_solver -> Some "([^"]+)"', impl).group(1) in ["z3"] and "bitwuzla-cxx" in impl and "colibrilib" in impl and "cvc5" in impl and "alt-ergo-lib" in impl))
use = re.search(r'match Solver_type.package_name solv_ty with?\n(.*?)\n((?:[^-]|\s)+)end', cm, re.S)
print("cmd_ls_uses_build_info_statically_linked_libraries = {}".format(True if use and "Build_info.V1.Statically_linked_libraries.find" in use.group(1) else False))
PYRepository: formalsec/smtml
Length of output: 1759
🏁 Script executed:
#!/bin/bash
set -euo pipefail
python3 - <<'PY'
from pathlib import Path
import re
ml = Path("src/smtml/solver_type.ml").read_text()
mli = Path("src/smtml/solver_type.mli").read_text()
cm = Path("src/bin/cmd_ls.ml").read_text()
mri = re.search(r'\(\*\* \[package_name solver\] (.*)\nval package_name', mli, re.S)
mcomment = mri.group(1) if mri else ""
print("function_comment =", mcomment.strip().replace("\n", " "))
print("function_comment_has_returns = ", bool(re.search(r'\breturns\b|Returns\b', mcomment, re.I)))
print("function_comment_has_param_tag = ", "`@param` solver" in mcomment)
print("function_comment_has_return_tag = ", "`@return`" in mcomment)
print("function_comment_mentions_none = ", bool(re.search(r'\bNone\b|no\s+linked-library|linked-library|package', mcomment)))
impl = re.search(r'let package_name = function\s*\n(.*?)\n[^ ]', ml, re.S).group(1)
print("smtzilla_returns_none = ", bool(re.search(r'smtzilla_solver->\s*None\s*$', impl)))
print("all_some_return_one_literal = ", bool(re.search(r'(?:Z3_solver|bitwuzla-cxx|colibrilib|cvc5|alt-ergo-lib)->\s*Some', impl)))
use = re.search(r'match Solver_type\.package_name solv_ty with\s*\n(.*?)\n((?:[^-]|\s)+?)end', cm, re.S)
print("uses_build_info_find = ", bool(use and "Build_info.V1.Statically_linked_libraries.find" in use.group(1)))
PYRepository: formalsec/smtml
Length of output: 467
Complete the public package_name contract.
The solver_type.mli declaration lacks @param and @return, and its description does not convey the None, Some "..." behavior. Document the returned string as a Smtml.Statically_linked_library identifier used by Build_info, or as a None for solvers without one, so future calls match the public contract.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@src/smtml/solver_type.mli` around lines 42 - 43, The public package_name
declaration needs complete contract documentation. Update the package_name
documentation in solver_type.mli with an `@param` entry for the solver, an `@return`
entry describing Some as the Smtml.Statically_linked_library identifier used by
Build_info and None for solvers without one, while preserving the existing
signature.
Source: Path instructions
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.