feat(scripts): add cross-reference tag tooling

Add two standalone scripts to support review of PRs that add `@[stacks]`,
`@[kerodon]`, or `@[wikidata]` attributes:

* `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.

Both scripts run via `lake env lean --run` and depend only on Lean core
(plus `curl` on `PATH` for the fetcher), so no Mathlib build is required
and a future CI workflow can drive them 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,20 @@ 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-snippet.lean` fetches a one-line label/description for one or more
+  `@[stacks ...]`, `@[kerodon ...]`, or `@[wikidata ...]` tag identifiers from
+  the upstream database. Used by the cross-reference review CI bot and also
+  callable manually:
+  `lake env lean --run scripts/crossref-snippet.lean wikidata Q42`.
+  Honours `CROSSREF_CACHE_DIR` for offline-friendly repeat lookups.
+- `extract-crossref-tags.lean` walks a `.lean` file (or the added lines of a
+  git diff range) and emits TSV with one row per `@[stacks ...]`,
+  `@[kerodon ...]`, or `@[wikidata ...]` attribute, paired with the
+  declaration it decorates. A byte-level scanner skips strings, comments,
+  and modifier keywords correctly.
+  `lake env lean --run scripts/extract-crossref-tags.lean --file Mathlib/Foo.lean`.
+
 **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