chore: rerun CI only when full-ci label is added or removed (#4136)

Previously, the CI would run upon every label addition, including things
like `builds-mathlib`
or `will-merge-soon`, possibly triggering a new PR release, new mathlib
builds etc. Very wasteful!

Unfortunately (but not surprisingly) Github does not offer a nice way of
saying
“this workflow depends on that label, please re-run if changed”. Not
enough
functional programmer or nix enthusiasts there, I guess…

So here is the next iteration trying to work with what we have from
Github:

A new workflow watches for (only) `full-ci` label addition or deletion,
and then re-runs
the CI job for the current PR.

Sounds simple? But remember, this is github!

* `github.event.pull_request.labels.*.name` is *not* updated when a job
is re-run.

(This is actually a reasonable step towards determinism, but doesn't
help us
   constructing this work-around.)
   
   Ok, so let’s use the API to fetch the current state of the label.

* There is no good way to say “find the latest run of workflow `"CI"` on
PR `$n`”.

The best approximation seems to search by branch and triggering event.
This can
probably go wrong if there are multiple PRs from different repos with
the same
head ref name (`patch-1` anyone?). Let’s hope that it doesn’t happen too
often.

* You cannot just rerun a workflow. You can only rerun a finished
workflow. So cancel
  it first. And `sleep` a bit…

So let’s see how well this will work. It’s plausibly an improvement.

.github/workflows/ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
   schedule:
     - cron: '0 7 * * *'  # 8AM CET/11PM PT
@@ -41,12 +40,18 @@ jobs:
     steps:
       - name: Run quick CI?
         id: set-quick
-        env:
-          quick: ${{
-            github.event_name == 'pull_request' && !contains( github.event.pull_request.labels.*.name, 'full-ci')
-           }}
+        # We do not use github.event.pull_request.labels.*.name here because
+        # re-running a run does not update that list, and we do want to be able to
+        # rerun the workflow run after settings the `full-ci` label.
         run: |
-          echo "quick=${{env.quick}}" >> "$GITHUB_OUTPUT"
+          if [ "${{ github.event_name }}" == 'pull_request' ]
+          then
+            echo "quick=$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels | any(.name == "full-ci") | not')" >> "$GITHUB_OUTPUT"
+          else
+            echo "quick=false" >> "$GITHUB_OUTPUT"
+          fi
+        env:
+          GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix

.github/workflows/nix-ci.yml

@@ -6,7 +6,6 @@ on:
     tags:
       - '*'
   pull_request:
-    types: [opened, synchronize, reopened, labeled]
   merge_group:
 
 concurrency:

.github/workflows/restart-on-label.yml

@@ -0,0 +1,31 @@
+name: Restart by label
+on:
+  pull_request_target:
+    types:
+      - unlabeled
+      - labeled
+jobs:
+  restart-on-label:
+    runs-on: ubuntu-latest
+    if: contains(github.event.label.name, 'full-ci')
+    steps:
+    - run: |
+        # Finding latest CI workflow run on current pull request
+        # (unfortunately cannot search by PR number, only base branch,
+        # and that is't even unique given PRs from forks, but the risk
+        # of confusion is low and the danger is mild)
+        run_id=$(gh run list -e pull_request -b "$head_ref" --workflow 'CI' --limit 1 \
+          --limit 1 --json databaseId --jq '.[0].databaseId')
+        echo "Run id: ${run_id}"
+        gh run view "$run_id"
+        echo "Cancelling (just in case)"
+        gh run cancel "$run_id" || echo "(failed)"
+        echo "Waiting for 10s"
+        sleep 10
+        echo "Rerunning"
+        gh run rerun "$run_id"
+      shell: bash
+      env:
+        head_ref: ${{ github.head_ref }}
+        GH_TOKEN: ${{ github.token }}
+        GH_REPO: ${{ github.repository }}