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

Method get

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

Return a cached managed project, creating it if necessary.

(cls, deps: tuple[str, ...] = ())

Source from the content-addressed store, hash-verified

113
114 @classmethod
115 def get(cls, deps: tuple[str, ...] = ()) -> ManagedProject:
116 """Return a cached managed project, creating it if necessary."""
117 version = lean_toolchain_version()
118 key = _cache_key(version, deps)
119 if key in cls._instances:
120 return cls._instances[key]
121
122 project_dir = _CACHE_ROOT / key
123 if not (project_dir / "lakefile.toml").exists():
124 _create_project(project_dir, version, deps)
125
126 inst = cls(project_dir)
127 cls._instances[key] = inst
128 return inst
129
130 def build(self) -> None:
131 """Run ``lake build`` in the managed project."""

Callers 2

project.pyFile · 0.45
_leanpy_git_revFunction · 0.45

Calls 3

lean_toolchain_versionFunction · 0.90
_cache_keyFunction · 0.85
_create_projectFunction · 0.85

Tested by

no test coverage detected