Commit 2026-03-02 16:30 812c2d66

View on Github →

ci: Decouple workflow scripts into the mathlib-ci repository (#35823) This PR migrates CI workflows to run trusted automation scripts from leanprover-community/mathlib-ci instead of using scripts from this repository. The goal is to decouple script evolution from mathlib4 workflow files.

  • Workflows using scripts check out leanprover-community/mathlib-ci and call a composite action at that exports both checkout_path and scripts_dir as env variables (CI_CHECKOUT_PATH, CI_SCRIPTS_DIR by default).
  • Updates affected workflows to use that action and call scripts from ${CI_SCRIPTS_DIR} across pr_summary, reporting, maintainer, nightly, verification, and zulip.
  • Includes a workflow to try to prevent broken references to scripts by scanning usages and cross referencing with the contents of the repository
  • Updates docs Prepared with Codex

Estimated changes