feat(scripts): add cross-reference tag tooling by kim-em · Pull Request #39662 · leanprover-community/mathlib4

kim-em · 2026-05-21T16:42:43Z

This PR adds two standalone scripts in scripts/ to support review of PRs that add @[stacks], @[kerodon], or @[wikidata] attributes. Neither needs a lakefile.lean entry — both run via lake env lean --run and depend only on Lean core (plus curl on PATH for the fetcher).

scripts/crossref-snippet.lean fetches a one-line label/description for one or more tags from the upstream database. Wikidata uses the wbgetentities API (with recovery when one bad QID poisons a batch); Stacks and Kerodon use the documented Gerby /data/tag/<TAG>/content/statement endpoint with a tolerant HTML→text strip that survives < inside math. Exit codes distinguish all-resolved (0) from missing (2) from transient network failure (3). When CROSSREF_CACHE_DIR is set, responses are memoised per (database, tag) so repeat lookups are instant.
scripts/extract-crossref-tags.lean walks a .lean file (or the added lines of a git diff range) and emits TSV of every cross-reference attribute it finds, paired with the declaration it decorates. A byte-level scanner correctly skips string literals and line/block comments, handles multi-attribute blocks (@[simp, stacks 01AB]), multi-line attribute blocks, doc comments between attribute and declaration, and modifier keywords (private, noncomputable, …). Signatures are collapsed to one line for downstream consumption.

Sample usage:

lake env lean --run scripts/crossref-snippet.lean wikidata Q11518
# Q11518 Pythagorean theorem  relation in Euclidean geometry among the three sides of a right triangle

lake env lean --run scripts/crossref-snippet.lean stacks 01AB
# 01AB Lemma 14.32.3 Lemma 14.32.3. Let \$A\$, \$B\$ be sets ...

lake env lean --run scripts/extract-crossref-tags.lean --file Mathlib/Algebra/CharP/Basic.lean
# stacks  Mathlib/Algebra/CharP/Basic.lean  195  09FS  First part. ...  instance  charP  instance charP (n : ℕ) [NeZero n] : CharP (Fin n) n

lake env lean --run scripts/extract-crossref-tags.lean --diff origin/master..HEAD --db wikidata

The scripts are deliberately text-only — they do not elaborate the files they inspect. That lets the companion CI workflow (#39666) operate on PR files as data without executing PR code under a privileged GitHub token.

Stacked follow-up PRs:

feat(CrossRefAttribute): info-view widget for cross-reference tags #39664 — LSP widget surfacing snippets in the editor when the cursor sits on a cross-reference attribute, sharing the fetch logic via a new Mathlib/Tactic/CrossRef/Fetch.lean module.
feat(ci): cross-reference tag review via post-build lint + workflow_run #39666 — GitHub Actions workflow that posts a once-per-PR comment with tag / signature / snippet tables and fails CI on unresolved tags (orchestrator lives in mathlib-ci#39).

🤖 Prepared with Claude Code

github-actions · 2026-05-21T16:44:04Z

PR summary bb78642748

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ AttrBlock
+ Clause
+ Database
+ Database.fetch
+ Database.gerbyBase?
+ Database.name
+ Database.ofString?
+ Database.ofString?_name
+ DeclHeader
+ DiffHunks
+ Mode
+ Record
+ Record.emit
+ Result
+ Result.emit
+ SrcPos
+ WikidataParse
+ afterFirst?
+ byteSlice
+ cacheFile?
+ cacheLoad
+ cacheStore
+ collapseSignature
+ declKeywords
+ extractFromFile
+ extractMain
+ extractUsage
+ fetchGerby
+ fetchGerbyAll
+ fetchUrl
+ fetchWikidata
+ findDecl
+ flattenWhitespace
+ gitDiffLeanFiles
+ jsonStrPath?
+ main
+ modifierKeywords
+ parseClause
+ parseDiff
+ parseExtractArgs
+ parseGerbyTitle
+ parseWikidataResponse
+ readIdent
+ readWord
+ recordInHunks
+ snippetMain
+ snippetUsage
+ splitAttrInstances
+ stripHtml
+ takeIdent
+ takeString
+ takeTag
+ takeUntilChar
+ tsvEscape
+ usage
+ userAgent
+ utf8Slice
+ wikidataBatchSize
+ wikidataResultOf

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.

⚠️ 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/crossref.lean

When a Mathlib declaration carries `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]`, the info view now shows the upstream label / description when the cursor sits on the attribute. The fetch is on-demand via an RPC call from the widget to the Lean server, which shells out to `curl`; we deliberately don't fetch at attribute-elaboration time so offline builds stay clean and the only network access is when an editing session opens the panel. Two new modules and a small refactor to the existing one: * `Mathlib/Tactic/CrossRef/Fetch.lean` (new) holds the `Database` enum and the snippet-fetch logic. The companion `scripts/crossref-snippet.lean` in the previous PR reimplements the same logic standalone for CI usage; the two are kept in sync deliberately so the CI script doesn't need a Mathlib build. * `Mathlib/Tactic/Widget/CrossRefHover.lean` (new) defines the widget itself: an `RpcEncodable` props record, a `RequestM` RPC method that calls `fetchSnippet`, and a `mk_rpc_widget%` Component that renders the result as Html. * `Mathlib/Tactic/CrossRefAttribute.lean` (modified) imports the two new modules, removes the now-duplicated `Database` / `databaseURL` / `databaseLabel` definitions, and calls `Widget.savePanelWidgetInfo` in each attribute's `add` handler. Tag storage, docstring rewriting, and the trace commands are untouched. If `curl` is missing or the upstream site is unreachable, the widget renders an inline error instead of blocking the LSP. The existing `MathlibTest/CrossRefAttribute.lean` suite continues to pass — none of the behaviour visible to it changes. Stacked on leanprover-community#39662 (scripts only). A third follow-up will add a GitHub Actions workflow that posts a once-per-PR comment with tag / signature / snippet tables. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

When a PR touches `Mathlib/**/*.lean` and adds `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]` attributes, this workflow posts (or updates, or deletes) a single bot comment with one row per added tag, showing the upstream label / description fetched from the source database, the Mathlib declaration's first-line signature, and the author's optional attribute comment. CI fails when any tag cannot be resolved upstream and emits a warning (not a failure) when only transient network errors occur. Three new pieces: * `scripts/crossref-pr-comment.py` — pure-stdlib Python orchestrator that drives `extract-crossref-tags.lean` then `crossref-snippet.lean` per database, formats the Markdown comment body with a hidden HTML marker for in-place updates, and returns a 0/1/2/3 exit code so the workflow can distinguish "nothing to post" from "post but pass" from "post and fail" from "post but treat as a network blip." * `.github/workflows/crossref_review.yml` — `pull_request_target` workflow with `pull-requests: write` (and only that). Installs elan, runs the orchestrator on the PR's diff range, finds the existing bot comment via `gh api … --jq` matching the marker, and `POST`s / `PATCH`es / `DELETE`s through the GitHub API. A startup gate exits cleanly when the branch pre-dates the companion scripts (so the workflow doesn't fail on PRs to an older base). * `docs/workflows.md` — new entry in the workflow inventory, matching the existing row format. Stacked on leanprover-community#39664 which adds the LSP widget side, which itself depends on leanprover-community#39662 (the scripts). Security note: the workflow runs the PR's own version of the scripts in the privileged `pull_request_target` context. The exposed token is GITHUB_TOKEN with only `pull-requests: write`, and the scripts only read .lean files and shell out to `curl` against three fixed upstream APIs, so the blast radius of a malicious script edit is limited to posting / editing PR comments. If maintainers prefer the trusted-only execution pattern used by `PR_summary.yml`, the orchestrator can move to mathlib-ci in a follow-up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

When a Mathlib declaration carries `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]`, the info view now shows the upstream label / description when the cursor sits on the attribute. The fetch is on-demand via an RPC call from the widget to the Lean server, which shells out to `curl`; we deliberately don't fetch at attribute-elaboration time so offline builds stay clean and the only network access is when an editing session opens the panel. Two new modules and a small refactor to the existing one: * `Mathlib/Tactic/CrossRef/Fetch.lean` (new) holds the `Database` enum and the snippet-fetch logic. The companion `scripts/crossref-snippet.lean` in the previous PR reimplements the same logic standalone for CI usage; the two are kept in sync deliberately so the CI script doesn't need a Mathlib build. * `Mathlib/Tactic/Widget/CrossRefHover.lean` (new) defines the widget itself: an `RpcEncodable` props record, a `RequestM` RPC method that calls `fetchSnippet`, and a `mk_rpc_widget%` Component that renders the result as Html. * `Mathlib/Tactic/CrossRefAttribute.lean` (modified) imports the two new modules, removes the now-duplicated `Database` / `databaseURL` / `databaseLabel` definitions, and calls `Widget.savePanelWidgetInfo` in each attribute's `add` handler. Tag storage, docstring rewriting, and the trace commands are untouched. If `curl` is missing or the upstream site is unreachable, the widget renders an inline error instead of blocking the LSP. The existing `MathlibTest/CrossRefAttribute.lean` suite continues to pass — none of the behaviour visible to it changes. Stacked on leanprover-community#39662 (scripts only). A third follow-up will add a GitHub Actions workflow that posts a once-per-PR comment with tag / signature / snippet tables. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Add `scripts/crossref.lean`, a single standalone tool to support review of PRs that add `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]` attributes. It exposes two subcommands: * `lake env lean --run scripts/crossref.lean snippet <db> <tag>...` fetches a one-line label/description for each tag from the upstream database. Wikidata uses the `wbgetentities` API (with recovery when one bad QID poisons a batch); Stacks and Kerodon use the documented Gerby `/data/tag/<TAG>/content/statement` endpoint with a tolerant HTML→text strip that survives `<` inside math. Exit codes distinguish all-resolved (0) from missing (2) from transient network failure (3). When `CROSSREF_CACHE_DIR` is set, responses are memoised per `(database, tag)` so repeat lookups are instant. * `lake env lean --run scripts/crossref.lean extract --file <path>...` (or `--diff <range>`) walks Lean source and emits TSV of every cross-reference attribute it finds, paired with the declaration it decorates. A byte-level scanner correctly skips string literals and line/block comments, handles multi-attribute blocks (`@[simp, stacks 01AB]`), multi-line attribute blocks, doc comments between attribute and declaration, and modifier keywords (`private`, `noncomputable`, …). Signatures are collapsed to one line for downstream consumption. The two subcommands share a single `Database` enum, with a roundtrip theorem `Database.ofString?_name` proving `name ∘ ofString?` is a section — so adding a fourth database fails to compile until both projections are updated together. The script imports only Lean core (plus `Std.Data.HashMap` for batching), so it can be invoked directly with `lake env lean --run` without any Mathlib build, and a future CI workflow can drive it on untrusted PR files without elaborating PR code. Companion follow-ups (separate PRs) will add an LSP widget that surfaces these snippets in the editor and a GitHub Actions workflow that posts a once-per-PR comment with tag / signature / snippet tables and fails CI on unresolved tags. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

When a Mathlib declaration carries `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]`, the info view now shows the upstream label / description when the cursor sits on the attribute. The fetch is on-demand via an RPC call from the widget to the Lean server, which shells out to `curl`; we deliberately don't fetch at attribute-elaboration time so offline builds stay clean and the only network access is when an editing session opens the panel. Two new modules and a small refactor to the existing one: * `Mathlib/Tactic/CrossRef/Fetch.lean` (new) holds the `Database` enum and the snippet-fetch logic. The companion `scripts/crossref-snippet.lean` in the previous PR reimplements the same logic standalone for CI usage; the two are kept in sync deliberately so the CI script doesn't need a Mathlib build. * `Mathlib/Tactic/Widget/CrossRefHover.lean` (new) defines the widget itself: an `RpcEncodable` props record, a `RequestM` RPC method that calls `fetchSnippet`, and a `mk_rpc_widget%` Component that renders the result as Html. * `Mathlib/Tactic/CrossRefAttribute.lean` (modified) imports the two new modules, removes the now-duplicated `Database` / `databaseURL` / `databaseLabel` definitions, and calls `Widget.savePanelWidgetInfo` in each attribute's `add` handler. Tag storage, docstring rewriting, and the trace commands are untouched. If `curl` is missing or the upstream site is unreachable, the widget renders an inline error instead of blocking the LSP. The existing `MathlibTest/CrossRefAttribute.lean` suite continues to pass — none of the behaviour visible to it changes. Stacked on leanprover-community#39662 (scripts only). A third follow-up will add a GitHub Actions workflow that posts a once-per-PR comment with tag / signature / snippet tables. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

faenuccio · 2026-05-26T04:30:58Z

+  `Mathlib/Tactic/CrossRefAttribute.lean`;
+- the `pretty` dict in `mathlib-ci`'s `scripts/crossref_review/crossref-pr-comment.py`.
+
+Within this file, the `ofString?_name` roundtrip theorem catches drift between


Why do you want this comment on this line (it is also repeated below, close to the theorem)?

faenuccio · 2026-05-26T04:31:21Z

+  `(database, tag)` so repeat lookups are instant.
+
+* `extract` walks a `.lean` file (or the added lines of a git diff range) and
+  emits TSV of every cross-reference attribute it finds, paired with the


can you expand out the abbreviation TSV?

TSV = tab-separated-value

faenuccio · 2026-05-26T04:41:28Z

+/-! ### Finding the declaration that follows an attribute block -/
+
+/-- Lean declaration kinds we care about. -/
+def declKeywords : List String :=


There was discussion about having more examples allowed in Mathlib; wouldn't you allow them? And what about axiom (in particular, what would you imagine the wikipedia entry for the Axiom of Choice to point to in Mathlib)? I see that you treat it as a modifier keywords but I don't understand why. Finally, I would also add inductive, no?

faenuccio · 2026-05-26T04:47:09Z

  top-level command (including preceding attributes and doc comments). It is copied to
  cloned repos at runtime and executed via `lake env lean --run`.

+**Cross-reference tag review**


Can you add a couple of examples? It would perhaps help to add in the PR description, and/or here, the intended use of the tool.

Suggested change

**Cross-reference tag review**

**Tooling for cross-reference tags**

faenuccio · 2026-05-26T04:58:14Z

+/-!
+# Cross-reference tag tooling
+
+A single standalone script supporting review of PRs that add `@[stacks ...]`,


Can you say something about how this tool is meant to support a review? In other words, when/why should a reviewer be encouraged to use it?

jcommelin · 2026-05-26T09:37:11Z

  top-level command (including preceding attributes and doc comments). It is copied to
  cloned repos at runtime and executed via `lake env lean --run`.

+**Cross-reference tag review**


Suggested change

**Cross-reference tag review**

**Tooling for cross-reference tags**

jcommelin · 2026-05-26T09:38:52Z

+/-- Replace any tab, newline, or carriage return with a single space and collapse
+runs of whitespace. The TSV output is one record per line, so we have to keep
+each field on one line; markdown-table escaping is a downstream concern. -/
+def flattenWhitespace (s : String) : String :=
+  let go : Char → (String × Bool) → (String × Bool) := fun c (acc, prevSpace) =>
+    let isWs := c == ' ' || c == '\t' || c == '\n' || c == '\r'
+    if isWs then
+      if prevSpace || acc.isEmpty then (acc, true)
+      else (acc.push ' ', true)
+    else
+      (acc.push c, false)
+  let (out, _) := s.toList.foldl (fun st c => go c st) ("", false)
+  out.trimAscii.toString


Can we not reuse something from core for this?

jcommelin · 2026-05-26T09:41:14Z

+/-- Best-effort HTML→text: drop everything from `<x` (where `x` is a letter,
+`/`, or `!`) up to and including the matching `>`, decode a handful of
+entities, collapse whitespace. The first-character check matters because
+the Stacks/Kerodon snippets embed LaTeX math like `0 < 1`, and a dumber


Are we sure they always have a space after <? Or is x<y going to cause troubles?

Do we even need a stripHtml function? Or can we just embed the html wherever this snippet is rendered (infoview / review pages)?

kim-em · 2026-05-27T08:21:41Z

Closing in favour of the much smaller #39876, which adds only scripts/dump_crossref_tags.lean (~80 LOC).

Following maintainer discussion, the bulk of this PR (the standalone snippet / extract subcommands, ~960 LOC) now lives in https://github.com/leanprover-community/external-tags. The mathlib4 side only needs to expose tagExt data to that downstream tool.

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

This was referenced May 21, 2026

feat(CrossRefAttribute): info-view widget for cross-reference tags #39664

Closed

feat(ci): cross-reference tag review via post-build lint + workflow_run #39666

Closed

kim-em force-pushed the crossref-tooling-scripts branch from 4ba4247 to 61c1da0 Compare May 21, 2026 18:59

kim-em mentioned this pull request May 22, 2026

refactor(crossref_review): consume TSV from mathlib4's post-build lint leanprover-community/mathlib-ci#39

Closed

kim-em marked this pull request as ready for review May 22, 2026 08:32

kim-em force-pushed the crossref-tooling-scripts branch from 61c1da0 to 49036a9 Compare May 22, 2026 09:56

kim-em force-pushed the crossref-tooling-scripts branch from 49036a9 to e676811 Compare May 22, 2026 09:59

kim-em force-pushed the crossref-tooling-scripts branch from e676811 to 4bc6411 Compare May 22, 2026 10:04

kim-em force-pushed the crossref-tooling-scripts branch from 4bc6411 to bb78642 Compare May 22, 2026 10:13

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026

faenuccio reviewed May 26, 2026

View reviewed changes

jcommelin reviewed May 26, 2026

View reviewed changes

kim-em mentioned this pull request May 26, 2026

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

Open

kim-em closed this May 27, 2026

	Cross-reference tag review
	Tooling for cross-reference tags

Uh oh!

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary bb78642748

Import changes for modified files

Declarations diff

⚠️ Scripts folder reminder

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kim-em commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

kim-em commented May 21, 2026 •

edited

Loading

github-actions Bot commented May 21, 2026 •

edited

Loading