Fix native CI: glibc C23 compat shim for leanc linking

Two-compiler strategy verified in Docker (Ubuntu 24.04):
1. System clang++ -stdlib=libc++ builds all deps (full system headers)
2. leanc compiles a C23 compat shim (glibc_isoc23_compat.c)
3. lake build links everything with leanc

The compat shim bridges the glibc version gap: system clang++ compiles
against glibc 2.38+ which redirects strtoull→__isoc23_strtoull when
_GNU_SOURCE is defined, but leanc's bundled older glibc lacks these
C23 symbols. The shim forwards them to the regular versions.

Author: junjihashimoto

.github/workflows/ci.yml

@@ -26,7 +26,8 @@ jobs:
       run: |
         sudo apt-get update
         sudo apt-get install -y cmake build-essential nlohmann-json3-dev \
-          uuid-dev libssl-dev python3 python3-pip
+          uuid-dev libssl-dev python3 python3-pip \
+          clang libc++-dev libc++abi-dev
 
     - name: Install Lean via elan
       run: |
@@ -38,20 +39,23 @@ jobs:
 
     - name: Build C++ FFI library
       run: |
-        # Use leanc (Lean's clang wrapper) so compiled code uses leanc's
-        # bundled glibc headers, matching the glibc leanc links against.
-        # System clang++ uses system glibc 2.39 headers which redirect
-        # strtoull→__isoc23_strtoull (C23), missing from leanc's older glibc.
-        # STATIC_LIBRARY skips link tests that fail with leanc's sysroot.
-        # LibUUID paths provided explicitly since leanc's sysroot hides them.
+        # Use system clang++ with libc++ so cmake can find all system
+        # libraries and headers (leanc's sysroot is too minimal for libzmq).
+        # The -stdlib=libc++ ensures C++ ABI matches Lean's linker.
         cmake -S . -B build-cmake \
-          -DCMAKE_C_COMPILER=leanc \
-          -DCMAKE_CXX_COMPILER=leanc \
-          -DCMAKE_TRY_COMPILE_TARGET_TYPE=STATIC_LIBRARY \
-          -DLibUUID_INCLUDE_DIR=/usr/include \
-          -DLibUUID_LIBRARY=/usr/lib/x86_64-linux-gnu/libuuid.a
+          -DCMAKE_C_COMPILER=clang \
+          -DCMAKE_CXX_COMPILER=clang++ \
+          -DCMAKE_CXX_FLAGS="-stdlib=libc++"
         cmake --build build-cmake
 
+    - name: Build glibc C23 compat shim
+      run: |
+        # System clang++ compiles against glibc 2.38+ which redirects
+        # strtoull→__isoc23_strtoull (C23) when _GNU_SOURCE is defined.
+        # leanc's bundled older glibc lacks these symbols, so we provide
+        # a shim compiled with leanc that forwards C23→regular versions.
+        leanc -c src/glibc_isoc23_compat.c -o build-cmake/glibc_isoc23_compat.o
+
     - name: Build Lean kernel
       run: lake build xlean
 

Dockerfile.native

@@ -0,0 +1,29 @@
+FROM ubuntu:24.04
+
+RUN apt-get update && apt-get install -y \
+    cmake build-essential nlohmann-json3-dev \
+    uuid-dev libssl-dev python3 python3-pip \
+    clang libc++-dev libc++abi-dev \
+    curl git
+
+# Install Lean via elan
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:v4.28.0-rc1
+ENV PATH="/root/.elan/bin:${PATH}"
+
+WORKDIR /app
+COPY . /app
+
+# Step 1: Build C++ FFI library with system clang++ -stdlib=libc++
+RUN cmake -S . -B build-cmake \
+      -DCMAKE_C_COMPILER=clang \
+      -DCMAKE_CXX_COMPILER=clang++ \
+      -DCMAKE_CXX_FLAGS="-stdlib=libc++" && \
+    cmake --build build-cmake
+
+# Step 2: Build glibc C23 compat shim with leanc
+RUN leanc -c src/glibc_isoc23_compat.c -o build-cmake/glibc_isoc23_compat.o
+
+# Step 3: Build Lean kernel
+RUN lake build xlean
+
+CMD ["bash"]

lakefile.lean

@@ -48,11 +48,15 @@ lean_exe xlean where
       -- All deps built from source via FetchContent; do NOT add system lib
       -- paths like -L/usr/lib/x86_64-linux-gnu because leanc uses --sysroot
       -- with its own bundled glibc, and system glibc conflicts (__libc_csu_init).
+      -- glibc_isoc23_compat.o provides __isoc23_strtoull etc. shims: system
+      -- clang++ compiles against glibc 2.38+ which redirects strtoull→C23
+      -- variants, but leanc's older glibc lacks them.
       #["-L./build-cmake/_deps/xeus-build",
         "-L./build-cmake/_deps/xeus-zmq-build",
         "-L./build-cmake/_deps/libzmq-build/lib",
         "-Wl,--start-group",
         "./build-cmake/libxeus_ffi.a",
+        "./build-cmake/glibc_isoc23_compat.o",
         "-lxeus", "-lxeus-zmq", "-lzmq",
         "-Wl,--end-group",
         "-lpthread", "-lm", "-ldl"]

src/glibc_isoc23_compat.c

@@ -0,0 +1,32 @@
+/*
+ * glibc C23 compatibility shim for leanc linking.
+ *
+ * When compiled with system clang++ against glibc >= 2.38, _GNU_SOURCE causes
+ * strtoull/strtoll to redirect to __isoc23_strtoull/__isoc23_strtoll (C23
+ * variants). But leanc's bundled older glibc lacks these symbols.
+ *
+ * This shim provides the missing symbols by forwarding to the regular versions
+ * available in leanc's glibc. No headers needed - just forward declarations.
+ */
+
+/* Forward declarations matching libc signatures */
+extern unsigned long long strtoull(const char *, char **, int);
+extern long long strtoll(const char *, char **, int);
+extern unsigned long strtoul(const char *, char **, int);
+extern long strtol(const char *, char **, int);
+
+unsigned long long __isoc23_strtoull(const char *nptr, char **endptr, int base) {
+    return strtoull(nptr, endptr, base);
+}
+
+long long __isoc23_strtoll(const char *nptr, char **endptr, int base) {
+    return strtoll(nptr, endptr, base);
+}
+
+unsigned long __isoc23_strtoul(const char *nptr, char **endptr, int base) {
+    return strtoul(nptr, endptr, base);
+}
+
+long __isoc23_strtol(const char *nptr, char **endptr, int base) {
+    return strtol(nptr, endptr, base);
+}