"""The Claude pilot (pilot.py), unchanged in method, on all twenty steps of the two arguments.

Proposer: Claude through isolated, stateless Claude Code calls (no tools, no files, no
project memory, each from an empty folder). It sees only the vocabulary, the postulates,
any lemmas it has itself proved for the current task, and the statement to prove --
never the repository's proofs. Each task is searched independently.
Statements: ../htps/heldout20.py.  Logs: runs20/.  Proofs: proofs20/.  Summary: summary20.json.
Usage: python3 pilot20.py [task ...]      (no argument: all twenty)
"""
import json, re, subprocess, sys, tempfile, time
from concurrent.futures import ThreadPoolExecutor
from pathlib import Path
HERE = Path(__file__).resolve().parent
sys.path.insert(0, str(HERE)); sys.path.insert(0, str(HERE.parent / "htps"))
import pilot, heldout20

pilot.PREAMBLE = heldout20.PREAMBLE
import os
SUFFIX = os.environ.get("RUN_SUFFIX", "")   # "b" for the repeat run
pilot.RUNS = HERE / f"runs20{SUFFIX}"; pilot.RUNS.mkdir(exist_ok=True)
UNFOLD = ("unfold MP001, MP002, MP003, MP007, MP008, MP009, MP010, MP011, MP012, OP001, OP006, SP001, OfItself, "
          "ThroughAnother, Necessary, Possible, InUniverse, DependsOn, Independent, NonExistencePossible, AggregateOfPossibles in *")
pilot.AUTOMATION = ["intros; firstorder.", f"{UNFOLD}; intros; firstorder.", f"{UNFOLD}; intros; intuition eauto.", f"{UNFOLD}; intros; tauto."]
TASKS = heldout20.TASKS

_check = pilot.Run.check
def _safe_check(self, *a, **k):
    """A proposed proof that makes Rocq run past its time limit is a rejected step, not a crash."""
    try:
        return _check(self, *a, **k)
    except subprocess.TimeoutExpired:
        return False, "Rocq check timed out (60 s)"
pilot.Run.check = _safe_check
PROOFS = HERE / f"proofs20{SUFFIX}"; PROOFS.mkdir(exist_ok=True)


def one(task):
    stmt = TASKS[task]
    run = pilot.Run(task)
    t0 = time.time()
    base = None
    for tac in pilot.AUTOMATION:
        ok, _ = run.check([], [], f"{task}_baseline", stmt, tac)
        if ok:
            base = tac; break
    run.record(kind="baseline", stmt=stmt, solved=base is not None, tactic=base)
    top = run.prove(stmt, 0, [])
    result = {"baseline_solved": base is not None, "pilot_solved": top is not None, "model_calls": run.calls,
              "seconds": round(time.time() - t0, 1)}
    if top:
        f = PROOFS / f"{task}.v"
        f.write_text(pilot.final_file(run, top))
        with tempfile.TemporaryDirectory() as d:
            g = Path(d) / "Final.v"; g.write_text(f.read_text())
            r = subprocess.run(["coqc", "-q", str(g)], capture_output=True, text=True, timeout=120)
        text = r.stdout + r.stderr
        axioms = re.findall(r"^(\S+) :", text.split("Axioms:")[-1], re.M) if "Axioms:" in text else []
        result.update(final_compiles=r.returncode == 0, forbidden=bool(re.search(r"\b(Admitted|admit|Axiom)\b", f.read_text())),
                      axioms=axioms, closed="Closed under the global context" in text, lemmas_used=len(run.lemmas))
    run.record(kind="result", **result)
    print(task, json.dumps(result), flush=True)
    return task, result


if __name__ == "__main__":
    tasks = sys.argv[1:] or list(TASKS)
    with ThreadPoolExecutor(4) as ex:
        summary = dict(ex.map(one, tasks))
    old = json.loads((HERE / f"summary20{SUFFIX}.json").read_text()) if (HERE / f"summary20{SUFFIX}.json").exists() else {}
    summary = {**old, **summary}
    (HERE / f"summary20{SUFFIX}.json").write_text(json.dumps(summary, indent=2))
    tasks = list(summary)
    ok = [t for t, r in summary.items() if r["pilot_solved"] and r.get("final_compiles") and not r.get("forbidden")
          and set(r.get("axioms", [])) <= {"classic"}]
    print(f"PROVED {len(ok)} of {len(tasks)}", flush=True)