doc(Boole): document SMT setup for cvc5 dynlib

[Robertboy18]

While working on Boole examples, I tried to run the README’s “Lean-based verification” workflow (import Smt / all_goals smt) and also the SMT pipeline (#eval Strata.Boole.verify "cvc5" ...). I ran into a couple of practical setup issues that aren’t currently spelled out in the docs, so this PR updates the README to make the “it just works” path clearer.

What I ran into

• #eval Strata.Boole.verify "cvc5" ... executes an external cvc5 binary, so it fails unless cvc5 is on PATH.
• For import Smt / the smt tactic, Lean needs to load cvc5’s native bindings at runtime; without passing --load-dynlib you can hit missing native-implementation errors. This isn’t VS Code-specific — it affects any way of running Lean.

What this PR does

• Updates Cslib/Languages/Boole/README.md to document these requirements explicitly (and to clarify the difference between “cvc5 on PATH” vs “load the dynlib for import Smt”).
• Adds a small helper script scripts/boole-smt.sh that runs lake env lean with best-effort setup:
  • prepends the vendored cvc5 binary from .lake/packages/cvc5/**/bin/cvc5 to PATH when available
  • passes --load-dynlib when the built cvc5 dynlib exists under .lake/packages/cvc5/.lake/build/lib
  • prints warnings/hints when either piece can’t be found

Testing

• Manual: ./scripts/boole-smt.sh Cslib/Languages/Boole/examples/MaxExample.lean (after the cvc5 package and dynlib are built).

[Copilot]

Pull request overview

Improves the Boole documentation and developer workflow for SMT-backed verification by clarifying the runtime requirements for cvc5 (binary on PATH vs. dynlib loading for import Smt) and providing a helper script to run Lean with the appropriate environment.

Changes:

• Document cvc5 runtime requirements for #eval Strata.Boole.verify "cvc5" ... and for import Smt / smt.
• Add scripts/boole-smt.sh to best-effort configure PATH and --load-dynlib when running lake env lean on a Boole example.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.

File	Description
scripts/boole-smt.sh	New helper script to run Lean with cvc5 PATH and dynlib loading set up.
Cslib/Languages/Boole/README.md	Expanded Boole README to explain cvc5 setup and point to the helper script for a smoother workflow.

[Robertboy18]

Addressed Copilot review items:

• scripts/boole-smt.sh: make it work when invoked outside the repo root by using lake -d "$ROOT" ... and resolving relative file paths against the repo root.
• scripts/boole-smt.sh: -h/--help now exits 0; missing args still exit 2.
• Documented scripts/boole-smt.sh in scripts/README.md.
• Fixed the Boole README link to MaxExample.lean (examples/MaxExample.lean).