From 8c3aefca932c120cb3790e00ae920e6a18e1f9b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Feb 2026 11:25:40 -0800 Subject: [PATCH] Delete .github/workflows/README-macos-headerpad.md --- .github/workflows/README-macos-headerpad.md | 88 --------------------- 1 file changed, 88 deletions(-) delete mode 100644 .github/workflows/README-macos-headerpad.md diff --git a/.github/workflows/README-macos-headerpad.md b/.github/workflows/README-macos-headerpad.md deleted file mode 100644 index dad0360b2..000000000 --- a/.github/workflows/README-macos-headerpad.md +++ /dev/null @@ -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