mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 12:35:59 +00:00
Code Activity

Fix Julia bindings linker errors on Windows MSVC

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-08-18 01:24:54 +00:00
parent b422e86f16
commit af652c7f6a
1 changed files with 0 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

47
test_julia_fix.md
View file

@ -1,47 +0,0 @@
# Julia Bindings Fix Validation
## Problem
The original issue was that when building Julia bindings on Windows with MSVC, users would get cryptic linker errors like:
```
z3jl.cpp.obj : error LNK2001: unresolved external symbol "__declspec(dllimport) struct jlcxx::CachedDatatype & __cdecl jlcxx::jlcxx_type(class std::type_index)"
...
..\..\..\z3jl.dll : fatal error LNK1120: 22 unresolved externals
```
This happened because:
1. Julia's CxxWrap provides MinGW import libraries (.dll.a files)
2. MSVC cannot link against MinGW import libraries (needs .lib files)
3. No clear error message was provided to users
## Solution Implemented
Added detection logic in `src/api/julia/CMakeLists.txt` that:
1. Detects when MSVC is being used on Windows
2. Checks if the JlCxx library is a MinGW import library (.dll.a)
3. Provides a clear error message with actionable solutions
## How the Fix Works
When `find_package(JlCxx REQUIRED)` finds a MinGW library but MSVC is being used, the build will now fail early with a helpful message:
```
Julia bindings build error: Incompatible CxxWrap library format detected.
The found libcxxwrap_julia library (/path/to/libcxxwrap_julia.dll.a) is a MinGW import library (.dll.a),
but Z3 is being built with MSVC which requires .lib format.
Solutions:
1. Use MinGW/GCC instead of MSVC to build Z3
2. Install a MSVC-compatible version of CxxWrap
3. Disable Julia bindings with -DZ3_BUILD_JULIA_BINDINGS=OFF
For more information, see: https://github.com/JuliaInterop/CxxWrap.jl#compiling-the-c-code
```
## Validation
- ✅ Build system works correctly on Linux/GCC (no impact)
- ✅ CMake build completes successfully
- ✅ All Z3 tests pass
- ✅ Basic Z3 functionality validated
- ✅ Julia bindings are correctly not built when not available
- ✅ Detection logic only triggers on Windows + MSVC combination
The fix provides a much better user experience by catching the incompatibility early and providing clear guidance.