MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / all_lean_runtime_libs

Function all_lean_runtime_libs

lean_py/utils.py:90–103  ·  view source on GitHub ↗

All shared libs in `lib/lean` that are likely needed at load time. Includes `libleanshared`, `libleanshared_*`, `libLake_shared`, and any other `lib*shared. ` siblings.

()

Source from the content-addressed store, hash-verified

88 ext = shared_lib_extension()
89 lib = lean_lib_dir() / f"libleanshared{ext}"
90 if lib.exists():
91 return lib
92 if bundle_dir():
93 # In a bundle we must not fall through to a toolchain lookup.
94 raise RuntimeError(f"libleanshared{ext} not found in bundle {lean_lib_dir()}")
95 # Fallback: scan LEAN_PATH (less reliable, retained for back-compat).
96 try:
97 out = run_command(["lake", "env", "printenv", "LEAN_PATH"])
98 for d in out.split(":"):
99 cand = Path(d) / f"libleanshared{ext}"
100 if cand.exists():
101 return cand
102 except Exception:
103 pass
104 raise RuntimeError(f"libleanshared{ext} not found in {lean_lib_dir()}")
105
106

Callers 1

__init__Function · 0.90

Calls 2

shared_lib_extensionFunction · 0.85
lean_lib_dirFunction · 0.85

Tested by

no test coverage detected