1"""Stage 5 gate: the Lean 4 project under formal/ must build with no `sorry` and no user axioms.23The build itself is slow (a few minutes, SAT solving) and needs the elan toolchain, so it only4runs when WP34_LEAN_BUILD=1 is set: WP34_LEAN_BUILD=1 .venv/bin/python -m pytest tests/test_formal_lean.py -v5The static checks (no sorry / no axiom / toolchain pinned / no Mathlib) always run.6"""7from __future__ import annotations8import os, re, shutil, subprocess9from pathlib import Path10import pytest1112ROOT = Path(__file__).resolve().parents[1]13FORMAL = ROOT / "formal"14LEAN_FILES = sorted((FORMAL / "Wp34").glob("*.lean")) + [FORMAL / "Wp34.lean"]151617def _strip_comments(src: str) -> str:18 src = re.sub(r"/-.*?-/", "", src, flags=re.S)19 return re.sub(r"--[^\n]*", "", src)202122def test_lean_sources_exist():23 assert (FORMAL / "lakefile.toml").exists()24 assert len(LEAN_FILES) >= 6252627def test_toolchain_pinned():28 assert (FORMAL / "lean-toolchain").read_text().strip() == "leanprover/lean4:v4.35.0"293031def test_no_mathlib_dependency():32 assert "mathlib" not in (FORMAL / "lakefile.toml").read_text().lower()33 for f in LEAN_FILES:34 assert "import Mathlib" not in f.read_text(), f353637@pytest.mark.parametrize("path", LEAN_FILES, ids=[p.name for p in LEAN_FILES])38def test_no_sorry_no_axiom(path: Path):39 code = _strip_comments(path.read_text())40 assert not re.search(r"\bsorry\b", code), f"sorry in {path.name}"41 assert not re.search(r"^\s*axiom\b", code, flags=re.M), f"axiom in {path.name}"42 assert "native_decide" not in code, f"native_decide in {path.name}"434445@pytest.mark.skipif(not os.environ.get("WP34_LEAN_BUILD"), reason="set WP34_LEAN_BUILD=1 to run lake build")46def test_lake_build_succeeds():47 env = dict(os.environ)48 env["PATH"] = str(Path.home() / ".elan" / "bin") + os.pathsep + env.get("PATH", "")49 if shutil.which("lake", path=env["PATH"]) is None:50 pytest.skip("lake (elan) not installed")51 r = subprocess.run(["lake", "build"], cwd=FORMAL, env=env, capture_output=True, text=True,52 timeout=1800)53 assert r.returncode == 0, r.stdout[-4000:] + r.stderr[-4000:]54 assert "error" not in r.stdout.lower()55