6ca23a7b8b
This PR fixes two issues discovered during the first test of the revised nightly release workflow (https://github.com/leanprover/lean4/pull/12461): **1. Date logic:** The `workflow_dispatch` path used `date -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 for `nightly-2026-02-13`, not find it, and create a fresh nightly instead of a revision. Now finds the latest `nightly-*` tag via `sort -rV` and creates a revision of that. **2. Mathlib trigger:** The "Update toolchain on mathlib4's nightly-testing branch" step was broken in two ways: - Workflow renamed: `nightly_bump_toolchain.yml` → `nightly_bump_and_merge.yml` (leanprover-community/mathlib4#34827) - `MATHLIB4_BOT` PAT expired after mathlib migrated to GitHub Apps (leanprover-community/mathlib4#34751) - Replace with `actions/create-github-app-token` using the `mathlib-nightly-testing` app, matching the pattern used in mathlib4's own workflows. 🤖 Prepared with Claude Code Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| actionlint.yml | ||
| awaiting-manual.yml | ||
| awaiting-mathlib.yml | ||
| backport.yml | ||
| build-template.yml | ||
| check-prelude.yml | ||
| check-stage0.yml | ||
| check-stdlib-flags.yml | ||
| ci.yml | ||
| copyright-header.yml | ||
| grove.yml | ||
| jira.yml | ||
| labels-from-comments.yml | ||
| pr-body.yml | ||
| pr-release.yml | ||
| pr-title.yml | ||
| restart-on-label.yml | ||
| stale.yml | ||
| update-stage0.yml | ||