Skip to content

Bazel: expose z3_static target for working macOS, win32 builds #7660

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.

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
merged 1 commit into from
Jun 3, 2025

Conversation

tsnl
Copy link
Contributor

@tsnl tsnl commented May 26, 2025

The current Bazel build files introduced in #7646 do not work on macOS or Windows. The current implementation expects libz3.so to be produced by the CMake build. However, on macOS and Windows, we produce libz3.dylib and z3.dll respectively.

Updating the Bazel build file to output libz3.dylib on macOS and z3.dll on Windows reveals more issues. On macOS, exposing libz3.dylib is insufficient because running executables linked against this dylib causes a runtime error, complaining that libz3<version>.dylib is not found. (TODO: report test results on Windows)

One solution is to specify both libz3.dylib and libz3<version>.dylib in the list of output shared libraries exposed by the cmake rule in the Bazel build. However, Bazel cannot depend on the contents of a VERSION file to determine CMake's outputs, meaning we'd have to hard-code the current Z3 version in the Bazel file and keep it in-sync with the rest of the project. Brittle.

A simpler workaround is to also expose the statically-linked libraries also produced by Z3. This is what I've done in this PR.


This PR adds the z3_static Bazel target to the BUILD.bazel file. This allows consumption of Z3 as a static library using the Bazel build system. It also unblocks users on macOS and Windows until the default z3_dynamic target can be fixed on those platforms.

@tsnl tsnl marked this pull request as draft May 26, 2025 03:03
@tsnl tsnl force-pushed the master branch 6 times, most recently from ac720cc to 0d44a35 Compare May 26, 2025 03:33
@tsnl tsnl changed the title Fix Bazel build for macOS, Windows Fix Bazel build on macOS, Windows May 26, 2025
@tsnl tsnl changed the title Fix Bazel build on macOS, Windows Bazel: expose z3_static target for working macOS, win32 builds May 26, 2025
@NikolajBjorner
Copy link
Contributor

@smolkaj - can you take a look?

@tsnl
Copy link
Contributor Author

tsnl commented May 27, 2025

@microsoft-github-policy-service agree

@tsnl
Copy link
Contributor Author

tsnl commented May 27, 2025

@smolkaj I have z3_static working on macOS. z3_dynamic doesn't work for me on macOS or Windows as configured.

@NikolajBjorner NikolajBjorner marked this pull request as ready for review May 27, 2025 15:53
@NikolajBjorner
Copy link
Contributor

Is MODULE.bazel.lock added as intended or by accident?

@NikolajBjorner
Copy link
Contributor

However, Bazel cannot depend on the contents of a VERSION file to determine CMake's outputs, meaning we'd have to hard-code the current Z3 version in the Bazel file and keep it in-sync with the rest of the project. Brittle.

Indeed. It already has been bit-rotting to 4.14.0 while current version is 4.15.1.
I update z3's version manually in four different files at the moment. (release.yml, nightly.yml, cmakelists.txt and mk_project.py)
This step can/should be scripted and/or there is something better to do with the scripts that could pick it up from CMakeLists.txt.

@tsnl
Copy link
Contributor Author

tsnl commented Jun 3, 2025

I've removed the MODULE.bazel.lock file. This file can checked in once the Bazel build files stabilize.

@NikolajBjorner, if you can tolerate updating a fifth file when there's a version change, I can update the PR to fix the dynamically-linked targets on macOS. The symmetry between BUILD.bazel and CMakeLists.txt should reduce the cognitive load of remembering to update these files.

Are there any other changes you'd like me to make? I'm happy to take a stab at adding some CI targets for the Bazel toolchain to avoid similar issues cropping up again.

One possible way to automate keeping the versions in sync would be to specify the version when configuring the build. CMake could read the Z3_VERSION variable as a configuration option when generating build files (e.g. cmake .. -GNinja -DZ3_VERSION=4.15.1). We'd need to generate the BUILD.bazel file from a template or by patching it before building, but this shouldn't be too bad, especially with proper tests.

@NikolajBjorner NikolajBjorner merged commit bcedb66 into Z3Prover:master Jun 3, 2025
10 checks passed
@NikolajBjorner
Copy link
Contributor

Thanks, taking the current improvements.
For Bazel, decisions on what to support has to be made by the contributors.
There is no dependency on this for building releases.

@smolkaj
Copy link
Contributor

smolkaj commented Jun 3, 2025

Nice!! Thanks for adding support for Mac and Windows, @tsnl.

Sorry for the silence, I just returned from parental leave.

@smolkaj
Copy link
Contributor

smolkaj commented Jun 3, 2025

On a related note -- I'd like to get Z3 added to the Bazel Central Registry eventually. Though I currently don't have cycles to take up this work myself.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants