From f47bb6194cade92c6e2456f80cd7939b055dd929 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 26 May 2026 14:39:56 +0000 Subject: [PATCH 1/4] feat(scripts): dump cross-reference tags to TSV for downstream review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 #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 --- scripts/dump_crossref_tags.lean | 84 +++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 scripts/dump_crossref_tags.lean diff --git a/scripts/dump_crossref_tags.lean b/scripts/dump_crossref_tags.lean new file mode 100644 index 00000000000000..66c1edc41cba8c --- /dev/null +++ b/scripts/dump_crossref_tags.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Lean +import Mathlib.Tactic.CrossRefAttribute + +/-! +# Dump every cross-reference tag in Mathlib to TSV + +```sh +lake env lean --run scripts/dump_crossref_tags.lean +``` + +Loads the elaborated Mathlib environment, walks `Mathlib.CrossRef.tagExt`, +and writes one TSV record per tag: + +``` +\t\t\t\t +``` + +This is the only piece of cross-reference review machinery that has to live +in mathlib4: the rest (snippet fetching, filtering by PR diff, Markdown +rendering, comment posting) is in `leanprover-community/external-tags` +and `leanprover-community/mathlib-ci`. The TSV emitted here is treated as +untrusted data by the privileged workflow_run consumer. + +Implementation: we use `importModules (loadExts := true)` rather than the +`withImportModules` wrapper, because the latter passes `loadExts := false` +and would leave `tagExt` empty for imported modules. + +Safety: fields are normalised (tabs / newlines in comments become single +spaces) and the whole file is capped at `maxBytes` to bound what a malicious +PR could emit. +-/ + +open Lean Mathlib.CrossRef + +/-- Hard cap on the output. The current population is ~55 KB (539 tags); we +allow ~50× headroom and refuse to emit anything larger. -/ +def maxBytes : Nat := 2 * 1024 * 1024 + +/-- Replace tabs, newlines, and carriage returns with single spaces so a +field can't break the TSV framing. -/ +def sanitiseField (s : String) : String := + s.replace "\t" " " |>.replace "\r\n" " " |>.replace "\n" " " |>.replace "\r" " " + +/-- Convert a module name like `` `Mathlib.Algebra.Foo `` to its source path +(e.g. `"Mathlib/Algebra/Foo.lean"`). -/ +def moduleToFilePath (m : Name) : String := + m.toString.replace "." "/" ++ ".lean" + +unsafe def run (outPath : System.FilePath) : IO UInt32 := do + initSearchPath (← findSysroot) + enableInitializersExecution + let env ← importModules (loadExts := true) #[`Mathlib] {} 1024 + let tagsPair : List Tag × Array (Array Tag) := + PersistentEnvExtension.getState tagExt env + let allTags := tagsPair.2.flatten.appendList tagsPair.1 + let mut rows : Array String := #[] + for tag in allTags do + let some mod := env.getModuleFor? tag.declName | continue + let file := moduleToFilePath mod + let dbName : String := match tag.database with + | .kerodon => "kerodon" + | .stacks => "stacks" + | .wikidata => "wikidata" + rows := rows.push s!"{dbName}\t{sanitiseField tag.tag}\t{tag.declName}\t\ + {sanitiseField file}\t{sanitiseField tag.comment}" + let body := String.intercalate "\n" rows.toList ++ if rows.isEmpty then "" else "\n" + if body.utf8ByteSize > maxBytes then + throw <| .userError s!"dump exceeds {maxBytes} bytes (got {body.utf8ByteSize})" + IO.FS.writeFile outPath body + IO.eprintln s!"Wrote {rows.size} cross-reference tag(s) to {outPath} \ + ({body.utf8ByteSize} bytes)." + return 0 + +unsafe def main (args : List String) : IO UInt32 := do + match args with + | [out] => run out + | _ => + IO.eprintln "Usage: lake env lean --run scripts/dump_crossref_tags.lean " + return 64 From e265200e4a9adf3400ed95f04eaa53b2b24b93cb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 27 May 2026 08:28:13 +0000 Subject: [PATCH 2/4] doc(scripts): document dump_crossref_tags.lean in scripts/README.md 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 --- scripts/README.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/scripts/README.md b/scripts/README.md index 1757c86e82e9d1..510d6247eb4d67 100644 --- a/scripts/README.md +++ b/scripts/README.md @@ -210,6 +210,14 @@ to module `Foo.Bar` (no `srcDir` indirection). you can convert `pick abc # x scripts/auto_commit.sh cmd` to `x scripts/auto_commit.sh cmd` (by deleting the "pick abc # " prefix), and git will re-run the command via exec. Example: `scripts/auto_commit.sh lake exe mk_all` +- `dump_crossref_tags.lean` walks `Mathlib.CrossRef.tagExt` in a fully built Mathlib environment + and writes one TSV row per `@[stacks ...]` / `@[kerodon ...]` / `@[wikidata ...]` tag with + columns `(database, tag, declName, module, comment)`. Used by the `cross-reference review` + workflow_run job (`.github/workflows/crossref_review.yml`) to hand off to the orchestrator in + [leanprover-community/external-tags](https://github.com/leanprover-community/external-tags). + The output is capped at 2 MB and TSV fields are sanitised so user-controlled comments cannot + break the framing. + Usage: `lake env lean --run scripts/dump_crossref_tags.lean `. - `parse_shake_output.py` parses the captured output of `lake shake` and reports the number of files changed and imports added/removed. Used by the `shake` workflow to populate the PR body and Zulip notification. Counts are printed to stdout and, if a second argument is given From 94072722f8129a50ba73cae096810016781fdcba Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 27 May 2026 10:13:05 +0000 Subject: [PATCH 3/4] doc(scripts): correct dump_crossref_tags safety claim + tag count MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- scripts/dump_crossref_tags.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/scripts/dump_crossref_tags.lean b/scripts/dump_crossref_tags.lean index 66c1edc41cba8c..4666a4420b9276 100644 --- a/scripts/dump_crossref_tags.lean +++ b/scripts/dump_crossref_tags.lean @@ -30,15 +30,18 @@ Implementation: we use `importModules (loadExts := true)` rather than the `withImportModules` wrapper, because the latter passes `loadExts := false` and would leave `tagExt` empty for imported modules. -Safety: fields are normalised (tabs / newlines in comments become single -spaces) and the whole file is capped at `maxBytes` to bound what a malicious -PR could emit. +Hygiene: fields are normalised (tabs / newlines in comments become single +spaces) so they can't break the TSV framing, and the whole file is capped +at `maxBytes`. This script lives in `scripts/` and runs with the PR's +permissions, so the cap is defence-in-depth — the trusted consumer +(mathlib-ci's `post-comment.sh`) enforces its own cap on the artifact +before parsing. -/ open Lean Mathlib.CrossRef -/-- Hard cap on the output. The current population is ~55 KB (539 tags); we -allow ~50× headroom and refuse to emit anything larger. -/ +/-- Hard cap on the output. The current population is ~55 KB (491 tags); +2 MB is ample headroom. -/ def maxBytes : Nat := 2 * 1024 * 1024 /-- Replace tabs, newlines, and carriage returns with single spaces so a From 15ba169deded5da4291411bf805a81152f456ced Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 27 May 2026 14:10:31 +0000 Subject: [PATCH 4/4] fix(scripts): sanitise tag.declName too in dump_crossref_tags MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- scripts/dump_crossref_tags.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/dump_crossref_tags.lean b/scripts/dump_crossref_tags.lean index 4666a4420b9276..cefb5a00d6edc3 100644 --- a/scripts/dump_crossref_tags.lean +++ b/scripts/dump_crossref_tags.lean @@ -69,7 +69,8 @@ unsafe def run (outPath : System.FilePath) : IO UInt32 := do | .kerodon => "kerodon" | .stacks => "stacks" | .wikidata => "wikidata" - rows := rows.push s!"{dbName}\t{sanitiseField tag.tag}\t{tag.declName}\t\ + rows := rows.push s!"{dbName}\t{sanitiseField tag.tag}\t\ + {sanitiseField tag.declName.toString}\t\ {sanitiseField file}\t{sanitiseField tag.comment}" let body := String.intercalate "\n" rows.toList ++ if rows.isEmpty then "" else "\n" if body.utf8ByteSize > maxBytes then