[BUILD] Migrate the Z3 dependency to mlc-z3-static - #20084
Open
Ubospica wants to merge 2 commits into
Open
Conversation
mlc-ai/package#110 folded the z3-static wheel into mlc-z3-static (import module mlc_z3_static, versions restart at 4.16.0 without the .post1 suffix). Point the Z3 toolchain references at the new package: - cmake/modules/contrib/Z3.cmake probes mlc_z3_static.config first and keeps the legacy z3_static.config probe as a fallback so existing environments and CI images keep working during the transition. - The pyproject.toml build requirement becomes mlc-z3-static>=4.16.0. - The CI docker image installs mlc-z3-static==4.16.0. mlc-z3-static must be published to PyPI before the CI docker images are rebuilt or wheels are built from this revision.
Contributor
|
Caution The consumer version of Gemini Code Assist on GitHub has been sunset. All code review activity has officially ceased. |
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
1 participant
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
mlc-ai/package#110 folded the
z3-staticwheel intomlc-z3-static(import modulemlc_z3_static; versions restart at 4.16.0 without the.post1suffix). This PR points TVM's Z3 toolchain references at the new package:cmake/modules/contrib/Z3.cmakeprobesmlc_z3_static.configfirst and keeps the legacyz3_static.configprobe as a fallback, so existing environments and the current CI images keep working during the transition.pyproject.tomlbuild requirement becomesmlc-z3-static>=4.16.0.mlc-z3-static==4.16.0.Note:
mlc-z3-staticis not on PyPI yet. This PR should land only after the wheel is published; the CMake fallback keeps current CI images working, but docker image rebuilds andpyproject.toml-based wheel builds need the package on PyPI.Verification
Since the wheel is not yet on PyPI, it was built locally from mlc-ai/package
main(254413e, the #110 merge commit) and its bundled smoke test passed (static and shared consumers compile, link, and solve).mlc_z3_staticand legacyz3_staticinstalled,USE_Z3=ONauto-detection linksmlc_z3_static/static/lib/libz3.a(new package preferred).z3-staticpackage installed, the fallback probe still finds it.libtvm_compiler.so, no runtimelibz3dependency (ldd).tests/python/arith/test_arith_z3.py: 52 passed.tests/python/arith/suite on the same toolchain: 1034 passed, 2 skipped, 26 xfailed.bash -non the docker install script passes.