diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index edde5be01f..88ec2fc028 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -392,13 +392,24 @@ def _check_axioms(root: Path) -> list[_QualityError]: temp_file.flush() try: - process = subprocess.run( - ["lake", "env", "lean", str(temp_path)], - cwd=root, - check=False, - capture_output=True, - text=True, - ) + try: + process = subprocess.run( + ["lake", "env", "lean", str(temp_path)], + cwd=root, + check=False, + capture_output=True, + text=True, + ) + except FileNotFoundError: + # `lake` not on PATH; surface a single advisory error rather + # than crashing the whole quality run. + return [ + _QualityError( + root / "LeanPool.lean", + 1, + "axiom audit skipped: `lake` not found", + ) + ] finally: temp_path.unlink(missing_ok=True) @@ -678,13 +689,23 @@ def _check_project_declarations( temp_file.flush() try: - process = subprocess.run( - ["lake", "env", "lean", str(temp_path)], - cwd=root, - check=False, - capture_output=True, - text=True, - ) + try: + process = subprocess.run( + ["lake", "env", "lean", str(temp_path)], + cwd=root, + check=False, + capture_output=True, + text=True, + ) + except FileNotFoundError: + # `lake` not on PATH (sandboxed CI, contributor without Lean). + # Treat the same as `--skip-lean-axioms`: emit a single advisory + # error so callers know the check was skipped, rather than crash. + return [ + _QualityError( + path, 1, "project declarations check skipped: `lake` not found" + ) + ] finally: temp_path.unlink(missing_ok=True) diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index c67d1c08e5..1cb4d93dfa 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -3,6 +3,7 @@ from __future__ import annotations from pathlib import Path +from unittest.mock import patch from lean_pool.quality import ( _axiom_audit_missing, @@ -190,6 +191,44 @@ def test_quality_check_accepts_project_card_after_imports(tmp_path: Path) -> Non assert not any("project card for p is out of date" in e.message for e in errors) +def test_quality_check_falls_back_when_lake_missing(tmp_path: Path) -> None: + """A missing `lake` binary yields a single advisory error, not a crash. + + The python_ci job runs without a Lean toolchain, so the subprocess + that invokes ``lake env lean`` raises ``FileNotFoundError``. The + quality module must catch that and emit a clear "skipped" message + rather than aborting the whole run. + """ + _write_minimal_repo(tmp_path) + (tmp_path / "LeanPool.lean").write_text( + "import LeanPool.Basic\nimport LeanPool.MyProj\n" + ) + card = ( + "/-!\n" + "# Test Project\n" + "\n" + "Source: arxiv:1234.5678\n" + "Authors: Test Author\n" + "Status: verified\n" + "Main declarations: `hello`\n" + "Tags: test\n" + "-/\n" + ) + (tmp_path / "LeanPool" / "MyProj.lean").write_text( + f"{HEADER}\nimport LeanPool.Basic\n\n{card}\ndef hello : Nat := 1\n" + ) + _write_project_yaml(tmp_path, [{"slug": "p", "entry_module": "LeanPool.MyProj"}]) + + with patch( + "lean_pool.quality.subprocess.run", + side_effect=FileNotFoundError("[Errno 2] No such file or directory: 'lake'"), + ): + errors = run_checks(tmp_path) + + messages = [error.message for error in errors] + assert any("`lake` not found" in message for message in messages) + + def test_quality_check_rejects_non_verified_status(tmp_path: Path) -> None: """Only `status: verified` projects may merge; `draft` is not accepted.""" _write_minimal_repo(tmp_path)