#!/usr/bin/env python3
"""Check proof generation from a project that depends on formalsw by path."""
from pathlib import Path
import subprocess
import tempfile

REPO = Path(__file__).resolve().parents[2]

with tempfile.TemporaryDirectory(prefix="formalsw-project-") as temporary:
    project = Path(temporary)
    subprocess.run(["git", "init", "-q", str(project)], check=True)
    (project / "lean-toolchain").write_text((REPO / "lean-toolchain").read_text())
    (project / "lakefile.toml").write_text(
        f'name = "external_proofs"\n[[require]]\nname = "formalsw"\npath = "{REPO}"\n'
    )
    for directory in ("left", "right"):
        (project / directory).mkdir()
        if directory == "left":
            subprocess.run(["git", "init", "-q", str(project / directory)], check=True)
        else:
            # A stray directory is not a nested worktree.
            (project / directory / ".git").mkdir()
        source = project / directory / "1.py"
        source.write_text(
            'def f(n: int) -> int:\n'
            '    """@formalsw: theorem returns (n : Int) : Returns(this_function(n))"""\n'
            '    return n\n'
        )
        module = f"{directory.capitalize()}.P1Ast"
        ast_module = ('left.«.formalsw».«1.py.ast»' if directory == "left"
                      else '«.formalsw».right.«1.py.ast»')
        imports = f'import {ast_module}\nimport FormalSW\n'
        if directory == "right":
            imports += 'import left.«1.py»\n'
        source.with_suffix(".py.lean").write_text(
            imports + f'namespace {directory}.«1»\nopen FormalSW.PyAst\n'
            f'theorem f.returns (n : Int) : (scalarFunction {module}.module "f" [.int n]).Returns := '
            '⟨.int n, .done rfl⟩\n'
            f'end {directory}.«1»\n'
        )
        result = subprocess.run(
            [str(REPO / "formalsw"), str(source)], cwd=project,
            text=True, capture_output=True,
        )
        assert result.returncode == 0, result.stdout + result.stderr
        assert f"All {1 if directory == 'left' else 2} checks passed" in result.stdout, result.stdout
    compiler_check = project / "compiler_check.lean"
    compiler_check.write_text(
        'import FormalSW\n'
        'def parsed : FormalSW.PyAst.Module := python_data% "def f(n):\\n    return n\\n"\n'
        'example : parsed.body.length = 1 := by decide\n'
    )
    result = subprocess.run(
        ["lake", "env", "lean", str(compiler_check)], cwd=project, text=True, capture_output=True,
    )
    assert result.returncode == 0, result.stdout + result.stderr
    # Checking only the importing solver must recheck the current dependency,
    # even when a previous successful object's cache remains on disk.
    left = project / "left" / "1.py"
    original = left.read_text()
    left.write_text(original.replace("return n", "return n + 1"))
    result = subprocess.run(
        [str(REPO / "formalsw"), str(project / "right" / "1.py")], cwd=project,
        text=True, capture_output=True,
    )
    assert result.returncode != 0, result.stdout
    assert "imported Python proof failed" in result.stderr, result.stderr
    left.write_text(original)
    left_proof = left.with_suffix(".py.lean")
    left_proof.write_text('import right.«1.py»\n' + left_proof.read_text())
    result = subprocess.run(
        [str(REPO / "formalsw"), str(project / "right" / "1.py")], cwd=project,
        text=True, capture_output=True,
    )
    assert result.returncode != 0, result.stdout
    assert "cyclic Python proof imports" in result.stderr, result.stderr
print("External projects, numeric filenames, and fresh proof dependencies passed")
