Validate documentation changes in pull requests

[jugglinmike]

In gh-16822, we re-implemented the website build process to use Sphinx via a GitHub Action. Soon after, we modified the script for use in validating pull requests. By performing all of the work except for final publication, we expected the script to verify that new patches would not introduce problems in the build process.

Contrary to our expectation, GitHub did not execute the script to validate new commits pushed to pull requests. We recognized this problem only after merging a faulty documentation patch.

We should work out how to change our configuration such that pull requests to the documentation are validated along these lines. My initial thought was to create a GitHub Workflow which listens to the pull_request event, but the GitHub documentation recommends use of the push event (which we do):

If you intend to use the pull_request event to trigger CI tests, it's recommended to listen to the push event.

@Hexcles any thoughts on this?

[Hexcles]

That whole paragraph reads quite confusing to me. GitHub sends pull_request events to the base repo for sure, but the push event is not quite clear -- I think it's sent to the fork (where the head branch is), so the push listener in the base repo wouldn't be able to react to. However, that makes the quoted recommendation almost senseless.

Then I discovered this article:

but right now when a pull request is opened from a fork to the upstream, there are a few oddities. The first is that it will only trigger the pull_request event - that makes sense because the associated push isn’t happening on the upstream repo.

which suggests we should also listen to pull_request events, but there's an extra complication:

the tests are run against the master branch, and the status isn’t reflected back to the pull request

The workaround in the article is suboptimal, too, so perhaps the best workaround is to create feature branches here instead of on a fork.

[jugglinmike]

Nice job finding that article. The workaround you suggest sounds good to me. Lets leave this issue open until we can implement something that will work for folks who can't push to this repository.

[jugglinmike]

Resolved via gh-19303.