chore: add mathlib4-nightly-available label (#11526)

This PR automatically adds
https://github.com/leanprover/lean4/labels/mathlib4-nightly-available to
a PR if a corresponding branch exists in
https://github.com/leanprover-community/mathlib4-nightly-testing. This
way, the `!bench mathlib` command can delay the benchmark job until
everything is ready.

.github/workflows/pr-release.yml

@@ -127,7 +127,7 @@ jobs:
               description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}",
             });
 
-      - name: Add label
+      - name: Add toolchain-available label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v8
         with:
@@ -515,6 +515,18 @@ jobs:
         run: |
           git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
 
+      - name: Add mathlib4-nightly-available label
+        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/github-script@v8
+        with:
+          script: |
+            await github.rest.issues.addLabels({
+              issue_number: ${{ steps.workflow-info.outputs.pullRequestNumber }},
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              labels: ['mathlib4-nightly-available']
+            })
+
       # We next automatically create a reference manual branch using this toolchain.
       # Reference manual CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously (and thus transitively SubVerso/Verso).