feat(CrossRefAttribute): info-view widget for cross-reference tags by kim-em · Pull Request #39664 · leanprover-community/mathlib4

kim-em · 2026-05-21T17:20:25Z

This PR teaches the info view to show the upstream label and description when the cursor sits on a @[stacks ...], @[kerodon ...], or @[wikidata ...] attribute. The fetch is on-demand via an RPC call from the widget to the Lean server, which shells out to curl; we deliberately do not 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 stacked 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, and the existing MathlibTest/CrossRefAttribute.lean suite continues to pass — none of the behaviour visible to it changes.

If curl is missing or the upstream site is unreachable, the widget renders an inline error instead of blocking the LSP.

depends on: feat(scripts): add cross-reference tag tooling #39662

🤖 Prepared with Claude Code

github-actions · 2026-05-21T17:21:47Z

PR summary a457ef6d92

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Tactic`	2
`Mathlib.Tactic.CrossRef.Fetch` (new file)	54

Declarations diff

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

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

mathlib-dependent-issues · 2026-05-21T17:33:14Z

This PR/issue depends on:

feat(scripts): add cross-reference tag tooling #39662
By Dependent Issues (🤖). Happy coding!

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>

eric-wieser · 2026-05-22T01:47:21Z

+private def fetchUrl (url : String) : IO (Nat × String) := do
+  let output ← IO.Process.output {
+    cmd := "curl"
+    args := #["-sSL", "--max-time", "10", "-A", userAgent,
+              "-w", "\n%{http_code}", url]
+  }
+  if output.exitCode != 0 then return (0, "")


Can we use Std.Http here instead? Or do the query javacsript-side?

Std.Http is not yet production ready.

Why would querying javascript-side be better than curl?

I guess I don't remember if we can rely on every lean installation having curl on the path.

eric-wieser · 2026-05-22T01:51:24Z

+/-- Best-effort HTML→text. We treat `<x…>` as a tag only when `x` is a letter,
+`/`, or `!`, so a literal `<` inside LaTeX (`0 < 1`) is preserved. -/
+private def stripHtml (html : String) : String :=
+  let chars := html.toList
+  let rec go : List Char → Bool → String → String
+    | [], _, acc => acc
+    | '<' :: rest, false, acc =>
+      match rest with
+      | c :: _ =>
+        if c.isAlpha || c == '/' || c == '!' then go rest true acc
+        else go rest false (acc.push '<')
+      | [] => acc.push '<'
+    | '>' :: rest, true, acc => go rest false acc
+    | _ :: rest, true,  acc => go rest true  acc
+    | c :: rest, false, acc => go rest false (acc.push c)
+  let raw := go chars false ""
+  let decoded := raw
+    |>.replace "&nbsp;" " "
+    |>.replace "&amp;" "&"
+    |>.replace "&lt;" "<"
+    |>.replace "&gt;" ">"
+    |>.replace "&quot;" "\""
+    |>.replace "&#39;" "'"
+  flattenWhitespace decoded


Why are we doing this when the infoview can display HTML?

Trying this out now.

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. Trusted-script execution pattern (same as `PR_summary.yml`): * The PR head is checked out into `pr-branch/` and used as DATA only — no code from it ever runs in this `pull_request_target` context. * The base ref is checked out into `base/`; its `scripts/extract-crossref-tags.lean` and `scripts/crossref-snippet.lean` are the trusted versions we actually invoke, and its `lean-toolchain` is what `lake env lean --run` picks up. * `mathlib-ci` is checked out via the shared `get-mathlib-ci` action; its `scripts/crossref_review/crossref-pr-comment.py` orchestrator (added in leanprover-community/mathlib-ci#39) drives the extract → snippet → format pipeline. * The resulting comment file is piped through `scripts/pr_summary/update_PR_comment.sh` for post-once / update-in-place behaviour. A startup gate exits cleanly when the base ref pre-dates the companion Lean scripts (e.g. against an older master), so the workflow doesn't fail spuriously. `docs/workflows.md` gains a new entry; `scripts/README.md` points at the mathlib-ci location for the orchestrator. Stacked on leanprover-community#39664 (LSP widget) and depends on the orchestrator landing in leanprover-community/mathlib-ci#39. 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>

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. Trusted-script execution pattern (same as `PR_summary.yml`): * The PR head is checked out into `pr-branch/` and used as DATA only — no code from it ever runs in this `pull_request_target` context. * The base ref is checked out into `base/`; its `scripts/extract-crossref-tags.lean` and `scripts/crossref-snippet.lean` are the trusted versions we actually invoke, and its `lean-toolchain` is what `lake env lean --run` picks up. * `mathlib-ci` is checked out via the shared `get-mathlib-ci` action; its `scripts/crossref_review/crossref-pr-comment.py` orchestrator (added in leanprover-community/mathlib-ci#39) drives the extract → snippet → format pipeline. * The resulting comment file is piped through `scripts/pr_summary/update_PR_comment.sh` for post-once / update-in-place behaviour. A startup gate exits cleanly when the base ref pre-dates the companion Lean scripts (e.g. against an older master), so the workflow doesn't fail spuriously. `docs/workflows.md` gains a new entry; `scripts/README.md` points at the mathlib-ci location for the orchestrator. Stacked on leanprover-community#39664 (LSP widget) and depends on the orchestrator landing in leanprover-community/mathlib-ci#39. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Split out a `Snippet` structure for the success payload and a `SnippetError` inductive for failures, then define `SnippetOutcome := Except SnippetError (Option Snippet)`. `.ok none` now represents an authoritatively missing tag, freeing us to use `Except` machinery on fetches. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Replaces splitOn "\n" + intercalate with two dropRightWhile passes over the trailing bytes. Same behavior, single scan over the tail. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

In response to leanprover-community#39664 (comment), collapse `Snippet` to a single `html : String` field and let the widget inject it via React's `dangerouslySetInnerHTML`. Stacks/Kerodon `<article>` elements now retain their structure — paragraphs, italics, and (after relative-`href` rewriting) clickable in-statement links to other tags. Wikidata snippets are HTML-escaped and wrapped in `<strong>` for the label. Drops the bespoke `stripHtml` / `parseGerbyTitle` helpers (~60 lines). We trust the three upstream sources and don't sanitize the markup. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

Closing — the info-view widget feature is dropped from this iteration to minimise mathlib4 review surface.

The snippet-fetching code from Mathlib/Tactic/CrossRef/Fetch.lean has been lifted into https://github.com/leanprover-community/external-tags and is used by the CI orchestrator. The auto-display info-view widget can be re-added later if there's interest, likely as an opt-in Lake package.

The existing Mathlib/Tactic/CrossRefAttribute.lean in master is unchanged.

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 21, 2026

kim-em mentioned this pull request May 21, 2026

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

Closed

2 tasks

kim-em force-pushed the crossref-tooling-widget branch from d0f86f7 to 63fd5cc Compare May 21, 2026 19:30

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Tactic/CrossRef/Fetch.lean Outdated

eric-wieser reviewed May 22, 2026

View reviewed changes

Comment thread Mathlib/Tactic/CrossRef/Fetch.lean Outdated

eric-wieser reviewed May 22, 2026

View reviewed changes

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

kim-em mentioned this pull request May 22, 2026

feat(scripts): add cross-reference tag tooling #39662

Closed

kim-em force-pushed the crossref-tooling-widget branch from 63fd5cc to 939db59 Compare May 22, 2026 09:57

kim-em force-pushed the crossref-tooling-widget branch from 939db59 to 3f0d35a Compare May 22, 2026 10:01

kim-em force-pushed the crossref-tooling-widget branch from 3f0d35a to 10ae9fe Compare May 22, 2026 10:05

kim-em and others added 2 commits May 22, 2026 10:13

kim-em force-pushed the crossref-tooling-widget branch from 10ae9fe to 157091c Compare May 22, 2026 10:16

kim-em and others added 3 commits May 22, 2026 10:19

refactor(CrossRef/Fetch): peel curl status off without split/rejoin

b2e4bda

Replaces splitOn "\n" + intercalate with two dropRightWhile passes over the trailing bytes. Same behavior, single scan over the tail. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

kim-em closed this May 27, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

feat(CrossRefAttribute): info-view widget for cross-reference tags#39664
kim-em wants to merge 5 commits into
leanprover-community:masterfrom
kim-em:crossref-tooling-widget

kim-em commented May 21, 2026

Uh oh!

github-actions Bot commented May 21, 2026 •

edited

Loading

Declarations diff

⚠️ Scripts folder reminder

Uh oh!

mathlib-dependent-issues Bot commented May 21, 2026

Uh oh!

eric-wieser May 22, 2026

Uh oh!

jcommelin May 22, 2026

Uh oh!

eric-wieser May 22, 2026

Uh oh!

Uh oh!

Uh oh!

eric-wieser May 22, 2026

Uh oh!

kim-em May 22, 2026

Uh oh!

kim-em commented May 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

kim-em commented May 21, 2026

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 a457ef6d92

Import changes for modified files

Declarations diff

⚠️ Scripts folder reminder

Uh oh!

mathlib-dependent-issues Bot commented May 21, 2026

Uh oh!

eric-wieser May 22, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin May 22, 2026

Choose a reason for hiding this comment

Uh oh!

eric-wieser May 22, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

eric-wieser May 22, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em May 22, 2026

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

github-actions Bot commented May 21, 2026 •

edited

Loading