From 92e28e51b3516761c4e58e203f95e419f433f4bd Mon Sep 17 00:00:00 2001 From: psong Date: Thu, 16 Jul 2026 12:10:13 +0800 Subject: [PATCH 1/7] Bump to latest Lean version v4.32.0 --- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 51c15df..9e7c5ac 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -427,8 +427,8 @@ extern_lib libleanffi pkg := do buildStaticLib (pkg.sharedLibDir / name) #[ct2O] -require batteries from git "https://github.com/leanprover-community/batteries.git" @ "main" -require aesop from git "https://github.com/leanprover-community/aesop" @ "master" +require batteries from git "https://github.com/leanprover-community/batteries.git" @ "023ce7d62a0531e22a5331e20b587817a80d49ff" +require aesop from git "https://github.com/leanprover-community/aesop" @ "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3" meta if get_config? env = some "dev" then -- dev is so not everyone has to build it require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 63f51ea..2544c30 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0-rc1 \ No newline at end of file +leanprover/lean4:v4.32.0 \ No newline at end of file From a10aba5a3e9b811fd52e4319562aa1c5544c3a35 Mon Sep 17 00:00:00 2001 From: psong Date: Thu, 16 Jul 2026 12:34:39 +0800 Subject: [PATCH 2/7] Bump deps --- lake-manifest.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 45c1864..c056302 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82", + "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries.git", "type": "git", "subDir": null, "scope": "", - "rev": "e535e4feb0aa360e59e7adf4837b91ffbfb8c943", + "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "023ce7d62a0531e22a5331e20b587817a80d49ff", "inherited": false, "configFile": "lakefile.toml"}], "name": "LeanCopilot", From 4fc2eae6654b03d44cb3a90a9890c4ac978610db Mon Sep 17 00:00:00 2001 From: psong Date: Thu, 16 Jul 2026 12:35:26 +0800 Subject: [PATCH 3/7] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 29a7bad..3a036e1 100644 --- a/README.md +++ b/README.md @@ -61,7 +61,7 @@ moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2 require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION" ``` -For stable Lean versions (e.g., `v4.29.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions (e.g., `v4.30.0-rc1`), set `LEAN_COPILOT_VERSION` to `main`. In either case, make sure the version is compatible with other dependencies such as mathlib. If your project uses lakefile.toml instead of lakefile.lean, it should include: +For stable Lean versions (e.g., `v4.32.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions (e.g., `v4.33.0-rc1`), set `LEAN_COPILOT_VERSION` to `main`. In either case, make sure the version is compatible with other dependencies such as mathlib. If your project uses lakefile.toml instead of lakefile.lean, it should include: ```toml [[require]] From 8a07d82c5dda15ce618e1503f9d01bc3e693bf8e Mon Sep 17 00:00:00 2001 From: psong Date: Mon, 17 Aug 2026 23:15:54 -0400 Subject: [PATCH 4/7] Fix OpenBLAS SIGILL, lean_exe libstdc++ link failure, and pin native deps - OpenBLAS: build with DYNAMIC_ARCH=1 so the shipped release artifact runtime-dispatches on CPU features instead of hardcoding whatever ISA extensions (e.g. AVX-512/cooperlake) happen to be on the CI build machine, which SIGILLs on older CPUs (#137). - libleanffi: on Linux, fold a small glibc-version-compat shim and (when available) the system's static libstdc++ directly into ct2.o before archiving, so a downstream `lean_exe` -- which Lean links against its own bundled libc++, never libstdc++ -- no longer hits undefined-symbol link errors for libstdc++/glibc entry points pulled in via CTranslate2's headers. `lean_lib` dynlib targets never hit this since undefined symbols in a `-shared` object are tolerated and resolved at load time (#196). - Pin the OpenBLAS and CTranslate2 git clones to known-good commits/tags instead of tracking their default branches unpinned. An unpinned OpenBLAS clone is exactly what broke PR #195's CI: a transient upstream regression (fixed in OpenMathLib/OpenBLAS@52f0572564, after our clone) made common.h fail to compile as C++. Co-Authored-By: Claude Sonnet 5 --- cpp/glibc_compat_stub.c | 43 +++++++++++++++ lakefile.lean | 116 +++++++++++++++++++++++++++++++++++++--- 2 files changed, 153 insertions(+), 6 deletions(-) create mode 100644 cpp/glibc_compat_stub.c diff --git a/cpp/glibc_compat_stub.c b/cpp/glibc_compat_stub.c new file mode 100644 index 0000000..5c7cd13 --- /dev/null +++ b/cpp/glibc_compat_stub.c @@ -0,0 +1,43 @@ +/* + * Compatibility shim for downstream `lean_exe` targets on Linux. + * + * Lean's bundled toolchain ships a hermetic, old glibc build (~2.26) for + * portability across host distros. When `libleanffi.a` is statically linked + * into a downstream executable and that executable also links a *system* + * `libstdc++.so` (see the libstdc++ note in the README), the system + * libstdc++ may reference glibc entry points that only exist in much newer + * glibc releases and have no equivalent in Lean's bundled one: + * + * - `__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. + * + * These forwarders satisfy the link when those symbols are otherwise + * undefined. Because this object is only one member of a static archive, it + * is pulled into the final link solely when one of these symbols is actually + * unresolved elsewhere -- it is a no-op whenever the host glibc (or Lean's + * bundled one) already provides them. + * + * Root-caused and originally proposed in + * https://github.com/lean-dojo/LeanCopilot/issues/196. + */ + +#include + +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; diff --git a/lakefile.lean b/lakefile.lean index 9e7c5ac..3d2dee8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -228,6 +228,15 @@ def runCmake (root : FilePath) (flags : Array String) : LogIO Unit := do error "Failed to run cmake" +/-- A commit on OpenBLAS's `develop` branch verified to build cleanly for us. +Update deliberately (not by tracking HEAD) -- see the comment where it's used. -/ +def openblasPin : String := "d9f362aae842bfc4949ea2c786341e0332822239" + +/-- A tagged CTranslate2 release verified to build cleanly for us. +Update deliberately (not by tracking `master`) -- see the comment where it's used. -/ +def ct2Pin : String := "v4.8.1" + + target libopenblas pkg : FilePath := do afterReleaseAsync pkg do let rootDir := pkg.buildDir / "OpenBLAS" @@ -236,7 +245,7 @@ target libopenblas pkg : FilePath := do createParentDirs dst let url := "https://github.com/OpenMathLib/OpenBLAS" - let depTrace := Hash.ofString url + let depTrace := Hash.ofString (url ++ openblasPin) setTrace depTrace buildFileUnlessUpToDate' dst do if getOS! == .windows then @@ -255,9 +264,26 @@ target libopenblas pkg : FilePath := do else logInfo s!"Cloning OpenBLAS from {url}" gitClone url pkg.buildDir + -- Pin to a commit on `develop` that includes the C++-compilation guard + -- around OpenBLAS's C11-atomics lock implementation + -- (OpenMathLib/OpenBLAS@52f0572564, "Guard use of C11 atomics against + -- C++ compilation"). Building an unpinned HEAD previously broke our CI + -- when a transient OpenBLAS regression made `common.h` fail to compile + -- as C++ (see lean-dojo/LeanCopilot#195). Bump this pin deliberately. + proc (quiet := true) { + cmd := "git" + args := #["checkout", openblasPin] + cwd := rootDir + } let numThreads := max 4 $ min 32 (← nproc) - let flags := #["NO_LAPACK=1", "NO_FORTRAN=1", s!"-j{numThreads}"] + -- `DYNAMIC_ARCH=1` makes OpenBLAS embed kernels for multiple x86_64/arm64 + -- microarchitectures and dispatch between them at runtime via CPUID, + -- instead of hardcoding whatever ISA extensions (e.g. AVX-512) happen to + -- be available on the machine that built the release artifact. Without + -- it, the artifact SIGILLs on any CPU lacking those extensions + -- (see lean-dojo/LeanCopilot#137). + let flags := #["NO_LAPACK=1", "NO_FORTRAN=1", "DYNAMIC_ARCH=1", s!"-j{numThreads}"] logInfo s!"Building OpenBLAS with `make{flags.foldl (· ++ " " ++ ·) ""}`" proc (quiet := true) { cmd := "make" @@ -300,14 +326,28 @@ target libctranslate2 pkg : FilePath := do createParentDirs dst let ct2URL := "https://github.com/OpenNMT/CTranslate2" - let depTrace := Hash.ofString ct2URL + let depTrace := Hash.ofString (ct2URL ++ ct2Pin) setTrace depTrace buildFileUnlessUpToDate' dst do logInfo s!"Cloning CTranslate2 from {ct2URL}" - if !(← (pkg.buildDir / "CTranslate2").pathExists) then + let ct2Dir := pkg.buildDir / "CTranslate2" + if !(← ct2Dir.pathExists) then let _ ← gitClone ct2URL pkg.buildDir + -- Pin to a tagged release instead of tracking `master` so that an + -- upstream regression can't silently break our CI the way an + -- unpinned OpenBLAS clone did (see lean-dojo/LeanCopilot#195 and the + -- `openblasPin` comment above). Bump this pin deliberately. + proc (quiet := true) { + cmd := "git" + args := #["checkout", ct2Pin] + cwd := ct2Dir + } + proc (quiet := true) { + cmd := "git" + args := #["submodule", "update", "--init", "--recursive"] + cwd := ct2Dir + } - let ct2Dir := pkg.buildDir / "CTranslate2" if getOS! == .windows then ensureDirExists $ ct2Dir / "build" let _out ← rawProc { @@ -373,6 +413,37 @@ def buildCpp (pkg : Package) (path : FilePath) (dep : Job FilePath) : SpawnM (Jo compileO oFile deps[0]! args (if getOS! == .windows then s!"{leanPath}/bin/clang.exe" else "c++") +/-- +Build the tiny glibc-version-compatibility shim (see `cpp/glibc_compat_stub.c`) +with the system C compiler. Linux only; see `libleanffi` below for why. +-/ +target glibc_compat_stub.o pkg : FilePath := do + let oFile := pkg.buildDir / "cpp" / "glibc_compat_stub.o" + let srcJob ← inputTextFile <| pkg.dir / "cpp/glibc_compat_stub.c" + afterReleaseSync pkg <| + buildFileAfterDep oFile (.collectList [srcJob]) fun deps => + compileO oFile deps[0]! #["-fPIC", "-O2"] "cc" + + +/-- +Find the absolute path to the system's static `libstdc++.a`, if the C++ +compiler's search paths include one (as opposed to only a dynamic +`libstdc++.so`). Returns `none` when unavailable. +-/ +def findLibstdcxxA : IO (Option FilePath) := do + let out ← IO.Process.output {cmd := "c++", args := #["-print-file-name=libstdc++.a"], stdin := .null} + if out.exitCode != 0 then + return none + let path : FilePath := out.stdout.trimAscii.toString + -- The driver echoes the bare name back, unresolved, when it can't find one. + if path.toString == "libstdc++.a" then + return none + if ← path.pathExists then + return some path + else + return none + + target ct2.o pkg : FilePath := do let ct2 ← libctranslate2.fetch if getOS! == .windows then @@ -424,7 +495,40 @@ target ct2.o pkg : FilePath := do extern_lib libleanffi pkg := do let name := nameToStaticLib "leanffi" let ct2O ← ct2.o.fetch - buildStaticLib (pkg.sharedLibDir / name) #[ct2O] + if getOS! != .linux then + buildStaticLib (pkg.sharedLibDir / name) #[ct2O] + else + let stubO ← glibc_compat_stub.o.fetch + -- Fold the glibc-compat shim and (when available) the system's static + -- libstdc++ directly into `ct2.o`'s object, so a downstream `lean_exe` -- + -- which Lean links against its own bundled libc++, never libstdc++ -- + -- doesn't hit undefined-symbol link errors for the libstdc++/glibc + -- entry points CTranslate2's headers pull into `ct2.cpp` + -- (see lean-dojo/LeanCopilot#196). A `lean_lib` dynlib target never + -- needed this: undefined symbols in a `-shared` object are tolerated and + -- resolved at load time via `libctranslate2.so`'s own libstdc++ + -- dependency, but a plain executable link requires every symbol + -- resolved up front. + let out := pkg.buildDir / "cpp" / "ct2_selfcontained.o" + let selfContained ← afterReleaseSync pkg <| buildFileAfterDep out + (.collectList [ct2O, stubO]) fun deps => do + createParentDirs out + let objArgs := deps.map FilePath.toString + let mut merged := false + if let some libstdcxxA ← findLibstdcxxA then + merged ← testProc { + cmd := "ld" + args := #["-r", "-o", out.toString] ++ objArgs ++ #[libstdcxxA.toString] + } + if !merged then + -- No static libstdc++ found (or folding it in failed) -- still merge + -- in just the glibc-compat shim, matching the pre-existing behaviour + -- for `lean_lib` targets. + proc (quiet := true) { + cmd := "ld" + args := #["-r", "-o", out.toString] ++ objArgs + } + buildStaticLib (pkg.sharedLibDir / name) #[selfContained] require batteries from git "https://github.com/leanprover-community/batteries.git" @ "023ce7d62a0531e22a5331e20b587817a80d49ff" From f39e5d200a6e76072872b89386c69aef27f9e84f Mon Sep 17 00:00:00 2001 From: psong Date: Mon, 17 Aug 2026 23:20:09 -0400 Subject: [PATCH 5/7] Add a lean_exe regression test for #196 and document the fix LeanCopilotTests was always a lean_lib, so CI never actually built a lean_exe depending on Lean Copilot -- exactly the target class that tripped the libstdc++ link failure in #196. Add a trivial leanffi_exe_smoke_test lean_exe and build it in CI right after the main build, before the (slower) model download/test steps. Also document the fix and its one remaining edge case (building from source without a static libstdc++.a available) in the README Caveats section. Co-Authored-By: Claude Sonnet 5 --- .github/workflows/ci.yml | 2 ++ LeanCopilotTests/ExeSmokeTest.lean | 16 ++++++++++++++++ README.md | 2 ++ lakefile.lean | 7 +++++++ 4 files changed, 27 insertions(+) create mode 100644 LeanCopilotTests/ExeSmokeTest.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 685cd5a..c309727 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -35,6 +35,8 @@ jobs: echo "$GITHUB_WORKSPACE/.lake/build/lib" >> $GITHUB_PATH - name: Build project run: ~/.elan/bin/lake build + - name: Build lean_exe smoke test + run: ~/.elan/bin/lake build leanffi_exe_smoke_test - name: Download model run: | ~/.elan/bin/lake exe LeanCopilot/download diff --git a/LeanCopilotTests/ExeSmokeTest.lean b/LeanCopilotTests/ExeSmokeTest.lean new file mode 100644 index 0000000..4eab63a --- /dev/null +++ b/LeanCopilotTests/ExeSmokeTest.lean @@ -0,0 +1,16 @@ +import LeanCopilot + +/-! +A minimal `lean_exe` that depends on Lean Copilot. + +This exists purely so CI actually link-tests a `lean_exe` target against +`libleanffi.a`, not just the `lean_lib` targets in the rest of this +directory. A `lean_exe`'s final link (unlike a `lean_lib`'s `.so`, which +tolerates undefined symbols resolved later at load time) requires every +symbol resolved up front, which is exactly what broke on Linux in +https://github.com/lean-dojo/LeanCopilot/issues/196. `LeanCopilotTests` +alone never caught that regression because it is a `lean_lib`. +-/ + +def main : IO Unit := + IO.println "Lean Copilot lean_exe smoke test OK" diff --git a/README.md b/README.md index 3a036e1..a64b7b7 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 downstream `lean_exe` target links against Lean's own bundled `libc++`, while Lean Copilot's native code (`ct2.cpp`) is compiled against the system's `libstdc++`. Lean Copilot bundles the needed `libstdc++`/glibc compatibility symbols directly into `libleanffi.a` so this is transparent when using an official release build. If you build Lean Copilot from source on a machine without a static `libstdc++.a` available (e.g. some minimal container images), a downstream `lean_exe` may still fail to link with undefined `libstdc++` symbols; see [#196](https://github.com/lean-dojo/LeanCopilot/issues/196) for a manual `moreLinkArgs` workaround in that case. + ## Getting in Touch * For general questions and discussions, please use [GitHub Discussions](https://github.com/lean-dojo/LeanCopilot/discussions). diff --git a/lakefile.lean b/lakefile.lean index 3d2dee8..38b9c0b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -172,6 +172,13 @@ lean_lib LeanCopilotTests { } +-- A minimal `lean_exe` depending on Lean Copilot -- see `ExeSmokeTest.lean` +-- for why this exists as a regression test on its own. +lean_exe leanffi_exe_smoke_test { + root := `LeanCopilotTests.ExeSmokeTest +} + + private def nameToVersionedSharedLib (name : String) (v : String) : String := if Platform.isWindows then s!"lib{name}.{v}.dll" else if Platform.isOSX then s!"lib{name}.{v}.dylib" From dad1b34a43f7c2fe89983c32148bb70bd6ad4a07 Mon Sep 17 00:00:00 2001 From: psong Date: Mon, 17 Aug 2026 23:36:05 -0400 Subject: [PATCH 6/7] Fix #196: don't statically bundle libstdc++ (duplicate-symbol conflict) CI caught a real bug in the previous approach: folding libstdc++.a into libleanffi.a via `ld -r` caused "duplicate symbol" link errors against Lean's own statically-linked libc++.a. libstdc++ and libc++ both define the same Itanium-ABI-mangled symbols for standard types with out-of-line definitions (std::logic_error, the __cxa_* exception runtime, etc. -- that mangling carries no implementation-specific tag), so statically linking both into one executable is a hard conflict, not just messy. Keep the part that's actually safe and sufficient: bundling the tiny glibc-compat shim as a plain extra archive member (no ABI surface overlap with libc++, so no collision risk). For the libstdc++ symbols themselves, downstream still needs a `moreLinkArgs` entry that links libstdc++ *dynamically* (a .so, not a duplicated static copy) -- Lean's own toolchain gives no way to inject that into a downstream lean_exe's link line automatically. Document the complete, correct recipe in the README instead of overclaiming a fully automatic fix. Co-Authored-By: Claude Sonnet 5 --- README.md | 11 +++++++- lakefile.lean | 71 ++++++++++++++++----------------------------------- 2 files changed, 32 insertions(+), 50 deletions(-) diff --git a/README.md b/README.md index a64b7b7..a6d5915 100644 --- a/README.md +++ b/README.md @@ -173,7 +173,16 @@ 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 downstream `lean_exe` target links against Lean's own bundled `libc++`, while Lean Copilot's native code (`ct2.cpp`) is compiled against the system's `libstdc++`. Lean Copilot bundles the needed `libstdc++`/glibc compatibility symbols directly into `libleanffi.a` so this is transparent when using an official release build. If you build Lean Copilot from source on a machine without a static `libstdc++.a` available (e.g. some minimal container images), a downstream `lean_exe` may still fail to link with undefined `libstdc++` symbols; see [#196](https://github.com/lean-dojo/LeanCopilot/issues/196) for a manual `moreLinkArgs` workaround in that case. +* On Linux, a downstream **`lean_exe`** target (as opposed to a `lean_lib`) links against Lean's own bundled, statically-linked `libc++`, while Lean Copilot's native code (`ct2.cpp`) is compiled against the system's `libstdc++`. A `lean_lib` never hits this (its `.so` tolerates undefined symbols, resolved later at load time), but a plain executable link requires every symbol resolved up front, so without extra configuration a `lean_exe` that depends on Lean Copilot fails to link with undefined `libstdc++` symbols. Lean Copilot cannot fully paper over this on its own: statically bundling libstdc++ itself would collide with Lean's already-statically-linked libc++ (both define the same ABI-mangled symbols for types like `std::logic_error`), so it can only be linked in dynamically, which downstream still has to opt into. If your project has a `lean_exe` target, add this to its `lakefile.toml`/`lakefile.lean` on Linux (adjust the `-L` path for your distro, e.g. via `gcc -print-file-name=libstdc++.so`): + + ```toml + moreLinkArgs = [ + "-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2", + "-Wl,-L/usr/lib/gcc/x86_64-linux-gnu/13", "-Wl,-lstdc++" + ] + ``` + + (`-Wl,-lstdc++`, not a plain `-lstdc++`: Lean's bundled clang driver silently rewrites a literal `-lstdc++` argument to link `libc++` instead, so it must be passed through to the linker directly.) See [#196](https://github.com/lean-dojo/LeanCopilot/issues/196) for the full root-cause writeup. ## Getting in Touch diff --git a/lakefile.lean b/lakefile.lean index 38b9c0b..dd6f992 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -432,25 +432,6 @@ target glibc_compat_stub.o pkg : FilePath := do compileO oFile deps[0]! #["-fPIC", "-O2"] "cc" -/-- -Find the absolute path to the system's static `libstdc++.a`, if the C++ -compiler's search paths include one (as opposed to only a dynamic -`libstdc++.so`). Returns `none` when unavailable. --/ -def findLibstdcxxA : IO (Option FilePath) := do - let out ← IO.Process.output {cmd := "c++", args := #["-print-file-name=libstdc++.a"], stdin := .null} - if out.exitCode != 0 then - return none - let path : FilePath := out.stdout.trimAscii.toString - -- The driver echoes the bare name back, unresolved, when it can't find one. - if path.toString == "libstdc++.a" then - return none - if ← path.pathExists then - return some path - else - return none - - target ct2.o pkg : FilePath := do let ct2 ← libctranslate2.fetch if getOS! == .windows then @@ -505,37 +486,29 @@ extern_lib libleanffi pkg := do if getOS! != .linux then buildStaticLib (pkg.sharedLibDir / name) #[ct2O] else + -- Bundle the glibc-compat shim as an extra archive member alongside + -- `ct2.o` (see `cpp/glibc_compat_stub.c`) so it's automatically available + -- to any downstream consumer, with no config needed on their end. + -- + -- This does *not* fully fix lean-dojo/LeanCopilot#196: `ct2.cpp` is + -- compiled against the system's libstdc++, but Lean links a plain + -- `lean_exe` against its own bundled, *statically linked* libc++ -- + -- never libstdc++. A `lean_lib` dynlib target never hits this, since + -- undefined symbols in a `-shared` object are tolerated and resolved at + -- load time via `libctranslate2.so`'s own libstdc++ dependency, but a + -- plain executable link requires every symbol resolved up front. + -- + -- We deliberately do *not* statically fold libstdc++ itself into this + -- archive to plug that gap: libstdc++ and libc++ both define the same + -- Itanium-ABI-mangled symbols for standard types with out-of-line + -- definitions (`std::logic_error`, the `__cxa_*` exception-handling + -- runtime, etc., since that mangling has no implementation-specific + -- tag), so statically linking both into one executable is a hard + -- "duplicate symbol" error, not just a style choice. A downstream + -- `lean_exe` on Linux still needs to *dynamically* link libstdc++ itself + -- via its own `moreLinkArgs` -- see the README's Caveats section. let stubO ← glibc_compat_stub.o.fetch - -- Fold the glibc-compat shim and (when available) the system's static - -- libstdc++ directly into `ct2.o`'s object, so a downstream `lean_exe` -- - -- which Lean links against its own bundled libc++, never libstdc++ -- - -- doesn't hit undefined-symbol link errors for the libstdc++/glibc - -- entry points CTranslate2's headers pull into `ct2.cpp` - -- (see lean-dojo/LeanCopilot#196). A `lean_lib` dynlib target never - -- needed this: undefined symbols in a `-shared` object are tolerated and - -- resolved at load time via `libctranslate2.so`'s own libstdc++ - -- dependency, but a plain executable link requires every symbol - -- resolved up front. - let out := pkg.buildDir / "cpp" / "ct2_selfcontained.o" - let selfContained ← afterReleaseSync pkg <| buildFileAfterDep out - (.collectList [ct2O, stubO]) fun deps => do - createParentDirs out - let objArgs := deps.map FilePath.toString - let mut merged := false - if let some libstdcxxA ← findLibstdcxxA then - merged ← testProc { - cmd := "ld" - args := #["-r", "-o", out.toString] ++ objArgs ++ #[libstdcxxA.toString] - } - if !merged then - -- No static libstdc++ found (or folding it in failed) -- still merge - -- in just the glibc-compat shim, matching the pre-existing behaviour - -- for `lean_lib` targets. - proc (quiet := true) { - cmd := "ld" - args := #["-r", "-o", out.toString] ++ objArgs - } - buildStaticLib (pkg.sharedLibDir / name) #[selfContained] + buildStaticLib (pkg.sharedLibDir / name) #[ct2O, stubO] require batteries from git "https://github.com/leanprover-community/batteries.git" @ "023ce7d62a0531e22a5331e20b587817a80d49ff" From b7dcc78c3abee10ab3117b47e08ef80a29bd2119 Mon Sep 17 00:00:00 2001 From: psong Date: Mon, 17 Aug 2026 23:50:22 -0400 Subject: [PATCH 7/7] Wire the documented libstdc++ recipe into the lean_exe smoke test The smoke test was still failing in CI exactly as #196 describes, because -- correctly -- libleanffi.a alone can't supply libstdc++ (see the previous commit). Give the smoke test the same moreLinkArgs a downstream project needs to add per the README, computed dynamically (via `c++ -print-file-name=libstdc++.so`) instead of hardcoding a distro-specific path, so CI validates the actual documented recipe end to end rather than just asserting the gap exists. Co-Authored-By: Claude Sonnet 5 --- lakefile.lean | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index dd6f992..0615862 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -89,6 +89,35 @@ def buildArchiveName : String := s!"{arch}-{os}.tar.gz" +/-- The directory containing `libName` according to `compiler`'s own search +paths, or `none` if `compiler` can't find one (e.g. it only has a `.a` where +we asked for a `.so`, or vice versa). -/ +def findLibraryDir (compiler libName : String) : IO (Option FilePath) := do + let out ← IO.Process.output {cmd := compiler, args := #[s!"-print-file-name={libName}"], stdin := .null} + if out.exitCode != 0 then + return none + let path : FilePath := out.stdout.trimAscii.toString + -- The driver echoes the bare name back, unresolved, when it can't find one. + if path.toString == libName then + return none + return path.parent + + +/-- +The `-Wl,...` flags a downstream `lean_exe` needs on Linux to dynamically +link the system's libstdc++. `libleanffi.a` can't provide this on its own -- +see the README's Caveats section and lean-dojo/LeanCopilot#196 for why -- +so this exists to let `leanffi_exe_smoke_test` below actually validate that +recipe in CI, the same way a downstream project's own `lakefile.toml` would. +-/ +def linuxLibstdcxxLinkArgs : Array String := + if getOS! != .linux then + #[] + else match run_io (findLibraryDir "c++" "libstdc++.so") with + | some dir => #[s!"-Wl,-L{dir}", "-Wl,-lstdc++"] + | none => #[] + + structure SupportedPlatform where os : SupportedOS arch : SupportedArch @@ -173,9 +202,12 @@ lean_lib LeanCopilotTests { -- A minimal `lean_exe` depending on Lean Copilot -- see `ExeSmokeTest.lean` --- for why this exists as a regression test on its own. +-- for why this exists as a regression test on its own. `moreLinkArgs` here +-- mirrors exactly what the README tells a downstream project to add on +-- Linux, so this also validates that documented recipe in CI. lean_exe leanffi_exe_smoke_test { root := `LeanCopilotTests.ExeSmokeTest + moreLinkArgs := linuxLibstdcxxLinkArgs }