bump to Lean v4.32.0 & fix bugs

.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

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"

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]]
@@ -173,6 +173,17 @@ 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 (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
 
 * For general questions and discussions, please use [GitHub Discussions](https://github.com/lean-dojo/LeanCopilot/discussions).  

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 <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;

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",

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
@@ -172,6 +201,16 @@ 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. `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
+}
+
+
 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"
@@ -228,6 +267,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 +284,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 +303,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 +365,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 +452,18 @@ 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"
+
+
 target ct2.o pkg : FilePath := do
   let ct2 ← libctranslate2.fetch
   if getOS! == .windows then
@@ -424,11 +515,36 @@ 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]
-
-
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ "main"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
+  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
+    buildStaticLib (pkg.sharedLibDir / name) #[ct2O, stubO]
+
+
+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"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.32.0-rc1
+leanprover/lean4:v4.32.0