Commit 2026-07-04 02:49 c093ecaf

feat(scripts): export wikidata/stacks/kerodon cross-references as JSON (#40701) This PR adds scripts/export_crossrefs.lean, which exports every declaration tagged with @[wikidata], @[stacks], or @[kerodon] (name, file, line, ids) as JSON, and a CI workflow that runs it after each successful master build and publishes the result to https://github.com/leanprover-community/crossref-exports. The CI workflow can also be triggered manually using workflow_dispatch. The credentials are provided by a new GitHub app "crossref-exports-app" under the leanprover-community organization with secrets set up in the "crossref-exports" repo environment.