[Merged by Bors] - feat: the multiGoal linter#12339
[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.
…ommunity/mathlib4 into adomani/lint_multiple_goals
adomani
left a comment
There was a problem hiding this comment.
Michael, thank you very much for the comment! I think that this is (finally) ready again for review!
Mathlib/Tactic/Linter/Multigoal.lean
Outdated
| |>.insert ``Lean.Parser.Tactic.case' | ||
| |>.insert `«tactic#adaptation_note_» | ||
|
|
||
| /-- these are `SyntaxNodeKind`s that block the linter. -/ |
There was a problem hiding this comment.
I added a longer explanation.
grunweg
left a comment
There was a problem hiding this comment.
Thank you for the changes (and sorry that I didn't find time to propose something myself). In particular, the new error message seems much clearer to me! I have some more comments on the comments. I think that is close to all I have to comment on this PR.
| ] | ||
|
|
||
| /-- 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 :-)
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
…ommunity/mathlib4 into adomani/lint_multiple_goals
adomani
left a comment
There was a problem hiding this comment.
Michael, thank you for all your reviewing effort!
| ] | ||
|
|
||
| /-- 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"...
|
bors d+ |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Bors merge |
|
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: |
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.