doc(Boole): document SMT setup for cvc5 dynlib

Cslib/Languages/Boole/README.md

@@ -17,6 +17,15 @@ Boole and Strata are implemented in Lean 4. Install Lean 4 by following the inst
 Some verification pipelines rely on external SMT solvers. You may use either **cvc5** or **Z3**; the
 examples in this repository assume `cvc5` is available on your `PATH`.
 
+In addition:
+
+- If you run `#eval Strata.Boole.verify "cvc5" <program>`, Lean will try to execute the external
+  `cvc5` binary. Make sure `cvc5` is on your `PATH` when running Lean.
+- If you use `import Smt` (e.g. to run `all_goals smt`), Lean also needs to load cvc5's native
+  bindings at runtime. This requires passing `--load-dynlib` to Lean (see below).
+- If you ran `lake update`, you likely already have a suitable `cvc5` binary under
+  `.lake/packages/cvc5`; `scripts/boole-smt.sh` can help run Lean with the right setup.
+
 ## Build Instructions
 
 Clone the `Boole-sandbox` branch of CSLib:
@@ -121,6 +130,15 @@ To invoke the SMT-based pipeline, add the following line:
 #eval Strata.Boole.verify "cvc5" maxExample
 ```
 
+If you are using the cvc5 binary vendored via Lake (under `.lake/packages/cvc5`), the easiest way
+to run a Boole file with the right environment is:
+
+```bash
+./scripts/boole-smt.sh Cslib/Languages/Boole/examples/MaxExample.lean
+```
+
+(Manual setup is also possible; the exact `cvc5` binary path is platform-dependent.)
+
 You should see output similar to the following in Lean's InfoView:
 
 ```
@@ -187,4 +205,17 @@ To use it, ensure you import:
 import Smt
 ```
 
-The full example is available in [`MaxExample.lean`](MaxExample.lean).
+To run files that import `Smt`, you may need to pass `--load-dynlib` so Lean can load cvc5's native
+bindings. For convenience, `scripts/boole-smt.sh` attempts to set up `PATH` and `--load-dynlib`
+automatically:
+
+```bash
+./scripts/boole-smt.sh Cslib/Languages/Boole/examples/MaxExample.lean
+```
+
+VS Code note: the `--load-dynlib` requirement is not VS Code-specific; it applies to any way of
+running Lean that loads and executes `Smt` code. If you want this to work in the editor, configure
+your Lean server to start with that extra argument (and ensure `cvc5` is on `PATH`, e.g. by starting
+VS Code from a shell where it is set).
+
+The full example is available in [`MaxExample.lean`](examples/MaxExample.lean).

scripts/README.md

@@ -55,3 +55,8 @@ to learn about it as well!
   ```bash
   bash scripts/weekly_lint_report.sh <output_file> <sha> <repo> <run_id>
   ```
+
+**Boole / SMT**
+- `boole-smt.sh`
+  Runs `lake env lean` with a best-effort setup for Boole/Strata SMT workflows: it tries to put the vendored
+  `cvc5` binary on `PATH` and to pass `--load-dynlib` for cvc5's native bindings (needed for `import Smt`).

scripts/boole-smt.sh

@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+usage() {
+  cat <<'EOF'
+Usage:
+  ./scripts/boole-smt.sh <file.lean> [lean_args...]
+
+Runs `lake env lean` with:
+  - `cvc5` added to PATH (from `.lake/packages/cvc5/.../bin` if available)
+  - `--load-dynlib` pointing at the built cvc5 Lean bindings (if available)
+
+This is useful for Boole/Strata examples that use:
+  - `#eval Strata.Boole.verify "cvc5" ...` (needs `cvc5` on PATH)
+  - `import Smt` / `smt` tactic (needs `--load-dynlib`)
+
+Notes:
+  - `<file.lean>` may be given as an absolute path, or as a path relative to the
+    repository root.
+EOF
+}
+
+if [[ "${1:-}" == "-h" ]] || [[ "${1:-}" == "--help" ]]; then
+  usage
+  exit 0
+fi
+if [[ $# -lt 1 ]]; then
+  usage
+  exit 2
+fi
+
+ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+FILE_ARG="$1"
+shift
+
+FILE="$FILE_ARG"
+if [[ "$FILE_ARG" != /* ]]; then
+  FILE="$ROOT/$FILE_ARG"
+fi
+
+if [[ ! -e "$FILE" ]]; then
+  echo "error: file not found: $FILE_ARG" >&2
+  exit 2
+fi
+
+DYNLIB_DIR="$ROOT/.lake/packages/cvc5/.lake/build/lib"
+DYNLIB=""
+if [[ -d "$DYNLIB_DIR" ]]; then
+  DYNLIB="$(ls -1 "$DYNLIB_DIR"/libcvc5_cvc5.* 2>/dev/null | head -n 1 || true)"
+fi
+
+LOAD_DYNLIB_ARGS=()
+if [[ -n "$DYNLIB" ]]; then
+  LOAD_DYNLIB_ARGS=(--load-dynlib="$DYNLIB")
+else
+  echo "warning: could not find cvc5 dynlib under $DYNLIB_DIR" >&2
+  echo "warning: files that use `import Smt` / the `smt` tactic may fail." >&2
+  echo "hint: run \`lake build Smt\` (or \`lake build\`) to build it." >&2
+fi
+
+CVC5_BIN_DIR=""
+while IFS= read -r -d '' cand; do
+  CVC5_BIN_DIR="$(dirname "$cand")"
+  break
+done < <(find "$ROOT/.lake/packages/cvc5" -maxdepth 4 -type f -name cvc5 -path '*/bin/cvc5' -print0 2>/dev/null || true)
+
+if [[ -n "$CVC5_BIN_DIR" ]]; then
+  export PATH="$CVC5_BIN_DIR:$PATH"
+else
+  echo "warning: could not find a `cvc5` binary under $ROOT/.lake/packages/cvc5" >&2
+  echo "warning: `#eval Strata.Boole.verify \"cvc5\" ...` may fail unless `cvc5` is on PATH." >&2
+fi
+
+exec lake -d "$ROOT" env lean "${LOAD_DYNLIB_ARGS[@]}" "$FILE" "$@"