Linux: libleanshared.so exports a partial _Unwind_* ABI, breaking C++ exceptions inside FFI libraries built against libstdc++

On Linux, libleanshared.so exports 10 of the 11 _Unwind_* symbols that the
system libstdc++.so.6 imports. Because it precedes libstdc++ in the global
symbol lookup scope, a C++ FFI dependency built against libstdc++ ends up
unwinding through two different unwinder implementations in a single throw, and
std::terminate runs even when a matching catch is present in the frame being
unwound.

The effect is that any @[extern] binding to a C++ library that throws
internally aborts the process (SIGABRT, Lean exit code 134) on Linux, while the
same code works on macOS.

Symptom

terminate called after throwing an instance of 'duckdb::CatalogException'
terminate called recursively
error: Lean exited with code 134

Note the absence of a what(): line. libstdc++'s verbose terminate handler
prints the exception type via a non-virtual call (which works), then rethrows
internally to obtain what(); that rethrow fails the same way and re-enters the
handler, which is what produces terminate called recursively.

The dependency is not at fault

Same machine, same prebuilt libduckdb.so, four error paths that throw
internally and are caught internally by DuckDB's C API:

context	result
plain C program, no Lean in the process	all four return an error code normally
identical calls inside bin/lean	abort as above

The catch is present in the binary: duckdb_appender_create_ext's cold section
calls __cxa_begin_catch and constructs from std::exception const&, and the
thrown type derives from std::runtime_error.

Root cause

Measured on Ubuntu 24.04 (libstdc++.so.6.0.33) with Lean v4.33.1:

libleanshared.so defines and exports, at default visibility:

_Unwind_DeleteException  _Unwind_ForcedUnwind  _Unwind_GetGR  _Unwind_GetIP
_Unwind_GetLanguageSpecificData  _Unwind_GetRegionStart  _Unwind_RaiseException
_Unwind_Resume  _Unwind_SetGR  _Unwind_SetIP

libstdc++.so.6 imports eleven. The four it does not get from
libleanshared.so are:

_Unwind_GetIPInfo  _Unwind_GetDataRelBase  _Unwind_GetTextRelBase  _Unwind_Resume_or_Rethrow

libleanshared.so is a direct DT_NEEDED of bin/lean, whereas
libstdc++.so.6 and libgcc_s.so.1 enter only as dependencies of the FFI
library, so libleanshared.so is searched first. A throw then proceeds:

1. __cxa_throw calls _Unwind_RaiseException → LLVM's unwinder in libleanshared.so
2. it builds an LLVM-layout _Unwind_Context and passes it to libstdc++'s __gxx_personality_v0
3. the personality routine calls _Unwind_GetIPInfo → libgcc's unwinder
4. libgcc reads an LLVM-layout context and returns an invalid IP
5. no landing pad matches → no handler found → std::terminate

libleanshared.so exports no __cxa_* or __gxx_personality_v0; the unwinder
is the only C++ runtime component that leaks.

Why exactly ten

-DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic' and
-Wl,-Bstatic … -lunwind in script/prepare-llvm-linux.sh link LLVM's
libunwind statically. Its entry points are split across two objects:
libunwind/src/UnwindLevel1.c defines exactly the ten observed, and
libunwind/src/UnwindLevel1-gcc-ext.c defines the GCC extensions, including all
four that are missing. libc++abi references the former, so UnwindLevel1.o is
pulled from the archive; nothing references the GCC extensions, so
UnwindLevel1-gcc-ext.o is not.

They survive -fvisibility=hidden because libunwind marks its entry points
__attribute__((visibility("default"))) unless _LIBUNWIND_HIDE_SYMBOLS is
defined.

This is not version-specific. The LEAN_CXX_STDLIB line is byte-identical from
v4.0.0 through master, and the export count is 10 in every release checked —
v4.0.0, v4.8.0, v4.15.0, v4.33.1 (x86_64 and aarch64) and v4.34.0-rc2.

Suggested fix

leanprover/lean-llvm's .github/workflows/build.yml already hides two of the
three C++ runtime components:

`# hide libc++ symbols in libleanshared`\
-DLIBCXX_HERMETIC_STATIC_LIBRARY=ON -DLIBCXXABI_HERMETIC_STATIC_LIBRARY=ON\

Adding -DLIBUNWIND_HIDE_SYMBOLS=ON would apply -fvisibility=hidden and
-D_LIBUNWIND_HIDE_SYMBOLS to the static unwind_static_objects target, so
libstdc++'s eleven imports would all resolve consistently to libgcc_s.so.1
while Lean's own libc++abi continues to use its statically linked libunwind.

Caveat: I have not tested that, and I have seen a report (in a non-Lean
project) that hiding the exports alone converted an abort into a segfault there,
paired with --unwindlib=libgcc as the eventual fix. So the flag may need
validating rather than assuming.

prepare-llvm-linux.sh:31 already carries the comment "general clang++
dependency, breaks cross-library C++ exceptions if linked statically" above the
libgcc_s.so copy, and #3500 fixed this same class of problem for Lean's own
code by making libgcc_s dynamic. That fix addressed Lean's half; the remaining
static libunwind affects third-party C++ FFI.

Workarounds, for anyone who lands here

• LD_PRELOAD=/usr/lib/x86_64-linux-gnu/libgcc_s.so.1 — preloaded objects
  precede the executable's DT_NEEDED, so all eleven symbols resolve to one
  complete implementation. Verified to fix it, with Lean's own exception handling
  still working. Not viable for a library whose consumers would each have to set
  it.
• Link the dependency statically into a single shared object together with a
  static libstdc++/libgcc and -Wl,--exclude-libs over those archives, so its
  exception machinery is bound at link time and never enters the global scope.
  This is what I ended up shipping.
• Note that merely adding -lgcc_s to the FFI library's own link line does not
  work: the dependency's DT_NEEDED already pulls in a versioned libgcc_s.so.1
  and libleanshared.so still precedes it. Scope order beats symbol versioning
  here.

Environment

• Lean v4.33.1 (also checked v4.0.0, v4.8.0, v4.15.0, v4.34.0-rc2)
• Ubuntu 24.04, x86_64 and aarch64, libstdc++.so.6.0.33
• macOS unaffected: Mach-O's two-level namespace binds the dependency directly
  to /usr/lib/libc++.1.dylib, so nothing can interpose it —
  prepare-llvm-macos.sh notes this explicitly

Happy to test a candidate toolchain build against a real C++ FFI dependency that
throws, if that would help.

🤖 Filed with Claude Code

Start with .github/workflows/build.yml and script/prepare-llvm-linux.sh, then inspect the static libunwind configuration and exported symbols in libleanshared.so. Build a candidate Linux toolchain and test it with a C++ FFI dependency that throws internally. Done means the dependency's exceptions are caught without SIGABRT and the unwinder symbols resolve consistently.