ci: add !downstream-check PR-validation workflow#39339
Draft
marcelolynch wants to merge 3 commits into
Draft
Conversation
Adds a comment-triggered workflow that lets maintainers validate a
mathlib4 PR against curated downstream Lean projects. A user comments
!downstream-check FLT, Toric --merge-branch, carleson@v1.2.3
on a PR and the workflow:
* gates the commenter on `author_association ∈ {OWNER, MEMBER,
COLLABORATOR}` (same risk-tier convention as other mathlib4 comment-
triggered workflows of this kind),
* calls `scripts/pr_check_downstream/validate_names.sh` from mathlib-ci
to parse the grammar + resolve the PR's merge ref,
* mints an App token and dispatches the heavy build workflow
`mathlib-pr-validation.yml` in
`leanprover-community/downstream-reports`,
* posts an ack comment on the PR.
Grammar (each comma-separated entry):
<name-or-slug>[@<rev>] [--merge-branch]
* `<name-or-slug>` — inventory short name (e.g. `FLT`) or GitHub
`owner/repo` slug. Resolved by the dispatched workflow.
* `@<rev>` — optional. Any git refspec for the downstream's checkout.
* `--merge-branch` — optional, per entry. Flips that entry from the
default LKG mode (cherry-pick PR onto the downstream's last-known-
good mathlib) to merge mode (build against the PR's merge tree).
The dispatched workflow does the actual `git clone` / `lake build`
work on `leanprover-community/downstream-reports`'s self-hosted
runner pool (no CI secrets in scope), and posts one consolidated
result comment back to the PR — verdict table + per-entry sections
covering pass / fail / infra-failure variants with master-health
framing when the snapshot records a current regression.
Companion changes:
* `leanprover-community/mathlib-ci` — the `validate_names.sh` and
`post_ack_comment.sh` scripts this workflow invokes (separate PR).
* `leanprover-community/downstream-reports` — the dispatched
`mathlib-pr-validation.yml` workflow + builders + comment renderer
(separate PR).
PR summary 4f58c4548cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
Bot
added
the
CI
mathlib-ci@bfc0f6f replaces the bash scripts with two composite Python actions; switch this workflow's `Validate downstream entries` and `Post ack comment` steps to use them directly via `uses: leanprover-community/mathlib-ci/.github/actions/...`. Two structural simplifications fall out of the migration: * The intermediate `Checkout local actions` (sparse-checkout for `get-mathlib-ci`) and `Get mathlib-ci` (set up `$CI_SCRIPTS_DIR`) steps are gone — we no longer source bash scripts. * The `Parse comment` step drops its empty-`rest` guard; the validate action handles empty input and POSTs a user-facing usage hint to the PR. Grammar errors now show up as a comment on the triggering PR (directly addressing the author), so a typo or unknown flag is diagnosed inline rather than burying the error in the workflow log. Runtime errors (unknown downstream, build failures, etc.) continue to come from the dispatched `downstream-reports` workflow on its own — the two repos stay decoupled, no inventory crosstalk needed here. The composite-action refs are pinned to mathlib-ci's feature branch (`marcelo/2026/05/DownstreamPrValidation`) for now; the follow-up once mathlib-ci merges is to pin to a commit SHA on master.
Match the established mathlib4 convention for consuming mathlib-ci actions: check out mathlib-ci once via `get-mathlib-ci` (the canonical SHA pin, auto-bumped by `update_dependencies.yml`), then reference the composite actions as `./ci-tools/.github/actions/...` local paths. Three direct-ref `uses:` lines collapse: * `leanprover-community/mathlib-ci/.github/actions/check-downstream-validate@<feature-branch>` → `./ci-tools/.github/actions/check-downstream-validate` * `leanprover-community/mathlib-ci/.github/actions/azure-create-github-app-token@3bb576...` → `./ci-tools/.github/actions/azure-create-github-app-token` * `leanprover-community/mathlib-ci/.github/actions/check-downstream-ack@<feature-branch>` → `./ci-tools/.github/actions/check-downstream-ack` Net effect: one place owns the mathlib-ci ref; bumping it touches a single line in `get-mathlib-ci/action.yml` instead of three `uses:` clauses across this workflow. Matches how other mathlib4 workflows consume mathlib-ci's scripts via `$CI_SCRIPTS_DIR`. Two new steps front the run: * Sparse-checkout mathlib4's `.github/actions/` (just enough to run `get-mathlib-ci`). * Run `get-mathlib-ci`, which checks out mathlib-ci at the canonical pinned SHA to `ci-tools/`. Merge ordering: this PR's workflow expects the check-downstream composite actions to be present in mathlib-ci at the SHA pinned by `get-mathlib-ci/action.yml`. When the corresponding mathlib-ci PR merges, `update_dependencies.yml` will auto-bump that pin; until then, smoke testing happens via `ci_dev.yml` (which has its own `mathlib_ci_ref` input for pointing at the feature branch).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a comment-triggered workflow that lets maintainers validate a mathlib4 PR against curated downstream Lean projects. A user comments
on a PR and the workflow:
author_association ∈ {OWNER, MEMBER, COLLABORATOR}scripts/pr_check_downstream/validate_names.shfrom mathlib-ci to parse the grammar + resolve the PR's merge refmathlib-pr-validation.ymlinleanprover-community/downstream-reports,Grammar (each comma-separated entry):
[@] [--merge-branch]
<name-or-slug>— inventory short name (e.g.FLT) or GitHubowner/reposlug. Resolved by the dispatched workflow.@<rev>— optional. Any git refspec for the downstream's checkout.--merge-branch— optional, per entry. Flips that entry from the default LKG mode (cherry-pick PR onto the downstream's last-known- good mathlib) to merge mode (build against the PR's merge tree).The dispatched workflow does the actual
git clone/lake buildwork onleanprover-community/downstream-reports's self-hosted runner pool (no CI secrets in scope), and posts one consolidated result comment back to the PR.Companion changes:
!downstream-checkPR-validation directive mathlib-ci#37 — thevalidate_names.shandpost_ack_comment.shscripts this workflow invokes (separate PR).