"""Stage 5 gate: the Lean 4 project under formal/ must build with no `sorry` and no user axioms.

The build itself is slow (a few minutes, SAT solving) and needs the elan toolchain, so it only
runs when WP34_LEAN_BUILD=1 is set:  WP34_LEAN_BUILD=1 .venv/bin/python -m pytest tests/test_formal_lean.py -v
The static checks (no sorry / no axiom / toolchain pinned / no Mathlib) always run.
"""
from __future__ import annotations
import os, re, shutil, subprocess
from pathlib import Path
import pytest

ROOT = Path(__file__).resolve().parents[1]
FORMAL = ROOT / "formal"
LEAN_FILES = sorted((FORMAL / "Wp34").glob("*.lean")) + [FORMAL / "Wp34.lean"]


def _strip_comments(src: str) -> str:
    src = re.sub(r"/-.*?-/", "", src, flags=re.S)
    return re.sub(r"--[^\n]*", "", src)


def test_lean_sources_exist():
    assert (FORMAL / "lakefile.toml").exists()
    assert len(LEAN_FILES) >= 6


def test_toolchain_pinned():
    assert (FORMAL / "lean-toolchain").read_text().strip() == "leanprover/lean4:v4.35.0"


def test_no_mathlib_dependency():
    assert "mathlib" not in (FORMAL / "lakefile.toml").read_text().lower()
    for f in LEAN_FILES:
        assert "import Mathlib" not in f.read_text(), f


@pytest.mark.parametrize("path", LEAN_FILES, ids=[p.name for p in LEAN_FILES])
def test_no_sorry_no_axiom(path: Path):
    code = _strip_comments(path.read_text())
    assert not re.search(r"\bsorry\b", code), f"sorry in {path.name}"
    assert not re.search(r"^\s*axiom\b", code, flags=re.M), f"axiom in {path.name}"
    assert "native_decide" not in code, f"native_decide in {path.name}"


@pytest.mark.skipif(not os.environ.get("WP34_LEAN_BUILD"), reason="set WP34_LEAN_BUILD=1 to run lake build")
def test_lake_build_succeeds():
    env = dict(os.environ)
    env["PATH"] = str(Path.home() / ".elan" / "bin") + os.pathsep + env.get("PATH", "")
    if shutil.which("lake", path=env["PATH"]) is None:
        pytest.skip("lake (elan) not installed")
    r = subprocess.run(["lake", "build"], cwd=FORMAL, env=env, capture_output=True, text=True,
                       timeout=1800)
    assert r.returncode == 0, r.stdout[-4000:] + r.stderr[-4000:]
    assert "error" not in r.stdout.lower()