Skip to content

ci: gate PR manual preview on user guide changes#765

Open
ejgallego wants to merge 1 commit intoleanprover:mainfrom
ejgallego:feat/ci-userguide-deploy
Open

ci: gate PR manual preview on user guide changes#765
ejgallego wants to merge 1 commit intoleanprover:mainfrom
ejgallego:feat/ci-userguide-deploy

Conversation

@ejgallego
Copy link
Contributor

@ejgallego ejgallego commented Feb 24, 2026

Summary

  • reduce noise only for PR previews: deploy/comment preview only when doc/UsersGuide/** changed
  • keep production deploy unchanged: pushes/merges to main still always deploy the manual
  • remove duplicated PR file-check logic by making pr-deploy.yml artifact-driven

Implementation

  • in ci.yml, use first-party actions/github-script (with inline supply-chain rationale) to detect UsersGuide changes on PRs
  • only upload html-manual-for-deploy when that predicate is true
  • in pr-deploy.yml, always attempt artifact download with if_no_artifact_found: ignore, and gate deploy/comment on steps.manual-artifact.outputs.found_artifact == 'true'

Tradeoff

  • small downside: PRs that only change Verso rendering internals will not get preview deployment/comments
  • this is acceptable IMO for PR preview noise reduction

@github-actions
Copy link
Contributor

Preview for this PR is ready! 🎉

@ejgallego ejgallego force-pushed the feat/ci-userguide-deploy branch from 5419f04 to 63827a0 Compare February 24, 2026 11:34
@ejgallego ejgallego changed the title ci: deploy manual only when user guide changes ci: deploy manual only for user guide changes Feb 24, 2026
@ejgallego ejgallego force-pushed the feat/ci-userguide-deploy branch from 63827a0 to a257ccb Compare February 24, 2026 11:37
@ejgallego ejgallego changed the title ci: deploy manual only for user guide changes ci: gate PR manual preview on user guide changes Feb 24, 2026
@ejgallego ejgallego removed the request for review from david-christiansen February 24, 2026 11:40
@ejgallego ejgallego marked this pull request as draft February 24, 2026 11:40
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.
@ejgallego ejgallego force-pushed the feat/ci-userguide-deploy branch from a257ccb to 9c64958 Compare February 24, 2026 11:42
@ejgallego ejgallego marked this pull request as ready for review February 24, 2026 11:55
@david-christiansen
Copy link
Collaborator

This would have made it more difficult to review the dark mode PR (#641), for example.

What's the major benefit here? How do the comments hurt anything?

@ejgallego
Copy link
Contributor Author

This would have made it more difficult to review the dark mode PR (#641), for example.

I agree.

What's the major benefit here? How do the comments hurt anything?

The main source of noise is that I now get a comment notification for all PRs in the GitHub web interface due to the bot.

Unfortunately there seems no way to filter those.

@david-christiansen
Copy link
Collaborator

What if we rejigger the CI so that it creates a deployment instead of posting a comment? If we can do that, then it may solve the issue.

@ejgallego
Copy link
Contributor Author

What if we rejigger the CI so that it creates a deployment instead of posting a comment? If we can do that, then it may solve the issue.

I didn't know about GH deployment, that seems a great idea, thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants