Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: the multiGoal linter #12339

Closed
wants to merge 109 commits into from

Conversation

mathlib-bors bot pushed a commit that referenced this pull request Apr 26, 2024
These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
A PR analogous to #12338: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
A PR analogous to #12338 and #12361: reformatting proofs following the multiple goals linter of #12339.
mathlib-bors bot pushed a commit that referenced this pull request May 11, 2024
These `·` are scoping when there is a single active goal.

These were found using a modification of the linter at #12339.
@adomani adomani removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 20, 2024
Copy link
Collaborator

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really: I view proofs as (syntax) "trees" and this is a "branch" of the "tree"...

Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
lakefile.lean Outdated Show resolved Hide resolved
-- 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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's get this linter in before the Lean bump :-)

Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 20, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
Copy link
Collaborator Author

@adomani adomani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Michael, thank you for all your reviewing effort!

Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
]

/-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from
their first application until the corresponding proof branch is closed.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really: I view proofs as (syntax) "trees" and this is a "branch" of the "tree"...

Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Show resolved Hide resolved
Mathlib/Tactic/Linter/Multigoal.lean Outdated Show resolved Hide resolved
lakefile.lean Outdated Show resolved Hide resolved
@adomani adomani removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 21, 2024
@kim-em
Copy link
Contributor

kim-em commented Oct 21, 2024

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 21, 2024

✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@adomani
Copy link
Collaborator Author

adomani commented Oct 21, 2024

Bors merge

mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
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]>
@kim-em
Copy link
Contributor

kim-em commented Oct 21, 2024

I guess bors is case sensitive?

bors merge

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 21, 2024

Already running a review

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 21, 2024
@kim-em
Copy link
Contributor

kim-em commented Oct 21, 2024

Nope, just didn't add the label for some reason.

@adomani
Copy link
Collaborator Author

adomani commented Oct 21, 2024

I had checked that bors was running, but did not notice the missing label...

@adomani
Copy link
Collaborator Author

adomani commented Oct 21, 2024

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 ·, so I put the PR quickly on the queue from my phone: I know that r+ has a tendency to be auto-corrected, but I did not think about capitalization of bors!

I'll test it some other time as well, to see if adding the label is case-sensitive.

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Oct 21, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: the multiGoal linter [Merged by Bors] - feat: the multiGoal linter Oct 21, 2024
@mathlib-bors mathlib-bors bot closed this Oct 21, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/lint_multiple_goals branch October 21, 2024 07:12
mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated large-import Automatically added label for PRs with a significant increase in transitive imports ready-to-merge This PR has been sent to bors. t-linter Linter
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants