Changelog

leanprover/lean4 · · 2 commits

Lean4 adds Linux SONAME support

Linux shared libraries now ship SONAMEs, with Lake loading adjusted to keep precompiled imports working; CI also tightens one cache step.

Vtec234 tydeu

Linux shared libraries now have SONAMEs (Vtec234b4fb9a7)

Lean now sets DT_SONAME for its Linux shared libraries (libInit_shared, libleanshared*, and libLake_shared), aligning Linux behavior with macOS install_name handling. This should make runtime linking for Lean/Lake artifacts more robust and fixes an existing Linux loader issue.

Lake precompiled-module loading was updated for Linux (Vtec234b4fb9a7)

Lake’s module dependency resolution now eagerly loads libLake_shared.so on Linux when plugins/dynlibs are present, because transitive runtime lookup can miss it otherwise. The commit also adds Linux platform detection/printing and updates extern_lib syntax docs/examples to recognize Linux explicitly.

Other misc changes

  • CI: remove continue-on-error from “Upload Lake Cache” so failures now fail the job (tydeufed67d9)