Return the lean-toolchain string (e.g. ``leanprover/lean4:v4.29.1``). Reads from the repo-root ``lean-toolchain`` file if available, otherwise falls back to parsing ``lean --version``.
()
| 20 | |
| 21 | @lru_cache(maxsize=1) |
| 22 | def lean_toolchain_version() -> str: |
| 23 | """Return the lean-toolchain string (e.g. ``leanprover/lean4:v4.29.1``). |
| 24 | |
| 25 | Reads from the repo-root ``lean-toolchain`` file if available, |
| 26 | otherwise falls back to parsing ``lean --version``. |
| 27 | """ |
| 28 | tc = Path(__file__).resolve().parent.parent / "lean-toolchain" |
| 29 | if tc.exists(): |
| 30 | return tc.read_text().strip() |
| 31 | # Fallback: parse "Lean (version 4.x.y, ...)" |
| 32 | out = run_command(["lean", "--version"]) |
| 33 | # Extract "leanprover/lean4:vX.Y.Z" from version string |
| 34 | for part in out.split(): |
| 35 | if part.startswith("4.") or part.startswith("v4."): |
| 36 | v = part.rstrip(",").lstrip("v") |
| 37 | return f"leanprover/lean4:v{v}" |
| 38 | return out |
| 39 | |
| 40 | |
| 41 | @lru_cache(maxsize=1) |