-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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
Conversation
ac720cc
to
0d44a35
Compare
z3_static
target for working macOS, win32 builds
@smolkaj - can you take a look? |
@microsoft-github-policy-service agree |
@smolkaj I have |
Is MODULE.bazel.lock added as intended or by accident? |
Indeed. It already has been bit-rotting to 4.14.0 while current version is 4.15.1. |
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 |
Thanks, taking the current improvements. |
Nice!! Thanks for adding support for Mac and Windows, @tsnl. Sorry for the silence, I just returned from parental leave. |
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. |
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 producelibz3.dylib
andz3.dll
respectively.Updating the Bazel build file to output
libz3.dylib
on macOS andz3.dll
on Windows reveals more issues. On macOS, exposinglibz3.dylib
is insufficient because running executables linked against this dylib causes a runtime error, complaining thatlibz3<version>.dylib
is not found. (TODO: report test results on Windows)One solution is to specify both
libz3.dylib
andlibz3<version>.dylib
in the list of output shared libraries exposed by thecmake
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 theBUILD.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 defaultz3_dynamic
target can be fixed on those platforms.