Skip to content

chore(build): remove bundled Z3 support - #3275

Open
SDAChess wants to merge 2 commits into
mainfrom
chore/remove-bundled-z3
Open

chore(build): remove bundled Z3 support#3275
SDAChess wants to merge 2 commits into
mainfrom
chore/remove-bundled-z3

Conversation

@SDAChess

Copy link
Copy Markdown
Collaborator

Summary

Remove the unused bundled-z3 feature and its remaining build, test, and documentation references. Builds now use toolchain-provided Z3 on Linux and macOS and the existing prebuilt Z3 path on Windows.

Related Issue

No issue required: mechanical build cleanup removing an unused feature and orphaned build infrastructure.

Changes

  • Remove bundled-z3 feature forwarding from the prover, server, and gateway crates.
  • Remove the Z3 source-build dependency chain from Cargo.lock.
  • Update build and E2E paths to use toolchain-provided Z3.
  • Remove obsolete bundled-Z3 CMake cache cleanup.
  • Remove the unused osxcross macOS Dockerfiles and their Trivy exclusion.
  • Update build, contributor, compute-driver, and Windows documentation.

Testing

  • mise run pre-commit passes
    • Could not start because local mise bootstrapping attempted to build Python without a C compiler.
  • Existing prover unit tests pass (27 passed)
  • Unit tests added/updated
  • E2E tests added/updated (not applicable)
  • cargo check --locked --offline -p openshell-gateway
  • Cargo lockfile checks
  • ShellCheck
  • Markdownlint
  • Agent infrastructure consistency audit
  • No bundled-z3, z3/bundled, or z3-src references remain

Checklist

  • Follows Conventional Commits
  • Commits are signed off (DCO)
  • Architecture docs updated (if applicable)

Signed-off-by: Simon Scatton <sscatton@nvidia.com>
@SDAChess SDAChess self-assigned this Sep 11, 2026
@SDAChess SDAChess added test:e2e Requires end-to-end coverage test:e2e-gpu Requires GPU end-to-end coverage test:e2e-kubernetes Requires Kubernetes end-to-end coverage labels Sep 11, 2026
@github-actions

Copy link
Copy Markdown

@github-actions

Copy link
Copy Markdown

Label test:e2e applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute the standard E2E suite after building the required gateway and supervisor images once. The matching required CI gate status on this PR will flip green automatically once the run finishes.

@github-actions

Copy link
Copy Markdown

Label test:e2e-kubernetes applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute Kubernetes HA and credential-driver E2E after building the required gateway and supervisor images once. This is an optional proof-of-life suite; failures are visible in the workflow run but do not publish a required CI gate status.

@github-actions

Copy link
Copy Markdown

Label test:e2e-gpu applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute GPU E2E after building the required supervisor image once. The matching required CI gate status on this PR will flip green automatically once the run finishes.

Comment thread CONTRIBUTING.md
elezar
elezar previously approved these changes Sep 11, 2026

@elezar elezar left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @SDAChess. Looks OK from my side, but it may be good to get @pimlock or @drew to weigh in here too.

@SDAChess
SDAChess enabled auto-merge September 11, 2026 10:42
@SDAChess
SDAChess added this pull request to the merge queue Sep 11, 2026
@SDAChess
SDAChess removed this pull request from the merge queue due to a manual request Sep 11, 2026
pimlock
pimlock previously approved these changes Sep 11, 2026
@pimlock
pimlock dismissed stale reviews from elezar and themself via 2fd3279 September 11, 2026 16:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

test:e2e Requires end-to-end coverage test:e2e-gpu Requires GPU end-to-end coverage test:e2e-kubernetes Requires Kubernetes end-to-end coverage

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants