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:

  1. Tag your PR with awaiting-CI (otherwise the !bench will start executing immediately)
  2. Send a !bench/!radar command

Estimated changes