doc(Boole): document SMT setup for cvc5 dynlib#389
Open
Robertboy18 wants to merge 2 commits intoleanprover:Boole-sandboxfrom
Open
doc(Boole): document SMT setup for cvc5 dynlib#389Robertboy18 wants to merge 2 commits intoleanprover:Boole-sandboxfrom
Robertboy18 wants to merge 2 commits intoleanprover:Boole-sandboxfrom
Conversation
Robertboy18
requested review from
chenson2018,
fmontesi and
kim-em
as code owners
There was a problem hiding this comment.
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 forimport Smt/smt. - Add
scripts/boole-smt.shto best-effort configurePATHand--load-dynlibwhen runninglake env leanon 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. |
Author
|
Addressed Copilot review items:
|
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
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.
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 externalcvc5binary, so it fails unlesscvc5is onPATH.import Smt/ thesmttactic, Lean needs to load cvc5’s native bindings at runtime; without passing--load-dynlibyou can hit missing native-implementation errors. This isn’t VS Code-specific — it affects any way of running Lean.What this PR does
Cslib/Languages/Boole/README.mdto document these requirements explicitly (and to clarify the difference between “cvc5 on PATH” vs “load the dynlib forimport Smt”).scripts/boole-smt.shthat runslake env leanwith best-effort setup:cvc5binary from.lake/packages/cvc5/**/bin/cvc5toPATHwhen available--load-dynlibwhen the built cvc5 dynlib exists under.lake/packages/cvc5/.lake/build/libTesting
./scripts/boole-smt.sh Cslib/Languages/Boole/examples/MaxExample.lean(after the cvc5 package and dynlib are built).