Generate a minimal Lake project on disk.
(
project_dir: Path,
lean_version: str,
deps: tuple[str, ...],
)
| 164 | |
| 165 | |
| 166 | def _create_project( |
| 167 | project_dir: Path, |
| 168 | lean_version: str, |
| 169 | deps: tuple[str, ...], |
| 170 | ) -> None: |
| 171 | """Generate a minimal Lake project on disk.""" |
| 172 | project_dir.mkdir(parents=True, exist_ok=True) |
| 173 | |
| 174 | # lean-toolchain |
| 175 | (project_dir / "lean-toolchain").write_text(f"{lean_version}\n") |
| 176 | |
| 177 | # lakefile.toml |
| 178 | lakefile = _generate_lakefile(deps, lean_version) |
| 179 | (project_dir / "lakefile.toml").write_text(lakefile) |
| 180 | |
| 181 | # Managed.lean |
| 182 | imports = ["import LeanPy", "import LeanPy.Kernel"] |
| 183 | for d in deps: |
| 184 | import_name = _KNOWN_DEPS[d][1] if d in _KNOWN_DEPS else d |
| 185 | imports.append(f"import {import_name}") |
| 186 | lean_src = "\n".join(imports) + '\n\n#export_python_registry "Managed"\n' |
| 187 | (project_dir / "Managed.lean").write_text(lean_src) |
| 188 | |
| 189 | |
| 190 | def _generate_lakefile( |
no test coverage detected