ci: add pr comment based on ci result

.github/workflows/ci-comment.yml

@@ -0,0 +1,60 @@
+# Uses `workflow_run` to securely add a comment to the PR that triggered CI.
+#
+# Important: For security, the `workflow_run` trigger runs the workflow from the default branch,
+# so any changes to this workflow must be made in the default branch to take effect.
+#
+# This workflow is neccesary because PRs opened by external forks do not have write access to
+# their PR, so the PR-triggered workflow can't add comments to the PR.
+# If this was in the CI workflow, it'd be tidier and easier to debug but unfortunately that
+# isn't possible due to the lower security context that the CI workflow runs in.
+name: CI comment
+
+on:
+  workflow_run:
+    workflows: ["CI"]
+    types:
+      - completed
+
+jobs:
+  summary:
+    if: github.event.workflow_run.event == 'pull_request'
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Download summaries
+        id: download
+        uses: actions/download-artifact@v4
+        with:
+          run-id: ${{ github.event.workflow_run.id }}
+          pattern: summary-*
+          merge-multiple: true
+          path: summaries
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Debug
+        run: ls -R
+
+      - name: Merge summaries
+        id: summary
+        run: |
+          echo "message<<EOF" >> $GITHUB_OUTPUT
+          for file in summaries/*; do
+            echo $(cat $file) >> $GITHUB_OUTPUT
+          done
+          echo "EOF" >> $GITHUB_OUTPUT
+
+      - name: Set PR comment
+        if: steps.summary.outputs.message
+        uses: marocchino/sticky-pull-request-comment@v2
+        with:
+          number: ${{ github.event.workflow_run.pull_requests[0].number }}
+          header: ${{ github.event.workflow_run.name }}
+          message: ${{ steps.summary.outputs.message }}
+
+      - name: Delete PR comment
+        if: ${{ !steps.summary.outputs.message }}
+        uses: marocchino/sticky-pull-request-comment@v2
+        with:
+          number: ${{ github.event.workflow_run.pull_requests[0].number }}
+          header: ${{ github.event.workflow_run.name }}
+          delete: true

.github/workflows/lint-comment.yml

@@ -1,61 +0,0 @@
-# We use `workflow_run` to securely add a comment to the PR.
-# PRs opened by external forks do not have write access to their PR, so can't add comments.
-name: PR lint comment
-
-on:
-  workflow_run:
-    workflows: ["Lint Clang", "Lint CMake"]
-    types:
-      - completed
-
-jobs:
-  upload:
-    runs-on: ubuntu-latest
-    if: github.event.workflow_run.event == 'pull_request'
-
-    steps:
-      - name: Download artifact
-        if: github.event.workflow_run.conclusion == 'failure'
-        id: download
-        uses: actions/download-artifact@v4
-        with:
-          run-id: ${{ github.event.workflow_run.id }}
-
-      - name: Debug
-        run: ls -R
-
-      - name: Read diff file
-        id: changes
-        run: |
-          file=$(find . -name '*.diff')
-          if [ -z "$file" ]; then
-            echo "No changes detected"
-            exit 0
-          fi
-
-          echo "file=$file" >> $GITHUB_OUTPUT
-          {
-            echo "diff<<EOF"
-            cat $file
-            echo "EOF"
-          } >> $GITHUB_OUTPUT
-
-      - name: PR comment (lint source hint)
-        if: steps.changes.outputs.diff
-        uses: marocchino/sticky-pull-request-comment@v2
-        with:
-          header: ${{ github.event.workflow_run.name }}
-          message: |
-            ❌ Lint failed: It looks like your changes don't match our code style.
-
-            🛠️ Please apply this patch with `git apply`:
-            ```diff
-            ${{ steps.changes.outputs.diff }}
-            ```
-
-      - name: Delete PR comment
-        if: ${{ !steps.changes.outputs.diff }}
-        uses: marocchino/sticky-pull-request-comment@v2
-        with:
-          header: ${{ github.event.workflow_run.name }}
-          delete: true