Skip to content

[Merged by Bors] - style: add nonterminal simp checker#7496

Closed
BoltonBailey wants to merge 18 commits intomasterfrom
BoltonBailey/nonterminal-simp-linter
Closed

[Merged by Bors] - style: add nonterminal simp checker#7496
BoltonBailey wants to merge 18 commits intomasterfrom
BoltonBailey/nonterminal-simp-linter

Conversation

@BoltonBailey
Copy link
Copy Markdown
Collaborator

@BoltonBailey BoltonBailey commented Oct 4, 2023 •
edited
Loading

Adds a linter that detects calls to simp where the next line is at the same indentation level.

Open in Gitpod

@BoltonBailey
Copy link
Copy Markdown
Collaborator Author

BoltonBailey commented Oct 4, 2023

I am noticing some examples of

simp
rfl

Is this supposed to be ok?

This was referenced Oct 4, 2023
Closed
Open
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 4, 2023
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Oct 4, 2023

Hmm, I thought you would write this in lean. Doing it in text seems brittle.

@BoltonBailey
Copy link
Copy Markdown
Collaborator Author

BoltonBailey commented Oct 5, 2023

Hmm, I thought you would write this in lean. Doing it in text seems brittle.

I guess you mean you thought I would write it in Lean rather than Python?

Seems like all the current infrastructure for writing linters centers on lint-style.py though. Presumably there is some Lean tool for parsing lean ASTs that could be useful, but I am not familiar with it. Perhaps the maintainers should consider whether they want to accept further changes to this file or instead get someone to rewrite it all in Lean. I'm happy to close this PR if it's the latter.

bors bot pushed a commit that referenced this pull request Oct 5, 2023
@BoltonBailey
chore: fix nonterminal simps (#7497)
19ca95b 
Fixes the nonterminal simps identified by #7496
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 5, 2023
adomani
adomani reviewed Oct 8, 2023
View reviewed changes
@BoltonBailey BoltonBailey added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Oct 8, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 10, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 19, 2023
@BoltonBailey BoltonBailey added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Oct 20, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 20, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 16, 2023

This PR/issue depends on:

@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 7, 2024
@jcommelin jcommelin requested a review from digama0 February 13, 2024 10:23
@BoltonBailey
Copy link
Copy Markdown
Collaborator Author

BoltonBailey commented Feb 14, 2024

Noticing now this _eq_3, which I think was previously disliked, so I'm removing that.

@digama0
Copy link
Copy Markdown
Member

digama0 commented Mar 2, 2024

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 2, 2024
@BoltonBailey @digama0
style: add nonterminal simp checker (#7496)
8b3f3f3 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 2, 2024

Build failed:

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Mar 2, 2024

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 2, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 2, 2024
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Mar 2, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 2, 2024
@BoltonBailey @digama0
style: add nonterminal simp checker (#7496)
8426743 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title style: add nonterminal simp checker [Merged by Bors] - style: add nonterminal simp checker Mar 2, 2024
@mathlib-bors mathlib-bors bot closed this Mar 2, 2024
@mathlib-bors mathlib-bors bot deleted the BoltonBailey/nonterminal-simp-linter branch March 2, 2024 22:40
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@BoltonBailey @digama0 @kbuzzard
style: add nonterminal simp checker (#7496)
17ef202 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@BoltonBailey @digama0 @dagurtomas
style: add nonterminal simp checker (#7496)
39c7182 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@BoltonBailey @digama0 @utensil
style: add nonterminal simp checker (#7496)
ab48160 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@BoltonBailey @digama0 @xgenereux
style: add nonterminal simp checker (#7496)
8d533f9 
Adds a linter that detects calls to `simp` where the next line is at the same indentation level.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@adomani adomani adomani left review comments

@digama0 digama0 Awaiting requested review from digama0

Assignees

@digama0 digama0

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@BoltonBailey @Ruben-VandeVelde @digama0 @fpvandoorn @adomani