[Merged by Bors] - style: a linter for four spaces#7283
[Merged by Bors] - style: a linter for four spaces#7283
Conversation
|
should be rebased once #7286 is merged |
913f1e2 to
8ebf091
Compare
|
after adding |
|
@alexjbest I'm trying to get this to work with reviewdog, but the "lint and suggest" workflow is skipped. Is there a way to make sure it will not be skipped? |
1685757 to
e2c90b9
Compare
|
waiting also for #7321 |
I recently changed it to skip draft prs, is that the reason it is skipping? In which case I'm sure it's fine to make your pr not a draft and mark it WIP instead |
efde12c to
da07667
Compare
Cool, now it is at least running. But it doesn't manage to make suggestions. |
|
That's possibly as reviewdog only makes suggestions on lines changed in your pr? I don't see any lean files changed in this pr so in that case it won't suggest anything |
|
That makes perfect sense! Then everything works as intended here... |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
f96a77a to
799bd72
Compare
Co-authored-by: Johan Commelin <johan@commelin.net>
|
During the time it took for the review of #7328, a few new cases where this new linter triggered where added to mathlib. I added fixed for them here. |
|
LGTM I think this will on average reduce the number of spacing comments people have to leave on PRs, so I'm in favour maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by alexjbest. |
| annotated_lines = list(annotate_comments(lines)) | ||
| for (_, line, is_comment), (next_line_nr, next_line, _) in zip(annotated_lines, | ||
| annotated_lines[1:]): | ||
| # Check if the current line matches "(lemma|theorem) .* :" |
There was a problem hiding this comment.
Should this match instance too?
There was a problem hiding this comment.
Sure, why not. I'm happy to add it either in this pull request or in a separate one....
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
LGTM bors merge |
|
✌️ mo271 can now approve this pull request. To approve and merge a pull request, simply reply with |
Includes an auto-fix feature with the `--fix` flag so that spacing suggestions will be automatically applied in review also. Co-authored-by: Moritz Firsching <firsching@google.com>
| annotated_lines[1:]): | ||
| # Check if the current line matches "(lemma|theorem) .* :" | ||
| new_next_line = next_line | ||
| if (not is_comment) and re.search(r"^(protected )?(def|lemma|theorem) (?!.*:=).*(where)?$", |
There was a problem hiding this comment.
| if (not is_comment) and re.search(r"^(protected )?(def|lemma|theorem) (?!.*:=).*(where)?$", | |
| if (not is_comment) and re.search(r"^(protected )?(def|lemma|theorem|instance) (?!.*:=).*(where)?$", |
There was a problem hiding this comment.
This also presumably won't match @[simp] lemma?
There was a problem hiding this comment.
Indeed, but we could be here all day trying to reproduce the grammar of lean declarations in python.
Like irreducible_def, private, noncomputable, etc. etc.
I don't think there is anything wrong with adding attributes here too, but after a point we really need to either do these things in lean itself (I assume once someone makes one such linter making the rest will be easy), or use something like tree-sitter at least so we aren't reimplementing this all the time.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
|
If anyone is interested I just saw this linter in action #7442, looks like it is working well! |
Includes an auto-fix feature with the
--fixflag so that spacing suggestions will be automatically applied in review also.