lean_exe link fails with undefined libstdc++ symbols from libleanffi.a (lean_lib works fine) #196

Activity

1. ide-developer commented on Aug 16, 2026

   

   ide-developer

   on Aug 16, 2026

   Last edited by ide-developer

   Author

   More actions

   Update: root cause fully nailed down, working fix found

   Continued digging into the mystery from the original report (-L + -lstdc++ present in the .rsp but having zero effect on the link). Both findings below have been independently verified — the executable now builds and runs.

   1. Why -lstdc++ silently did nothing (confirmed in clang's own source)

   Clang's driver silently rewrites any literal -lstdc++ argument before it ever reaches the linker — this isn't sysroot- or platform-specific, it's a deliberate, hardcoded driver behavior:

   • clang/lib/Driver/Driver.cpp (TranslateInputArgs): a literal -l argument with value stdc++ gets rewritten to an internal reserved marker, OPT_Z_reserved_lib_stdcxx.
   • clang/lib/Driver/ToolChains/CommonArgs.cpp (AddLinkerInputs): when that marker shows up among the linker inputs, it's replaced by whatever ToolChain::AddCXXStdlibLibArgs decides based on GetCXXStdlibType() — for this Lean-bundled clang (22.1.4), that's libc++, so it silently emits an extra -lc++ instead.

   Verified this directly: clang -v on both the real failing .rsp and a trivial clang t.c -lstdc++ -v minimal repro shows the final ld.lld invocation never contains -lstdc++ at all — it's swapped for a no-op extra -lc++ (Lean's own recipe already links -lc++/-lc++abi explicitly). That's why the flag appeared to do nothing despite being correctly positioned in moreLinkArgs and despite the target library genuinely exporting the needed symbols.

   Bypass: anything that doesn't parse as a literal -l option with value exactly stdc++ escapes this rewrite. -Wl,-lstdc++ works (routes around the driver's arg-matching entirely, since -Wl,-wrapped payloads aren't checked against OPT_l). Note the corresponding -L must stay a plain -L flag (not -Wl,-L...) — -Wl,-L doesn't get hoisted into the search-path list the way plain -L does.

   2. A second, distinct bug this exposed once libstdc++ was actually linked

   With the real libstdc++ finally linked, four new undefined symbols appeared: __isoc23_strtoul, __isoc23_strtoull, __isoc23_strtoll, __libc_single_threaded.

   Root cause: Lean's toolchain bundles its own hermetic glibc 2.26 build for portability (lib/glibc/libc.so — confirmed via its ELF interpreter path pointing at a Nix-store glibc 2.26 build), but the system's libstdc++.so.6 (built by Fedora's GCC 13 against glibc 2.38) calls glibc entry points that are genuinely new in glibc 2.32/2.38 and have no older-ABI equivalent:

   • __isoc23_strtoul/__isoc23_strtoull/__isoc23_strtoll — C23 changed strtol-family semantics (0b binary-prefix support when base==0); glibc ≥2.38 ships these as new, separately-versioned entry points alongside the classic ones.
   • __libc_single_threaded — a fast-path hint for shared_ptr refcounting, exposed since glibc ≥2.32.

   I confirmed the naive fix (pointing -L at the real system glibc ahead of Lean's bundled one) trades this for a worse problem: Lean's bundled Scrt1.o startup code needs __libc_csu_init/__libc_csu_fini, which modern glibc (≥2.34) removed entirely — so overriding -lc resolution wholesale breaks CRT startup linkage instead. This is a genuine toolchain-generation mismatch (Lean's fixed old-glibc baseline vs. anything built against a modern system glibc), not something fixable by -L/-l reordering alone.

   Working resolution: leave libc/CRT linkage untouched; add a tiny compatibility object defining the 4 missing symbols as trivial forwarders to the classic pre-C23 strtoul/strtoull/strtoll (safe here since neither CTranslate2's npy-header parser nor nlohmann::json's number scanner ever rely on 0b-prefix parsing), plus __libc_single_threaded = false (the always-safe, conservative answer — just forces the atomic/thread-safe refcounting path).

   /* glibc_compat_stub.c */
   #include <stdlib.h>
   
   unsigned long __isoc23_strtoul(const char *nptr, char **endptr, int base) {
       return strtoul(nptr, endptr, base);
   }
   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);
   }
   _Bool __libc_single_threaded = 0;

   Compiled with the system's plain gcc (Lean's own clang sysroot ships no libc headers at all): gcc -c glibc_compat_stub.c -o glibc_compat_stub.o -fPIC -O2, then linked in as a plain object file via moreLinkArgs.

   Final working lakefile.toml diff

   - moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
   + moreLinkArgs = ["./glibc_compat_stub.o", "-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2", "-Wl,-L/usr/lib/gcc/x86_64-redhat-linux/13", "-Wl,-lstdc++"]

   (the -L/usr/lib/gcc/x86_64-redhat-linux/13 path is this machine's Fedora-13 GCC install dir — find the equivalent on other distros via gcc -print-file-name=libstdc++.so or similar)

   Verification (independently re-confirmed from a full clean rebuild)

   $ lake build leancopilot_demo_pkg:exe
   ...
   ✔ [714/714] Built leancopilot_demo_pkg:exe (1.3s)
   Build completed successfully (714 jobs).
   
   $ ./.lake/build/bin/leancopilot_demo_pkg
   Hello, world!
   $ echo $?
   0
   

   Happy to open a PR against lakefile.lean if a maintainer wants this baked into the libctranslate2/libleanffi build recipe directly (e.g. adding the -Wl,-lstdc++ + a bundled version of the glibc-compat stub to the Linux link flags), rather than leaving it as a per-downstream-project workaround.
2. Peiyang-Song

   added 4 commits that reference this issue on Aug 18, 2026

   Fix OpenBLAS SIGILL, lean_exe libstdc++ link failure, and pin native …

   ...

   8a07d82

   Add a lean_exe regression test for #196 and document the fix

   ...

   f39e5d2

   Fix #196: don't statically bundle libstdc++ (duplicate-symbol conflict)

   ...

   dad1b34

   Wire the documented libstdc++ recipe into the lean_exe smoke test

   ...

   b7dcc78
3. Peiyang-Song commented on Aug 18, 2026

   

   Peiyang-Song

   on Aug 18, 2026

   Member

   More actions

   Fixed in #195 (built on top of the investigation here). Thanks.

   1. libleanffi.a now automatically bundles the glibc-compat shim on Linux, so that half is transparent: no downstream config needed.
   2. Statically folding libstdc++ itself into libleanffi.a turned out to be unsound (confirmed by CI): it causes duplicate-symbol errors against Lean's own statically-linked libc++, since both standard library implementations define identically-mangled symbols for types like std::logic_error. So a downstream lean_exe on Linux still needs a moreLinkArgs entry that dynamically links libstdc++, documented as a complete, copy-pasteable recipe in the README's Caveats section.
   3. Added a lean_exe smoke test to CI (leanffi_exe_smoke_test) that builds with that exact recipe on every run. The existing suite only ever built a lean_lib, so this specific failure mode had no regression coverage before.

   Closing this issue as a result.
4. Peiyang-Song

   closed this as completedon Aug 18, 2026
5. JadeCong

   added a commit that references this issue on Aug 20, 2026

   Bump to Lean v4.33.0 and support prebuilt system libraries

   ...

   196d567