Commit 2025-09-15 13:59 35ebe148

View on Github →

feat(CI): nightly-testing regression report (#29506) This PR adds a workflow that builds the nightly-testing-green branch with extra linting options enabled, and reports the results on Zulip. We currently can use this to catch places where grind doesn't solve goals that linarith/omega/ring can solve. Example output to Zulip:

Mathlib's nightly-testing branch (0f4ee783b5dac29751bce6be710a445e89159a69) regression run completed. Warnings: 283

| | Warning description | |

Estimated changes

Created .github/workflows/nightly-regression-report.yml

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

modified def grindReplacementWith

modified def linarithToGrind

modified def omegaToGrind

modified def ringToGrind

Created scripts/zulip_build_report.sh