From 9c649584c411bfd008abeb59c9e869bbafaa33c2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Tue, 24 Feb 2026 12:14:58 +0100
Subject: [PATCH] ci: gate PR manual preview on user guide changes

Reduce noise only for pull requests by restricting PR preview deploys/comments to changes under doc/UsersGuide/.

This keeps production deployment behavior unchanged:
- pushes/merges to main still always deploy the manual

Implementation details:
- keep first-party actions/github-script check in ci.yml (with inline supply-chain rationale) for PR changed-files detection
- upload `html-manual-for-deploy` only when UsersGuide files changed
- in pr-deploy.yml, remove duplicated path-check logic and gate deploy/comment directly on whether that artifact exists (`found_artifact`)

Small downside: PRs that only change Verso rendering internals will not get preview deployment/comments.
---
 .github/workflows/ci.yml        | 29 ++++++++++++++++++++++++++++-
 .github/workflows/pr-deploy.yml |  4 ++++
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 686c994d..cf48642a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -233,8 +233,35 @@ jobs:
                   set -e
                   echo "message=$(git log -1 --pretty=format:"%s")" >> "$GITHUB_OUTPUT"
 
-            - name: Upload HTML manual for PR deployment
+            # We intentionally avoid third-party path-filter actions here to reduce
+            # CI supply-chain exposure; this uses only first-party GitHub actions.
+            - id: user-guide-changes
+              name: Check for user guide changes
               if: github.event_name == 'pull_request'
+              uses: actions/github-script@v8
+              with:
+                  github-token: ${{ secrets.GITHUB_TOKEN }}
+                  script: |
+                      const pull_number = context.payload.pull_request.number;
+                      const files = await github.paginate(
+                        github.rest.pulls.listFiles,
+                        {
+                          owner: context.repo.owner,
+                          repo: context.repo.repo,
+                          pull_number,
+                          per_page: 100,
+                        },
+                        (response) => response.data ?? []
+                      );
+                      const changed = files.some((file) =>
+                        file.filename.startsWith('doc/UsersGuide/')
+                      );
+                      core.setOutput('changed', changed ? 'true' : 'false');
+
+            - name: Upload HTML manual for PR deployment
+              if:
+                  github.event_name == 'pull_request' && steps.user-guide-changes.outputs.changed ==
+                  'true'
               uses: actions/upload-artifact@v6
               with:
                   name: html-manual-for-deploy
diff --git a/.github/workflows/pr-deploy.yml b/.github/workflows/pr-deploy.yml
index 912f0511..0a7f46a8 100644
--- a/.github/workflows/pr-deploy.yml
+++ b/.github/workflows/pr-deploy.yml
@@ -26,15 +26,18 @@ jobs:
                   sourceRunId: ${{ github.event.workflow_run.id }}
 
             - name: Download HTML manual artifact
+              id: manual-artifact
               uses: dawidd6/action-download-artifact@v15
               with:
                   run_id: ${{ github.event.workflow_run.id }}
                   name: html-manual-for-deploy
                   path: html-manual
                   allow_forks: true
+                  if_no_artifact_found: ignore
 
             - name: Deploy to Netlify
               id: netlify
+              if: steps.manual-artifact.outputs.found_artifact == 'true'
               uses: nwtgck/actions-netlify@v3.0
               with:
                   publish-dir: html-manual
@@ -54,6 +57,7 @@ jobs:
                   NETLIFY_SITE_ID: "8a89abd8-095b-4496-a9c1-381d2d5629ec"
 
             - name: Post deployment comment on PR
+              if: steps.manual-artifact.outputs.found_artifact == 'true'
               uses: marocchino/sticky-pull-request-comment@v2
               with:
                   number: ${{ steps.pr-info.outputs.pullRequestNumber }}