Build and return a :class:`Kernel` backed by this project.
(self)
| 136 | return LeanLibrary.from_lake(self._dir, "Managed", build=True) |
| 137 | |
| 138 | def kernel(self) -> Kernel: |
| 139 | """Build and return a :class:`Kernel` backed by this project.""" |
| 140 | lib = self.library() |
| 141 | k = Kernel(lib) |
| 142 | sp = run_command( |
| 143 | ["lake", "env", "printenv", "LEAN_PATH"], |
| 144 | cwd=str(self._dir), |
| 145 | ) |
| 146 | k.init_search(sp) |
| 147 | k.load(["Init", "LeanPy.Z3"]) |
| 148 | return k |
| 149 | |
| 150 | @property |
| 151 | def path(self) -> Path: |
no test coverage detected