fix: nightly revision date logic and mathlib trigger auth#12463
Merged
fix: nightly revision date logic and mathlib trigger auth#12463
Conversation
This PR fixes two issues with the nightly release workflow:
1. The `workflow_dispatch` path used `date -u +%F` (current UTC date) to compute the
base nightly name, but a manual re-release should revise the *most recent* nightly,
not today's date. Now finds the latest `nightly-*` tag and creates a revision of that.
2. The mathlib4 nightly-testing trigger was broken:
- Workflow renamed: `nightly_bump_toolchain.yml` → `nightly_bump_and_merge.yml`
- `MATHLIB4_BOT` PAT expired after mathlib migrated to GitHub Apps
- Replace with `actions/create-github-app-token` using the `mathlib-nightly-testing`
app (requires `MATHLIB_NIGHTLY_TESTING_APP_ID` and
`MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY` secrets to be configured)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
kim-em
force-pushed
the
nightly-rev-followup
branch
from
da5d067 to
be097c5
Compare
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
1 participant
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.
This PR fixes two issues discovered during the first test of the revised nightly release workflow (#12461):
1. Date logic: The
workflow_dispatchpath useddate -u +%F(current UTC date) to find the base nightly to revise. If the most recent nightly was from yesterday (e.g.nightly-2026-02-12) but UTC has rolled over to Feb 13, the code would look fornightly-2026-02-13, not find it, and create a fresh nightly instead of a revision. Now finds the latestnightly-*tag viasort -rVand creates a revision of that.2. Mathlib trigger: The "Update toolchain on mathlib4's nightly-testing branch" step was broken in two ways:
nightly_bump_toolchain.yml→nightly_bump_and_merge.yml([Merged by Bors] - chore(CI): combine nightly bump and pr-testing merge workflows leanprover-community/mathlib4#34827)MATHLIB4_BOTPAT expired after mathlib migrated to GitHub Apps ([Merged by Bors] - chore: migrate nightly-testing workflows to GitHub App leanprover-community/mathlib4#34751)actions/create-github-app-tokenusing themathlib-nightly-testingapp, matching the pattern used in mathlib4's own workflows.🤖 Prepared with Claude Code