Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
kim-em wants to merge 1 commit into
base: master
Choose a base branch
from
+971 −0
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions scripts/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading