Add weekly metrics workflow (AFP coverage + performance) published to the README

.github/workflows/metrics.yml

@@ -0,0 +1,75 @@
+name: metrics
+
+on:
+  workflow_dispatch:
+    inputs:
+      sample:
+        description: "Number of AFP files to sample"
+        default: "500"
+  schedule:
+    - cron: '0 4 * * 1'   # 04:00 UTC every Monday
+
+# Allow the job to commit the refreshed README back to the repo.
+permissions:
+  contents: write
+
+concurrency:
+  group: metrics
+  cancel-in-progress: false
+
+jobs:
+  metrics:
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: "3.12"
+
+      - name: Install Poetry
+        uses: snok/install-poetry@v1
+        with:
+          version: latest
+          virtualenvs-create: true
+          virtualenvs-in-project: true
+
+      - name: Install dependencies
+        run: poetry install --all-extras --no-interaction
+
+      - name: Compute cache week
+        id: week
+        run: echo "week=$(date -u +%G-%V)" >> "$GITHUB_OUTPUT"
+
+      - name: Cache AFP corpus
+        uses: actions/cache@v4
+        with:
+          path: corpus
+          # Weekly key: refreshes the corpus each ISO week, reused within the
+          # week (e.g. for manual re-runs). No restore-keys, so a new week is a
+          # genuine miss and the fetch script downloads the latest release.
+          key: afp-corpus-${{ steps.week.outputs.week }}
+
+      - name: Fetch AFP corpus
+        run: bash metrics/fetch_corpus.sh corpus
+
+      - name: Measure coverage and performance
+        env:
+          METRICS_SAMPLE: ${{ github.event.inputs.sample || '500' }}
+        run: poetry run python metrics/measure.py
+
+      - name: Update README
+        run: poetry run python metrics/update_readme.py
+
+      - name: Commit refreshed metrics
+        run: |
+          git config user.name  "metrics-bot"
+          git config user.email "metrics-bot@users.noreply.github.com"
+          git add README.rst metrics/metrics.json
+          # Pushing with the default GITHUB_TOKEN does not retrigger workflows;
+          # [skip ci] is belt-and-suspenders. No-op stays green.
+          git commit -m "chore: update AFP metrics [skip ci]" || { echo "no changes"; exit 0; }
+          git push

.gitignore

@@ -46,3 +46,4 @@ pip-wheel-metadata/
 pytestdebug.log
 scripts/
 src/_pytest/_version.py
+corpus/

README.rst

@@ -33,6 +33,19 @@ methods, and a few rarely-used commands are still rejected. Treat a successful
 parse as authoritative and a failure as "not yet supported" rather than "invalid
 Isabelle".
 
+Metrics
+=======
+
+Parser coverage and performance against the latest `Archive of Formal Proofs
+<https://www.isa-afp.org/>`_ release, refreshed weekly by the ``metrics``
+workflow (and on demand via *Run workflow*):
+
+.. METRICS:START
+
+*Not measured yet — the* ``metrics`` *workflow populates this on its first run.*
+
+.. METRICS:END
+
 Requirements
 ============
 

metrics/fetch_corpus.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+# Download and extract the latest AFP release into the corpus directory.
+# No-op if the corpus is already present (e.g. restored from cache).
+set -euo pipefail
+
+DEST="${1:-corpus}"
+URL="${AFP_URL:-https://isa-afp.org/release/afp-current.tar.gz}"
+
+mkdir -p "$DEST"
+if find "$DEST" -name '*.thy' -print -quit 2>/dev/null | grep -q .; then
+  echo "Corpus already present in '$DEST' ($(find "$DEST" -name '*.thy' | wc -l) .thy files) - skipping download."
+  exit 0
+fi
+
+echo "Downloading $URL ..."
+tmp="$(mktemp --suffix=.tar.gz)"
+curl -fsSL "$URL" -o "$tmp"
+
+echo "Extracting ..."
+tar -xzf "$tmp" -C "$DEST"
+rm -f "$tmp"
+
+# Record the release name: the extracted top-level directory (e.g. afp-2026-06-01).
+version="$(find "$DEST" -maxdepth 1 -mindepth 1 -type d -name 'afp-*' -printf '%f\n' | head -1 || true)"
+[ -n "$version" ] && echo "$version" > "$DEST/AFP_VERSION"
+
+echo "Extracted $(find "$DEST" -name '*.thy' | wc -l) .thy files (${version:-unknown})."

metrics/measure.py

@@ -0,0 +1,135 @@
+"""Measure parser coverage and performance against an AFP corpus.
+
+Parses a fixed (seeded) random sample of theory files from the corpus, recording
+how many parse successfully and how fast, and writes the figures to
+``metrics/metrics.json``. A per-file timeout bounds the run; timeouts count as
+"not parsed" (the Earley chart can grow super-linearly on large files).
+
+Configuration via environment variables:
+  CORPUS_DIR       corpus location (default: corpus)
+  METRICS_SAMPLE   number of files to sample (default: 500; 0 = all)
+  METRICS_TIMEOUT  per-file timeout in seconds (default: 15)
+  METRICS_SEED     RNG seed for the sample (default: 42)
+  METRICS_OUT      output path (default: metrics/metrics.json)
+"""
+
+import datetime
+import glob
+import json
+import os
+import random
+import signal
+import statistics
+import sys
+import time
+from concurrent.futures import ProcessPoolExecutor, as_completed
+from typing import Any
+
+# Make isabelle_parser importable in pool workers regardless of start method
+# (spawn/forkserver re-import this module, re-running this line) or whether the
+# package is installed.
+sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.abspath(__file__))))
+
+CORPUS = os.environ.get("CORPUS_DIR", "corpus")
+SAMPLE = int(os.environ.get("METRICS_SAMPLE", "500"))
+TIMEOUT = int(os.environ.get("METRICS_TIMEOUT", "15"))
+SEED = int(os.environ.get("METRICS_SEED", "42"))
+OUT = os.environ.get("METRICS_OUT", "metrics/metrics.json")
+
+_parser = None
+
+
+def _get_parser() -> Any:
+    global _parser
+    if _parser is None:
+        from isabelle_parser import load_parser
+
+        _parser = load_parser()
+    return _parser
+
+
+def _parse_one(path: str) -> tuple[str, int, float]:
+    try:
+        data = open(path, errors="replace").read()
+    except Exception:
+        return ("error", 0, 0.0)
+    size = len(data.encode("utf-8", "replace"))
+
+    def _alarm(signum: int, frame: Any) -> None:
+        raise TimeoutError()
+
+    signal.signal(signal.SIGALRM, _alarm)
+    signal.setitimer(signal.ITIMER_REAL, TIMEOUT)
+    start = time.time()
+    try:
+        _get_parser().parse(data)
+        status = "ok"
+    except TimeoutError:
+        status = "timeout"
+    except Exception:
+        status = "fail"
+    finally:
+        signal.setitimer(signal.ITIMER_REAL, 0)
+    return (status, size, time.time() - start)
+
+
+def main() -> None:
+    files = sorted(glob.glob(os.path.join(CORPUS, "**", "*.thy"), recursive=True))
+    if not files:
+        raise SystemExit(f"No .thy files found under '{CORPUS}'.")
+    random.seed(SEED)
+    random.shuffle(files)
+    if SAMPLE:
+        files = files[:SAMPLE]
+
+    version = "unknown"
+    vfile = os.path.join(CORPUS, "AFP_VERSION")
+    if os.path.exists(vfile):
+        version = open(vfile).read().strip()
+
+    workers = os.cpu_count() or 2
+    counts = {"ok": 0, "fail": 0, "timeout": 0, "error": 0}
+    ok_times = []
+    total_bytes = 0
+    wall_start = time.time()
+    with ProcessPoolExecutor(max_workers=workers) as ex:
+        for fut in as_completed([ex.submit(_parse_one, f) for f in files]):
+            status, size, dt = fut.result()
+            counts[status] += 1
+            total_bytes += size
+            if status == "ok":
+                ok_times.append(dt)
+    wall = time.time() - wall_start
+
+    attempted = len(files)
+    metrics = {
+        "afp_version": version,
+        "sample_size": attempted,
+        "workers": workers,
+        "timeout_budget_s": TIMEOUT,
+        "ok": counts["ok"],
+        "fail": counts["fail"],
+        "timeout": counts["timeout"],
+        "error": counts["error"],
+        "coverage_pct": round(100 * counts["ok"] / attempted, 1),
+        "timeout_pct": round(100 * counts["timeout"] / attempted, 1),
+        "wall_seconds": round(wall, 1),
+        "files_per_sec": round(attempted / wall, 2) if wall else None,
+        "mb_per_sec": round(total_bytes / 1e6 / wall, 3) if wall else None,
+        "median_ok_parse_s": round(statistics.median(ok_times), 3)
+        if ok_times
+        else None,
+        "measured_at": datetime.datetime.now(datetime.timezone.utc).strftime(
+            "%Y-%m-%d %H:%M UTC"
+        ),
+    }
+
+    os.makedirs(os.path.dirname(OUT), exist_ok=True)
+    with open(OUT, "w") as fh:
+        json.dump(metrics, fh, indent=2)
+        fh.write("\n")
+    print(json.dumps(metrics, indent=2))
+
+
+if __name__ == "__main__":
+    main()

metrics/update_readme.py

@@ -0,0 +1,67 @@
+"""Inject the latest metrics into README.rst between the METRICS markers.
+
+Reads metrics/metrics.json and rewrites the block delimited by
+``.. METRICS:START`` and ``.. METRICS:END`` with an RST table.
+"""
+
+import json
+import os
+from typing import Any
+
+README = os.environ.get("README", "README.rst")
+METRICS = os.environ.get("METRICS_OUT", "metrics/metrics.json")
+
+
+def build_table(m: dict[str, Any]) -> str:
+    def row(metric: str, value: Any) -> str:
+        return f"   * - {metric}\n     - {value}\n"
+
+    fps = m.get("files_per_sec")
+    mbs = m.get("mb_per_sec")
+    throughput = (
+        f"{fps} files/s · {mbs} MB/s (×{m.get('workers', '?')} workers)"
+        if fps is not None
+        else "n/a"
+    )
+    median = m.get("median_ok_parse_s")
+    median_s = f"{median} s" if median is not None else "n/a"
+
+    table = ".. list-table::\n   :header-rows: 1\n   :widths: 45 55\n\n"
+    table += row("Metric", "Value")
+    table += row("AFP snapshot", m.get("afp_version", "unknown"))
+    table += row("Files sampled", m.get("sample_size", "?"))
+    table += row("Parse coverage", f"{m.get('coverage_pct')}% ({m.get('ok')} parsed)")
+    table += row(
+        f"Timeouts (> {m.get('timeout_budget_s')}s)",
+        f"{m.get('timeout_pct')}% ({m.get('timeout')})",
+    )
+    table += row("Throughput", throughput)
+    table += row("Median parse time (parsed files)", median_s)
+    table += row("Measured", m.get("measured_at", "?"))
+    table += (
+        "\n*Coverage is the share of a seeded random sample of AFP theory files "
+        "that parse within the timeout; a whole file counts as failed if any "
+        "statement fails. Updated weekly by the metrics workflow.*\n"
+    )
+    return table
+
+
+def main() -> None:
+    m = json.load(open(METRICS))
+    text = open(README).read()
+    block = build_table(m)
+    start, end = ".. METRICS:START", ".. METRICS:END"
+    i = text.find(start)
+    j = text.find(end)
+    if i == -1 or j == -1 or j < i:
+        raise SystemExit(
+            "METRICS markers not found in README; expected "
+            "'.. METRICS:START' and '.. METRICS:END'."
+        )
+    new = text[: i + len(start)] + "\n\n" + block + "\n" + text[j:]
+    open(README, "w").write(new)
+    print(f"Updated {README}.")
+
+
+if __name__ == "__main__":
+    main()