paper_api_audit.py

#!/usr/bin/env python3
# Copyright (c) 2026 David Roe. All rights reserved.
# Released under Apache 2.0 license as described in the file LICENSE.
# Authors: David Roe, roed@mit.edu, using Claude Opus-4.8 and Fable-5
"""Extract the paper-facing Lean API from rendered PreTeXt HTML.

The stable key is the theorem-like article's HTML id, not its displayed number.
Lean declarations are read from the `data-lean-ref` attributes generated by
PaperForge.  The resulting table can therefore be regenerated after the paper
is reorganized without guessing from theorem numbers.

Usage:
    python3 scripts/paper_api_audit.py /path/to/paper.html
"""

from __future__ import annotations

import argparse
import re
from dataclasses import dataclass, field
from html.parser import HTMLParser
from pathlib import Path


RESULT = re.compile(r"^(Theorem|Proposition|Lemma|Corollary|Definition)\s+")


@dataclass
class PaperResult:
    stable_id: str
    title_parts: list[str] = field(default_factory=list)
    lean_refs: list[str] = field(default_factory=list)

    @property
    def title(self) -> str:
        compact = " ".join(" ".join(self.title_parts).split())
        return re.sub(r"\s+([.,;:])", r"\1", compact)


class ResultParser(HTMLParser):
    def __init__(self) -> None:
        super().__init__(convert_charrefs=True)
        self.results: list[PaperResult] = []
        self.current: PaperResult | None = None
        self.article_depth = 0
        self.heading_depth = 0

    def handle_starttag(self, tag: str, attrs: list[tuple[str, str | None]]) -> None:
        attributes = dict(attrs)
        if tag == "article":
            if self.current is None:
                self.current = PaperResult(attributes.get("id") or "")
                self.article_depth = 1
            else:
                self.article_depth += 1
        elif self.current is not None and tag in {"h3", "h4", "h5", "h6"}:
            self.heading_depth += 1
        elif self.current is not None and tag == "a":
            ref = attributes.get("data-lean-ref")
            if ref and ref.startswith("GQ2.") and ref not in self.current.lean_refs:
                self.current.lean_refs.append(ref)

    def handle_endtag(self, tag: str) -> None:
        if self.current is None:
            return
        if tag in {"h3", "h4", "h5", "h6"} and self.heading_depth:
            self.heading_depth -= 1
        elif tag == "article":
            self.article_depth -= 1
            if self.article_depth == 0:
                if self.current.stable_id and RESULT.match(self.current.title):
                    self.results.append(self.current)
                self.current = None

    def handle_data(self, data: str) -> None:
        if self.current is not None and self.heading_depth:
            self.current.title_parts.append(data)


def parse_results(path: Path) -> list[PaperResult]:
    parser = ResultParser()
    parser.feed(path.read_text())
    ids = [result.stable_id for result in parser.results]
    if len(ids) != len(set(ids)):
        raise SystemExit("paper API audit: duplicate stable result ids")
    return parser.results


def main() -> None:
    argument_parser = argparse.ArgumentParser(description=__doc__)
    argument_parser.add_argument("paper_html", type=Path)
    args = argument_parser.parse_args()
    results = parse_results(args.paper_html)
    linked = sum(len(result.lean_refs) for result in results)
    print("| Stable result id | Current paper title | Lean declarations |")
    print("|---|---|---|")
    for result in results:
        refs = "<br>".join(f"`{ref}`" for ref in result.lean_refs) or "—"
        print(f"| `{result.stable_id}` | {result.title} | {refs} |")
    print()
    print(f"{len(results)} named results; {linked} GQ2 Lean links.")


if __name__ == "__main__":
    main()