mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
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>