feat(scripts): add cross-reference tag tooling

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>

Author: kim-em

scripts/README.md

@@ -242,6 +242,18 @@ to module `Foo.Bar` (no `srcDir` indirection).
   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**
+- `crossref.lean` is a single standalone tool for `@[stacks ...]`,
+  `@[kerodon ...]`, and `@[wikidata ...]` attributes. It has 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.
+    Honours `CROSSREF_CACHE_DIR` for offline-friendly repeat lookups.
+  - `lake env lean --run scripts/crossref.lean extract --file <path>...` (or
+    `--diff <range>`) walks the Lean source and emits TSV with one row per
+    cross-reference attribute, paired with the declaration it decorates. A
+    byte-level scanner skips strings, comments, and modifier keywords correctly.
+  Used by the cross-reference review CI bot.
+
 **Managing downstream repos**
 - `downstream_repos.yml` contains basic information about significant downstream repositories.
 - `downstream-tags.py` is a script to check whether a given tag exists on the downstream