chore: rerun CI only when full-ci label is added or removed

[nomeata]

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.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-05-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-05-11 14:16:50)