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

Method _diagnostic

lean_py/library.py:335–341  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

333 build_root = lake_path / ".lake" / "build"
334 lib_dir = build_root / "lib"
335
336 def _find(name: str) -> Path | None:
337 """Locate `lib<name>.<ext>` produced by `lake build`.
338
339 Naming has shifted across Lake versions:
340 * old: `lib<name>.<ext>`
341 * newer (>= late 2025): `lib<package>_<name>.<ext>`,
342 so a same-name package + lib produces e.g.
343 `libTestLib_TestLib.dylib`.
344

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected