feat(CI): bench-after-CI (#21414)

Adds a CI step that checks if the `bench-after-CI` label is present.  If so, it adds a comment `!bench` once CI passes, triggering a benchmarking run.

The management is as follow:
* the label `bench-after-CI` is applied manually while CI is running;
* once CI passes the lint phase, if the label is present, a bot comments `!bench`, starting the bench process;
* when the bench process terminates, it posts the report;
* this triggers the bench-summary bot to post the summary *and* to remove the label.

Meanwhile, the label `bench-after-CI` is in the list of labels that `bors` rejects.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60bench-after-CI.60.3F)

I added the label to this PR, ~~but I am not sure whether the workflow will act on it, since the code is not in `master`~~ and the automation worked.

.github/build.in.yml

@@ -339,6 +339,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/bench_summary_comment.yml

@@ -33,3 +33,11 @@ jobs:
         env:
           PR:  ${{ github.event.issue.number }}
           GH_TOKEN: ${{secrets.GITHUB_TOKEN}}
+
+      - name: Remove "bench-after-CI"
+        # we use curl rather than octokit/request-action so that the job won't fail
+        # (and send an annoying email) if the labels don't exist
+        run: |
+          curl --request DELETE \
+            --url https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/labels/bench-after-CI \
+            --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}'

.github/workflows/bors.yml

@@ -349,6 +349,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build.yml

@@ -356,6 +356,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

.github/workflows/build_fork.yml

@@ -353,6 +353,15 @@ jobs:
           # Only return if PR is still open
           filterOutClosed: true
 
+      - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI')
+        name: If `bench-after-CI` is present, add a `!bench` comment.
+        uses: GrantBirki/comment@v2
+        with:
+          token: ${{ secrets.AUTO_MERGE_TOKEN }}
+          issue-number: ${{ steps.PR.outputs.number }}
+          body: |
+            !bench
+
       - id: remove_labels
         name: Remove "awaiting-CI"
         # we use curl rather than octokit/request-action so that the job won't fail

bors.toml

@@ -1,7 +1,7 @@
 status = ["Build", "Lint style"]
 use_squash_merge = true
 timeout_sec = 28800
-block_labels = ["WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI"]
+block_labels = ["WIP", "blocked-by-other-PR", "merge-conflict", "awaiting-CI", "bench-after-CI"]
 delete_merged_branches = true
 update_base_for_deletes = true
 cut_body_after = "---"