fix(docker): add openshell-prover to Dockerfile skeleton stages and provide z3#800
Open
johntmyers wants to merge 8 commits intomainfrom
Open
fix(docker): add openshell-prover to Dockerfile skeleton stages and provide z3#800johntmyers wants to merge 8 commits intomainfrom
johntmyers wants to merge 8 commits intomainfrom
Conversation
The openshell-prover crate was added as a dependency of openshell-cli in #741 but the Docker build infrastructure was not updated. Cargo workspace resolution requires every crate manifest to be present even when only building a subset of packages. Add openshell-prover Cargo.toml, mkdir, and stub lib.rs to the skeleton stages of all affected Dockerfiles. Also add the previously missing openshell-policy and openshell-tui entries to the python-wheels Dockerfiles where they were absent.
The openshell-prover crate depends on z3. For Linux-targeted builds (python-wheels), install libz3-dev to link against the system library. For macOS cross-compilation (python-wheels-macos, cli-macos), compile z3 from source via the bundled-z3 feature since system libz3-dev only provides a Linux .so, not a macOS .dylib. Add a bundled-z3 forwarding feature to openshell-cli so both cargo and maturin can activate it uniformly.
…ndgen Switch all CLI builds to bundled-z3 (compile z3 from source) instead of relying on system libz3-dev. This is required because: - Linux musl CLI builds cannot link against glibc libz3.so - macOS cross-compilation has no system z3 available - Distributable Python wheels should not depend on runtime libz3 Add libclang-dev to all CLI Dockerfiles since z3-sys uses bindgen which requires libclang at compile time. Add openshell-prover to the sed workspace scope in both release workflows so Cargo can resolve the path dependency from openshell-cli.
|
🌿 Preview your docs: https://nvidia-preview-pr-800.docs.buildwithfern.com/openshell |
…compiler musl-tools only provides musl-gcc (C compiler wrapper), not musl-g++. The z3 bundled cmake build needs a C++ compiler to compile z3 from source. Use the system g++ since z3 exposes a C-linkage API and libstdc++ is statically linked in the final musl binary.
Using system g++ directly produces object files with glibc symbols like __printf_chk that don't exist in musl. Instead, create a musl-g++ wrapper that mirrors musl-gcc: it invokes g++ with the musl-gcc.specs file, which redirects include and library paths to musl. This ensures z3 compiles against musl headers and avoids glibc symbol references.
The musl-gcc.specs approach strips all system include paths via -nostdinc, which removes C++ standard library headers and breaks std::atomic detection in z3's cmake build. Simpler approach: the only glibc-specific symbols z3 was pulling in were __printf_chk and similar __*_chk functions generated by _FORTIFY_SOURCE hardening. Disabling _FORTIFY_SOURCE makes g++ emit standard printf/memcpy/etc. calls that musl provides, while keeping all C++ headers intact.
pimlock
previously approved these changes
Apr 10, 2026
In Alpine, Rust build scripts are compiled for the musl host target which defaults to static linking. Static musl binaries cannot dlopen, causing bindgen to fail when loading libclang.so for z3 FFI generation. Set CARGO_HOST_RUSTFLAGS="-C target-feature=-crt-static" so build scripts are dynamically linked (can dlopen) while the target CLI binary stays static.
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
3 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.
Summary
The openshell-prover crate was added in #741 as a dependency of openshell-cli but the Docker build infrastructure was not updated, breaking all Docker builds that resolve the workspace.
Related Issue
Regression from #741.
Changes
openshell-proverCargo.toml,mkdir, and stublib.rsto the skeleton stages of all affected Dockerfiles (Dockerfile.images,Dockerfile.python-wheels,Dockerfile.python-wheels-macos,Dockerfile.cli-macos)openshell-policyandopenshell-tuiskeleton entries in the python-wheels Dockerfiles (also path deps of openshell-cli)libz3-devtoDockerfile.python-wheelsfor native Linux z3 linkingcmaketoDockerfile.python-wheels-macosand enable--features bundled-z3on both macOS cross-compile Dockerfiles to compile z3 from source (systemlibz3-devonly provides a Linux.so, not a macOS.dylib)bundled-z3forwarding feature toopenshell-cliso bothcargo buildandmaturin buildcan activate it uniformlyTesting
mise run pre-commitpassesChecklist