"""Build and audit the submission using the supplied, fixed Lean environment.

Use `lake env python3 build.py` when Lake's fixed dependencies are installed.
Alternatively pass --lean and --lean-path, or set LEAN_EXE and LEAN_PATH.
This script does not download dependencies or read environment.json.
"""
import argparse
import json
import os
from pathlib import Path
import subprocess


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--lean", default=os.environ.get("LEAN_EXE", "lean"))
    parser.add_argument("--lean-path", default=os.environ.get("LEAN_PATH", ""))
    args = parser.parse_args()
    root = Path(__file__).resolve().parent
    out = root / ".build"
    out.mkdir(exist_ok=True)
    env = os.environ.copy()
    env["LEAN_PATH"] = os.pathsep.join(
        part for part in (str(out), str(root), args.lean_path) if part
    )
    version = subprocess.check_output(
        [args.lean, "--version"], cwd=root, env=env, text=True
    )
    if "4.29.1" not in version or "f72c35b3f637c8c6571d353742168ab66cc22c00" not in version:
        raise RuntimeError("The required Lean 4.29.1 compiler commit is not active")
    print(version.strip(), flush=True)
    backgrounds = [
        "ch_01_foundations/gauge_space",
        "ch_01_foundations/operator_space",
        "ch_01_foundations/metric_entropy",
        "ch_02_operator_bounds/lip_matrix",
        "ch_02_operator_bounds/decoupling",
        "ch_02_operator_bounds/single_channel",
    ]
    files = ["formal_oet/vol_01/" + name + ".lean" for name in backgrounds]
    files += ["Main.lean", "Audit.lean"]
    for name in files:
        target = out / Path(name).with_suffix(".olean")
        target.parent.mkdir(parents=True, exist_ok=True)
        subprocess.run(
            [args.lean, "-o", str(target), name], cwd=root, env=env, check=True
        )

    ledger = json.loads((root / "alignment.json").read_text(encoding="utf-8"))
    audit = json.loads((out / "audit.json").read_text(encoding="utf-8"))
    counts = [3, 3, 1, 2, 1, 8, 4, 3, 3, 3, 3, 2, 3, 3, 2,
              3, 4, 3, 3, 1, 2, 1, 3, 2, 2, 3, 2, 2, 5, 4]
    expected = {f"CH03-D{n:02}" for n in range(1, 9)}
    expected |= {f"CH03-P{p:02}-{n:02}"
                 for p, count in enumerate(counts, 1)
                 for n in range(1, count + 1)}
    items = ledger["items"]
    if ledger["case_id"] != "MG-C003" or ledger["version"] != "0.1.1":
        raise RuntimeError("Wrong alignment case or version")
    if len(items) != 92 or {item["id"] for item in items} != expected:
        raise RuntimeError("Alignment must contain each of the 92 IDs exactly once")
    owners = {}
    for item in items:
        if item["status"] != "complete" or not item["representation"].strip():
            raise RuntimeError("An obligation is not marked complete with a representation")
        if not item["declarations"] or not set(item["dependencies"]) <= expected:
            raise RuntimeError("Invalid declarations or dependency IDs")
        for declaration in item["declarations"]:
            name, file = declaration["name"], declaration["file"]
            permitted = file == "Main.lean" or (
                item["id"] == "CH03-D07" and
                file == "formal_oet/vol_01/ch_01_foundations/metric_entropy.lean"
            )
            module = file.removesuffix(".lean").replace("/", ".")
            if not permitted or name not in audit or audit[name]["module"] != module:
                raise RuntimeError(f"Missing or wrongly located declaration: {declaration}")
            owners.setdefault(name, item["id"])
    for item in items:
        roots = {declaration["name"] for declaration in item["declarations"]}
        visited, dependencies = set(roots), set()
        todo = [used for name in roots for used in audit[name]["uses"]]
        while todo:
            name = todo.pop()
            if name in visited:
                continue
            visited.add(name)
            if name in owners and owners[name] != item["id"]:
                dependencies.add(owners[name])
            elif name in audit:
                todo.extend(audit[name]["uses"])
        if dependencies != set(item["dependencies"]):
            raise RuntimeError(f"Dependency mismatch for {item['id']}")
    print("Compiled and audited; all 92 alignment entries validated.")


if __name__ == "__main__":
    main()