feat: allow addition of release-ci label via comment (#5343)

Updates the PR labeling workflow to allow an external contributor to add
the `release-ci` label to their own PR via comment. This is allows users
on Windows and Intel-based macs to generate toolchains for local
testing. The pull request template is also updated to reflect this.

-----

See Zulip discussion
[here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/No.20binary.20for.20lean.20PR.20testing.20locally).

.github/PULL_REQUEST_TEMPLATE.md

@@ -5,6 +5,7 @@
 * Include the link to your `RFC` or `bug` issue in the description.
 * If the issue does not already have approval from a developer, submit the PR as draft.
 * The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
+* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN` for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing `release-ci` on its own line.
 * If you rebase your PR onto `nightly-with-mathlib` then CI will test Mathlib against your PR.
 * You can manage the `awaiting-review`, `awaiting-author`, and `WIP` labels yourself, by writing a comment containing one of these labels on its own line.
 * Remove this section, up to and including the `---` before submitting.

.github/workflows/labels-from-comments.yml

@@ -1,6 +1,7 @@
-# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, or `WIP` labels,
-# by commenting on the PR or issue.
-# Other labels from this set are removed automatically at the same time.
+# This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
+# or `release-ci` labels by commenting on the PR or issue.
+# If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
+# from that set are removed automatically at the same time.
 
 name: Label PR based on Comment
 
@@ -10,7 +11,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci'))
     runs-on: ubuntu-latest
 
     steps:
@@ -25,6 +26,7 @@ jobs:
           const awaitingReview = commentLines.includes('awaiting-review');
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
+          const releaseCI = commentLines.includes('release-ci');
 
           if (awaitingReview || awaitingAuthor || wip) {
             await github.rest.issues.removeLabel({ owner, repo, issue_number, name: 'awaiting-review' }).catch(() => {});
@@ -41,3 +43,7 @@ jobs:
           if (wip) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['WIP'] });
           }
+
+          if (releaseCI) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
+          }