ci: update splice-bot, enable splice-bot merge (leanprover-community#36935)

This bumps the version of the SpliceBot ([changes](leanprover-community/SpliceBot@146ee71...a463ae1)) to include support for "label commands" and gives `mathlib-splicebot` the ability to use the `auto-merge-after-CI` label. 

After this is merged, maintainers will be able to type `splice-bot merge` in a pull request review comment and the splicebot will do its thing, and also apply the `auto-merge-after-CI` label, which will cause the PR to be merged if CI passes. Note that this also makes normal usage stricter -- `splice-bot trailing text` will be interpreted as a label command, and will fail.

The `label_command` input is set to a repo variable so that we can adjust it if needed without opening a PR. For now I have added the following in the `SPLICEBOT_LABEL_COMMANDS` variable:
```json
[
  {
    "command": "merge",
    "label": "auto-merge-after-CI",
    "min_repo_permission": "disabled",
    "allowed_teams": ["leanprover-community/mathlib-maintainers"]
  }
]
```

Author: bryangingechen

.github/workflows/build_template.yml

@@ -937,7 +937,8 @@ jobs:
       - if: >- # bot usernames will cause this step to error with "Could not resolve to a User..."
           contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') &&
           steps.get-label-actor.outputs.username != 'mathlib-nolints' &&
-          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies'
+          steps.get-label-actor.outputs.username != 'mathlib-update-dependencies' &&
+          steps.get-label-actor.outputs.username != 'mathlib-splicebot'
         name: check team membership
         uses: tspascoal/get-user-teams-membership@57e9f42acd78f4d0f496b3be4368fc5f62696662 # v3.0.0
         id: actorTeams
@@ -952,6 +953,7 @@ jobs:
           (
             steps.get-label-actor.outputs.username == 'mathlib-nolints' ||
             steps.get-label-actor.outputs.username == 'mathlib-update-dependencies' ||
+            steps.get-label-actor.outputs.username == 'mathlib-splicebot' ||
             contains(steps.actorTeams.outputs.teams, 'mathlib-maintainers') ||
             contains(steps.actorTeams.outputs.teams, 'bot-users')
           )

.github/workflows/splice_bot.yaml

@@ -9,7 +9,7 @@ permissions: {}
 jobs:
   call-splice-bot:
     if: ${{ contains(github.event.comment.body, 'splice-bot') }}
-    uses: leanprover-community/SpliceBot/.github/workflows/splice.yaml@fdb442693d6f613b25d2599ad64fd87cf019b9ce # master
+    uses: leanprover-community/SpliceBot/.github/workflows/splice.yaml@a463ae17022e8eb5929a208c1b136aeebcaf77e1 # master
     with:
       # Optional override; omit to use the reusable workflow's default "master"
       base_ref: master

.github/workflows/splice_bot_wf_run.yaml

@@ -45,15 +45,16 @@ jobs:
           owner: leanprover-community
 
       - name: Run splice bot action
-        uses: leanprover-community/SpliceBot/.github/actions/splice-wf-run@146ee716fab40e9cae384b9932fded8b9999b16d
+        uses: leanprover-community/SpliceBot/.github/actions/splice-wf-run@a463ae17022e8eb5929a208c1b136aeebcaf77e1
         with:
           source_workflow: ${{ github.event.workflow_run.name }}
           push_to_fork: leanprover-community/mathlib4_copy
-          min_repo_permission: 'write'
+          min_repo_permission: 'disabled'
           allow_pr_author: 'true'
           allowed_teams: |
             leanprover-community/mathlib-reviewers
             leanprover-community/mathlib-maintainers
           token: ${{ steps.token.outputs.token }}
           authz_token: ${{ steps.authz-token.outputs.token }}
           branch_token: ${{ steps.branch-token.outputs.token }}
+          label_commands: ${{ vars.SPLICEBOT_LABEL_COMMANDS }}