bump to Lean v4.32.0 & fix bugs - #195
Merged
Merged
Conversation
Member
Author
|
Merging after all tests pass. |
…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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
Member
Author
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
latest stable version.