feat: post comments about changes to crossref tags#44
Open
kim-em wants to merge 8 commits into
Open
Conversation
Add scripts/crossref_review/post-comment.sh. Invoked from mathlib4's
.github/workflows/crossref_review.yml after the
privilege-escalation-bridge delivers the TSV produced by
scripts/dump_crossref_tags.lean in mathlib4.
Pipeline:
1. Filter the TSV by gh pr diff --name-only to records whose source
module is among the PR's changed .lean files.
2. Install elan if missing, clone leanprover-community/external-tags
at the pinned SHA, build crossref-render.
3. Run crossref-render on the filtered TSV; capture Markdown body.
4. Hand off to scripts/pr_summary/update_PR_comment.sh to post-or-update
the bot comment.
5. Exit non-zero if any tag was missing upstream, so the workflow_run
check turns red on the PR.
Replaces leanprover-community#39, which contained a ~350 LOC Python orchestrator that did
snippet fetching, Markdown rendering, and comment posting inline. All of
that now lives in leanprover-community/external-tags; this script is the
GitHub-Actions-specific plumbing only.
Pinning external-tags to an immutable SHA (in EXTERNAL_TAGS_SHA at the
top of the script) preserves the trust story: the privileged workflow_run
job runs only code from this repo, which in turn runs only code from
external-tags at a known revision. Bumping the pin is a one-line PR
where reviewers diff external-tags@<OLD>..<NEW>.
Companion mathlib4 PRs:
- leanprover-community/mathlib4#39876 (dump script)
- leanprover-community/mathlib4#39877 (workflow shim)
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Code review (Codex) found six should-fix issues plus a missed caching opportunity. Address all of them: * TSV size cap is now enforced in trusted code (stat-then-parse), not just in the PR-controlled dump script. The dump script's 2 MB cap was documented as a security boundary; it wasn't one. * Validate that PR_NUMBER and HEAD_SHA from the bridge payload match their expected shapes (decimal and 40-char hex) before we use them. * Stale-run check: gh pr view --json headRefOid. If the PR head has moved since the build that produced our TSV (force-push between build and comment), exit cleanly. Otherwise we'd post a misleading comment describing an old state of the PR. * Don't silently treat a failed `gh pr diff` as "no .lean files in this PR". Capture into a tempfile and only tolerate grep's no-match exit. * Use crossref-render's exit code (1 = missing) instead of greping the rendered Markdown for **missing**. Combined with the new Markdown escaping in external-tags f56909c, the previous grep was both brittle (any rename of the rendered text broke it) and PR-controllable (a tag comment of literal **missing** would force-red the check). * CROSSREF_RENDER_BIN env var: if set, skip the clone+build and use the prebuilt binary. The mathlib4 workflow_run YAML now pre-builds and caches crossref-render across runs, so the orchestrator no longer pays ~1 min per PR comment. Script stays runnable standalone when invoked outside CI (no env var → fall back to clone+build). * Bump EXTERNAL_TAGS_SHA to f56909c70b3ed7cc607a6110c04f25bd19d55731: picks up the Markdown escaping fix referenced above and a couple of small standalone-tool fixes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Picks up an external-tags cleanup pass (3be1259f38231e10c40b8fbe0329d2d43d823006): * deletes dead code (fetchOne, fetchWikidataOne, fetchGerbyOne in Fetch.lean); * fixes a bug in PRArtifact.lean (workflow-name filter excluded fork PRs); * fixes the extractDir location for crossref-review --pr; * drops the unimplemented --build-locally flag from crossref-review; * ungarbles a docstring comment; * refreshes README, lakefile (all 3 exes default-target), and CI smoke tests (now also exercise crossref-render against hostile input). No behaviour changes for the orchestrator path; the prebuilt crossref-render binary that the workflow caches will be rebuilt at this new SHA on next cache miss. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The README still described post-comment.sh as cloning external-tags on every run, but since the mathlib4 workflow_run shim caches the prebuilt binary, the clone+build path is only the fallback. Step list also missed the new validation and stale-run-skip steps. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…timeout Substantive update to the orchestrator. The previous design rendered every cross-reference tag in any file the PR touched; a 1000-file maintenance PR would fire on hundreds of unchanged tags. The new design subtracts a master baseline so only tags this PR actually authored appear in the comment. What changed: * Merge-base baseline diff. Look up the PR's merge-base SHA via the GitHub compare API, find the master CI run at that exact commit, and download its `crossref-tags-baseline` artifact (uploaded by mathlib4#39877). Pass it to crossref-render via --baseline-tsv so rows that match a baseline row verbatim are dropped. Missing baseline (artifact expired, build never ran) is non-fatal: we skip the subtraction and log a warning. * Per-database tag-shape regex validation. Master mathlib's attribute parsers enforce these shapes, but the producer is PR-controlled. Defence in depth — a malicious dump emitting a tag like "../../etc" is rejected before reaching the renderer. * Wall-clock timeout on the renderer (180s). Each upstream snippet fetch has a 10s curl timeout; this caps total render time regardless of row count or upstream latency. * Pass --strict to crossref-render so producer bugs / malicious artifacts can't silently hide rows from the bot comment (malformed rows are now a hard error). * Row-count cap (500) after baseline + regex filtering, as a final safety net. * Bump EXTERNAL_TAGS_SHA to 4634089 to pick up the matching --baseline-tsv / --strict / percent-encoded URL changes in crossref-render. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…oaden baseline lookup Three robustness fixes: * Delete orphaned bot comments. Previously, if a PR initially added a cross-reference tag and then the author removed it (or the file containing it), the orchestrator would exit cleanly without touching the existing bot comment — leaving a stale comment that misrepresents the current PR state. All "exit clean, nothing to render" paths now delete the prior comment (matched by marker prefix). * Skip the comment update if the rendered body is byte-identical to the existing one. Each PR push otherwise generates an "updated comment" notification for subscribers even when nothing changed. * Drop --branch master from the baseline run lookup. The dump output is a function of the elaborated environment at the SHA, so a CI run on any branch with that exact head SHA produces an equivalent baseline. This handles PRs targeting non-master branches (stacked PRs, PRs against nightly-testing, etc.) when the merge-base happens to have a CI artifact from another branch. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…dead array The row cap was being applied to the regex-validated, changed-files- filtered TSV but BEFORE baseline subtraction. A maintenance PR touching many files containing existing tags could exceed MAX_FILTERED_ROWS (500) even though the baseline diff would later reduce the render set to ~0. That turned innocent refactors into failed privileged checks. Now the orchestrator subtracts the baseline in shell (one awk pass) before counting and before invoking the renderer. The cap is applied to the actual render set. The renderer no longer needs --baseline-tsv from this orchestrator (we already did it); Cli/Review still uses the flag directly. Also dropped the unused TAG_REGEXES associative array — the regexes are inlined in the case at the validation step, which reads better. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Picks up the bridge-vs-baseline retention clarification in Crossrefs/PRArtifact.lean's module docstring. No behaviour change. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 task
kim-em
changed the title
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.
This PR adds
scripts/crossref_review/post-comment.sh, the privileged orchestrator for the cross-reference tag review pipeline. It's invoked from mathlib4's crossref_review.yml (mathlib4 #39877) after theprivilege-escalation-bridgedelivers the TSV produced by mathlib4'sscripts/dump_crossref_tags.lean.Filters the TSV by the PR's changed
.leanfiles, downloads and subtracts the merge-base baseline, regex-validates each tag, then invokescrossref-renderfrom a pinnedexternal-tagsSHA (with--strictand a wall-clock timeout) to fetch upstream snippets and render the Markdown bot comment. Posts, updates, or deletes the comment accordingly; skips the update if the body is byte-identical. Detailed pipeline and trust notes are in the script header.Bumping the pinned
external-tagsSHA is a one-line PR; reviewers diffexternal-tags@<OLD>..<NEW>.🤖 Prepared with Claude Code