Skip to content

fix: use macos-13 for x86_64-apple-darwin, build static Z3 for musl#43

Merged
AkiraTamai merged 1 commit intodevelopfrom
devin/1772814020-fix-cross-compile-ci
Mar 6, 2026
Merged

fix: use macos-13 for x86_64-apple-darwin, build static Z3 for musl#43
AkiraTamai merged 1 commit intodevelopfrom
devin/1772814020-fix-cross-compile-ci

Conversation

@AkiraTamai
Copy link
Copy Markdown
Collaborator

@AkiraTamai AkiraTamai commented Mar 6, 2026

Summary

Fixes the remaining two release CI failures from v0.2.6:

  1. x86_64-apple-darwin: macos-latest now runs on ARM (M-series), so brew install z3 llvm@17 installs arm64 libraries that can't link into an x86_64 binary (ld: warning: ignoring file ... found architecture 'arm64', required architecture 'x86_64'). Fix: pin to macos-13 (last Intel runner).

  2. x86_64-unknown-linux-musl: The musl linker could not find -lz3 because the apt libz3-dev package provides a glibc shared library. Fix: the musl step now installs LLVM 17 from apt and builds Z3 4.13.4 from source as a static library (-DZ3_BUILD_LIBZ3_SHARED=OFF), with the Z3_SYS_Z3_HEADER and Z3_SYS_Z3_LIB_DIR env vars pointing to the static build.

The Ubuntu system deps step now skips for musl targets (!matrix.musl) since the musl step handles all its own dependencies.

Review & Testing Checklist for Human

  • Z3 static build uses mixed compilers (musl-gcc for C, g++ for C++). Z3 is primarily C++, so the resulting static library's C++ portions are compiled with glibc-linked g++. This may cause linker failures when producing the final musl binary if it pulls in glibc symbols or can't resolve libstdc++ statically. If this fails in CI, consider switching to CC=musl-gcc CXX=musl-gcc with -lstdc++ added manually, or building Z3 with the full musl cross-compilation toolchain.
  • LLVM libraries for the musl target are still glibc-based (installed from apt). The v0.2.6 musl error was specifically cannot find -lz3, but the linker also tries to dynamically link -lffi, -lrt, -ldl, -lxml2, -lstdc++ etc. These may fail even after Z3 is fixed. If so, the musl target may need a fundamentally different approach (e.g. cross tool with Docker, or dropping the musl target).
  • Z3 version 4.13.4 compatibility with z3-sys 0.8.1. Verify the pinned Z3 version matches what the Rust z3-sys crate expects. A mismatch could cause compile-time or runtime ABI issues.
  • macos-13 deprecation timeline. GitHub will eventually remove macos-13 runners. This is a short-term fix. Consider future migration strategies (universal binaries, Rosetta-based builds on ARM, or dropping x86_64-apple-darwin).
  • Tag a new release (e.g., v0.2.7) to verify all 5 matrix targets pass CI. This workflow only runs on tag pushes.

Notes


Open with Devin

- x86_64-apple-darwin: switch from macos-latest (ARM M-series) to
  macos-13 (Intel). macos-latest now runs on ARM, so brew installs
  arm64 Z3/LLVM which can't link into x86_64 binaries.

- x86_64-unknown-linux-musl: the musl step now installs LLVM 17 and
  builds Z3 from source as a static library. The previous approach
  relied on libz3-dev from apt (glibc shared lib) which the musl
  linker could not find.

- Ubuntu deps step now skips for musl target (musl has its own
  dedicated step with static Z3 build).

Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
@devin-ai-integration
Copy link
Copy Markdown
Contributor

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

  • Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
  • Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

  • Disable automatic comment and CI monitoring

@AkiraTamai AkiraTamai marked this pull request as ready for review March 6, 2026 16:33
@AkiraTamai AkiraTamai merged commit d7aa64d into develop Mar 6, 2026
Copy link
Copy Markdown
Contributor

@devin-ai-integration devin-ai-integration Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Devin Review found 1 potential issue.

View 4 additional findings in Devin Review.

Open in Devin Review

Comment on lines +71 to +72
-DCMAKE_C_COMPILER=musl-gcc \
-DCMAKE_CXX_COMPILER=g++ \
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🔴 Mixed musl-gcc/g++ compilers will produce Z3 static library with glibc C++ runtime dependencies

The Z3 static build uses CMAKE_C_COMPILER=musl-gcc for C files but CMAKE_CXX_COMPILER=g++ for C++ files. Z3 is primarily a C++ project, so most of the object files in the resulting static library will be compiled with g++ and will contain references to glibc's libstdc++ and libc symbols. When this static library is later linked into the musl-target Rust binary (cargo build --release --target x86_64-unknown-linux-musl), it will either fail at link time due to glibc/musl symbol conflicts, or produce a binary that is not truly statically linked. Both compilers should use the musl toolchain—for example, CMAKE_CXX_COMPILER=g++ should also be changed to a musl-compatible C++ wrapper, or the entire build should use the system gcc/g++ and rely on static linking with musl at the final Rust link step.

Prompt for agents
In .github/workflows/release.yml, lines 69-73, the cmake configuration for the musl Z3 build uses mixed compilers: musl-gcc for C and g++ for C++. Since Z3 is primarily C++, the resulting static library will contain glibc-linked object files that are incompatible with the musl target.

Two possible fixes:

1. Use the same system gcc/g++ for both and rely on static linking at the cargo level:
   Remove the -DCMAKE_C_COMPILER=musl-gcc line and -DCMAKE_CXX_COMPILER=g++ line entirely (use system defaults), and ensure -DCMAKE_POSITION_INDEPENDENT_CODE=ON is kept. The musl linker invoked by cargo for the x86_64-unknown-linux-musl target will handle static linking.

2. Create a musl-compatible C++ wrapper. For example, create a script musl-g++ that wraps g++ with musl flags, similar to how musl-gcc works, and use -DCMAKE_CXX_COMPILER=musl-g++.

Option 1 is simpler and more commonly used for building static dependencies for musl targets.
Open in Devin Review

Was this helpful? React with 👍 or 👎 to provide feedback.

@AkiraTamai AkiraTamai deleted the devin/1772814020-fix-cross-compile-ci branch March 6, 2026 16:35
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.

1 participant