"""Lean Refactor Arena — competition UI.

This Space is UI-only. It renders the site, accepts submissions, and shows
progress + leaderboards. All Lean compilation and scoring happens on a
dedicated evaluation worker that talks to this Space exclusively through the
storage bucket mounted at /data:

  uploads/<user>/<ts>.jsonl     submission archive        (written here)
  jobs/pending/<sid>.json       job queue                 (written here,
                                                           consumed by worker)
  status/<user>.json            per-user progress         (written by worker,
                                                           polled here)
  leaderboard.json              scored results            (written by worker,
                                                           read here)
  worker/heartbeat.json         worker liveness           (written by worker)
  compat_logs/...               full compile logs         (written by worker)

Nothing in this container installs or runs Lean.
"""

import base64
import html
import json
import os
import re
import shutil
from datetime import datetime, timezone
from pathlib import Path

import gradio as gr

from benchmark import (
    BENCHMARK,
    SOURCES,
    benchmark_file_link,
    benchmark_header,
    benchmark_names,
    benchmark_signature,
    benchmark_source,
    benchmark_versions,
    original_heartbeats,
    original_length,
)
from leaderboard import Leaderboard


# ── Storage plumbing ──────────────────────────────────────────────────────────
def _data_root() -> Path:
    """Bucket mount if present, else a local dir (dev runs outside HF)."""
    persistent = Path("/data")
    if persistent.is_dir() and os.access(persistent, os.W_OK):
        return persistent
    d = Path("/tmp/lra-data")
    d.mkdir(parents=True, exist_ok=True)
    return d


def _uploads_dir() -> Path:
    d = _data_root() / "uploads"
    d.mkdir(parents=True, exist_ok=True)
    return d


def _jobs_pending_dir() -> Path:
    d = _data_root() / "jobs" / "pending"
    d.mkdir(parents=True, exist_ok=True)
    return d


def _status_root() -> Path:
    d = _data_root() / "status"
    d.mkdir(parents=True, exist_ok=True)
    return d


def _safe_user(user: str) -> str:
    return re.sub(r"[^A-Za-z0-9_-]", "_", user)[:40] or "anon"


def _sanitize(name: str) -> str:
    s = re.sub(r"[^A-Za-z0-9_]", "_", name or "")[:60]
    return s or "Anon"


def _validate_user(user: str) -> str:
    user = (user or "").strip()
    if not user:
        raise ValueError("Username is required.")
    if len(user) > 40:
        raise ValueError("Username must be 40 characters or fewer.")
    return user


def _archive_upload(user: str, source: str) -> tuple[str | None, str | None]:
    """Copy an uploaded JSONL into the bucket. Returns (abs_path, rel_path)."""
    ts = datetime.now(timezone.utc).strftime("%Y%m%dT%H%M%SZ")
    user_dir = _uploads_dir() / _safe_user(user)
    user_dir.mkdir(parents=True, exist_ok=True)
    dest = user_dir / f"{ts}.jsonl"
    try:
        shutil.copyfile(source, dest)
        return str(dest), f"uploads/{_safe_user(user)}/{ts}.jsonl"
    except Exception:
        return None, None


def _status_path(user: str) -> Path:
    return _status_root() / f"{_safe_user(user)}.json"


def _write_status(
    user: str, submission_id: str, status: str,
    rows: list, message: str,
) -> None:
    """Atomically persist the current submission status for `user`."""
    p = _status_path(user)
    payload = {
        "user": user,
        "submission_id": submission_id,
        "status": status,
        "progress_rows": rows,
        "message": message,
        "ts": datetime.now(timezone.utc).isoformat(timespec="seconds"),
    }
    try:
        tmp = p.with_suffix(".json.tmp")
        tmp.write_text(json.dumps(payload))
        os.replace(tmp, p)
    except Exception:
        pass


def submission_status(user: str):
    """Read the persisted status for `user` (written by the evaluation
    worker). Returns (rows, status_md)."""
    user = (user or "").strip()
    if not user:
        return [], ""
    try:
        p = _status_path(user)
        if not p.exists():
            return [], ""
        d = json.loads(p.read_text())
    except Exception:
        return [], ""
    rows = d.get("progress_rows", []) or []
    msg = d.get("message", "") or ""
    status = d.get("status", "")
    ts = d.get("ts", "")
    prefix = {
        "queued": "📨", "running": "⏳", "done": "✅", "error": "❌",
    }.get(status, "")
    md = (f"{prefix} {msg}" if prefix else msg)
    if ts:
        md += f"  \n_updated {ts}_"
    return rows, md


def _enqueue_job(
    user: str, track: str, submission_id: str,
    upload_rel: str | None, num_rows: int,
) -> None:
    """Drop a job file for the evaluation worker to pick up."""
    payload = {
        "schema_version": 1,
        "user": user,
        "track": track,
        "submission_id": submission_id,
        "upload": upload_rel,
        "num_rows": num_rows,
        "ts": datetime.now(timezone.utc).isoformat(timespec="seconds"),
    }
    p = _jobs_pending_dir() / f"{submission_id}_{_safe_user(user)}.json"
    tmp = p.with_suffix(".json.tmp")
    tmp.write_text(json.dumps(payload, indent=2))
    os.replace(tmp, p)


# ── Submission intake ─────────────────────────────────────────────────────────
# Patterns we refuse to accept in user proofs. Lean's `#eval` and `IO`
# primitives execute at elaboration time with full filesystem and process
# access on the evaluation worker; the rest are ways to bypass the kernel.
_FORBIDDEN_PATTERNS: list[tuple[str, "re.Pattern[str]"]] = [
    ("#eval", re.compile(r"#\s*eval\b")),
    ("#reduce", re.compile(r"#\s*reduce\b")),
    ("IO.", re.compile(r"\bIO\.")),
    ("unsafe def/fun/theorem", re.compile(r"\bunsafe\s+(def|fun|theorem|lemma)\b")),
    ("extern", re.compile(r"\bextern\b")),
    ("initialize", re.compile(r"\binitialize\b")),
    ("@[implemented_by]", re.compile(r"@\[\s*implemented[_]?[Bb]y\b")),
    ("@[extern]", re.compile(r"@\[\s*extern\b")),
]


def _check_forbidden(code: str) -> str | None:
    for label, pat in _FORBIDDEN_PATTERNS:
        if pat.search(code):
            return label
    return None


TRACK_LABELS = {
    "Closed-source LLM": "closed",
    "Open-source LLM": "open",
}

# Flip to True once the evaluation worker is live.
SUBMISSIONS_ENABLED = False
SUBMISSIONS_READY_DATE = "August 12, 2026"


def verify_and_submit(user, track_label, file):
    """Pre-validate a submission, archive it to the bucket, and enqueue a job
    for the evaluation worker. Returns immediately; the worker updates
    status/<user>.json as it compiles, which the UI polls."""
    if not SUBMISSIONS_ENABLED:
        return [], (
            "⚠️ **Submissions are not open yet.** Automated evaluation and "
            f"scoring is being prepared and will be ready by "
            f"**{SUBMISSIONS_READY_DATE}**. Please try again then."
        )
    try:
        user = _validate_user(user)
    except ValueError as e:
        return [], f"**Error:** {e}"
    track = TRACK_LABELS.get(track_label)
    if track is None:
        return [], "**Error:** pick a track (closed-source or open-source LLM)."
    if file is None:
        return [], "**Error:** upload a JSONL file."
    path = file if isinstance(file, str) else getattr(file, "name", None)
    if not path:
        return [], "**Error:** bad upload."

    # Cheap pre-validation so obviously broken files never reach the worker.
    bench = set(benchmark_names())
    n_rows, n_scored, problems = 0, 0, []
    try:
        with open(path, "r", encoding="utf-8") as f:
            for idx, raw in enumerate(f):
                if not raw.strip():
                    continue
                n_rows += 1
                try:
                    entry = json.loads(raw)
                except json.JSONDecodeError as e:
                    problems.append(f"line {idx + 1}: bad JSON ({str(e)[:80]})")
                    continue
                name = str(entry.get("name") or "")
                proof = str(entry.get("proof") or "")
                if not name or not proof:
                    problems.append(f"line {idx + 1}: needs `name` and `proof`")
                    continue
                bad = _check_forbidden(proof)
                if bad:
                    problems.append(f"`{name}`: proof contains `{bad}`, not allowed")
                    continue
                if name in bench:
                    n_scored += 1
    except Exception as e:
        return [], f"**Error:** could not read upload: {e}"

    if problems:
        listing = "\n".join(f"- {p}" for p in problems[:10])
        more = f"\n- …and {len(problems) - 10} more" if len(problems) > 10 else ""
        return [], f"**Rejected — fix these and re-upload:**\n{listing}{more}"
    if n_rows == 0:
        return [], "**Error:** the file has no rows."
    if n_scored == 0:
        return [], (
            "**Error:** no row names a benchmark theorem — nothing would be "
            "scored. Check `name` against the Benchmark tab."
        )

    submission_id = datetime.now(timezone.utc).strftime("%Y%m%dT%H%M%SZ")
    _, rel = _archive_upload(user, path)
    if rel is None:
        return [], "**Error:** could not store the upload; try again."
    _enqueue_job(user, track, submission_id, rel, n_rows)
    _write_status(
        user, submission_id, "queued", [],
        "Submission queued for the evaluation worker. You can close this "
        "tab — progress appears here under the same username.",
    )
    return [], (
        f"📨 **Submission queued** as `{user}` on the "
        f"**{track_label}** track ({submission_id}).  \n"
        f"{n_scored}/{n_rows} row(s) match benchmark theorems and will be "
        f"scored on the dedicated evaluation worker.  \n"
        f"**You can close this tab** — re-enter the same username to watch "
        f"progress, or check the Leaderboard once it's done."
    )


# ── Admin endpoints (token-gated, hidden) ─────────────────────────────────────
def _check_admin_token(token: str) -> bool:
    expected = os.environ.get("ADMIN_RESET_TOKEN", "")
    return bool(expected) and token == expected


def admin_reset(token: str) -> str:
    """Wipe leaderboard + uploads + jobs + logs from /data. Token-gated."""
    if not _check_admin_token(token):
        return "denied"
    out = []
    data_dir = _data_root()
    lb = data_dir / "leaderboard.json"
    if lb.exists():
        lb.unlink()
        out.append("removed leaderboard.json")
    for sub in ("uploads", "compat_logs", "status", "jobs"):
        target = data_dir / sub
        if target.exists():
            shutil.rmtree(target, ignore_errors=True)
            out.append(f"removed {sub}/")
    LB.data = {"users": {}}
    LB.path.parent.mkdir(parents=True, exist_ok=True)
    return "ok: " + ", ".join(out) if out else "ok: nothing to remove"


def _compat_logs_root() -> Path | None:
    d = _data_root() / "compat_logs"
    return d if d.is_dir() else None


def compat_list(token: str, user: str = "", submission_id: str = "") -> str:
    """List stored compile logs (written by the worker). Token-gated."""
    if not _check_admin_token(token):
        return "denied"
    root = _compat_logs_root()
    if root is None:
        return "no logs"
    if not user:
        entries = sorted(p.name for p in root.iterdir() if p.is_dir())
        return "\n".join(entries) if entries else "(empty)"
    user_dir = root / _safe_user(user)
    if not user_dir.is_dir():
        return "not found"
    if not submission_id:
        entries = sorted(p.name for p in user_dir.iterdir() if p.is_dir())
        return "\n".join(entries) if entries else "(empty)"
    sub_dir = user_dir / submission_id
    if not sub_dir.is_dir():
        return "not found"
    entries = sorted(p.name for p in sub_dir.iterdir() if p.is_file())
    return "\n".join(entries) if entries else "(empty)"


def compat_log(
    token: str, user: str, submission_id: str, name: str, version: str,
) -> str:
    """Return the full text of one compile log. Token-gated."""
    if not _check_admin_token(token):
        return "denied"
    root = _compat_logs_root()
    if root is None:
        return "no logs"
    ver_safe = version.replace(".", "_")
    p = root / _safe_user(user) / submission_id / f"{_sanitize(name)}__{ver_safe}.log"
    if not p.is_file():
        return f"not found: {p}"
    try:
        return p.read_text()
    except Exception as e:
        return f"read error: {e}"


LB = Leaderboard()

BENCHMARK_JSONL_PATH = "/home/user/app/benchmark_data_warmup.jsonl"
if not Path(BENCHMARK_JSONL_PATH).exists():
    _local_bench = Path(__file__).resolve().parent / "benchmark_data_warmup.jsonl"
    if _local_bench.exists():
        BENCHMARK_JSONL_PATH = str(_local_bench)

# Contribution guide (rendered on the Contribute tab). The leading H1 is
# dropped — the tab supplies its own themed heading.
_CONTRIB_PATH = Path(__file__).resolve().parent / "contribution.md"
try:
    _contrib_lines = _CONTRIB_PATH.read_text(encoding="utf-8").splitlines()
    if _contrib_lines and _contrib_lines[0].startswith("# "):
        _contrib_lines = _contrib_lines[1:]
    CONTRIBUTION_MD = "\n".join(_contrib_lines).strip()
except OSError:
    CONTRIBUTION_MD = "_Contribution guide coming soon._"

ASSETS_DIR = Path(__file__).resolve().parent / "assets"
SPONSOR_ASSETS_DIR = ASSETS_DIR / "sponsors"
BENCH_ASSETS_DIR = ASSETS_DIR / "benchmarks"
APP_ICON_PATH = ASSETS_DIR / "icon.png"

try:
    _icon_b64 = base64.b64encode(APP_ICON_PATH.read_bytes()).decode("ascii")
    APP_ICON_DATA_URI = f"data:image/png;base64,{_icon_b64}"
except OSError:
    APP_ICON_DATA_URI = ""

# ── Sponsors ──────────────────────────────────────────────────────────────────
SPONSORS: list[dict[str, str]] = [
    {"name": "AWS", "image": "assets/sponsors/aws.png", "url": "https://aws.amazon.com/"},
    {"name": "Simon Fraser University", "image": "assets/sponsors/sfu.png", "url": "https://www.sfu.ca/"},
    {"name": "Cslib", "image": "assets/sponsors/cslib.png", "url": "https://cs-lean.github.io/"},
    {"name": "PhysLib", "image": "assets/sponsors/physlib.png", "url": "https://physlib.io/"},
    {"name": "ArkLib", "image": "assets/sponsors/arklib.png", "url": "https://github.com/Verified-zkEVM/ArkLib"},
    {"name": "The University of Texas at Austin", "image": "assets/sponsors/ut_austin.png", "url": "https://www.utexas.edu/"},
]

# Corpus logo files (assets/benchmarks/); falls back to a text badge.
SOURCE_LOGOS = {
    "strata": "assets/benchmarks/strata.png",
    "physlib": "assets/benchmarks/physlib.png",
    "cslib": "assets/benchmarks/cslib.png",
    "arklib": "assets/benchmarks/arklib.png",
    "putnambench": "assets/benchmarks/putnambench.png",
}

PRIZE_PER_TRACK = "$5,000"
CLOSED_BUDGET = "≤ US$3 API spend per problem"
OPEN_BUDGET = "4× 80 GB A100 · ≤ 48 h for the full benchmark"
FULL_BENCH_SIZE = 50
FULL_BENCH_RELEASE = "October 1, 2026"
DEADLINE = "November 25, 2026"

DISCORD_URL = ""   # invite link — coming soon
ZULIP_URL = ""     # channel link — coming soon

# The workshop this competition is part of.
WORKSHOP_URL = "https://vericodegen.github.io/"
WORKSHOP_NAME = "AI for Verifiable Coding"
WORKSHOP_VENUE = "NeurIPS 2026, Atlanta · Dec 12–13"
WORKSHOP_LINK = (
    f"<a href='{WORKSHOP_URL}' target='_blank' rel='noopener'>"
    f"{WORKSHOP_NAME}</a>"
)

# Shown wherever prize / benchmark-size numbers appear.
DISCLAIMER = (
    "Prize amounts and benchmark size are provisional and may be adjusted "
    "before Sep 1, 2026."
)


# ── Presentation helpers ──────────────────────────────────────────────────────
def _fmt_int(n) -> str:
    try:
        return f"{int(n):,}"
    except Exception:
        return "0"


def _benchmark_stats() -> list[tuple[str, str, str]]:
    return [
        (_fmt_int(FULL_BENCH_SIZE), "Benchmark problems",
         f"full benchmark released Oct 1 · {len(benchmark_names())}-problem "
         "subset live now"),
        (_fmt_int(len(SOURCES)), "Source repositories",
         "Strata · PhysLib · CSLib · ArkLib · PutnamBench"),
        ("2", "Competition tracks",
         "closed-source LLM · open-source LLM"),
        (PRIZE_PER_TRACK, "Prize per track",
         "plus a dedicated talk at the workshop"),
    ]


def _stat_band_html() -> str:
    cells = "".join(
        "<div class='lra-stat'>"
        f"<div class='lra-stat-num'>{value}</div>"
        f"<div class='lra-stat-label'>{label}</div>"
        f"<div class='lra-stat-note'>{note}</div>"
        "</div>"
        for value, label, note in _benchmark_stats()
    )
    return f"<section class='lra-stat-band'>{cells}</section>"


_LEAN_KEYWORDS = (
    "theorem", "lemma", "example", "def", "by", "fun", "intro", "intros",
    "exact_mod_cast", "exact", "simp_all", "simpa", "simp", "decide",
    "constructor", "refine", "rfl", "rw", "calc", "have", "show", "from",
    "with", "set_option", "import", "open", "sorry", "apply", "omega",
    "norm_num", "ring", "nlinarith", "linarith", "interval_cases", "induction",
)
_LEAN_KW_RE = re.compile(r"\b(" + "|".join(_LEAN_KEYWORDS) + r")\b")


def _lean_highlight(src: str) -> str:
    """Tiny, dependency-free Lean syntax highlighter for illustrative snippets."""
    s = src.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;")
    out = []
    for line in s.split("\n"):
        idx = line.find("--")
        code, comment = (line[:idx], line[idx:]) if idx != -1 else (line, "")
        code = _LEAN_KW_RE.sub(r"<span class='k'>\1</span>", code)
        code = re.sub(r"\b(\d[\d.]*)\b", r"<span class='n'>\1</span>", code)
        if comment:
            comment = f"<span class='c'>{comment}</span>"
        out.append(code + comment)
    return "<pre class='lra-code'><code>" + "\n".join(out) + "</code></pre>"


def _asset_uri(rel: str) -> str:
    path = Path(__file__).resolve().parent / rel
    return f"/gradio_api/file={path}"


def _sponsor_strip_html() -> str:
    if not SPONSORS:
        return ""
    items = []
    for sp in SPONSORS:
        name = sp.get("name", "Sponsor")
        image = sp.get("image", "")
        url = sp.get("url", "")
        logo = (
            f"<img src='{_asset_uri(image)}' alt='{name}' loading='lazy'>"
            if image else f"<span>{name}</span>"
        )
        if url:
            logo = f"<a href='{url}' target='_blank' rel='noopener' title='{name}'>{logo}</a>"
        items.append(f"<div class='lra-logo'>{logo}</div>")
    return (
        "<section class='lra-sponsors'>"
        "<div class='lra-kicker'>Supported by</div>"
        f"<div class='lra-logo-row'>{''.join(items)}</div>"
        "</section>"
    )


def _timeline_html() -> str:
    steps = [
        ("Now → Sep 30, 2026", "Warm-up — submissions open",
         f"The public {len(benchmark_names())}-problem development subset is "
         "live and submissions are open now. Tune your pipeline and climb the "
         "practice leaderboard."),
        ("Oct 1, 2026", "Full benchmark",
         f"The full {FULL_BENCH_SIZE}-problem benchmark is released and the "
         "leaderboard is refreshed — entries are evaluated on the full "
         "benchmark (proofs + code + tech report) from here on."),
        ("Nov 25, 2026", "Deadline & awards",
         "Submissions close. Organizers reproduce the top entries; each track "
         f"winner receives {PRIZE_PER_TRACK} and a dedicated presentation at "
         f"the {WORKSHOP_LINK} workshop ({WORKSHOP_VENUE})."),
    ]
    cells = "".join(
        "<div class='lra-tl-step'>"
        f"<div class='lra-tl-when'>{when}</div>"
        f"<div class='lra-tl-name'>{name}</div>"
        f"<p>{desc}</p>"
        "</div>"
        for when, name, desc in steps
    )
    return (
        "<section class='lra-card'>"
        "<div class='lra-kicker'>Timeline</div>"
        "<h2>From warm-up to awards</h2>"
        "<p class='lra-lead'>Submissions are <b>open now</b> on the public "
        f"subset. The full {FULL_BENCH_SIZE}-problem benchmark drops "
        "<b>Oct 1</b> and the leaderboard refreshes; everything closes "
        "<b>Nov 25, 2026</b>.</p>"
        f"<div class='lra-tl-grid'>{cells}</div>"
        "</section>"
    )


def _tracks_html(compact: bool = True) -> str:
    closed_pts = [
        "Use any <b>closed-source frontier LLM</b> through its API — and build "
        "whatever harness you like around it.",
        f"<b>Budget:</b> {CLOSED_BUDGET}.",
        "<b>Submit:</b> refactored proofs + the code that produced them, so "
        "organizers can reproduce the run + short tech report.",
    ]
    open_pts = [
        "Use <b>open-source models</b> (publicly available weights). "
        "Post-train them, build a harness around them, or both.",
        f"<b>Budget:</b> must run on {OPEN_BUDGET}.",
        "<b>Submit:</b> refactored proofs + code (training and inference), so "
        "organizers can reproduce the run + short tech report.",
    ]

    def card(tag, name, pts):
        lis = "".join(f"<li>{p}</li>" for p in pts)
        return (
            "<div class='lra-track'>"
            f"<div class='lra-metric-tag'>{tag}</div>"
            f"<div class='lra-track-name'>{name}</div>"
            f"<ul>{lis}</ul>"
            f"<div class='lra-track-prize'>🏆 Winner: <b>{PRIZE_PER_TRACK}</b> "
            f"+ a dedicated talk at the {WORKSHOP_LINK} workshop</div>"
            "</div>"
        )

    note = (
        "<p class='lra-lead' style='margin-top:14px'>Tech report format and "
        "the full fine print live in <b>Tracks &amp; Rules → Tech "
        f"report</b>. <i>{DISCLAIMER}</i></p>"
        if compact else
        f"<p class='lra-lead' style='margin-top:14px'><i>{DISCLAIMER}</i></p>"
    )
    return (
        "<section class='lra-card'>"
        "<div class='lra-kicker'>Two tracks</div>"
        "<h2>Pick your compute, pick your track</h2>"
        "<p class='lra-lead'>The arena runs the same benchmark under two "
        "resource regimes, ranked separately.</p>"
        "<div class='lra-track-grid'>"
        + card("track 1", "Closed-source LLM", closed_pts)
        + card("track 2", "Open-source LLM", open_pts)
        + "</div>"
        + note
        + "</section>"
    )


def _sources_html(heading: bool = True) -> str:
    cards = []
    for key, meta in SOURCES.items():
        logo_rel = SOURCE_LOGOS.get(key)
        logo = (
            f"<img class='lra-src-logo' src='{_asset_uri(logo_rel)}' "
            f"alt='{meta['label']}' loading='lazy'>"
            if logo_rel else ""
        )
        cards.append(
            "<div class='lra-src'>"
            f"{logo}"
            "<div class='lra-src-body'>"
            f"<div class='lra-src-name'><a href='{meta['url']}' target='_blank' "
            f"rel='noopener'>{meta['label']}</a></div>"
            f"<p>{meta['blurb']}</p>"
            "</div></div>"
        )
    head = (
        "<div class='lra-kicker'>The benchmark</div>"
        "<h2>Real proofs from real developments</h2>"
        "<p class='lra-lead'>Every problem is a long reference proof taken "
        "verbatim from an active formalization project (plus a slice of "
        "competition mathematics), selected in consultation with the "
        "repository maintainers. Your job: re-prove the same statement "
        "shorter, cheaper, and more robustly. The current set is a "
        "<b>development subset</b> — the <b>full benchmark</b> is released "
        f"on <b>{FULL_BENCH_RELEASE}</b>.</p>"
        if heading else ""
    )
    return (
        "<section class='lra-card'>"
        + head
        + f"<div class='lra-src-grid'>{''.join(cards)}</div>"
        + "</section>"
    )


def _metric_cards_html() -> str:
    metrics = [
        ("length reduction %", "Proof Length",
         "Decrease in proof token counts compared against the original proof "
         "before refactoring. Higher is better."),
        ("heartbeat reduction %", "Compilation Cost",
         "Change in Lean's <a href='https://lean-lang.org/doc/reference/latest/IO/Timing/#IO___getNumHeartbeats' target='_blank' rel='noopener noreferrer'><code>#count_heartbeats</code></a>, "
         "the number of “small” memory allocations performed on the current "
         "execution thread. Positive values indicate cheaper (typically "
         "faster) compilation; negative values indicate costlier compilation."),
        ("zero-shot %", "Version transfer",
         "The fraction of a problem's listed Lean toolchains on which the "
         "accepted proof compiles unchanged."),
    ]
    cards = "".join(
        "<div class='lra-metric'>"
        f"<div class='lra-metric-tag'>{tag}</div>"
        f"<div class='lra-metric-name'>{name}</div>"
        f"<p>{desc}</p>"
        "</div>"
        for tag, name, desc in metrics
    )
    return (
        "<section class='lra-card lra-scoring'>"
        "<div class='lra-kicker'>How scoring works</div>"
        "<h2>Three numbers, one ranking</h2>"
        "<p class='lra-lead'>Every accepted proof is scored on two reduction "
        "axes and a cross-version transfer check. The default rank — "
        "<b>combined %</b> — is the mean of all three; rows that fail to "
        "compile, change the statement, or contain <code>sorry</code> score "
        "zero.</p>"
        f"<div class='lra-metric-grid'>{cards}</div>"
        "</section>"
    )


def _claims_html() -> str:
    shorter_cheap = _lean_highlight(
        "-- 3-line proof · 4,331,226 heartbeats\n"
        "theorem amc12_2001_p21\n"
        "    (a b c d : ℕ)\n"
        "    (h₀ : a * b * c * d = Nat.factorial 8)\n"
        "    (h₁ : a * b + a + b = 524)\n"
        "    (h₂ : b * c + b + c = 146)\n"
        "    (h₃ : c * d + c + d = 104) :\n"
        "    ↑a - ↑d = (10 : ℤ) := by\n"
        "  norm_num [Nat.factorial] at h₀\n"
        "  have : b ≤ 525 := by nlinarith\n"
        "  interval_cases b <;> simp_all <;> nlinarith"
    )
    longer_cheap = _lean_highlight(
        "-- 130+ line proof · 157,079 heartbeats  (27× cheaper)\n"
        "theorem amc12_2001_p21\n"
        "    (a b c d : ℕ) ... :\n"
        "    ↑a - ↑d = (10 : ℤ) := by\n"
        "  -- factor: (x+1)(y+1) = x*y + x + y + 1\n"
        "  have h₄ : (a + 1) * (b + 1) = 525 := by ...\n"
        "  have h₅ : (b + 1) * (c + 1) = 147 := by ...\n"
        "  have h₆ : (c + 1) * (d + 1) = 105 := by ...\n"
        "  -- pin b via gcd, then back-solve each variable\n"
        "  have h₇ : b = 20 := by\n"
        "    have : b + 1 ∣ Nat.gcd 525 147 := Nat.dvd_gcd ‹_› ‹_›\n"
        "    interval_cases b <;> omega\n"
        "  have h₈ : a = 24 := by ...\n"
        "  have h₉ : c = 6  := by ...\n"
        "  have h₁₀ : d = 14 := by ...\n"
        "  exact_mod_cast h₁₁"
    )
    compat_ok = _lean_highlight(
        "-- Lean v4.24.0  ✓ compiles\n"
        "-- a single term ≤ the whole nonneg sum\n"
        "example (f : ℕ → ℝ) (hf : Summable f)\n"
        "    (hpos : ∀ n, 0 ≤ f n) :\n"
        "    f 0 ≤ ∑' n, f n :=\n"
        "  le_tsum hf 0 (fun j _ => hpos j)"
    )
    compat_bad = _lean_highlight(
        "-- Lean v4.28.0  ✗ unknown identifier 'le_tsum'\n"
        "example (f : ℕ → ℝ) (hf : Summable f)\n"
        "    (hpos : ∀ n, 0 ≤ f n) :\n"
        "    f 0 ≤ ∑' n, f n :=\n"
        "  le_tsum hf 0 (fun j _ => hpos j)"
    )
    return (
        "<section class='lra-claims'>"
        "<div class='lra-claim'>"
        "<div class='lra-claim-copy'>"
        "<div class='lra-kicker'>Why it is hard</div>"
        "<h2>Shorter <span class='lra-accent'>≠</span> cheaper</h2>"
        "<p>Two proofs of the same miniF2F theorem, "
        "<code>amc12_2001_p21</code>. The 3-line version leans on a single heavy "
        "cascade — <code>interval_cases</code> over <code>b ≤ 525</code> firing "
        "<code>nlinarith</code> and <code>simp_all</code> across hundreds of "
        "branches — and burns <b>4,331,226 heartbeats</b>. The explicit 130-line "
        "version factors the constraints and pins each variable by hand for just "
        "<b>157,079</b> — over <b>27× cheaper</b> to elaborate. Optimizing only for "
        "shorter text can wreck compilation cost; the arena scores both.</p>"
        "</div>"
        f"<div class='lra-code-pair'>{shorter_cheap}{longer_cheap}</div>"
        "</div>"
        "<div class='lra-claim'>"
        "<div class='lra-claim-copy'>"
        "<div class='lra-kicker'>Why it matters</div>"
        "<h2>Lean ships weekly. Does your proof still <span class='lra-accent'>compile?</span></h2>"
        "<p>The same proof, two toolchains. <code>le_tsum</code> — <i>any single "
        "term of a nonnegative summable series is at most its total</i> — resolves "
        "on one toolchain but a later release answers <code>unknown identifier "
        "'le_tsum'</code>. Lemmas are renamed and removed every release, so a "
        "proof that is flawless today can rot tomorrow. Every benchmark problem "
        "lists the toolchains it is re-checked on, and the transfer rate is a "
        "third of your score.</p>"
        "</div>"
        f"<div class='lra-code-pair'>{compat_ok}{compat_bad}</div>"
        "</div>"
        "</section>"
    )


def _community_html() -> str:
    def btn(label, url, icon):
        if url:
            return (
                f"<a class='lra-paper-btn' href='{url}' target='_blank' "
                f"rel='noopener'>{icon} {label}</a>"
            )
        return (
            f"<span class='lra-paper-btn lra-btn-soon' title='Link coming soon'>"
            f"{icon} {label} · coming soon</span>"
        )
    return (
        "<section class='lra-card'>"
        "<div class='lra-kicker'>Community</div>"
        "<h2>Questions? Join the conversation</h2>"
        "<p class='lra-lead'>Announcements, rule clarifications, and technical "
        "Q&amp;A happen on our channels — invite links will appear here "
        "shortly.</p>"
        "<div class='lra-cite-actions'>"
        + btn("Discord", DISCORD_URL, "💬")
        + " "
        + btn("Zulip", ZULIP_URL, "🗨️")
        + "</div>"
        "</section>"
    )


# ── Leaderboard rendering ─────────────────────────────────────────────────────
LB_COLUMNS = [
    ("rank", "#", "", False, False),
    ("user", "Submitter", "", False, False),
    ("combined", "Combined %",
     "Mean of length reduction, heartbeat reduction, and zero-shot transfer.",
     True, True),
    ("length", "Length reduction %",
     "Decrease in proof token counts compared against the original proof "
     "before refactoring. Higher is better.",
     True, True),
    ("heartbeat", "Heartbeat reduction %",
     "Change in Lean's <a href='https://lean-lang.org/doc/reference/latest/IO/"
     "Timing/#IO___getNumHeartbeats' target='_blank' rel='noopener noreferrer'>"
     "<code>#count_heartbeats</code></a>, the number of “small” memory "
     "allocations performed on the current execution thread. Positive values "
     "indicate cheaper (typically faster) compilation; negative values "
     "indicate costlier compilation.",
     True, True),
    ("zeroshot", "Zero-shot %",
     "Fraction of each problem's listed Lean toolchains on which the accepted "
     "proof compiles unchanged.",
     True, True),
    ("submitted", "Submitted", "", False, False),
]


def _lb_bar_cell(col: str, sort_val, *, display: str, bar_pct: float, negative: bool = False) -> str:
    w = max(0.0, min(100.0, float(bar_pct)))
    cls = "lra-bar neg" if negative else "lra-bar"
    return (
        f"<td data-col='{col}' data-sort='{sort_val}'>"
        f"<div class='lra-cell-num'>{display}</div>"
        f"<div class='{cls}'><span style='width:{w:.1f}%'></span></div>"
        "</td>"
    )


def _lb_na_cell(col: str) -> str:
    return (
        f"<td data-col='{col}' data-sort=''>"
        "<div class='lra-cell-num lra-na'>—</div></td>"
    )


def _lb_pos_cell(col: str, val) -> str:
    if val is None:
        return _lb_na_cell(col)
    return _lb_bar_cell(col, val, display=f"{val}%", bar_pct=val, negative=val < 0)


def _lb_diverging_cell(col: str, val) -> str:
    if val is None:
        return _lb_na_cell(col)
    w = min(100.0, abs(float(val))) / 2.0          # half-track == 100%
    side = "neg" if val < 0 else "pos"
    return (
        f"<td data-col='{col}' data-sort='{val}'>"
        f"<div class='lra-cell-num'>{val}%</div>"
        "<div class='lra-bar diverging'>"
        f"<span class='lra-bar-fill {side}' style='width:{w:.1f}%'></span></div>"
        "</td>"
    )


def _lb_row_html(r: list) -> str:
    rank, user, len_pct, hb_pct, combined, survival_str, _compiled_str, submitted = r
    user_e = html.escape(str(user))

    # survival_str comes as e.g. "80.0% (8/10)"; show only the percentage.
    m = re.match(r"\s*(-?\d+(?:\.\d+)?)", survival_str or "")
    surv_val = float(m.group(1)) if m else None

    if surv_val is None:
        zeroshot_cell = _lb_na_cell("zeroshot")
    else:
        zeroshot_cell = _lb_bar_cell(
            "zeroshot", surv_val, display=f"{surv_val:.1f}%",
            bar_pct=surv_val)

    cells = [
        f"<td class='rank' data-col='rank' data-sort='{rank}'>{rank}</td>",
        f"<td class='who' data-col='user' data-sort='{user_e.lower()}'>{user_e}</td>",
        _lb_pos_cell("combined", combined),
        _lb_pos_cell("length", len_pct),
        _lb_diverging_cell("heartbeat", hb_pct),
        zeroshot_cell,
        f"<td data-col='submitted' data-sort='{html.escape(str(submitted))}'>"
        f"{html.escape(str(submitted))}</td>",
    ]
    return f"<tr data-rank='{rank}'>" + "".join(cells) + "</tr>"


def _lb_header_html() -> str:
    ths = []
    for key, label, tip, _numeric, higher in LB_COLUMNS:
        better = "<span class='lra-better' title='Higher is better'>(↑)</span>" if higher else ""
        has_tip = " has-tip" if tip else ""
        tip_html = f"<div class='lra-tip'>{tip}</div>" if tip else ""
        ths.append(
            f"<th data-col='{key}' data-sortable='1' class='lra-thcell{has_tip}'>"
            "<span class='lra-th'>"
            f"<span class='lra-th-label'>{label}</span>"
            f"{better}"
            "<span class='lra-sort'></span>"
            "</span>"
            f"{tip_html}"
            "</th>"
        )
    return "<thead><tr>" + "".join(ths) + "</tr></thead>"


# Submitters hidden from every public leaderboard display (internal test
# runs). Their records stay in leaderboard.json; they are filtered at render
# time only.
HIDDEN_SUBMITTERS = {
    "Claude Opus 4.8",
    "Gemini 3 Flash",
    "Deepseek V4 Pro",
    "Claude Code - DeepSeek-V4-Pro (Max)",
}


def _rows_for_display(track: str) -> list:
    rows = [
        r for r in LB.leaderboard_rows(track=track)
        if str(r[1]) not in HIDDEN_SUBMITTERS
    ]
    for i, r in enumerate(rows, start=1):
        r[0] = i
    return rows


def _lb_render(rows: list, *, table_id: str) -> str:
    if not rows:
        return (
            "<div class='lra-empty'>No submissions on this track yet — "
            "the first verified run lands here.</div>"
        )
    body_rows = "".join(_lb_row_html(r) for r in rows)
    return (
        f"<div class='lra-lb' id='{table_id}'>"
        "<div class='lra-table-wrap'><table class='lra-table'>"
        f"{_lb_header_html()}"
        f"<tbody>{body_rows}</tbody></table></div></div>"
    )


def _leaderboard_closed_html() -> str:
    LB.reload()
    return _lb_render(_rows_for_display("closed"), table_id="lra-lb-closed")


def _leaderboard_open_html() -> str:
    LB.reload()
    return _lb_render(_rows_for_display("open"), table_id="lra-lb-open")


def _preview_html(limit: int = 5) -> str:
    closed = _rows_for_display("closed")[:limit]
    open_ = _rows_for_display("open")[:limit]
    return (
        "<section class='lra-card lra-preview'>"
        "<div class='lra-kicker'>Leaderboard</div>"
        "<h2>Current front-runners</h2>"
        "<div class='lra-preview-pick'>"
        "<button type='button' class='lra-pickbtn active' data-track='closed'>"
        "🔒 Closed-source LLM track</button>"
        "<button type='button' class='lra-pickbtn' data-track='open'>"
        "🔓 Open-source LLM track</button>"
        "</div>"
        "<div class='lra-preview-panel' data-track='closed'>"
        + _lb_render(closed, table_id="lra-lb-home-closed")
        + "</div>"
        "<div class='lra-preview-panel' data-track='open' style='display:none'>"
        + _lb_render(open_, table_id="lra-lb-home-open")
        + "</div>"
        "</section>"
    )


# ── Benchmark tab content ─────────────────────────────────────────────────────
def _bench_details_md() -> str:
    if not BENCHMARK:
        return "_No benchmark loaded._"
    parts = ["### Statements to prove\n"]
    for name in benchmark_names():
        info = BENCHMARK[name]
        src_key = info.get("source") or ""
        label = SOURCES.get(src_key, {}).get("label", src_key)
        link = benchmark_file_link(name)
        link_md = f" · [source file]({link})" if link else ""
        header = (info.get("header") or "").rstrip()
        header_block = (
            f"**Header (imports/options supplied automatically):**\n\n"
            f"```\n{header}\n```\n\n" if header else ""
        )
        versions = ", ".join(benchmark_versions(name)) or "—"
        parts.append(
            f"<details><summary><code>{html.escape(name)}</code> — {label}, "
            f"{_fmt_int(info['original_proof_length'])} reference tokens"
            f"</summary>\n\n"
            f"{header_block}"
            f"**Statement your `proof` must reproduce (then add `:= by ...`):**\n\n"
            f"```\n{info['statement']}\n```\n\n"
            f"**Evaluated on:** {versions}{link_md}\n\n"
            f"</details>"
        )
    return "\n".join(parts)


# ── Page assembly ─────────────────────────────────────────────────────────────
def _hero_html() -> str:
    return (
        "<section class='lra-hero'>"
        "<div class='lra-eyebrow'>Competition · two tracks · "
        f"{PRIZE_PER_TRACK} prize per track</div>"
        "<h1>Can your agent make Lean proofs <span class='lra-accent'>better</span>, "
        "not just correct?</h1>"
        "<p class='lra-hero-lead'>Lean Refactor Arena is a competition for "
        "refactoring Lean&nbsp;4 proofs — from <b>Strata, PhysLib, CSLib, "
        "ArkLib, and PutnamBench</b> — to be <b>shorter</b>, <b>cheaper to "
        "compile</b>, and <b>more robust across toolchain versions</b>. "
        "Compete in the <b>closed-source frontier LLM track</b> or the "
        "<b>open-source model track</b>; each track's winner takes "
        f"<b>{PRIZE_PER_TRACK}</b> and a talk at the {WORKSHOP_LINK} workshop "
        f"({WORKSHOP_VENUE}).</p>"
        "</section>"
    )


ARXIV_URL = "https://arxiv.org/abs/2605.20244"
CITATION_BIBTEX = (
    "@article{lu2026lean,\n"
    "  title={Lean Refactor: Multi-Objective Controllable Proof Optimization "
    "via Agentic Strategy Search},\n"
    "  author={Lu, Jialin and Kong, Soonho and Stehling, Rodrigo and Yang, Kaiyu "
    "and Wang, Zhangyang and Sun, Weiran and Chen, Wuyang},\n"
    "  journal={arXiv preprint arXiv:2605.20244},\n"
    "  year={2026}\n"
    "}"
)


def _cite_html() -> str:
    bib = html.escape(CITATION_BIBTEX)
    return (
        "<section class='lra-card lra-cite'>"
        "<div class='lra-kicker'>Citation</div>"
        "<h2>Cite this work</h2>"
        "<p class='lra-lead'>If you use Lean Refactor Arena or the benchmark in "
        "your research, please cite the paper.</p>"
        "<div class='lra-cite-actions'>"
        f"<a class='lra-paper-btn' href='{ARXIV_URL}' target='_blank' "
        "rel='noopener noreferrer'>📄 Paper</a>"
        "</div>"
        f"<pre class='lra-code lra-bib'><code>{bib}</code></pre>"
        "</section>"
    )


def _home_body_html() -> str:
    return (
        "<div class='lra-home'>"
        + _sponsor_strip_html()
        + _stat_band_html()
        + _timeline_html()
        + _tracks_html()
        + _sources_html()
        + _claims_html()
        + _metric_cards_html()
        + _preview_html()
        + _community_html()
        + _cite_html()
        + "</div>"
    )


def refresh_home():
    LB.reload()
    return _home_body_html()


def _select_tab(tab_id: str):
    return gr.Tabs(selected=tab_id)


APP_CSS = """
:root {
  --bg: #f6f7f2;
  --paper: #ffffff;
  --ink: #14201a;
  --muted: #5c6b62;
  --line: rgba(20, 32, 26, 0.10);
  --green: #0f6b50;
  --green-deep: #0a3f30;
  --gold: #b9842b;
  --accent: #d84a3a;
  --shadow: 0 18px 50px rgba(15, 40, 30, 0.10);
}
.gradio-container {
  background:
    radial-gradient(900px 460px at 14% -8%, rgba(15, 107, 80, 0.10), transparent 70%),
    radial-gradient(720px 380px at 96% 0%, rgba(185, 132, 43, 0.08), transparent 70%),
    linear-gradient(180deg, #fbfcf8 0%, var(--bg) 46%, #ffffff 100%);
  color: var(--ink);
  font-family: Inter, ui-sans-serif, system-ui, -apple-system, "Segoe UI", sans-serif;
}
/* Center the content column. Gradio's own `.contain` rule sets margin-right:0,
   which beat a non-!important `margin: 0 auto` and shoved the page right. */
.gradio-container .contain {
  max-width: 1180px !important;
  margin-left: auto !important;
  margin-right: auto !important;
}
footer { display: none !important; }

/* Tab nav: pin readable colours regardless of the viewer's dark mode. */
.tab-container button[role="tab"]:hover:not(.selected),
.tab-nav button:hover:not(.selected) {
  background-color: rgba(15, 107, 80, 0.10) !important;
  color: var(--green) !important;
}
.tab-container button[role="tab"]:not(.selected),
.tab-nav button:not(.selected) { color: var(--ink) !important; }
.tab-container button[role="tab"].selected,
.tab-nav button.selected { color: var(--green) !important; }

/* top bar */
.lra-topbar {
  display: flex; align-items: center; justify-content: space-between;
  gap: 12px; padding: 6px 2px 2px;
}
.lra-brand { display: flex; align-items: center; gap: 14px; font-weight: 800; font-size: 1.6rem; letter-spacing: -0.01em; }
.lra-brand .dot {
  width: 22px; height: 22px; border-radius: 7px;
  background: linear-gradient(135deg, var(--green), var(--green-deep));
  box-shadow: inset 0 1px 0 rgba(255,255,255,0.25);
}
.lra-brand .lra-logo {
  width: 60px; height: 60px; border-radius: 15px; object-fit: cover;
  box-shadow: inset 0 1px 0 rgba(255,255,255,0.25);
}
.lra-pill {
  font-size: 0.72rem; font-weight: 800; text-transform: uppercase; letter-spacing: 0.10em;
  color: var(--gold); background: rgba(185,132,43,0.12);
  border: 1px solid rgba(185,132,43,0.30); border-radius: 999px; padding: 3px 10px;
}
.lra-statusbar:empty { display: none; }
.lra-statusbar > div, .lra-statusbar { margin: 8px 0 2px; }

/* shared */
.lra-kicker {
  color: var(--green); font-size: 0.74rem; font-weight: 800;
  letter-spacing: 0.14em; text-transform: uppercase;
}
.lra-accent { color: var(--accent); }
.lra-home { display: flex; flex-direction: column; gap: 20px; padding-bottom: 8px; }
.lra-card {
  background: var(--paper); border: 1px solid var(--line);
  border-radius: 16px; padding: 30px; box-shadow: var(--shadow);
}
.lra-card h2, .lra-claim-copy h2 {
  margin: 8px 0 12px; font-size: clamp(1.5rem, 2.6vw, 2.1rem);
  line-height: 1.1; letter-spacing: -0.015em;
}
.lra-lead { color: var(--muted); max-width: 760px; line-height: 1.65; }
code {
  background: rgba(15,107,80,0.08); color: #0c5a44;
  padding: 1px 6px; border-radius: 6px; font-size: 0.86em;
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
}

/* hero */
.lra-hero { padding: 40px 4px 6px; }
.lra-eyebrow {
  color: var(--green); font-size: 0.8rem; font-weight: 800;
  letter-spacing: 0.16em; text-transform: uppercase;
}
.lra-hero h1 {
  margin: 14px 0 18px; max-width: 940px;
  font-size: clamp(2.4rem, 5.2vw, 4rem); line-height: 1.04;
  letter-spacing: -0.025em; font-weight: 800;
}
.lra-hero-lead {
  max-width: 800px; color: var(--muted);
  font-size: clamp(1.02rem, 1.6vw, 1.18rem); line-height: 1.7;
}
.lra-hero-lead b { color: var(--ink); }

/* CTA row (real gradio buttons) — compact + left-aligned */
.lra-cta-row {
  gap: 12px !important; margin: 4px 0 10px !important;
  flex-wrap: wrap; justify-content: flex-start !important;
}
.lra-cta-row > * { flex: 0 0 auto !important; min-width: 0 !important; }
.lra-cta-row button {
  width: auto !important; white-space: nowrap;
  border-radius: 10px !important; font-weight: 700 !important;
  padding: 12px 24px !important; font-size: 0.98rem !important;
  box-shadow: none !important;
}

/* stat band */
.lra-stat-band {
  display: grid; grid-template-columns: repeat(4, 1fr); gap: 4px;
  background: linear-gradient(135deg, var(--green-deep), #0c5340 70%, #0e6149);
  border-radius: 16px; padding: 30px 20px; box-shadow: var(--shadow);
  border: 1px solid rgba(255,255,255,0.08);
}
.lra-stat { text-align: center; padding: 6px 14px; position: relative; }
.lra-stat + .lra-stat::before {
  content: ""; position: absolute; left: 0; top: 14%; height: 72%;
  width: 1px; background: rgba(255,255,255,0.14);
}
.lra-stat-num {
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
  font-size: clamp(1.8rem, 4vw, 2.8rem); font-weight: 600; line-height: 1;
  color: #f4efe6; letter-spacing: -0.02em;
}
.lra-stat-label {
  margin-top: 12px; color: #e8f3ee; font-size: 0.8rem;
  font-weight: 800; letter-spacing: 0.06em; text-transform: uppercase;
}
.lra-stat-note { margin-top: 4px; color: rgba(225,240,233,0.62); font-size: 0.78rem; }

/* timeline */
.lra-tl-grid { display: grid; grid-template-columns: repeat(3, 1fr); gap: 16px; margin-top: 18px; }
.lra-tl-step {
  background: #fbfdfb; border: 1px solid var(--line); border-radius: 13px;
  padding: 20px; position: relative;
}
.lra-tl-when {
  display: inline-block; font-family: ui-monospace, Menlo, monospace;
  font-size: 0.8rem; font-weight: 700; color: var(--gold);
  background: rgba(185,132,43,0.10); border-radius: 7px; padding: 3px 9px;
}
.lra-tl-name { margin: 12px 0 6px; font-weight: 800; font-size: 1.05rem; }
.lra-tl-step p { color: var(--muted); font-size: 0.92rem; line-height: 1.55; margin: 0; }

/* tracks */
.lra-track-grid { display: grid; grid-template-columns: 1fr 1fr; gap: 16px; margin-top: 18px; }
.lra-track {
  background: #fbfdfb; border: 1px solid var(--line); border-radius: 13px;
  padding: 22px; display: flex; flex-direction: column;
}
.lra-track-name { margin: 12px 0 8px; font-weight: 800; font-size: 1.25rem; }
.lra-track ul { margin: 0 0 14px 18px; padding: 0; color: var(--muted); line-height: 1.6; }
.lra-track li { margin-bottom: 8px; font-size: 0.95rem; }
.lra-track li b { color: var(--ink); }
.lra-track-prize {
  margin-top: auto; padding: 10px 14px; border-radius: 9px;
  background: rgba(185,132,43,0.10); border: 1px solid rgba(185,132,43,0.25);
  color: #7a5211; font-size: 0.92rem;
}

/* benchmark sources */
.lra-src-grid { display: grid; grid-template-columns: 1fr 1fr; gap: 14px; margin-top: 18px; }
.lra-src {
  display: flex; gap: 14px; align-items: flex-start;
  background: #fbfdfb; border: 1px solid var(--line); border-radius: 13px; padding: 18px;
}
.lra-src-logo {
  width: 52px; height: 52px; border-radius: 11px; object-fit: contain;
  background: #ffffff; border: 1px solid var(--line); flex: 0 0 auto; padding: 4px;
}
.lra-src-name { font-weight: 800; font-size: 1.02rem; display: flex; align-items: baseline; gap: 10px; flex-wrap: wrap; }
.lra-src-name a { color: var(--ink); text-decoration: none; border-bottom: 1px dotted var(--muted); }
.lra-src-name a:hover { color: var(--green); border-color: var(--green); }
.lra-src-body p { color: var(--muted); font-size: 0.9rem; line-height: 1.55; margin: 6px 0 0; }

/* claims */
.lra-claims { display: flex; flex-direction: column; gap: 20px; }
.lra-claim {
  display: grid; grid-template-columns: 0.82fr 1fr; gap: 26px;
  align-items: center; background: var(--paper); border: 1px solid var(--line);
  border-radius: 16px; padding: 28px 30px; box-shadow: var(--shadow);
}
.lra-claim-copy h2 { font-size: clamp(1.45rem, 2.6vw, 2rem); }
.lra-claim-copy p { color: var(--muted); line-height: 1.65; margin-top: 2px; }
.lra-code-pair { display: grid; gap: 12px; }
.lra-code {
  margin: 0; background: #0e1512; color: #d8e6df;
  border: 1px solid rgba(120,180,150,0.16); border-radius: 12px;
  padding: 16px 18px; overflow-x: auto;
  font-size: 0.82rem; line-height: 1.6;
  font-family: ui-monospace, SFMono-Regular, Menlo, monospace;
  box-shadow: inset 0 1px 0 rgba(255,255,255,0.04);
}
.lra-code code { background: none; color: inherit; padding: 0; font-size: inherit; }
.lra-code .k { color: #ff8fb3; }
.lra-code .n { color: #e9c07b; }
.lra-code .c { color: #6f8a7e; font-style: italic; }

/* scoring metrics */
.lra-metric-grid {
  display: grid; grid-template-columns: repeat(3, 1fr); gap: 16px; margin-top: 18px;
}
.lra-metric {
  background: #fbfdfb; border: 1px solid var(--line); border-radius: 13px; padding: 20px;
}
.lra-metric-tag {
  display: inline-block; font-family: ui-monospace, Menlo, monospace;
  font-size: 0.82rem; font-weight: 700; color: var(--green);
  background: rgba(15,107,80,0.10); border-radius: 7px; padding: 3px 9px;
}
.lra-metric-name { margin: 12px 0 6px; font-weight: 800; font-size: 1.05rem; }
.lra-metric p { color: var(--muted); font-size: 0.92rem; line-height: 1.55; margin: 0; }

/* citation + link-buttons */
.lra-cite-actions { margin: 16px 0; }
.lra-paper-btn {
  display: inline-flex; align-items: center; gap: 8px;
  padding: 10px 18px; border-radius: 10px; font-weight: 800; font-size: 0.95rem;
  color: #ffffff !important; text-decoration: none !important;
  background: linear-gradient(135deg, var(--green), var(--green-deep));
  box-shadow: 0 6px 18px rgba(15,107,80,0.22);
  transition: transform .12s ease, box-shadow .12s ease;
}
.lra-paper-btn:hover { transform: translateY(-1px); box-shadow: 0 10px 24px rgba(15,107,80,0.30); }
.lra-btn-soon {
  background: linear-gradient(135deg, #8aa198, #6d827a); cursor: default;
  box-shadow: none; opacity: 0.85;
}
.lra-btn-soon:hover { transform: none; box-shadow: none; }
.lra-bib {
  white-space: pre-wrap; word-break: break-word; overflow-x: auto;
  font-size: 0.82rem; margin: 0;
}

/* leaderboard table */
.lra-lb { margin-top: 16px; }

/* home leaderboard-preview track picker */
.lra-preview-pick { display: flex; gap: 10px; margin: 14px 0 4px; flex-wrap: wrap; }
.lra-pickbtn {
  padding: 12px 22px; font-size: 1rem; font-weight: 800; cursor: pointer;
  border: 1px solid var(--line); border-radius: 999px;
  background: var(--paper); color: var(--ink);
  transition: border-color .15s ease, color .15s ease, box-shadow .15s ease;
}
.lra-pickbtn:hover { border-color: var(--green); color: var(--green); }
.lra-pickbtn.active {
  background: linear-gradient(135deg, var(--green), var(--green-deep));
  color: #ffffff; border-color: transparent;
  box-shadow: 0 6px 18px rgba(15,107,80,0.22);
}
.lra-pickbtn.active:hover { color: #ffffff; }
.lra-table-wrap {
  overflow: visible; border: 1px solid var(--line);
  border-radius: 14px; background: var(--paper);
}
.lra-table { width: 100%; table-layout: fixed; border-collapse: separate; border-spacing: 0; font-size: 0.9rem; }
.lra-table th, .lra-table td {
  padding: 10px 12px; border-bottom: 1px solid var(--line); text-align: left; vertical-align: middle;
  overflow-wrap: anywhere; word-break: break-word;
}
.lra-table th[data-col='rank'] { width: 44px; }
.lra-table th[data-col='user'] { width: 14%; }
.lra-table th[data-col='submitted'] { width: 92px; }
.lra-table thead th {
  position: sticky; top: 0; z-index: 5; background: var(--paper);
  color: var(--muted); font-size: 0.76rem; font-weight: 800;
  cursor: pointer; user-select: none; white-space: normal;
  box-shadow: inset 0 -1px 0 var(--line);
}
.lra-table thead th:hover { color: var(--ink); }
.lra-th { display: inline-flex; align-items: baseline; gap: 4px; flex-wrap: wrap; }
.lra-better { color: var(--green); font-weight: 800; font-size: 0.95rem; }
.lra-sort { font-size: 1.05em; color: #2f6fb0; }
.lra-sort::after { content: '▾'; opacity: 0.5; }
.lra-table thead th[data-dir='asc'] .lra-sort::after { content: '▲'; opacity: 1; }
.lra-table thead th[data-dir='desc'] .lra-sort::after { content: '▼'; opacity: 1; }
.lra-table thead th[data-dir] { color: var(--ink); }
.lra-thcell.has-tip .lra-th-label { border-bottom: 1px dotted var(--muted); }
.lra-tip { display: none; }
.lra-tip-float {
  display: none; position: fixed; z-index: 9999; width: 280px; max-width: 76vw;
  background: var(--ink); color: #f2f5f2; text-align: left; font-weight: 500;
  letter-spacing: 0; font-size: 0.8rem; line-height: 1.5;
  padding: 10px 12px; border-radius: 10px; box-shadow: var(--shadow); white-space: normal;
}
.lra-tip-float a { color: #bfe9d3; text-decoration: underline; text-underline-offset: 2px; }
.lra-tip-float code { background: rgba(255,255,255,0.22); color: #ffffff; padding: 1px 5px; border-radius: 4px; font-size: 0.92em; }
.lra-table tbody tr:nth-child(even) { background: rgba(20,32,26,0.025); }
.lra-table tbody tr:hover { background: rgba(15,107,80,0.06); }
.lra-table td.rank { font-family: ui-monospace, Menlo, monospace; color: var(--green); font-weight: 700; white-space: nowrap; }
.lra-table td.who { font-weight: 700; }
.lra-table td.who a { color: var(--ink); text-decoration: none; border-bottom: 1px dotted var(--muted); }
.lra-table td.who a:hover { color: var(--green); border-color: var(--green); }
.lra-cell-num { font-variant-numeric: tabular-nums; }
.lra-cell-num.lra-na { color: var(--muted); opacity: 0.7; }
.lra-bar { margin-top: 5px; height: 5px; border-radius: 3px; background: rgba(20,32,26,0.08); overflow: hidden; }
.lra-bar > span { display: block; height: 100%; border-radius: 3px; background: linear-gradient(90deg, var(--green), var(--green-deep)); }
.lra-bar.neg > span { background: var(--accent); }
.lra-bar.diverging { position: relative; overflow: visible; }
.lra-bar.diverging::before { content: ''; position: absolute; left: 50%; top: -2px; bottom: -2px; width: 1px; background: rgba(20,32,26,0.32); }
.lra-bar.diverging .lra-bar-fill { position: absolute; top: 0; bottom: 0; border-radius: 2px; }
.lra-bar.diverging .lra-bar-fill.pos { left: 50%; background: linear-gradient(90deg, var(--green), var(--green-deep)); }
.lra-bar.diverging .lra-bar-fill.neg { right: 50%; background: var(--accent); }
.lra-table td[data-col='combined'] .lra-cell-num,
.lra-table td[data-col='length'] .lra-cell-num,
.lra-table td[data-col='heartbeat'] .lra-cell-num { font-weight: 600; }
.lra-df table { table-layout: auto !important; }
.lra-df th, .lra-df td { white-space: normal !important; overflow-wrap: anywhere; word-break: break-word; vertical-align: top; }
.lra-df th .header-content, .lra-df th span { white-space: normal !important; }
.lra-empty {
  margin-top: 16px; padding: 26px; text-align: center; color: var(--muted);
  border: 1px dashed var(--line); border-radius: 12px; background: #fbfdfb;
}

/* sponsors */
.lra-sponsors { text-align: center; padding: 14px 0 6px; }
.lra-sponsors .lra-kicker { color: var(--muted); font-size: 1.15rem; margin-bottom: 6px; }
.lra-logo-row {
  display: flex; flex-wrap: wrap; align-items: center; justify-content: center;
  gap: 40px; margin-top: 16px;
}
.lra-logo { display: flex; align-items: center; justify-content: center; }
.lra-logo img {
  height: 62px; max-width: 260px; object-fit: contain;
  filter: grayscale(0.35); opacity: 0.88; transition: filter .2s, opacity .2s;
}
.lra-logo:hover img { filter: grayscale(0); opacity: 1; }

/* leaderboard track selector: large, unmissable pills */
.lra-track-tabs .tab-nav button, .lra-track-tabs button[role="tab"] {
  font-size: 1.12rem !important; font-weight: 800 !important;
  padding: 16px 30px !important;
  border-radius: 12px 12px 0 0 !important;
}
.lra-track-tabs .tab-nav button.selected,
.lra-track-tabs button[role="tab"].selected {
  background: rgba(15,107,80,0.10) !important;
  box-shadow: inset 0 -3px 0 var(--green) !important;
}

/* big benchmark download button */
.lra-download-btn {
  max-width: 420px !important;
  font-size: 1.08rem !important; font-weight: 800 !important;
  padding: 16px 30px !important; border-radius: 12px !important;
  margin: 10px 0 18px !important;
}

/* page intros for inner tabs */
.lra-intro {
  background: var(--paper); border: 1px solid var(--line); border-radius: 14px;
  padding: 22px 26px; margin-bottom: 16px; box-shadow: var(--shadow);
}
.lra-intro h2 { margin: 6px 0 8px; font-size: 1.5rem; letter-spacing: -0.015em; }
.lra-intro p { color: var(--muted); line-height: 1.6; margin: 0; max-width: 860px; }
.lra-intro p b { color: var(--ink); }

/* Keep native Gradio text readable regardless of the viewer's light/dark theme. */
.dark {
  --body-text-color: #14201a;
  --body-text-color-subdued: #5c6b62;
  --block-background-fill: #ffffff;
  --block-title-text-color: #14201a;
  --block-label-text-color: #5c6b62;
  --block-info-text-color: #5c6b62;
  --input-background-fill: #ffffff;
  --input-text-color: #14201a;
  --input-placeholder-color: #8a978f;
  --border-color-primary: rgba(20, 32, 26, 0.14);
  --table-even-background-fill: #ffffff;
  --table-odd-background-fill: #fbfdfb;
  --table-text-color: #14201a;
  color-scheme: light;
}

div[data-testid="dataframe"] { border-radius: 12px !important; overflow: hidden; }

@media (max-width: 900px) {
  .lra-claim { grid-template-columns: 1fr; }
  .lra-stat-band { grid-template-columns: repeat(2, 1fr); row-gap: 22px; }
  .lra-stat:nth-child(3)::before { display: none; }
  .lra-metric-grid, .lra-tl-grid, .lra-track-grid, .lra-src-grid { grid-template-columns: 1fr; }
}
@media (max-width: 560px) {
  .lra-stat-band { grid-template-columns: 1fr; }
  .lra-stat::before { display: none !important; }
  .lra-card, .lra-claim { padding: 20px; }
}
"""


# Client-side interactivity for the custom tables (sort/search/columns +
# header tooltips). Attached at the document level so it survives Gradio's
# periodic gr.HTML re-renders.
LB_JS = """
<script>
(function () {
  function num(v) { var n = parseFloat(v); return isNaN(n) ? null : n; }
  // ---- header hover tooltips (fixed-positioned, clip-proof) ----
  var tf = null, hideTimer = null;
  function ensureFloat() {
    if (tf) return tf;
    tf = document.createElement('div');
    tf.className = 'lra-tip-float';
    document.body.appendChild(tf);
    tf.addEventListener('mouseenter', function () { clearTimeout(hideTimer); });
    tf.addEventListener('mouseleave', hideTip);
    return tf;
  }
  function hideTip() { clearTimeout(hideTimer); hideTimer = setTimeout(function () { if (tf) tf.style.display = 'none'; }, 150); }
  document.addEventListener('mouseover', function (e) {
    var th = e.target.closest && e.target.closest('.lra-thcell.has-tip');
    if (!th) return;
    var src = th.querySelector('.lra-tip'); if (!src) return;
    var f = ensureFloat();
    clearTimeout(hideTimer);
    f.innerHTML = src.innerHTML;
    f.style.display = 'block';
    var r = th.getBoundingClientRect();
    var fw = f.offsetWidth, fh = f.offsetHeight;
    var left = Math.max(8, Math.min(r.left + r.width / 2 - fw / 2, window.innerWidth - fw - 8));
    var top = r.bottom + 6;
    if (top + fh > window.innerHeight - 8) top = r.top - fh - 6;   // open upward if no room below
    f.style.left = left + 'px';
    f.style.top = Math.max(8, top) + 'px';
  });
  document.addEventListener('mouseout', function (e) {
    var th = e.target.closest && e.target.closest('.lra-thcell.has-tip');
    if (!th) return;
    var to = e.relatedTarget;
    if (to && to.closest && (to.closest('.lra-thcell.has-tip') === th || to.closest('.lra-tip-float'))) return;
    hideTip();
  });

  document.addEventListener('click', function (e) {
    if (!e.target.closest) return;
    if (e.target.closest('.lra-tip-float')) return;   // let tooltip links work, don't sort
    if (e.target.closest('a')) return;                // let links in cells work, don't sort
    // home leaderboard-preview track picker
    var pk = e.target.closest('.lra-pickbtn');
    if (pk) {
      var sec = pk.closest('.lra-preview');
      var tr = pk.getAttribute('data-track');
      Array.prototype.forEach.call(sec.querySelectorAll('.lra-pickbtn'), function (b) {
        b.classList.toggle('active', b === pk);
      });
      Array.prototype.forEach.call(sec.querySelectorAll('.lra-preview-panel'), function (pl) {
        pl.style.display = pl.getAttribute('data-track') === tr ? '' : 'none';
      });
      return;
    }
    var th = e.target.closest('.lra-table th[data-sortable]');
    if (th) {
      var table = th.closest('table');
      var ths = Array.prototype.slice.call(table.querySelectorAll('th[data-sortable]'));
      var idx = Array.prototype.indexOf.call(th.parentNode.children, th);
      var cur = th.getAttribute('data-dir') || 'none';
      var next = cur === 'desc' ? 'asc' : (cur === 'asc' ? 'none' : 'desc');
      ths.forEach(function (h) { if (h !== th) h.removeAttribute('data-dir'); });
      if (next === 'none') th.removeAttribute('data-dir');
      else th.setAttribute('data-dir', next);
      var tbody = table.querySelector('tbody');
      var rows = Array.prototype.slice.call(tbody.querySelectorAll('tr'));
      rows.sort(function (a, b) {
        if (next === 'none') return (num(a.dataset.rank) || 0) - (num(b.dataset.rank) || 0);
        var av = a.children[idx].dataset.sort, bv = b.children[idx].dataset.sort;
        var an = num(av), bn = num(bv), c;
        if (an !== null && bn !== null) c = an - bn;
        else c = String(av || '').localeCompare(String(bv || ''));
        return next === 'asc' ? c : -c;
      });
      rows.forEach(function (r) { tbody.appendChild(r); });
      return;
    }
  });
})();
</script>
"""

with gr.Blocks(
    title="Lean Refactor Arena",
    theme=gr.themes.Soft(primary_hue="green", neutral_hue="stone"),
    css=APP_CSS,
    head=LB_JS,
) as demo:
    gr.HTML(
        "<div class='lra-topbar'>"
        "<div class='lra-brand'>"
        + (
            f"<img class='lra-logo' src='{APP_ICON_DATA_URI}' alt='Lean Refactor Arena logo'/>"
            if APP_ICON_DATA_URI
            else "<span class='dot'></span>"
        )
        + "Lean Refactor Arena</div>"
        "<span class='lra-pill'>Warm-up phase · full benchmark drops Oct 1</span>"
        "</div>"
    )

    with gr.Tabs() as app_tabs:
        # ── Home ──────────────────────────────────────────────────────────────
        with gr.Tab("Home", id="home"):
            gr.HTML(value=_hero_html())
            with gr.Row(elem_classes=["lra-cta-row"]):
                home_submit_btn = gr.Button("Submit your proofs", variant="primary")
                home_lb_btn = gr.Button("View the leaderboard", variant="secondary")
                home_rules_btn = gr.Button("Tracks & rules", variant="secondary")
            home_body = gr.HTML(value=_home_body_html())
            gr.Timer(value=60).tick(refresh_home, outputs=home_body)

        # ── Tracks & Rules ────────────────────────────────────────────────────
        with gr.Tab("Tracks & Rules", id="rules"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>Competition rules</div>"
                "<h2>Tracks, budgets, and what you must submit</h2>"
                "<p>The arena runs one benchmark under two resource regimes, "
                "ranked separately. Enter either track — or both, with "
                "separate submissions. This competition is part of the "
                f"{WORKSHOP_LINK} workshop at {WORKSHOP_VENUE}.</p>"
                "</div>"
            )
            gr.HTML(value=_tracks_html(compact=False))
            gr.Markdown(
                "### Closed-source LLM track\n\n"
                "- **Models.** Any closed-source frontier LLM accessed through "
                "its API (e.g. GPT, Claude, Gemini). You may build arbitrary "
                "harnesses around the model.\n"
                f"- **Budget.** API spend is capped at **US$3 per problem**, "
                "measured at the provider's list prices. Your tech report "
                "must state the models used and the per-problem spend.\n"
                "- **Deliverables.** The refactored proofs (JSONL), the "
                "complete harness code, and a short tech report — enough for "
                "the organizers to reproduce your results.\n\n"
                "### Open-source LLM track\n\n"
                "- **Models.** Open-source models only — weights must be "
                "publicly available. You may post-train them, build a harness "
                "around them, or both.\n"
                "- **Budget.** Inference must be deployable on at most "
                "**4× 80 GB A100 GPUs**, and the full benchmark run must "
                "complete within **48 hours** on that hardware.\n"
                "- **Deliverables.** The refactored proofs (JSONL), all code "
                "(post-training and inference/harness), and a short tech "
                "report — enough for the organizers to reproduce your "
                "results.\n\n"
                "### Scoring (both tracks)\n\n"
                "Each submitted proof is checked against the original "
                "statement (changing the statement voids the row), compiled, "
                "and scored on:\n\n"
                "1. **Length reduction %** — token count of the proof body vs "
                "the reference proof.\n"
                "2. **Heartbeat reduction %** — Lean elaboration cost via "
                "[`#count_heartbeats`](https://lean-lang.org/doc/reference/latest/IO/Timing/#IO___getNumHeartbeats) "
                "vs the reference proof.\n"
                "3. **Zero-shot transfer %** — the fraction of the problem's "
                "listed Lean toolchains (its `version_info`) on which the "
                "proof compiles unchanged.\n\n"
                "The leaderboard ranks by **combined %** — the mean of the "
                "three. Proofs that fail to compile, use `sorry`, or trip the "
                "forbidden-pattern filter (`#eval`, `IO.*`, `unsafe`, "
                "`extern`, …) score zero.\n\n"
                "### Prizes\n\n"
                f"- **{PRIZE_PER_TRACK}** for the winner of each track.\n"
                "- A **dedicated presentation slot** at the "
                f"[{WORKSHOP_NAME}]({WORKSHOP_URL}) workshop "
                f"({WORKSHOP_VENUE}) for each track winner.\n\n"
                f"_{DISCLAIMER}_\n\n"
                "### Tech report\n\n"
                "Every submission must be accompanied by a **short technical "
                "report** describing the approach, models, and budget "
                "accounting. Detailed formatting instructions will be "
                "released later.\n\n"
                "### Timeline\n\n"
                "| Phase | Dates | What happens |\n"
                "|---|---|---|\n"
                "| Warm-up — submissions open | now – Sep 30, 2026 | Public "
                "development subset live; submissions accepted on the "
                "practice benchmark |\n"
                f"| Full benchmark | {FULL_BENCH_RELEASE} | Full "
                f"{FULL_BENCH_SIZE}-problem benchmark released; leaderboard "
                "refreshed — entries are evaluated on the full benchmark "
                "(proofs + code + tech report) from here on |\n"
                f"| Deadline | {DEADLINE} | Submissions close |\n"
                "| Review & awards | after Nov 25, 2026 | Organizers reproduce "
                "top entries; winners announced and presented at the "
                "workshop |\n\n"
                "### Additional rules\n\n"
                "- Results must be **reproducible** from the submitted code "
                "within the stated budget; organizers will re-run top "
                "entries.\n"
                "- One team may enter **both tracks** with separate "
                "submissions.\n"
                "- Rule clarifications will be posted on the community "
                "channels (Discord / Zulip — links coming soon) and this "
                "page.\n"
            )

        # ── Leaderboard ───────────────────────────────────────────────────────
        with gr.Tab("Leaderboard", id="leaderboard"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>Development subset</div>"
                "<h2>Leaderboard</h2>"
                "<p>Each track is ranked separately — pick a track below. "
                "Every <b>reduction %</b> compares a submission to the "
                "reference proof — higher is better, negative means the proof "
                "got bigger or slower. Rows rank by <b>combined %</b>, the "
                "mean of length reduction, heartbeat reduction, and zero-shot "
                "transfer. <b>Zero-shot %</b> is the fraction of each "
                "problem's listed toolchains the same proof compiles on, "
                "unchanged. Click a column header to re-sort. This board runs "
                "on the development subset; it will be <b>refreshed on "
                "Oct 1</b> when the full benchmark is released.</p>"
                "</div>"
            )
            refresh_btn = gr.Button("↻ Refresh", size="sm")
            with gr.Tabs(elem_classes=["lra-track-tabs"]):
                with gr.Tab("🔒 Closed-source LLM track"):
                    lb_closed = gr.HTML(value=_leaderboard_closed_html())
                with gr.Tab("🔓 Open-source LLM track"):
                    lb_open = gr.HTML(value=_leaderboard_open_html())

        # ── Benchmark ─────────────────────────────────────────────────────────
        with gr.Tab("Benchmark", id="benchmark"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>The corpus</div>"
                "<h2>What you are refactoring</h2>"
                "<p>Every problem is a <b>long reference proof</b> lifted "
                "verbatim from an active open-source Lean development, plus a "
                "slice of competition mathematics — selected in consultation "
                "with the repository maintainers. Project problems are "
                "compiled <b>in place inside their repository</b> — the "
                "surrounding imports, notation, and sibling declarations are "
                "all live. PutnamBench problems are self-contained against "
                f"Mathlib. <b>The current {len(benchmark_names())} problems "
                "are a development subset</b>: build your pipeline against "
                f"them now; the <b>full {FULL_BENCH_SIZE}-problem benchmark</b> "
                f"is released on <b>{FULL_BENCH_RELEASE}</b>. "
                f"<i>{DISCLAIMER}</i></p>"
                "</div>"
            )
            gr.HTML(value=_sources_html(heading=False))
            gr.DownloadButton(
                "📥  Download Benchmark Data",
                value=BENCHMARK_JSONL_PATH,
                variant="primary",
                size="lg",
                elem_classes=["lra-download-btn"],
            )
            gr.Markdown(
                "### Data format\n\n"
                "Each line of the JSONL is one problem with these fields:\n\n"
                "| Field | Meaning |\n"
                "|---|---|\n"
                "| `name` | Unique theorem id — the `name` in your submission "
                "must match it exactly. |\n"
                "| `source` | Which corpus the problem comes from: `strata`, "
                "`physlib`, `cslib`, `arklib`, or `putnambench`. |\n"
                "| `statement` | The theorem statement without the proof. "
                "Your refactored proof must keep it unchanged. |\n"
                "| `src` | The original declaration — statement plus the "
                "reference proof you are trying to beat. |\n"
                "| `proof_length` | Token count of the reference proof; the "
                "denominator for length reduction %. |\n"
                "| `num_lines` | Line count of the reference proof. |\n"
                "| `header` | Imports and options for self-contained "
                "PutnamBench problems. Empty for project problems, which are "
                "compiled inside their repository where the imports already "
                "exist. |\n"
                "| `file_path`, `url`, `start_line`, `end_line` | Where the "
                "declaration lives in its source repository. Empty for "
                "PutnamBench problems, which don't belong to a repository. |\n"
                "| `version_info` | The list of `{version: commit}` pairs the "
                "proof is compiled against for the zero-shot transfer score. "
                "|\n\n"
                "**About `version_info`.** For **project problems** (Strata, "
                "PhysLib, CSLib, ArkLib), each entry pins a commit of the "
                "*source repository* corresponding to that Lean toolchain "
                "version. For **PutnamBench problems**, the versions are "
                "**Mathlib release tags** (`v4.25.0`, `v4.26.0`, `v4.27.0`) "
                "and the commit hashes are the corresponding "
                "[mathlib4](https://github.com/leanprover-community/mathlib4) "
                "commits — the proof is compiled against each of those "
                "Mathlib versions.\n"
            )
            gr.Markdown(_bench_details_md())

        # ── Submit ────────────────────────────────────────────────────────────
        with gr.Tab("Submit", id="submit"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>Submission</div>"
                "<h2>Upload a JSONL of refactored proofs</h2>"
                "<p>Each row names a benchmark theorem and carries a full Lean "
                "declaration in <code>proof</code>. Your file is checked here, "
                "then compiled and scored on our <b>dedicated evaluation "
                "worker</b> — results appear on the leaderboard when the run "
                "finishes. During the warm-up phase you only need the proofs; "
                "entries on the full benchmark (from Oct 1) also require code "
                "and a short tech report.</p>"
                "</div>"
            )
            gr.Markdown(
                "### Steps\n\n"
                "1. **Download** the benchmark from the **Benchmark** tab. "
                "See that tab for the problem list and what each field "
                "means.\n"
                "2. **Write a shorter / cheaper `proof`** for the theorems you "
                "want to improve. Keep the statement identical; only the "
                "proof after `:=` is yours.\n"
                "3. **Pick your track and a stable username, then upload.** "
                "You can close the tab and re-enter the same username to "
                "watch progress.\n\n"
                "### JSONL schema\n\n"
                "```json\n"
                '{"name": "theorem_id", "proof": "theorem theorem_id ... := by tactic"}\n'
                "```\n\n"
                "- `name` must match a benchmark id for the row to be scored.\n"
                "- `proof` is the full declaration; the body after `:=` is "
                "tokenized for the length metric.\n"
                "- Compile failure, a changed statement, or `sorry` ⇒ 0% on "
                "all axes.\n"
            )
            track_in = gr.Radio(
                choices=list(TRACK_LABELS.keys()),
                label="Track",
                value=None,
            )
            with gr.Row():
                user_in = gr.Textbox(label="Username", placeholder="your-handle")
                file_in = gr.File(
                    label="Your JSONL",
                    file_types=[".jsonl", ".json", ".txt"],
                    type="filepath",
                )
            submit_btn = gr.Button("Verify & Submit", variant="primary")
            submit_status = gr.Markdown("")
            progress_df = gr.Dataframe(
                headers=["theorem", "scored", "status", "length",
                         "length reduction %", "heartbeats",
                         "heartbeat reduction %", "notes"],
                datatype=["str", "str", "str", "number", "number",
                          "number", "number", "str"],
                row_count=(0, "dynamic"),
                wrap=True,
                elem_classes=["lra-df"],
                interactive=False,
            )

        # ── Community ─────────────────────────────────────────────────────────
        with gr.Tab("Community", id="community"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>Group chat</div>"
                "<h2>Talk to the organizers and other teams</h2>"
                "<p>We run a <b>Discord</b> server and a <b>Zulip</b> "
                "channel. Invite links will be posted here shortly.</p>"
                "</div>"
            )
            gr.HTML(value=_community_html())

        # ── About ─────────────────────────────────────────────────────────────
        with gr.Tab("About", id="about"):
            gr.Markdown(
                "### What this is\n\n"
                "Lean Refactor Arena asks whether AI systems can make existing "
                "Lean developments **better**, not merely **correct**. Formal "
                "libraries accumulate long, slow, brittle proofs; the arena "
                "measures whether your system can rewrite them — same "
                "statement, better proof — across three axes at once.\n\n"
                "The benchmark draws long reference proofs from four active "
                "formalization projects — "
                "[Strata](https://github.com/strata-org/Strata) (program "
                "verification, AWS), "
                "[PhysLib](https://github.com/leanprover-community/physlib) "
                "(formalized physics), "
                "[CSLib](https://github.com/leanprover/cslib) (computer "
                "science), and "
                "[ArkLib](https://github.com/Verified-zkEVM/ArkLib) (verified "
                "cryptography) — plus "
                "[PutnamBench](https://github.com/trishullab/PutnamBench) "
                "competition problems. Project problems are compiled in place "
                "inside their repositories; PutnamBench problems are "
                "self-contained against Mathlib.\n\n"
                "### The competition\n\n"
                "Two tracks, ranked separately: **closed-source LLM** (API "
                "models + any harness, ≤ US$3 per problem) and **open-source "
                "LLM** (public weights, post-training and/or harness, "
                "4× 80 GB A100 for ≤ 48 h). Each track's winner receives "
                f"**{PRIZE_PER_TRACK}** and a dedicated talk at the "
                f"[{WORKSHOP_NAME}]({WORKSHOP_URL}) workshop "
                f"({WORKSHOP_VENUE}), which this competition is part of. See "
                "**Tracks & Rules** for details.\n\n"
                "### Scoring (multi-objective)\n\n"
                "- **Length reduction %** — decrease in proof token count vs "
                "the reference proof.\n"
                "- **Heartbeat reduction %** — change in Lean's "
                "[`#count_heartbeats`](https://lean-lang.org/doc/reference/latest/IO/Timing/#IO___getNumHeartbeats) "
                "elaboration cost vs the reference.\n"
                "- **Zero-shot transfer %** — fraction of the problem's listed "
                "Lean toolchains on which the proof compiles unchanged.\n"
                "- **Combined %** — mean of the three; the default ranking.\n\n"
                "Compile failure, a changed statement, or `sorry` scores zero "
                "for that row.\n\n"
                "### How evaluation runs\n\n"
                "This Space is the front door: it validates and queues "
                "submissions. Compilation and scoring run on a **dedicated "
                "evaluation worker** with the full Lean toolchains and "
                "repository checkouts pre-built — no compilation happens in "
                "this Space. Progress streams back to the Submit tab and the "
                "leaderboard updates automatically.\n\n"
                "### Built with the support of\n\n"
                "AWS · Simon Fraser University · The University of Texas at "
                "Austin · CSLib · PhysLib · ArkLib."
            )

        # ── Contribute ────────────────────────────────────────────────────────
        with gr.Tab("Contribute", id="contribute"):
            gr.HTML(
                "<div class='lra-intro'>"
                "<div class='lra-kicker'>Grow the benchmark</div>"
                "<h2>Contributing: harvesting long Lean proofs</h2>"
                "<p>The benchmark grows with the community. If you maintain or "
                "know a Lean development with long, expensive proofs, we'd "
                "love to include them — here's what makes a good candidate "
                "problem.</p>"
                "</div>"
            )
            gr.Markdown(CONTRIBUTION_MD)

        # ── Cite ──────────────────────────────────────────────────────────────
        with gr.Tab("Cite", id="cite"):
            gr.HTML(value=_cite_html())

    home_lb_btn.click(lambda: _select_tab("leaderboard"), outputs=app_tabs, api_name=False)
    home_submit_btn.click(lambda: _select_tab("submit"), outputs=app_tabs, api_name=False)
    home_rules_btn.click(lambda: _select_tab("rules"), outputs=app_tabs, api_name=False)

    submit_btn.click(
        verify_and_submit,
        [user_in, track_in, file_in],
        [progress_df, submit_status],
        api_name="verify_and_submit",
    )

    refresh_btn.click(_leaderboard_closed_html, None, lb_closed, api_name="leaderboard")
    refresh_btn.click(_leaderboard_open_html, None, lb_open, api_name=False)

    # Poll the persisted submission status for whatever username is in the box.
    # The evaluation worker updates status/<user>.json as it compiles.
    gr.Timer(value=15).tick(
        submission_status,
        inputs=[user_in],
        outputs=[progress_df, submit_status],
    )

    # Auto-refresh the leaderboards so finished submissions appear without
    # the user having to click Refresh.
    gr.Timer(value=60).tick(_leaderboard_closed_html, outputs=lb_closed)
    gr.Timer(value=60).tick(_leaderboard_open_html, outputs=lb_open)

    # Populate the leaderboards + home on every page load (the baked `value=`
    # is only the build-time snapshot; refresh fns re-read the bucket first).
    demo.load(_leaderboard_closed_html, outputs=lb_closed)
    demo.load(_leaderboard_open_html, outputs=lb_open)
    demo.load(refresh_home, outputs=home_body)

    # Hidden admin endpoints — gated by env-var ADMIN_RESET_TOKEN.
    _admin_tok = gr.Textbox(visible=False)
    _admin_out = gr.Textbox(visible=False)
    _admin_btn = gr.Button(visible=False)
    _admin_btn.click(admin_reset, _admin_tok, _admin_out, api_name="admin_reset")

    _cl_tok = gr.Textbox(visible=False)
    _cl_user = gr.Textbox(visible=False)
    _cl_sid = gr.Textbox(visible=False)
    _cl_out = gr.Textbox(visible=False)
    _cl_btn = gr.Button(visible=False)
    _cl_btn.click(
        compat_list, [_cl_tok, _cl_user, _cl_sid], _cl_out,
        api_name="compat_list",
    )

    _log_tok = gr.Textbox(visible=False)
    _log_user = gr.Textbox(visible=False)
    _log_sid = gr.Textbox(visible=False)
    _log_name = gr.Textbox(visible=False)
    _log_ver = gr.Textbox(visible=False)
    _log_out = gr.Textbox(visible=False)
    _log_btn = gr.Button(visible=False)
    _log_btn.click(
        compat_log,
        [_log_tok, _log_user, _log_sid, _log_name, _log_ver],
        _log_out,
        api_name="compat_log",
    )


if __name__ == "__main__":
    demo.queue(default_concurrency_limit=None).launch(
        server_name="0.0.0.0",
        server_port=int(os.environ.get("GRADIO_SERVER_PORT", "7860")),
        allowed_paths=[
            BENCHMARK_JSONL_PATH,
            str(SPONSOR_ASSETS_DIR),
            str(BENCH_ASSETS_DIR),
        ],
        favicon_path=str(APP_ICON_PATH),
    )