Skip to content

Commit e7d236a

Browse files
Fix native CI: use leanc for ABI-compatible FFI build
Lean's linker uses its own sysroot + libc++. Building the FFI library with system GCC (libstdc++) causes ABI mismatches (__libc_csu_fini, std::__cxx11::basic_string undefined symbols). - CI: use leanc as cmake compiler with STATIC_LIBRARY try-compile - lakefile.lean: remove -lstdc++/-lgcc_s, add -lzmq for system ZMQ
1 parent 2913fff commit e7d236a

File tree

2 files changed

+13
-4
lines changed

2 files changed

+13
-4
lines changed

.github/workflows/ci.yml

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,13 @@ jobs:
3838

3939
- name: Build C++ FFI library
4040
run: |
41-
cmake -S . -B build-cmake
41+
# Use leanc (Lean's clang wrapper) so the FFI library uses libc++,
42+
# matching Lean's linker ABI. STATIC_LIBRARY skips cmake link tests
43+
# that fail with leanc's custom sysroot.
44+
cmake -S . -B build-cmake \
45+
-DCMAKE_C_COMPILER=leanc \
46+
-DCMAKE_CXX_COMPILER=leanc \
47+
-DCMAKE_TRY_COMPILE_TARGET_TYPE=STATIC_LIBRARY
4248
cmake --build build-cmake
4349
4450
- name: Build Lean kernel

lakefile.lean

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -42,15 +42,18 @@ lean_exe xlean where
4242
"-Wl,-rpath,@executable_path/../../../build-cmake/_deps/xeus-zmq-build",
4343
"-lxeus", "-lxeus-zmq", "-lstdc++"]
4444
else -- Linux
45+
-- FFI library must be built with leanc (Lean's clang/libc++) for ABI
46+
-- compatibility. Lean's linker uses its own sysroot and libc++, so
47+
-- libstdc++ and GCC runtime are not needed.
4548
#["-Wl,--start-group",
4649
"./build-cmake/libxeus_ffi.a",
4750
"-L./build-cmake/_deps/xeus-build",
4851
"-L./build-cmake/_deps/xeus-zmq-build",
49-
"-lxeus", "-lxeus-zmq",
52+
"-L./build-cmake/_deps/libzmq-build/lib",
53+
"-lxeus", "-lxeus-zmq", "-lzmq",
5054
"-Wl,--end-group",
51-
"-L/usr/lib/gcc/x86_64-linux-gnu/13",
5255
"-L/usr/lib/x86_64-linux-gnu",
53-
"-lstdc++", "-lgcc_s", "-lpthread", "-lm", "-ldl"]
56+
"-lpthread", "-lm", "-ldl"]
5457

5558
/-- Script to build xlean via cmake -/
5659
script buildXlean do

0 commit comments

Comments
 (0)