[Merged by Bors] - feat: the multiGoal linter #12339
Conversation
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
These `·` are scoping when there is a single active goal. These were found using a modification of the linter at #12339.
adomani
removed
the
awaiting-author
| ] | ||
|
|
||
| /-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from | ||
| their first application until the corresponding proof branch is closed. |
There was a problem hiding this comment.
Thank you; this is much clearer! I'm stumbling a bit over the term "proof branch" - I don't know a better term though. (Do you?)
There was a problem hiding this comment.
Not really: I view proofs as (syntax) "trees" and this is a "branch" of the "tree"...
| -- The warning generated by `linter.style.multiGoal` is not suppressed by `#guard_msgs`, | ||
| -- because the linter is run on `#guard_msgs` itself. This is a known issue, see e.g. | ||
| -- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60 | ||
| -- We jump through an extra hoop here to silence the warning. |
There was a problem hiding this comment.
Let's get this linter in before the Lean bump :-)
grunweg
added
the
awaiting-author
Preparation for #12339.
Co-authored-by: grunweg <[email protected]>
…ommunity/mathlib4 into adomani/lint_multiple_goals
| ] | ||
|
|
||
| /-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from | ||
| their first application until the corresponding proof branch is closed. |
There was a problem hiding this comment.
Not really: I view proofs as (syntax) "trees" and this is a "branch" of the "tree"...
adomani
removed
the
awaiting-author
|
bors d+ |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Bors merge |
A linter that makes sure that, when multiple goals are present, they are enclosed in `·`s. Adaptations (the order is chronological, there should be no dependency among them): * #12338, * #12361, * #12372, * #12560, * #12834, * #12381, * #12908, * #14939, plus many many more that this comment is too small to contain. Co-authored-by: Michael Rothgang <[email protected]>
|
I guess bors is case sensitive? bors merge |
|
Already running a review |
|
Nope, just didn't add the label for some reason. |
|
I had checked that |
|
I had noticed that the commits to master between when this PR was green and when it was approved looked like they would have not introduced some missing I'll test it some other time as well, to see if adding the label is case-sensitive. |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
A linter that makes sure that, when multiple goals are present, they are enclosed in
·s.Adaptations (the order is chronological, there should be no dependency among them):
plus many many more that this comment is too small to contain.