[Merged by Bors] - feat(ci): Emit error messages in a way understood by github #5726
Conversation
eric-wieser
force-pushed
the
github-matchers
branch
from
ef7d180
to
f4ff376
Compare
eric-wieser
changed the title
eric-wieser
added
awaiting-review
There was a problem hiding this comment.
Very neat!
Note that detect_errors.py is used in a few other projects: e.g. https://github.com/leanprover-community/azure-scripts/blob/master/.github/workflows/nolints.yml and https://github.com/leanprover-community/lean-web-editor/blob/master/.github/workflows/build.yml
Do you happen to know how GitHub will treat build errors in those projects?
No, but I'd be surprised if it does something different to what is happening in this one. It's probably a good thing I didn't use the separate problem-matcher json file, as it wouldn't have found that. |
This one is a different file with the same name. |
🤦 Ah, my bad. |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
OK, let's try it out. Thanks! |
github-actions
bot
added
ready-to-merge
This uses the commands described [here](https://github.com/actions/toolkit/blob/master/docs/commands.md#log-level), for which [the implementation](https://github.com/actions/toolkit/blob/af821474235d3c5e1f49cee7c6cf636abb0874c4/packages/core/src/command.ts#L36-L94) provides a slightly clearer spec. This means github now annotates broken lines, and highlights the error in red. Originally I tried to implement this using "problem matchers", but these do not support multi-line error messages. Supporting this in the linter is something that I'll leave for a follow-up PR. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
|
Looks like this even works when the error is in a file not changed in the PR:
|
This uses the commands described [here](https://github.com/actions/toolkit/blob/master/docs/commands.md#log-level), for which [the implementation](https://github.com/actions/toolkit/blob/af821474235d3c5e1f49cee7c6cf636abb0874c4/packages/core/src/command.ts#L36-L94) provides a slightly clearer spec. This means github now annotates broken lines, and highlights the error in red. Originally I tried to implement this using "problem matchers", but these do not support multi-line error messages. Supporting this in the linter is something that I'll leave for a follow-up PR. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
This uses the commands described here, for which the implementation provides a slightly clearer spec.
This means github now annotates broken lines, and highlights the error in red.
Originally I tried to implement this using "problem matchers", but these do not support multi-line error messages.
Supporting this in the linter is something that I'll leave for a follow-up PR.
Click the "files changed" tab to see the automated failure comment added by github.
The "checks tab" shows
The downside is that the plaintext output no longer shows filename / line numbers: