Commit b77378e
refactor(crossref_review): consume TSV from mathlib4's post-build lint step
The mathlib4 cross-reference review pipeline is moving from a text-based
extractor running independently in a `pull_request_target` workflow to an
elaboration-based lint step that runs in the build pipeline's `post_steps`
job after `lake exe cache get`. The lint step emits a machine-readable
TSV (db / tag / declName / file / comment) as an artifact, and a
`workflow_run`-triggered companion downloads it here.
This commit rewrites `scripts/crossref_review/crossref-pr-comment.py` so
it:
* Takes `--tsv` (the path to the artifact) instead of two checkout paths.
* Defensively parses the TSV (unknown databases dropped, missing fields
padded). Nothing from PR-derived input is executed.
* Fetches snippets directly via Python's `urllib` — Wikidata via the
batched `wbgetentities` API, Stacks/Kerodon via the documented Gerby
`/data/tag/<TAG>/content/statement` endpoint. Gerby fetches are
parallelised with `ThreadPoolExecutor(max_workers=8)` to keep the
workflow under a minute on PRs that touch large files.
* Constructs the Markdown comment in trusted code (no longer relies on
PR-derived Markdown), still using the `### Cross-reference tags added
by this PR` sentinel so `update_PR_comment.sh` can dedupe.
* Exits 0 / 1 / 2 / 3 with the same grammar as before.
Stacked on leanprover-community/mathlib4#39666
upcoming force-push, which adds the post-build lint step and rewires
`crossref_review.yml` as `workflow_run`-triggered.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>1 parent 3c72af0 commit b77378e
1 file changed
Lines changed: 235 additions & 150 deletions
0 commit comments