feat(docs): fix Windows bundled-z3 build command in CONTRIBUTING.md - #3141
Merged
Conversation
The Windows MSVC example built openshell-cli with --features bundled-z3, but openshell-cli has no Z3 dependency and does not declare that feature. Point the example at openshell-prover instead, clarify which crates link Z3, and note the CMake 4.4.3+ requirement for building Z3 from source. Fixes #3062 Signed-off-by: pkhodade-NV <pkhodade@nvidia.com>
|
Auto-sync is disabled for draft pull requests in this repository. Workflows must be run manually. Contributors can view more details about this message here. |
Fix the CMake minimum version (3.16, matching the locked z3-src/Z3 4.16.0 CMakeLists.txt, not 4.4.3). Make the Z3 dependency wording more explicit: openshell-prover links Z3 directly, openshell-server depends on the prover, and the openshell-gateway binary crate depends on openshell-server in turn, both forwarding bundled-z3 down to openshell-prover/bundled-z3; openshell-cli has no Z3 dependency. Add a separate Windows full build section using the windows:build:x64 mise task, which produces openshell-gateway.exe and openshell.exe, keeping the existing prover-only cargo build example under Prerequisites for consistency with macOS/Linux. Signed-off-by: pkhodade-NV <pkhodade@nvidia.com>
openshell-prover has no bindgen dependency (z3-sys 0.11.0 only depends on pkg-config and z3-src, which only depends on cmake), so building just that crate does not require libclang. Move the LIBCLANG_PATH requirement to the Windows full build section, where it is actually needed because that build also compiles bindgen-using crates such as the MXC driver. Signed-off-by: pkhodade-NV <pkhodade@nvidia.com>
pkhodade-NV
marked this pull request as ready for review
September 3, 2026 11:46
pkhodade-NV
requested review from
a team,
derekwaynecarr,
mrunalp and
sjenning
as code owners
September 3, 2026 11:46
pkhodade-NV
changed the title
drew
approved these changes
Sep 3, 2026
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
2 participants
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.
The Windows MSVC example built openshell-cli with --features bundled-z3, but openshell-cli has no Z3 dependency and does not declare that feature. Point the example at openshell-prover instead, clarify which crates link Z3, and note the CMake requirement for building Z3 from source.
Fixes #3062
Summary
Windows MSVC build instructions in CONTRIBUTING.md referenced
openshell-cli --features bundled-z3, butopenshell-clihas no Z3 dependency and does not declare that feature, so the documented command fails.Related Issue
Fixes #3062
Changes
openshell-prover(the crate that actually declares the feature) instead ofopenshell-cli.openshell-proverlinks Z3 directly,openshell-serverdepends on the prover, and theopenshell-gatewaybinary crate depends onopenshell-serverin turn, both forwardingbundled-z3down toopenshell-prover/bundled-z3;openshell-clihas no Z3 dependency.bundled-z3feature.windows:build:x64mise task, which producesopenshell-gateway.exeandopenshell.exe, keeping the existing prover-onlycargo buildexample under Prerequisites for consistency with macOS/Linux docs.Testing
Documentation-only change; verified the corrected cargo command references a package (
openshell-prover) that declares thebundled-z3feature in itsCargo.toml, and confirmed the CMake 3.16+ minimum against the locked Z3 4.16.0CMakeLists.txt.mise run pre-commitnot applicable (docs-only Markdown change)Checklist