ci: add SizeComment workflow to post binary size diffs on PRs

New workflow mirroring GnuComment.yml: triggers on workflow_run of
make, downloads the size-comment artifact for the corresponding PR,
and posts the per-binary size comparison as a PR comment when there
is something significant to report.

Author: sylvestre

.github/workflows/SizeComment.yml

@@ -0,0 +1,83 @@
+name: SizeComment
+
+# spell-checker:ignore zizmor backquote
+
+on:
+  workflow_run:
+    workflows: ["make"]
+    types:
+      - completed  # zizmor: ignore[dangerous-triggers]
+
+permissions: {}
+jobs:
+  post-comment:
+    permissions:
+      actions: read  #  to list workflow runs artifacts
+      pull-requests: write  #  to comment on pr
+
+    runs-on: ubuntu-latest
+    if: >
+      github.event.workflow_run.event == 'pull_request'
+    steps:
+      - name: 'Download artifact'
+        uses: actions/github-script@v9
+        with:
+          script: |
+            // List all artifacts from the make workflow run
+            var artifacts = await github.rest.actions.listWorkflowRunArtifacts({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              run_id: ${{ github.event.workflow_run.id }},
+            });
+
+            // Download the "size-comment" artifact, which contains a PR
+            // number (NR) and result.txt produced by compare_size_results.py.
+            var matchArtifact = artifacts.data.artifacts.filter((artifact) => {
+              return artifact.name == "size-comment"
+            })[0];
+            if (!matchArtifact) {
+              core.info("No size-comment artifact found; nothing to post.");
+              return;
+            }
+            var download = await github.rest.actions.downloadArtifact({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              artifact_id: matchArtifact.id,
+              archive_format: 'zip',
+            });
+            var fs = require('fs');
+            fs.writeFileSync('${{ github.workspace }}/size-comment.zip', Buffer.from(download.data));
+      - name: 'Unzip artifact'
+        run: |
+          if [ -f size-comment.zip ]; then
+            unzip size-comment.zip
+          fi
+
+      - name: 'Comment on PR'
+        uses: actions/github-script@v9
+        with:
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          script: |
+            var fs = require('fs');
+            if (!fs.existsSync('./NR') || !fs.existsSync('./result.txt')) {
+              core.info("No size comment payload to post.");
+              return;
+            }
+            var issue_number = Number(fs.readFileSync('./NR'));
+            if (!issue_number) {
+              core.info("No PR number; skipping.");
+              return;
+            }
+            var content = fs.readFileSync('./result.txt');
+            // Only comment when there is something meaningful to say.
+            // compare_size_results.py only writes the file when there is a
+            // significant change, so an empty/short body is treated as
+            // "nothing to report".
+            if (content.toString().trim().length > 0) {
+              await github.rest.issues.createComment({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                issue_number: issue_number,
+                body: 'Binary size comparison:\n```\n' + content + '```'
+              });
+            }