Add z3-static publishing and enable static Z3 wheel builds#103
Merged
Conversation
TVM resolves Z3 from the PyPI z3-staticlib package (PIC static libz3 + headers) declared as a build-system requirement in its pyproject.toml, so USE_Z3=ON links Z3 statically and the wheel gains no shared libz3 dependency. No auditwheel changes are needed.
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request updates the scripts/build_mlc_ai_wheel_manylinux.sh script to enable Z3 in the CMake configuration (USE_Z3 ON), noting that Z3 is linked statically from the z3-staticlib build requirement. There are no review comments to address, and I have no additional feedback to provide.
Important
The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.
Add a packages/z3-staticlib subproject that builds upstream Z3 into py3-none platform wheels containing headers, CMake package files, and a PIC static library. Also align manylinux TVM/MLC-LLM builds on gcc-toolset-13 and raise macOS deployment targets to 14.0 so the static Z3 artifacts are consumed with a compatible toolchain.
Ubospica
changed the title
Use the workflow-provided STATICLIB_Z3_TAG as the Python distribution version so future Z3 static wheel releases keep package metadata aligned with the upstream Z3 artifact version.
Replace the setuptools setup.py subclass with a scikit-build-core/CMake build that stages the static Z3 artifacts through the existing builder script. Remove the copy_wheel helper in favor of cibuildwheel's direct no-op copy command, and stamp the dynamic package version from the selected upstream Z3 tag.
tqchen
approved these changes
Jun 11, 2026
Ubospica
changed the title
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.
Summary
packages/z3-static, a scikit-build-core Python package that builds upstream Z3 intopy3-none-<platform>wheels containing headers, CMake package files, and a PIC static library. Z3 source is downloaded by the builder script from the requested upstream tag and is not checked into this repository.Publish Z3 static wheelsworkflow for Linux x86_64/aarch64, macOS arm64/x86_64, Windows AMD64, and sdist artifacts, with optional PyPI trusted publishing under the MLC AI account.gcc-toolset-13, matching the plannedz3-staticLinux toolchain, and raise macOS deployment targets to 14.0 before consuming static Z3 artifacts.USE_Z3in the TVM manylinux wheel build so TVM can statically link Z3 once thez3-staticwheels are published.Verification
z3-staticsdist locally with scikit-build-core without triggering a Z3 source build.STATICLIB_Z3_ALLOW_SOURCE_BUILD=1fails fast instead of compiling Z3 implicitly.z3_static/__init__.py,z3_static/_version.py, and the helper scripts.