From 904bdeae511ca0691a422f5c8a476aa863309e47 Mon Sep 17 00:00:00 2001 From: ide-developer Date: Sun, 16 Aug 2026 14:26:18 +0200 Subject: [PATCH] Document lean_exe libstdc++ link failure on Linux (#196) A lean_exe target in a downstream project can fail to link with undefined libstdc++ symbols even when a lean_lib target in the same project builds and works fine, because Lean's executable link recipe statically links libc++/libc++abi and never links libstdc++, while Lean Copilot's native code is built against system libstdc++. Add a Caveats entry pointing to the full root-cause analysis and working moreLinkArgs workaround in #196. --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 29a7bad..c47a791 100644 --- a/README.md +++ b/README.md @@ -173,6 +173,8 @@ theorem mul_left_comm : ∀ a b c : G, a * (b * c) = b * (a * c) * In some cases, `search_proof` produces an erroneous proof with error messages like `fail to show termination for ...`. A temporary workaround is changing the theorem's name before applying `search_proof`. You can change it back after `search_proof` completes. +* On Linux, a `lean_exe` target (as opposed to a `lean_lib` target) in a downstream project may fail to link with `undefined symbol` errors for libstdc++ types (e.g. `vtable for std::basic_ifstream`), even though a `lean_lib` target in the same project builds and runs Lean Copilot correctly. This happens because Lean's own executable link recipe statically links `libc++`/`libc++abi` and never links `libstdc++`, while Lean Copilot's native code (`libleanffi.a`/CTranslate2) is built against the system's `libstdc++`. See [#196](https://github.com/lean-dojo/LeanCopilot/issues/196) for the full root-cause analysis and a working per-project `moreLinkArgs` workaround. + ## Getting in Touch * For general questions and discussions, please use [GitHub Discussions](https://github.com/lean-dojo/LeanCopilot/discussions).