package_core: write PR comment with status

Author: pillo79

.github/workflows/leave_pr_comment.yml

@@ -0,0 +1,60 @@
+# SPDX-License-Identifier: Apache-2.0
+
+name: Leave PR comment
+
+on:
+  workflow_run:
+    workflows: ["Package, test and upload core"]
+    types:
+      - completed
+
+permissions:
+  contents: read
+  pull-requests: write
+
+jobs:
+  comment-on-pr:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Download artifact
+        uses: dawidd6/action-download-artifact@ac66b43f0e6a346234dd65d4d0c8fbb31cb316e5 # v11
+        with:
+          workflow: package-core.yml
+          run_id: ${{ github.event.workflow_run.id }}
+          name: comment-request
+          if_no_artifact_found: ignore
+
+      - name: Load PR number
+        run: |
+          echo "PR_NUM=$(cat pr_number || true)" >> $GITHUB_ENV
+
+      - name: Check PR number
+        id: check-pr
+        uses: carpentries/actions/check-valid-pr@2e20fd5ee53b691e27455ce7ca3b16ea885140e8 # v0.15.0
+        with:
+          pr: ${{ env.PR_NUM }}
+          sha: ${{ github.event.workflow_run.head_sha }}
+
+      - name: Validate PR number
+        if: ${{ steps.check-pr.outputs.VALID != 'true' }}
+        run: |
+          echo "ABORT: PR number validation failed!"
+          exit 1
+
+      - name: Update PR comment
+        if: ${{ steps.check-pr.outputs.VALID == 'true' }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          GH_REPO: ${{ github.repository }}
+        run: |
+          BODY="$(cat comment_body || echo '# :fire: CI failure processing logs!')"
+
+          # delete existing comment, if present, then add a new one
+          gh pr comment ${PR_NUM} --delete-last --yes || true
+          gh pr comment ${PR_NUM} --body "${BODY}"
+
+      - name: Clean up intermediate artifacts
+        if: ${{ steps.check-pr.outputs.VALID == 'true' }}
+        uses: geekyeggo/delete-artifact@v5.1.0
+        with:
+          name: comment-request

.github/workflows/package_core.yml

@@ -320,6 +320,21 @@ jobs:
           cat full_log >> $GITHUB_STEP_SUMMARY
           echo "CI_RESULT=$(cat result)" > $GITHUB_OUTPUT
 
+          if [ "${{ github.event_name }}" == "pull_request" ]; then
+            mkdir -p comment-request
+            echo "${{ github.event.pull_request.number }}" > comment-request/pr_number
+            echo -e "## Built \`$(extra/get_core_version.sh)\`\n" > comment-request/comment_body
+            echo >> comment-request/comment_body
+            cat summary | sed -e 's!\${\\color{\S*}\(.*\)}\$!\1!g' -e 's!\\%!%!g' >> comment-request/comment_body
+          fi
+
+      - name: Archive comment information
+        uses: actions/upload-artifact@v4
+        if: ${{ github.event_name == 'pull_request' }}
+        with:
+          name: comment-request
+          path: comment-request/
+
       - name: Clean up intermediate artifacts
         uses: geekyeggo/delete-artifact@v5.1.0
         with: