Skip to content

feat(docs): fix Windows bundled-z3 build command in CONTRIBUTING.md #3141

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
drew merged 3 commits into from
Sep 3, 2026
+26 −8
Merged

feat(docs): fix Windows bundled-z3 build command in CONTRIBUTING.md #3141

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5f4a7a6
docs: fix Windows bundled-z3 build command in CONTRIBUTING.md
pkhodade-NV Sep 2, 2026
f6d7573
docs: address review feedback on bundled-z3 build docs
pkhodade-NV Sep 3, 2026
02193da
docs: drop unneeded LIBCLANG_PATH from prover-only Windows build
pkhodade-NV Sep 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 26 additions & 8 deletions CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -296,11 +296,16 @@ Project requirements:
- Rust 1.90+
- Python 3.11+
- Docker (running)
- CMake 3.16+ (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` 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
Expand All @@ -314,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:
compiles Z3 from source during the Rust build and requires CMake 3.16+:

```bash
cargo build -p openshell-prover --features bundled-z3
Expand All @@ -328,16 +333,29 @@ 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
cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3
```

### 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. 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\<Edition>\VC\Tools\Llvm\x64\bin'
cargo build -p openshell-cli --target x86_64-pc-windows-msvc --features bundled-z3
mise run --skip-tools windows:build:x64
```

To use a local x64 Z3 release with the Windows task wrapper:
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'
Expand Down
Loading