Add weekly metrics workflow (AFP coverage + performance) published to the README#12
Merged
Conversation
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) <noreply@anthropic.com>
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.
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).
christiankissig
added a commit
that referenced
this pull request
Jul 7, 2026
… the README (#12) * 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. * ci: re-trigger checks [empty] * 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. * 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). ---------
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A new
metricsGitHub Actions workflow that measures parser coverage and performance against the latest AFP release and publishes the figures into the README. Independent of normal CI.When it runs
0 4 * * 1(Mon 04:00 UTC)workflow_dispatch(with an optional sample size input)push, so it never interferes with the test workflow.What it measures (
metrics/measure.py)A seeded random sample of AFP
.thyfiles is parsed with a per-file timeout; results →metrics/metrics.json:The corpus
metrics/fetch_corpus.shdownloadsafp-current.tar.gzand extracts it tocorpus/(gitignored). Cached with a per-ISO-week key — refreshes weekly, reused for same-week re-runs; a new week is a genuine miss that pulls the latest release.Publishing into the README
metrics/update_readme.pyrewrites the block between.. METRICS:START/.. METRICS:ENDmarkers inREADME.rstwith an RSTlist-table. The job commits it back:GITHUB_TOKEN(does not retrigger workflows) +[skip ci]belt-and-suspenders;|| { echo "no changes"; exit 0; }keeps no-op weeks green;permissions: contents: write.Notes
master), so this takes effect once merged.metrics/*.pypassruff/ruff format/isort/mypy.🤖 Generated with Claude Code