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

Closed
kim-em wants to merge 1 commit into from
+971 −0
Closed

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

@faenuccio faenuccio May 26, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add a couple of examples? It would perhaps help to add in the PR description, and/or here, the intended use of the tool.

@jcommelin jcommelin May 26, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
**Cross-reference tag review**
**Tooling for cross-reference tags**

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