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

File project.py

lean_py/project.py:None–None  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

1"""Managed Lake projects for zero-config Std/Mathlib loading.
2
3:class:`ManagedProject` creates and caches a Lake project under
4``~/.lean_py/managed/<hash>/`` so users can load Std or Mathlib without

Callers

nothing calls this directly

Calls 1

getMethod · 0.45

Tested by

no test coverage detected