Commit 2025-12-02 19:39 782f6c4c
View on Github →ci: decommission speedcenter (#32358)
Since the speedcenter has been shut down and replaced by https://radar.lean-lang.org/, this PR updates or removes all the speedcenter-related infrastructure I could find in mathlib.
The most significant change is that the bench-after-CI label no longer has any effect. Instead, radar respects the existing awaiting-CI tag for !bench commands. The workflow that replaces bench-after-CI is now:
- Tag your PR with
awaiting-CI(otherwise the!benchwill start executing immediately) - Send a
!bench/!radarcommand