diff --git a/test_julia_fix.md b/test_julia_fix.md deleted file mode 100644 index d1b25c0f9..000000000 --- a/test_julia_fix.md +++ /dev/null @@ -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. \ No newline at end of file