ci: use sticky-pull-request-comment for updating PR comment (#35160)

Replace custom PR comment update logic with `marocchino/sticky-pull-request-comment` for consistency across workflows

Author: marcelolynch

.github/workflows/label_new_contributor.yml

@@ -24,12 +24,14 @@ jobs:
       contents: read
     steps:
       - name: Label PR and report count
+        id: contributor-check
         uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v8.0.0
         with:
           script: |
             const MIN_MERGED = 5;
             const creator = context.payload.sender.login;
             const { owner, repo } = context.repo;
+            core.setOutput('should_welcome', 'false');
 
             console.log(`Checking closed issues for user: ${creator}`);
 
@@ -77,47 +79,7 @@ jobs:
                 repo,
                 labels: ['new-contributor']
               });
-
-              // Check if we already posted a welcome comment (idempotency)
-              const WELCOME_MARKER = '<!-- mathlib-welcome-comment -->';
-              let alreadyWelcomed = false;
-              for await (const response of github.paginate.iterator(
-                github.rest.issues.listComments,
-                {
-                  issue_number: context.issue.number,
-                  owner,
-                  repo,
-                  per_page: 100,
-                }
-              )) {
-                if (response.data.some(c => c.body.includes(WELCOME_MARKER))) {
-                  alreadyWelcomed = true;
-                  break;
-                }
-              }
-
-              if (!alreadyWelcomed) {
-                console.log('Posting welcome comment for new contributor...');
-                const body = [
-                  WELCOME_MARKER,
-                  '## Welcome new contributor!',
-                  'Thank you for contributing to Mathlib! If you haven\'t done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).',
-                  '',
-                  'We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn\'t have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr).',
-                  '',
-                  'If you haven\'t already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR.',
-                  '',
-                  'Thank you again for joining our community.',
-                ].join('\n');
-                await github.rest.issues.createComment({
-                  issue_number: context.issue.number,
-                  owner,
-                  repo,
-                  body,
-                });
-              } else {
-                console.log('Welcome comment already exists, skipping.');
-              }
+              core.setOutput('should_welcome', 'true');
             }
 
             console.log('Creating check run with a message about the PR count by this author...');
@@ -134,3 +96,18 @@ jobs:
                 summary: message,
               },
             });
+
+      - name: Post welcome comment for new contributor
+        if: steps.contributor-check.outputs.should_welcome == 'true'
+        uses: marocchino/sticky-pull-request-comment@773744901bac0e8cbb5a0dc842800d45e9b2b405 # v2.9.4
+        with:
+          header: 'New Contributor Welcome'
+          message: |
+            ## Welcome new contributor!
+            Thank you for contributing to Mathlib! If you haven't done so already, please review our [contribution guidelines](https://leanprover-community.github.io/contribute/index.html), as well as the [style guide](https://leanprover-community.github.io/contribute/style.html) and [naming conventions](https://leanprover-community.github.io/contribute/naming.html).
+
+            We use a [review queue](https://leanprover-community.github.io/queueboard/review_dashboard.html) to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the `awaiting-author` tag, or another reason described in the [Lifecycle of a PR](https://leanprover-community.github.io/contribute/index.html#lifecycle-of-a-pr).
+
+            If you haven't already done so, please come to [https://leanprover.zulipchat.com/](https://leanprover.zulipchat.com/), introduce yourself, and mention your new PR.
+
+            Thank you again for joining our community.