CI: run `pr.yml` when changed

[johnyf]

Changes

• run the CI configuration of file pr.yml when pushing a collection of commits that change the file pr.yml
• run monthly the CI configuration of file pr.yml

An alternative is to run when pushing to a specific branch, for example to a branch named test_pr_yml:

on:
    pull_request:
    push:
        branches: test_pr_yml

(possibly followed by a cron schedule:).

No branches filter is specified, because GitHub Actions conjoin the constraints defined by the filters branches and and paths. Since the diff is computed using the base of the pushed commits, any change to the file pr.yml within the range of pushed commits will trigger a test run for the file pr.yml. So changes to pr.yml cannot escape CI testing.

Using a paths filter is automatic, so does not require remembering to push to a branch with a specific name.

Motivation

Before opening a pull request that changed the file .github/workflows/pr.yml, I made an error: the prefix env. was missing from the line:

https://github.com/tlaplus/tlapm/blob/ea92944b1f00748e12a071da7b94ad93e23a0528/.github/workflows/pr.yml#L38

This error in YAML raised an error on GitHub Actions, and the CI tests failed before starting to run.

GitHub Actions checks the YAML files that are to be run. If there is a syntax error in YAML files under the directory .github/workflows/, whether the error is found without GitHub Actions running the workflow defined in that YAML file might depend on the kind of syntax error:

• a syntax error that results in ungrammatical YAML, would prevent GitHub Actions from parsing the YAML file, and so from deciding whether to run the file's workflow or not, and

• a syntax error that is YAML, but is a semantic error for GitHub Actions (as was the missing env. mentioned above), might be detected only when the workflow defined by that YAML file is run.

It seems that the second case was what happened.

[johnyf]

Thank you for reviewing and approving the changes, I rebased and merged this pull request.