fix: nightly revision date logic and mathlib trigger auth (#12463)

This PR fixes two issues discovered during the first test of the revised
nightly release workflow
(#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>

Author: kim-em

.github/workflows/ci.yml

@@ -60,22 +60,20 @@ jobs:
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
-            BASE_NIGHTLY="nightly-$(date -u +%F)"
             if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: find next available revision if base nightly exists
-              if git rev-parse "refs/tags/$BASE_NIGHTLY" >/dev/null 2>&1; then
-                REV=1
-                while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
-              else
-                LEAN_VERSION_STRING="$BASE_NIGHTLY"
-              fi
+              # Manual re-release: create a revision of the most recent nightly
+              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
+              # Strip any existing -revK suffix to get the base date tag
+              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
+              REV=1
+              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
+                REV=$((REV + 1))
+              done
+              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
               # Scheduled: do nothing if commit already has a different tag
-              LEAN_VERSION_STRING="$BASE_NIGHTLY"
+              LEAN_VERSION_STRING="nightly-$(date -u +%F)"
               if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
                 echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
               fi
@@ -513,8 +511,18 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
+      - name: Generate mathlib nightly-testing app token
+        id: mathlib-app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        continue-on-error: true
+        with:
+          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+          owner: leanprover-community
+          repositories: mathlib4-nightly-testing
       - name: Update toolchain on mathlib4's nightly-testing branch
+        if: steps.mathlib-app-token.outcome == 'success'
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_and_merge.yml
         env:
-          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}
+          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}