mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 10:35:36 +00:00
Code Activity

Delete .github/workflows/README-macos-headerpad.md

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-02-08 11:25:40 -08:00 • committed by GitHub
parent e685ea45ed
commit 8c3aefca93
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

88
.github/workflows/README-macos-headerpad.md vendored
View file

@ -1,88 +0,0 @@
# macOS Dylib Header Padding Validation
## Background
Release 4.15.5 broke `install_name_tool` on macOS with "larger updated load commands do not fit" errors. The Mach-O dylib headers lacked sufficient padding for install name modifications.
See:
- Issue: https://github.com/Z3Prover/z3/issues/8532
- Fix: https://github.com/Z3Prover/z3/pull/8535
## The Problem
macOS dynamic libraries (dylibs) have a Mach-O header that includes "load commands" specifying various metadata, including the library's install name. Tools like `install_name_tool` can modify these load commands to change paths.
However, if the header doesn't have sufficient padding, modifying the install name to a longer path will fail with:
```
error: changing install names or rpaths can't be redone for: libz3.dylib (for architecture arm64)
because larger updated load commands do not fit (the program must be relinked,
and you may need to use -headerpad or -headerpad_max_install_names)
```
This breaks tools like [setup-z3](https://github.com/cda-tum/setup-z3) which need to modify the install name to absolute paths in CI environments.
## The Solution
### Build-Time Fix
The Z3 build system now unconditionally adds `-Wl,-headerpad_max_install_names` when building shared libraries on macOS:
- **Python build system**: Modified `scripts/mk_util.py` to apply the flag unconditionally (not just when ML bindings are enabled)
- **CMake build system**: Added `target_link_options` to all macOS shared libraries (libz3, z3java, z3jl, OCaml bindings)
### Validation Jobs
To prevent this issue from recurring, we've added validation jobs to the CI/CD pipeline that test whether `install_name_tool` can successfully modify the dylib install names.
#### Workflows with Validation
1. **nightly.yml** - Nightly builds
- `validate-macos-headerpad-x64`: Validates x64 macOS builds
- `validate-macos-headerpad-arm64`: Validates ARM64 macOS builds
- These jobs run after the build stage and before deployment
2. **release.yml** - Release builds
- `validate-macos-headerpad-x64`: Validates x64 macOS builds
- `validate-macos-headerpad-arm64`: Validates ARM64 macOS builds
- These jobs run after the build stage and before publication
3. **nightly-validation.yml** - Post-deployment validation
- `validate-macos-headerpad-x64`: Validates published x64 builds
- `validate-macos-headerpad-arm64`: Validates published ARM64 builds
- These jobs run after releases are published to verify the artifacts
#### How Validation Works
Each validation job:
1. Downloads the macOS build artifact
2. Extracts the zip file and locates `libz3.dylib`
3. Uses `otool -D` to read the current install name
4. Attempts to change the install name to a long path similar to what setup-z3 uses:
```
/Users/runner/hostedtoolcache/z3/latest/x64/z3-4.15.5-x64-osx-15.7.3/bin/libz3.dylib
```
5. Verifies the change succeeded
6. Fails the build if headerpad is insufficient
#### Test Path Selection
The validation uses paths that match the length and structure of real-world usage by setup-z3. The actual test paths used are:
- x64: `/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib`
- ARM64: `/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib`
These paths are representative of the GitHub Actions hosted tool cache paths. For example, setup-z3 might use paths like:
- `/Users/runner/hostedtoolcache/z3/latest/x64/z3-4.15.5-x64-osx-15.7.3/bin/libz3.dylib`
The test paths use `z3-test-dir` instead of actual version numbers to remain version-agnostic while maintaining the same path length characteristics.
## Impact
With these validations in place:
- Releases with insufficient header padding will fail CI before publication
- Users won't encounter `install_name_tool` errors when using Z3 in CI
- The issue can be detected and fixed immediately during development
## References
- Original issue: https://github.com/Z3Prover/z3/issues/8532
- Fix PR: https://github.com/Z3Prover/z3/pull/8535
- Previous similar issue: https://github.com/Z3Prover/z3/pull/7623
- setup-z3 action: https://github.com/cda-tum/setup-z3