From 5f4a7a670448776f2713609bfd6855619db6301b Mon Sep 17 00:00:00 2001 From: pkhodade-NV Date: Wed, 2 Sep 2026 17:22:22 +0530 Subject: [PATCH 1/3] docs: fix Windows bundled-z3 build command in CONTRIBUTING.md 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 --- CONTRIBUTING.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b1a789496f..c4d392e2e9 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -296,11 +296,14 @@ Project requirements: - Rust 1.90+ - Python 3.11+ - Docker (running) +- CMake 4.4.3+ (only required when building with the `bundled-z3` feature) ### Z3 installation -The `openshell-prover` crate links against Z3. On macOS and Linux, install the -system Z3 development package; `z3-sys` discovers it through `pkg-config`. +The `openshell-prover`, `openshell-server`, and `openshell-gateway` crates link +against Z3; `openshell-cli` has no Z3 dependency and does not declare a +`bundled-z3` feature. On macOS and Linux, install the system Z3 development +package; `z3-sys` discovers it through `pkg-config`. ```bash # macOS @@ -314,7 +317,7 @@ sudo dnf install z3-devel ``` If you prefer not to install Z3 system-wide, use the bundled Z3 feature. This -compiles Z3 from source during the Rust build: +compiles Z3 from source during the Rust build and requires CMake 4.4.3+: ```bash cargo build -p openshell-prover --features bundled-z3 @@ -334,7 +337,7 @@ the default search path, set `LIBCLANG_PATH` to the directory containing ```powershell $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\\VC\Tools\Llvm\x64\bin' -cargo build -p openshell-cli --target x86_64-pc-windows-msvc --features bundled-z3 +cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3 ``` To use a local x64 Z3 release with the Windows task wrapper: From f6d7573360a5c32c10927ddd5d2ff17d2572c2f2 Mon Sep 17 00:00:00 2001 From: pkhodade-NV Date: Thu, 3 Sep 2026 13:12:23 +0530 Subject: [PATCH 2/3] docs: address review feedback on bundled-z3 build docs 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 --- CONTRIBUTING.md | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index c4d392e2e9..0253d15fa0 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -296,14 +296,16 @@ Project requirements: - Rust 1.90+ - Python 3.11+ - Docker (running) -- CMake 4.4.3+ (only required when building with the `bundled-z3` feature) +- CMake 3.16+ (only required when building with the `bundled-z3` feature) ### Z3 installation -The `openshell-prover`, `openshell-server`, and `openshell-gateway` crates link -against Z3; `openshell-cli` has no Z3 dependency and does not declare a -`bundled-z3` feature. On macOS and Linux, install the system Z3 development -package; `z3-sys` discovers it through `pkg-config`. +The `openshell-prover` crate links directly against Z3. The `openshell-server` +crate depends on the prover, and the `openshell-gateway` binary crate depends +on `openshell-server` in turn; both forward a `bundled-z3` feature down to +`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on +Z3. On macOS and Linux, install the system Z3 development package; `z3-sys` +discovers it through `pkg-config`. ```bash # macOS @@ -317,7 +319,7 @@ sudo dnf install z3-devel ``` If you prefer not to install Z3 system-wide, use the bundled Z3 feature. This -compiles Z3 from source during the Rust build and requires CMake 4.4.3+: +compiles Z3 from source during the Rust build and requires CMake 3.16+: ```bash cargo build -p openshell-prover --features bundled-z3 @@ -340,7 +342,19 @@ $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\\VC\T cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3 ``` -To use a local x64 Z3 release with the Windows task wrapper: +### Windows full build + +To build the full set of Windows binaries, including `openshell-gateway.exe` +and `openshell.exe`, use the `windows:build:x64` mise task instead of a +single-crate `cargo build`. It builds Z3 from source (bundled) by default: + +```powershell +$env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\\VC\Tools\Llvm\x64\bin' +mise run --skip-tools windows:build:x64 +``` + +To use a local x64 Z3 release instead of the bundled build, set +`Z3_LIBRARY_PATH_OVERRIDE` and `Z3_SYS_Z3_HEADER` before running the task: ```powershell $env:Z3_LIBRARY_PATH_OVERRIDE='C:\path\to\z3-4.16.0-x64-win\bin' From 02193dadcbfee66e9ffb5e8a9011aaaf772325e7 Mon Sep 17 00:00:00 2001 From: pkhodade-NV Date: Thu, 3 Sep 2026 17:13:31 +0530 Subject: [PATCH 3/3] docs: drop unneeded LIBCLANG_PATH from prover-only Windows build 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 --- CONTRIBUTING.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 0253d15fa0..40d51e395d 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -333,12 +333,10 @@ For x86-64 Windows MSVC builds, use one of these Z3 paths: is set. - Bundled Z3: pass `--features bundled-z3` so `z3-sys` builds Z3 from source. -Both Windows paths still require `libclang.dll` for `bindgen`. If LLVM is not on -the default search path, set `LIBCLANG_PATH` to the directory containing -`libclang.dll`. +`openshell-prover` itself has no `bindgen`/`libclang` dependency, so building +just this crate does not require `LIBCLANG_PATH`: ```powershell -$env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\\VC\Tools\Llvm\x64\bin' cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3 ``` @@ -346,7 +344,10 @@ cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundl To build the full set of Windows binaries, including `openshell-gateway.exe` and `openshell.exe`, use the `windows:build:x64` mise task instead of a -single-crate `cargo build`. It builds Z3 from source (bundled) by default: +single-crate `cargo build`. It builds Z3 from source (bundled) by default. A +full build also compiles crates that use `bindgen` (e.g. the MXC driver on +Windows), so it requires `libclang.dll`; if LLVM is not on the default search +path, set `LIBCLANG_PATH` to the directory containing `libclang.dll`: ```powershell $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\\VC\Tools\Llvm\x64\bin'