diff --git a/.github/workflows/metrics.yml b/.github/workflows/metrics.yml new file mode 100644 index 0000000..d3f0b5f --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index a928965..4c06dae 100644 --- a/.gitignore +++ b/.gitignore @@ -46,3 +46,4 @@ pip-wheel-metadata/ pytestdebug.log scripts/ src/_pytest/_version.py +corpus/ diff --git a/README.rst b/README.rst index ff728cd..2e68460 100644 --- a/README.rst +++ b/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 +`_ 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 ============ diff --git a/metrics/fetch_corpus.sh b/metrics/fetch_corpus.sh new file mode 100755 index 0000000..d6195d5 --- /dev/null +++ b/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})." diff --git a/metrics/measure.py b/metrics/measure.py new file mode 100644 index 0000000..d9d43dd --- /dev/null +++ b/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() diff --git a/metrics/update_readme.py b/metrics/update_readme.py new file mode 100644 index 0000000..7b0bfed --- /dev/null +++ b/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()