Since we are using it in the other jobs, we may as well use it here. As a
bonus, it will make the job work even if the target of the pull request
isn't the main branch.
Most of the time, we are not committing changes to the tools. Move the
unit tests for the lint and generation tools to a separate PR workflow,
that is only run if anything in the tools/ folder is modified in the PR.
This saves time in the normal case.
This runs faster and allows for future improvements.
Similar to the linter workflow, we remove the Circle-CI-specific stuff
from the file in tools/scripts/, and into .github/workflows/.
We use another external action (tj-actions/verify-changed-files) to check
that generating the tests didn't create any new changes. This is basically
a companion action to the tj-actions/changed-files used in the linter job.
This should help contributors notice and fix linter errors when they
occur. Apparently it's as easy as printing a magic string to stdout, who
knew!
The lint tool doesn't give line numbers so we place the annotations at
line 1 for the time being.
After the previous commit, it doesn't do much, only passes the linting
exceptions file on the command line. Instead, make the lint.exceptions
file the default for that argument (if it exists), and remove the shell
script.
This runs faster and allows for future improvements.
I'm following a general principle of keeping code that isn't portable
between CI providers inside the config file for the CI provider. So in
this case we remove the Circle-CI-specific stuff from the file in
tools/scripts/, and into .github/workflows/. We use an external action
(tj-actions/changed-files) to gather the list of files to lint.