From e8c52a84d2b63cec1ac3daeb1d6fbbf18957c8f5 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 09:51:04 +0100 Subject: [PATCH 1/4] Add weekly metrics workflow (AFP coverage + performance) A new `metrics` GitHub Actions workflow measures parser coverage and performance against the latest AFP release and publishes the figures into the README: - Triggers: weekly cron (Mon 04:00 UTC) + manual workflow_dispatch (with an optional sample-size input). Not on push, so normal CI is unaffected. - Corpus: downloads afp-current.tar.gz via metrics/fetch_corpus.sh, cached per ISO week (refreshes weekly, reused for same-week re-runs). - Measurement: metrics/measure.py parses a seeded random sample with a per-file timeout and records coverage %, timeout %, throughput, and median parse time to metrics/metrics.json. - Publishing: metrics/update_readme.py rewrites the block between the `.. METRICS:START` / `.. METRICS:END` markers in README.rst with an RST table; the job commits it back with the default GITHUB_TOKEN and `[skip ci]` (no workflow retrigger), staying green on no-op weeks. corpus/ is gitignored. The metrics scripts pass ruff/isort/mypy. Co-Authored-By: Claude Opus 4.8 (1M context) --- .github/workflows/metrics.yml | 75 +++++++++++++++++++ .gitignore | 1 + README.rst | 13 ++++ metrics/fetch_corpus.sh | 26 +++++++ metrics/measure.py | 135 ++++++++++++++++++++++++++++++++++ metrics/update_readme.py | 70 ++++++++++++++++++ 6 files changed, 320 insertions(+) create mode 100644 .github/workflows/metrics.yml create mode 100755 metrics/fetch_corpus.sh create mode 100644 metrics/measure.py create mode 100644 metrics/update_readme.py 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..dbce3bc --- /dev/null +++ b/metrics/fetch_corpus.sh @@ -0,0 +1,26 @@ +#!/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" + +# Record the release name (the tarball's top-level directory, e.g. afp-2026-06-01). +version="$(tar -tzf "$tmp" | head -1 | cut -d/ -f1)" +echo "Extracting $version ..." +tar -xzf "$tmp" -C "$DEST" --strip-components=1 +rm -f "$tmp" +echo "$version" > "$DEST/AFP_VERSION" + +echo "Extracted $(find "$DEST" -name '*.thy' | wc -l) .thy files from $version." 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..82ba9f5 --- /dev/null +++ b/metrics/update_readme.py @@ -0,0 +1,70 @@ +"""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 +import re +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) + new, n = re.subn( + r"(\.\. METRICS:START\n).*?(\n\.\. METRICS:END)", + lambda mo: mo.group(1) + "\n" + block + mo.group(2), + text, + flags=re.S, + ) + if n == 0: + raise SystemExit( + "METRICS markers not found in README; expected " + "'.. METRICS:START' and '.. METRICS:END'." + ) + open(README, "w").write(new) + print(f"Updated {README} ({n} block).") + + +if __name__ == "__main__": + main() From 977d759c1c7e5de6977c0b69f279ac7b51d33aa6 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 09:56:39 +0100 Subject: [PATCH 2/4] ci: re-trigger checks [empty] From 1466656e34477e8593de85085a0f72af353b15cb Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 09:59:54 +0100 Subject: [PATCH 3/4] Fix mypy str/bytes error in update_readme (avoid re.subn overload) CI's mypy flagged the re.subn lambda's overload resolution as bytes. Replace the regex-callable replacement with a plain marker splice; drop the now-unused re import. --- metrics/update_readme.py | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/metrics/update_readme.py b/metrics/update_readme.py index 82ba9f5..7b0bfed 100644 --- a/metrics/update_readme.py +++ b/metrics/update_readme.py @@ -6,7 +6,6 @@ import json import os -import re from typing import Any README = os.environ.get("README", "README.rst") @@ -51,19 +50,17 @@ def main() -> None: m = json.load(open(METRICS)) text = open(README).read() block = build_table(m) - new, n = re.subn( - r"(\.\. METRICS:START\n).*?(\n\.\. METRICS:END)", - lambda mo: mo.group(1) + "\n" + block + mo.group(2), - text, - flags=re.S, - ) - if n == 0: + 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} ({n} block).") + print(f"Updated {README}.") if __name__ == "__main__": From f54338fb1a8d1a760e3b183f58b3349d29cab9c5 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Wed, 3 Jun 2026 10:22:36 +0100 Subject: [PATCH 4/4] Fix fetch_corpus.sh aborting on tar|head SIGPIPE under pipefail Found by actually running the fetch: 'tar -tzf | head -1' under set -o pipefail makes tar receive SIGPIPE (head closes early), failing the pipeline and aborting before extraction. Detect the release name from the extracted directory instead (drop --strip-components so the afp-* dir is present); verified end-to-end against the live AFP tarball (10098 .thy files, version afp-2026-06-01, idempotent re-run). --- metrics/fetch_corpus.sh | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/metrics/fetch_corpus.sh b/metrics/fetch_corpus.sh index dbce3bc..d6195d5 100755 --- a/metrics/fetch_corpus.sh +++ b/metrics/fetch_corpus.sh @@ -16,11 +16,12 @@ echo "Downloading $URL ..." tmp="$(mktemp --suffix=.tar.gz)" curl -fsSL "$URL" -o "$tmp" -# Record the release name (the tarball's top-level directory, e.g. afp-2026-06-01). -version="$(tar -tzf "$tmp" | head -1 | cut -d/ -f1)" -echo "Extracting $version ..." -tar -xzf "$tmp" -C "$DEST" --strip-components=1 +echo "Extracting ..." +tar -xzf "$tmp" -C "$DEST" rm -f "$tmp" -echo "$version" > "$DEST/AFP_VERSION" -echo "Extracted $(find "$DEST" -name '*.thy' | wc -l) .thy files from $version." +# 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})."