feat(ci): cross-reference tag review via post-build dump + workflow_run shim by kim-em · Pull Request #39877 · leanprover-community/mathlib4

kim-em · 2026-05-26T14:43:48Z

This PR adds the cross-reference tag review pipeline on the mathlib4 side. Three new steps in post_steps of build_template.yml run scripts/dump_crossref_tags.lean, upload its TSV unconditionally as a plain crossref-tags-baseline artifact (30-day retention), and on PR builds also emit a privileged crossref-tags-bridge via privilege-escalation-bridge. A new crossref_review.yml workflow_run listener consumes the bridge, caches and pre-builds crossref-render from a pinned external-tags ref, and invokes the orchestrator in mathlib-ci #44.

Trust model: the privileged job runs only code from mathlib-ci@<pinned SHA> (which in turn only runs external-tags@<pinned SHA>). The TSV is parsed as untrusted data; user-controllable fields are escaped before going into the bot comment.

depends on: feat(scripts): dump cross-reference tags to TSV for downstream review #39876

🤖 Prepared with Claude Code

Add scripts/dump_crossref_tags.lean: a ~70-line standalone tool that loads the elaborated Mathlib environment, walks Mathlib.CrossRef.tagExt, and writes one TSV record per tagged declaration with columns (database, tag, declName, module, comment). This is the only piece of cross-reference review machinery that needs to live in mathlib4 — the rest (snippet fetching, filtering by PR diff, Markdown rendering, comment posting) lives in https://github.com/leanprover-community/external-tags and https://github.com/leanprover-community/mathlib-ci. The TSV emitted here is consumed by the privileged workflow_run job and treated as untrusted data; fields are normalised so tabs/newlines in user-controlled comments can't break the TSV framing, and the output is capped at 2 MB defensively (current population is ~55 KB, 491 tags). The script uses importModules (loadExts := true) rather than the withImportModules wrapper because the latter passes loadExts := false and would leave tagExt empty for imported modules. Replaces leanprover-community#39662 (which added the full standalone script in-tree at ~1k LOC). Per https://leanprover.zulipchat.com/#narrow/dm/110087,112680-dm/near/597848507, the bulk of that script now lives in https://github.com/leanprover-community/external-tags. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

github-actions · 2026-05-26T14:45:18Z

PR summary 72bdf5bd2d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ maxBytes
+ moduleToFilePath
+ sanitiseField

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

.github/workflows/build_template.yml
.github/workflows/crossref_review.yml

⚠️ Scripts folder reminder

This PR adds files under scripts/.
Please consider whether each added script belongs in this repository or in leanprover-community/mathlib-ci.

A script belongs in mathlib-ci if it is a CI automation script that interacts with GitHub (e.g. managing labels, posting comments, triggering bots), runs from a trusted external checkout in CI, or requires access to secrets.

A script belongs in this repository (scripts/) if it is a developer or maintainer tool to be run locally, a code maintenance or analysis utility, a style linting tool, or a data file used by the library's own linters.

See the mathlib-ci README for more details.

Added scripts files:

scripts/dump_crossref_tags.lean

mathlib-dependent-issues · 2026-05-26T15:23:09Z

This PR/issue depends on:

feat(scripts): dump cross-reference tags to TSV for downstream review #39876
By Dependent Issues (🤖). Happy coding!

The lint-style action fails CI on undocumented scripts. Adds an entry in the "CI workflow" section pointing to the workflow_run consumer and the external-tags repo. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The "Safety" paragraph claimed the 2 MB cap "bounds what a malicious PR could emit". It doesn't — this script lives in scripts/ and runs with the PR's permissions, so a malicious PR can remove the cap. The cap is defence-in-depth; the trusted bound lives downstream in mathlib-ci's post-comment.sh. Also: 491 tags in master today, not 539 (the earlier number was a text-scan count; the actual elaborated population is 491). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The tag, module, and comment fields all pass through sanitiseField before being written to TSV, but tag.declName was interpolated raw. Lean `Name`s can contain backtick-quoted segments (`«weird name»`) and in principle could include tabs or newlines; the one unsanitised field in a "framing-safe" TSV is inconsistent and risks breaking the downstream parser. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…un shim Stack on top of the dump_crossref_tags.lean PR. Adds two pieces: * .github/workflows/build_template.yml: three new steps in `post_steps`, after the import-graph upload. Run scripts/dump_crossref_tags.lean to produce crossref-tags.tsv. For pull_request_target builds, build a bridge payload (pr_number, head_sha) and emit it via leanprover-community/privilege-escalation-bridge/emit using artifact name `crossref-tags-bridge`. Non-PR builds skip the emit. * .github/workflows/crossref_review.yml: workflow_run listener on the two `continuous integration` workflows. Consumes the bridge artifact via privilege-escalation-bridge/consume, checks out leanprover-community/mathlib-ci, and invokes its scripts/crossref_review/post-comment.sh orchestrator. The orchestrator clones leanprover-community/external-tags at a pinned SHA and uses it to fetch snippets and render the PR comment. Replaces leanprover-community#39666. The original PR rolled its own artifact upload + PR number resolution fallback chain (~158 LOC) and included the snippet fetcher in scripts/crossref.lean (~760 LOC). This version delegates to the existing privilege-escalation-bridge infrastructure (same pattern as olean_report.yaml + olean_report_wf_run.yaml) and to external-tags, cutting the mathlib4 surface to ~97 LOC. Trust model: the privileged workflow_run job runs only code from mathlib-ci@<pinned SHA> (which runs only code from external-tags at a pinned SHA). Nothing from the build artifact is interpreted as code; the TSV is parsed as untrusted data with user-controllable fields escaped before interpolation into the comment. Depends on leanprover-community#39876. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

validate-ci-scripts-paths fails CI for direct actions/checkout of mathlib-ci. Switch to the local composite action under .github/actions/get-mathlib-ci, matching olean_report_wf_run.yaml and the other workflow_run jobs. The composite action sets CI_SCRIPTS_DIR and pins the mathlib-ci ref via .github/workflows/update_dependencies.yml. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…runs The orchestrator used to clone external-tags and lake-build crossref-render on every PR comment. That's elan install (~10s of curl/extract) + Lean toolchain download (~30s) + source compile (~10s) per PR, paid on the workflow_run job side of every fork PR. This restructure makes the workflow_run job: 1. Read the pinned EXTERNAL_TAGS_SHA out of mathlib-ci's post-comment.sh (single source of truth — bumping the pin remains a one-line PR to mathlib-ci, and this YAML picks the new value up automatically). 2. Restore a single actions/cache covering ~/.elan and external-tags/, keyed by that SHA + runner OS. Cache scope means same paths across runs, so lake-built rpaths into ~/.elan/toolchains/ stay valid. 3. On cache miss, install elan + clone + lake build once and the cache captures the result for subsequent runs. 4. Always run the orchestrator with CROSSREF_RENDER_BIN pointing at the prebuilt binary. The orchestrator (mathlib-ci 051c44c) honours that env var; if unset it falls back to clone+build, keeping the script standalone-runnable. Expected steady-state: ~5s of cache restore + the orchestrator's actual work (filter TSV, fetch snippets, post comment). First run after a pin bump: the usual ~1 min, then cached again. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The dump only feeds the crossref-tags-bridge artifact, which is itself only emitted on pull_request_target events (see the existing emit guard). Skip the dump too — saves a couple seconds per push to master and bors/staging branches. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Move the rationale into a block above the step (PR-only + see-the-script for the format) instead of restating what the named script does. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The orchestrator that posts the PR comment used to render every cross-reference tag in any file the PR touched. A maintenance PR that touches a thousand files (without changing tags) would still fire on hundreds of unchanged tags. The right semantics is to subtract tags that already existed at the PR's merge-base commit. This change unconditionally uploads the dump output as a plain `crossref-tags-baseline` artifact (5-day retention, ~55 KB). The privileged workflow_run job (crossref_review.yml + mathlib-ci's post-comment.sh) looks up the PR's merge-base SHA via the GitHub compare API, downloads the matching master baseline, and passes it to crossref-render via `--baseline-tsv`. Only rows that don't match a baseline row verbatim are rendered. PR runs still also emit the privileged `crossref-tags-bridge` artifact for the workflow_run consumer; non-PR (master / bors / staging) runs only upload the plain baseline. Cost: ~2 seconds per non-PR build to run the dump (cached Mathlib build is already loaded). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

PRs that sit idle for a week or two should still find a baseline at their merge-base SHA. With 5-day retention they'd fall back to "changed-files only" rendering (which fires on every cross-reference tag in any touched file — noisy on maintenance PRs). Baseline is ~55 KB per master push, so 30 days of retention is trivial.

github-actions Bot added the CI Modifies the continuous integration setup or other automation label May 26, 2026

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 26, 2026

kim-em force-pushed the crossref-review-workflow branch 2 times, most recently from 0341083 to c210307 Compare May 27, 2026 09:28

kim-em force-pushed the crossref-review-workflow branch from c210307 to cab174a Compare May 27, 2026 10:13

kim-em and others added 8 commits May 27, 2026 14:10

doc(ci): trim crossref dump step comment

8e5f468

Move the rationale into a block above the step (PR-only + see-the-script for the format) instead of restating what the named script does. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

kim-em force-pushed the crossref-review-workflow branch from 0ed75ef to 72bdf5b Compare May 27, 2026 14:10

This was referenced May 27, 2026

feat(scripts): dump cross-reference tags to TSV for downstream review #39876

Open

[Merged by Bors] - doc: add wikidata cross references #39909

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(ci): cross-reference tag review via post-build dump + workflow_run shim#39877

feat(ci): cross-reference tag review via post-build dump + workflow_run shim#39877
kim-em wants to merge 11 commits into
leanprover-community:masterfrom
kim-em:crossref-review-workflow

kim-em commented May 26, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented May 26, 2026 •

edited

Loading

Declarations diff

⚠️ Workflow documentation reminder

⚠️ Scripts folder reminder

Uh oh!

mathlib-dependent-issues Bot commented May 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

kim-em commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented May 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 72bdf5bd2d

Import changes for modified files

Declarations diff

⚠️ Workflow documentation reminder

⚠️ Scripts folder reminder

Uh oh!

mathlib-dependent-issues Bot commented May 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

kim-em commented May 26, 2026 •

edited

Loading

github-actions Bot commented May 26, 2026 •

edited

Loading