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

@@ -45,7 +45,7 @@ open Lean
 
 /-- The three supported cross-reference databases.
 
-When adding a new case, also update each of these (none are exhaustiveness-checked):
+When adding a new case, also update each of these:
 - `Database.ofString?`, `Database.name`, `Database.fetch`, `gerbyBase?` below;
 - the `databases` list in `scripts/extract-crossref-tags.lean`;
 - the `Mathlib.CrossRef.Database` enum in `Mathlib/Tactic/CrossRefAttribute.lean`