From eefcbbb37bdc897e66ec1bea5fec98b0aecc4e7f Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 8 Jan 2024 07:44:01 +0100
Subject: [PATCH] chore: pr-release.yaml: indicate information using github
 status (#3137)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When looking at a PR I sometimes wonder which `nightly` release is this
based on, and is used for the mathlib testing.

Right now, the action uses a label (`toolchain-available`) for this, but
a label cannot easily carry more information.

It seems a rather simple way to communicate extra information is by
setting [commit
statuses](https://docs.github.com/en/rest/commits/statuses?apiVersion=2022-11-28#create-a-commit-status);
with this change the following statuses will appear in the PR:


![statusses](https://github.com/leanprover/lean4/assets/148037/e32a24da-065e-406a-adb3-8dca8c0f157f)

One could also use
[checks](https://docs.github.com/en/rest/checks/runs?apiVersion=2022-11-28#create-a-check-run)
to add more information, even with a nicely formatted markdown
description as in [this
example](https://github.com/nomeata/lean4/pull/1/checks?check_run_id=20165137082),
but it seems there you can’t set a summary that’s visible without an
extra click, and Github seems to associate these checks to “the first
workflow”, which is odd. So using statuses seems fine here.

Often one uses bots writing PR comments for this purpose, but that's a
bit noisy (extra notifications etc.), especially for stuff that happens
on every PR, but isn’t always interesting/actionable

If this works well, we can use this for more pieces of information, and
a link can be added as well.
---
 .github/workflows/pr-release.yml | 37 ++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
index bdeb49d192..214dc2aea5 100644
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -6,6 +6,10 @@
 # Instead we use `workflow_run`, which essentially allows us to escalate privileges
 # (but only runs the CI as described in the `master` branch, not in the PR branch).
 
+# The main specification/documentation for this workflow is at
+# https://leanprover-community.github.io/contribute/tags_and_branches.html
+# Keep that in sync!
+
 name: PR release
 
 on:
@@ -69,6 +73,20 @@ jobs:
           # The token used here must have `workflow` privileges.
           GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
+      - name: Report release status
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
+        uses: actions/github-script@v6
+        with:
+          script: |
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR toolchain",
+              description: "${{ github.repository_owner }}/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}",
+            });
+
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: actions/github-script@v7
@@ -172,6 +190,25 @@ jobs:
             echo "mathlib_ready=true" >> $GITHUB_OUTPUT
           fi
 
+      - name: Report mathlib base
+        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }} && steps.ready.outputs.mathlib_ready == 'true'
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const description =
+              process.env.MOST_RECENT_NIGHTLY ?
+              "nightly-" + process.env.MOST_RECENT_NIGHTLY :
+              "not branched off nightly";
+            await github.rest.repos.createCommitStatus({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              sha: "${{ steps.workflow-info.outputs.sourceHeadSha }}",
+              state: "success",
+              context: "PR branched off:",
+              description: description,
+            });
+
+
       # We next automatically create a Mathlib branch using this toolchain.
       # Mathlib CI will be responsible for reporting back success or failure
       # to the PR comments asynchronously.