feat: add SHA-suffixed PR release tags (#8702)

This PR enhances the PR release workflow to create both short format and
SHA-suffixed release tags. Creates both pr-release-{PR_NUMBER} and
pr-release-{PR_NUMBER}-{SHORT_SHA} tags, generates separate releases for
both formats, adds separate GitHub status checks, and updates
Batteries/Mathlib testing branches to use SHA-suffixed tags for exact
commit traceability.

This removes the need for downstream repositories to deal with the
toolchain changing without the toolchain name changing.

Author: kim-em

.github/workflows/pr-release.yml

@@ -48,17 +48,28 @@ jobs:
           git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
           git -C lean4.git fetch -n origin master
           git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          
+          # Create both the original tag and the SHA-suffixed tag
+          SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          SHORT_SHA="${SHORT_SHA:0:7}"
+          
+          # Export the short SHA for use in subsequent steps
+          echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
+
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
+          
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
       - name: Delete existing release if present
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          # Try to delete any existing release for the current PR.
+          # Try to delete any existing release for the current PR (just the version without the SHA suffix).
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-      - name: Release
+      - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: softprops/action-gh-release@v2
         with:
@@ -73,7 +84,22 @@ jobs:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
-      - name: Report release status
+      - name: Release (SHA-suffixed format)
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: softprops/action-gh-release@v2
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
+        env:
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+
+      - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
         with:
@@ -87,6 +113,20 @@ jobs:
               description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
             });
 
+      - name: Report release status (SHA-suffixed format)
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/github-script@v7
+        with:
+          script: |
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR toolchain (SHA-suffixed)",
+              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
+            });
+
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
@@ -282,16 +322,18 @@ jobs:
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, pushing an empty commit."
+            echo "Branch already exists, updating lean-toolchain."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
-            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
+            git add lean-toolchain
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -346,21 +388,23 @@ jobs:
           if [ "$EXISTS" = "0" ]; then
             echo "Branch does not exist, creating it."
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
-            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
             lake update batteries
             git add lakefile.lean lake-manifest.json
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
-            echo "Branch already exists, merging $BASE and bumping Batteries."
+            echo "Branch already exists, updating lean-toolchain and bumping Batteries."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
             # The Mathlib `nightly-testing` branch or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
+            echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
+            git add lean-toolchain
             lake update batteries
             git add lake-manifest.json
-            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes