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

[ide-developer]

Summary

Building a [[lean_exe]] target in a project that depends on LeanCopilot fails to link with dozens of undefined symbol errors for basic libstdc++ types (std::basic_ifstream, std::filesystem::path, std::__cxx11::basic_string, exception-handling primitives, etc.) — all originating from ct2.cpp inside LeanCopilot's own libleanffi.a. A [[lean_lib]] target that imports and actually calls LeanCopilot (suggest_tactics) in the exact same project builds and runs correctly — only the executable-target link fails. I've root-caused this precisely (see below) but was not able to find a working link-time fix despite several targeted attempts, which I'm reporting honestly rather than claiming a false resolution.

Environment

OS	Fedora Linux 39 (Server Edition), kernel 6.8.4-200.fc39.x86_64
gcc	13.2.1 (system)
clang/lld (Lean's bundled toolchain)	clang version 22.1.4 / lld, from the Lean toolchain itself
Lean/Lake	4.32.0-rc1 / Lake 5.0.0-src via elan (the toolchain LeanCopilot v4.31.0 pins)
LeanCopilot	tag v4.31.0, commit 2458f7339df4d90643cdc6eb3fbbe968cd73ac78

(Also reproduces, same symptom, on the same machine's macOS-adjacent setup is irrelevant here — this is Linux-only, since macOS builds CTranslate2 against Accelerate rather than OpenBLAS/system libstdc++; not tested on macOS since the underlying ABI mismatch doesn't apply there.)

Minimal reproduction

lakefile.toml

name = "leancopilot_demo_pkg"
version = "0.1.0"
defaultTargets = ["leancopilot_demo_pkg"]
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
precompileModules = true

[[lean_lib]]
name = "LeancopilotDemoPkg"

[[lean_exe]]
name = "leancopilot_demo_pkg"
root = "Main"

[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "v4.31.0"

LeancopilotDemoPkg/Basic.lean:

import LeanCopilot

example (a b : Nat) : a + b = b + a := by
  suggest_tactics

Main.lean is the default lake new template (def main : IO Unit := IO.println "hello" — doesn't even reference LeanCopilot directly, it's just the default [[lean_exe]] entry point).

lake build LeancopilotDemoPkg   # succeeds, suggest_tactics genuinely works (see below)
lake build leancopilot_demo_pkg:exe   # fails, see error below

What works

$ lake build LeancopilotDemoPkg
...
info: LeancopilotDemoPkg/Basic.lean:4:2: Try these:
  [apply] simp [Nat.add_comm]
Build completed successfully (710 jobs).

This is a genuine, fresh model-inference call (confirmed via Built LeancopilotDemoPkg.Basic (7-10s), not a cached replay) — LeanCopilot's ML pipeline is fully functional in the library target.

What fails

Full error output (click to expand)

✖ [714/714] Building leancopilot_demo_pkg:exe (920ms)
trace: .> /home/jdanek/.elan/toolchains/leanprover--lean4---v4.32.0-rc1/bin/clang -o .../leancopilot_demo_pkg @.../leancopilot_demo_pkg.rsp
info: stderr:
ld.lld: error: undefined symbol: std::__throw_logic_error(char const*)
>>> referenced by ct2.cpp
>>>               ct2.o:(...) in archive .../LeanCopilot/.lake/build/lib/libleanffi.a

ld.lld: error: undefined symbol: std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::_M_create(unsigned long&, unsigned long)
>>> referenced by ct2.cpp ... (21 more references)

ld.lld: error: undefined symbol: std::__throw_bad_array_new_length()
ld.lld: error: undefined symbol: std::__throw_length_error(char const*)
ld.lld: error: undefined symbol: std::__cxx11::basic_string<...>::reserve(unsigned long)
ld.lld: error: undefined symbol: std::__cxx11::basic_string<...>::_M_append(char const*, unsigned long)
ld.lld: error: undefined symbol: std::__cxx11::basic_string<...>::append(char const*)
ld.lld: error: undefined symbol: std::__cxx11::basic_string<...>::_M_dispose()   (249 references)
ld.lld: error: undefined symbol: std::__atomic_futex_unsigned_base::_M_futex_wait_until(...)
ld.lld: error: undefined symbol: std::__throw_out_of_range(char const*)
ld.lld: error: undefined symbol: std::__exception_ptr::exception_ptr::_M_addref()
ld.lld: error: undefined symbol: std::rethrow_exception(std::__exception_ptr::exception_ptr)
ld.lld: error: undefined symbol: std::__throw_future_error(int)
ld.lld: error: undefined symbol: std::filesystem::__cxx11::path::_List::_List()
ld.lld: error: undefined symbol: std::filesystem::__cxx11::path::_M_split_cmpts()
ld.lld: error: undefined symbol: std::filesystem::status(std::filesystem::__cxx11::path const&)
ld.lld: error: undefined symbol: std::filesystem::__cxx11::path::_List::_Impl_deleter::operator()(...)
ld.lld: error: undefined symbol: std::basic_ifstream<char, std::char_traits<char>>::basic_ifstream(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>> const&, std::_Ios_Openmode)
ld.lld: error: undefined symbol: vtable for std::basic_ifstream<char, std::char_traits<char>>
ld.lld: error: undefined symbol: vtable for std::basic_filebuf<char, std::char_traits<char>>

ld.lld: error: too many errors emitted, stopping now (use --error-limit=0 to see all errors)
clang: error: linker command failed with exit code 1
error: external command '.../clang' exited with code 1
error: build failed

(Full untruncated log available if useful — trimmed here to representative errors; roughly 15 distinct symbol names, ~300 total references, all traced to ct2.cpp inside libleanffi.a.)

Root cause (confirmed via the actual link command)

The response file (.rsp) for the leancopilot_demo_pkg:exe link step shows Lean's own exe-link recipe:

...
".../LeanCopilot/.lake/build/lib/libleanffi.a"
"-L./.lake/packages/LeanCopilot/.lake/build/lib"
"-lctranslate2"
...
"-Wl,--start-group" "-lleancpp" "-lLean" "-Wl,--end-group"
"-lStd"
"-Wl,--start-group" "-lInit" "-lleanrt" "-Wl,--end-group"
"-Wl,-Bstatic" "-lc++" "-lc++abi" "-Wl,-Bdynamic"
"-lLake"
...

libstdc++ never appears anywhere in this link line — Lean statically links its own bundled libc++/libc++abi (LLVM's C++ runtime) for executables. But libleanffi.a's ct2.cpp (and everything it pulls in from CTranslate2) is compiled by the system g++, and every undefined symbol above uses the GCC-specific std::__cxx11 inline-namespace mangling — these symbols simply don't exist in libc++ at all; they're libstdc++-only.

This is presumably why the library target works: a .so/dynlib built for --load-dynlib loading resolves its libstdc++ dependency at runtime, transitively via libctranslate2.so.4/libopenblas.so.0 (which are themselves normal system-g++ binaries dynamically linked against libstdc++.so.6, already present in the process by the time Lean dlopens LeanCopilot's .so). The executable link is a from-scratch static/dynamic combination that never provides libstdc++ at all, so the moment libleanffi.a's object code is pulled into that link (regardless of whether Main.lean itself even calls anything LeanCopilot-related — it's pulled in transitively because the library depends on it), it's dead on arrival.

What I tried (honestly reporting a non-fix)

Since moreLinkArgs is user-configurable, I tried adding -lstdc++ there, expecting it to supply the missing symbols. This did not work cleanly, and I want to report the actual investigation rather than a false "add -lstdc++ and it's fixed":

1. Plain "-lstdc++" added to moreLinkArgs: same undefined-symbol list, unchanged. Turned out this Fedora system has only the runtime /usr/lib64/libstdc++.so.6 — the unversioned -lstdc++-resolvable dev symlink (libstdc++.so) exists only under GCC's own private directory, /usr/lib/gcc/x86_64-redhat-linux/13/libstdc++.so (confirmed via rpm -ql libstdc++-devel — the package is installed, it's just not on clang's default search path). Since Lean's clang invocation passes an explicit --sysroot pointing at the Lean toolchain directory (not /), it apparently doesn't auto-detect the host's real GCC installation directory the way an unwrapped system clang normally would.
2. "-l:libstdc++.so.6" (referencing the versioned runtime lib directly by exact name, bypassing the need for the dev symlink): failed outright with ld.lld: error: unable to find library -l:libstdc++.so.6 — confirming /usr/lib64 genuinely isn't on the search path for this sysroot-scoped invocation at all.
3. "-L/usr/lib/gcc/x86_64-redhat-linux/13" + "-lstdc++" (explicit -L to the real, confirmed-present dev symlink — file confirms it's a genuine symlink to a real ELF .so.6.0.32, not a linker script): the library is now presumably found (no more "unable to find library" error), and both LeancopilotDemoPkg.Basic:dynlib and LeancopilotDemoPkg:shared build fine with this flag present — but the final leancopilot_demo_pkg:exe link step still fails with the exact same, byte-for-byte identical list of undefined symbols, despite the .rsp file (re-verified after the build) genuinely containing "-L/usr/lib/gcc/x86_64-redhat-linux/13" "-lstdc++" right after libleanffi.a. I independently confirmed via nm -D that /usr/lib64/libstdc++.so.6.0.32 does export the missing symbols (e.g. _ZSt19__throw_logic_errorPKc@@GLIBCXX_3.4), so the symbols genuinely exist in a library that's ostensibly on the link line — I could not determine why the linker isn't using them for this specific target.

I don't have enough visibility into Lake's own moreLinkArgs application per-target (whether it's actually applied identically to :exe vs :shared targets' final link steps) or into lld's exact archive-vs-shared-library resolution order in this scenario to go further — flagging this precisely in case it's either a Lake bug (moreLinkArgs not fully honored for the exe target's own link recipe) or a subtler lld interaction, since I've run out of ideas I can verify from outside the build system's own internals.

Why this matters

Any downstream project that wants to ship a lean_exe (not just a library) using LeanCopilot on Linux hits this immediately and unconditionally — it's not input- or model-dependent, it fails at pure link time before any LeanCopilot code even runs. Happy to share the full untruncated build logs, .rsp files, or test further configurations if that helps narrow this down.

[ide-developer]

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.

[Peiyang-Song]

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.