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

Merge pull request #8541 from Z3Prover/copilot/update-nightly-build-test-process

Browse source 
Add macOS dylib headerpad fix and CI validation
This commit is contained in:
Nikolaj Bjorner 2026-02-08 12:43:45 -08:00 • committed by GitHub
commit 45fd779621
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 330 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

108
.github/workflows/nightly-validation.yml vendored
View file

@ -672,3 +672,111 @@ jobs:
$wheel = Get-ChildItem wheels/*.whl | Select-Object -First 1
pip install $wheel.FullName
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
# ============================================================================
# MACOS DYLIB HEADERPAD VALIDATION
# ============================================================================
validate-macos-headerpad-x64:
name: "Validate macOS x64 dylib headerpad"
runs-on: macos-13
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
timeout-minutes: 30
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS x64 build from release
env:
GH_TOKEN: ${{ github.token }}
run: |
TAG="${{ github.event.inputs.release_tag }}"
if [ -z "$TAG" ]; then
TAG="Nightly"
fi
gh release download $TAG --pattern "*x64-osx*.zip" --dir downloads
- name: Extract build
run: |
cd downloads
unzip *x64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd downloads/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi
validate-macos-headerpad-arm64:
name: "Validate macOS ARM64 dylib headerpad"
runs-on: macos-latest
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
timeout-minutes: 30
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS ARM64 build from release
env:
GH_TOKEN: ${{ github.token }}
run: |
TAG="${{ github.event.inputs.release_tag }}"
if [ -z "$TAG" ]; then
TAG="Nightly"
fi
gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
- name: Extract build
run: |
cd downloads
unzip *arm64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd downloads/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi

104
.github/workflows/nightly.yml vendored
View file

@ -70,6 +70,106 @@ jobs:
path: dist/*.zip
retention-days: 2
# ============================================================================
# VALIDATION STAGE
# ============================================================================
validate-macos-headerpad-x64:
name: "Validate macOS x64 dylib headerpad"
needs: [mac-build-x64]
runs-on: macos-latest
timeout-minutes: 15
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS x64 Build
uses: actions/download-artifact@v7.0.0
with:
name: macOsBuild
path: artifacts
- name: Extract build
run: |
cd artifacts
unzip z3-*-x64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd artifacts/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi
validate-macos-headerpad-arm64:
name: "Validate macOS ARM64 dylib headerpad"
needs: [mac-build-arm64]
runs-on: macos-latest
timeout-minutes: 15
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS ARM64 Build
uses: actions/download-artifact@v7.0.0
with:
name: MacArm64
path: artifacts
- name: Extract build
run: |
cd artifacts
unzip z3-*-arm64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd artifacts/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi
ubuntu-build:
name: "Ubuntu build"
runs-on: ubuntu-latest
@ -562,7 +662,9 @@ jobs:
ubuntu-doc,
python-package,
nuget-package-x64,
nuget-package-x86
nuget-package-x86,
validate-macos-headerpad-x64,
validate-macos-headerpad-arm64
]
runs-on: ubuntu-latest
steps:

104
.github/workflows/release.yml vendored
View file

@ -89,6 +89,106 @@ jobs:
path: dist/*.zip
retention-days: 7
# ============================================================================
# VALIDATION STAGE
# ============================================================================
validate-macos-headerpad-x64:
name: "Validate macOS x64 dylib headerpad"
needs: [mac-build-x64]
runs-on: macos-15
timeout-minutes: 15
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS x64 Build
uses: actions/download-artifact@v7.0.0
with:
name: macOsBuild
path: artifacts
- name: Extract build
run: |
cd artifacts
unzip z3-*-x64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd artifacts/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi
validate-macos-headerpad-arm64:
name: "Validate macOS ARM64 dylib headerpad"
needs: [mac-build-arm64]
runs-on: macos-15
timeout-minutes: 15
steps:
- name: Checkout code
uses: actions/checkout@v6.0.2
- name: Download macOS ARM64 Build
uses: actions/download-artifact@v7.0.0
with:
name: MacArm64
path: artifacts
- name: Extract build
run: |
cd artifacts
unzip z3-*-arm64-osx*.zip
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
- name: Test install_name_tool with headerpad
run: |
cd artifacts/$Z3_DIR/bin
# Get the original install name
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "Original install name: $ORIGINAL_NAME"
# Create a test path with same length as typical setup-z3 usage
# This simulates what setup-z3 does: changing to absolute path
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib"
# Try to change the install name - this will fail if headerpad is insufficient
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
# Verify the change was successful
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
echo "New install name: $NEW_NAME"
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
echo "✓ install_name_tool succeeded - headerpad is sufficient"
else
echo "✗ install_name_tool failed to update install name"
exit 1
fi
ubuntu-build:
name: "Ubuntu build"
runs-on: ubuntu-latest
@ -582,7 +682,9 @@ jobs:
ubuntu-doc,
python-package,
nuget-package-x64,
nuget-package-x86
nuget-package-x86,
validate-macos-headerpad-x64,
validate-macos-headerpad-arm64
]
runs-on: ubuntu-latest
steps:

2
scripts/mk_util.py
View file

@ -2749,8 +2749,6 @@ def mk_config():
CXXFLAGS = '%s -arch arm64' % CXXFLAGS
LDFLAGS = '%s -arch arm64' % LDFLAGS
SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS
# Add header padding for macOS to allow install_name_tool to modify the dylib
# This fixes issues where install_name_tool fails with "larger updated load commands do not fit"
if IS_OSX:
SLIBFLAGS += ' -Wl,-headerpad_max_install_names'

5
src/CMakeLists.txt
View file

@ -155,6 +155,11 @@ endif()
# so that if those are also shared libraries they are referenced by `libz3.so`.
target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
# On macOS, add headerpad for install_name_tool compatibility
if(CMAKE_SYSTEM_NAME STREQUAL "Darwin" AND Z3_BUILD_LIBZ3_SHARED)
target_link_options(libz3 PRIVATE "-Wl,-headerpad_max_install_names")
endif()
################################################################################
# Create include directory with headers for easier developer integration
################################################################################

5
src/api/java/CMakeLists.txt
View file

@ -54,6 +54,11 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
endif()
# FIXME: Should this library have SONAME and VERSION set?
# On macOS, add headerpad for install_name_tool compatibility
if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
endif()
# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")

5
src/api/julia/CMakeLists.txt
View file

@ -39,6 +39,11 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
target_link_options(z3jl PRIVATE "-Wl,-headerpad_max_install_names")
endif()
# On macOS, add headerpad for install_name_tool compatibility
if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
target_link_options(z3jl PRIVATE "-Wl,-headerpad_max_install_names")
endif()
option(Z3_INSTALL_JULIA_BINDINGS "Install Julia bindings when invoking install target" ON)
if(Z3_INSTALL_JULIA_BINDINGS)
install(TARGETS z3jl

3
src/api/ml/CMakeLists.txt
View file

@ -159,8 +159,7 @@ endif()
if( APPLE )
# set(ocaml_rpath "@executable_path/../libz3${so_ext}")
# Add header padding to allow install_name_tool to modify the dylib
# This fixes issues where install_name_tool fails with "larger updated load commands do not fit"
# Add headerpad for install_name_tool compatibility on macOS
list(APPEND c_lib_deps "-ldopt" "-Wl,-headerpad_max_install_names")
elseif( UNIX )
set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}")