refactor(crossref_review): consume TSV from mathlib4's post-build lint#39

Open

kim-em wants to merge 36 commits into

leanprover-community:masterfrom

kim-em:crossref-review

Commits on May 22, 2026

Move nightly-docgen.yml, nightly-regression-report.yml to this repository

marcelolynch
authored and
kim-em
committed
Incorporate changes from Anne's PR

marcelolynch
authored and
kim-em
committed
step

marcelolynch
authored and
kim-em
committed
step

marcelolynch
authored and
kim-em
committed
step

marcelolynch
authored and
kim-em
committed
change api key variable

marcelolynch
authored and
kim-em
committed
fix: Fix quoting in env variables

marcelolynch
authored and
kim-em
committed
Correct email

marcelolynch
authored and
kim-em
committed
feat: fast GitHub App token minting via Azure Key Vault signing (#6)

marcelolynch
authored and
kim-em
committed
feat: Add action to mint Azure Storage token (#3)

marcelolynch
authored and
kim-em
committed
fix: Set pipefail in scripts that pipe builds to tee (#12)

marcelolynch
authored and
kim-em
committed
fix: handle Zulip rate limits in emoji reactions script (#8)

kim-em
and
claude
committed
fix: handle missing nightly-testing branch in merge script (#14)

kim-em
and
claude
committed
fix: report full backward.* option names in tech debt metrics (#15)

kim-em
and
claude
committed
fix: `declarations_diff.sh` can't handle `public` modifier (#16)

Komyyy
authored and
kim-em
committed
fix: configure nightly-testing remote in merge script (#18)
kim-em
committed
chore: drop info message counts from Zulip build report (#19)
kim-em
committed
fix: look up existing lean-pr-testing comments under the current bot identity (#20)
kim-em
committed
docs: actionable instructions for running tech debt script locally (#22)

kim-em
and
claude
committed
fix(verify_commits.sh): replay auto commits in isolated worktrees, surface errors in PR comment (#26)

authored and
kim-em
committed
feat(olean_diff.py): script for comparing oleans (#24)

bryangingechen
authored and
kim-em
committed
feat: report number of `@[expose]`d public sections as tech debt (#25)

Vierkantor
authored and
kim-em
committed
fix local run instructions (#27)

justus-springer
authored and
kim-em
committed
feat: make printing info optional for zulip_build_report.sh (#23)

chenson2018
authored and
kim-em
committed
feat: add tech debt counter for disabled varHead simp warnings (#21)

kim-em
and
claude
committed
fix: require all CI outcomes to succeed before adding `builds-mathlib` (#29)

kim-em
and
claude
committed
feat: classify tech debt into weak and strong (#28)

Vierkantor
authored and
kim-em
committed
chore: temporarily mark disabled deprecation lints as weak tech debt (#31)

Vierkantor
authored and
kim-em
committed
fix: surface curl HTTP errors in lean-pr-testing-comments.sh (#32)

kim-em
and
claude
committed
chore: route Zulip notifications to nightly-testing-mathlib (#33)
kim-em
committed
fix: tolerate 404 in `remove_label` in lean-pr-testing-comments.sh (#34)

committed
fix: filter tech debt rows by level using a literal pipe (#36)

committed
chore: use `git switch --detach` when checking out a commit hash (#35)

Vierkantor
authored and
kim-em
committed
feat: orchestrator for the mathlib4 cross-reference tag review bot

kim-em
and
claude
committed
refactor(crossref_review): consume TSV from mathlib4's post-build lint step

kim-em
and
claude
committed
fix(crossref_review): harden Markdown escaping for PR-author input

kim-em
and
claude
committed