test style linters / reviewdog in a clean branch #15934
Conversation
github-actions
bot
added
the
new-contributor
PR summary 065be92098Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
|
@grunweg Here's a test of the style linters in a branch with no changes to the workflow files. As in #15781, the linter errors show up in the logs but are not acted upon by reviewdog (the usual linter step also shows the same errors but doesn't complain either). |
bryangingechen
changed the title
While at it, tweak the formatting of error messages slightly: avoid an extra newline after the Python output, and pluralise errors more correctly.
|
Thanks for the clean reproduction. I found the error, and it is indeed a regression from the rewrite (sorry!). |
While at it, tweak the formatting of error messages slightly: avoid an extra newline after the Python output, and pluralise errors more correctly. Now, we ought to use allUnexpectedError.size for checking: otherwise, we may print about how to fix 0 errors :-)
…nto bgc_test_reviewdog
… into bgc_test_reviewdog
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
| @@ -152,13 +152,13 @@ identity holds. | |||
| -/ | |||
| lemma act_act_self_eq (x y : S) : (x ◃ y) ◃ x = x ◃ y := by | |||
| have h : (x ◃ y) ◃ x = (x ◃ y) ◃ (x ◃ 1) := by rw [act_one] | |||
| rw [h, ← Shelf.self_distrib, act_one] | |||
| rw [h, ←Shelf.self_distrib, act_one] | |||
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| rw [h, ←Shelf.self_distrib, act_one] | |
| rw [h, ← Shelf.self_distrib, act_one] |
|
|
||
| lemma act_idem (x : S) : (x ◃ x) = x := by rw [← act_one x, ← Shelf.self_distrib, act_one] | ||
|
|
||
| lemma act_self_act_eq (x y : S) : x ◃ (x ◃ y) = x ◃ y := by | ||
| have h : x ◃ (x ◃ y) = (x ◃ 1) ◃ (x ◃ y) := by rw [act_one] | ||
| rw [h, ← Shelf.self_distrib, one_act] | ||
| rw [h, ←Shelf.self_distrib, one_act] |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| rw [h, ←Shelf.self_distrib, one_act] | |
| rw [h, ← Shelf.self_distrib, one_act] |
Not to be merged! A cleaner test to demonstrate a possible issue with the linters introduced in #15051 and found here.