Skip to content

[Merged by Bors] - chore: adapt to multiple goal linter 6#12834

Closed
adomani wants to merge 10 commits intomasterfrom
adomani/use_cdots_6
Closed

[Merged by Bors] - chore: adapt to multiple goal linter 6#12834
adomani wants to merge 10 commits intomasterfrom
adomani/use_cdots_6

Conversation

@adomani
Copy link
Copy Markdown
Contributor

@adomani adomani commented May 12, 2024

Another halfway split of #12381 on the way to #12352.

Open in Gitpod

This was referenced May 12, 2024
Closed
Closed
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 12, 2024
@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 May 12, 2024
grunweg
grunweg approved these changes May 12, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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.

Looks good to me: in a few places, I would tweak the code a little further (but these are minor comments).

grunweg added a commit that referenced this pull request May 12, 2024
@grunweg
chore: remove some stream-of-conciousness syntax for obtain
b44cc51 
Similar to #11045; discovered in #12834.
@grunweg
chore: use refine instead of refine'
80d874a 
In three files which are modified in #12834 or #12381: in my opinion,
the unprimed version makes these modifications easier to read.
This was referenced May 12, 2024
Closed
Closed
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented May 12, 2024 •
edited
Loading

Filed #12850 and #12851 with the style tweaks I suggested. Reviews welcome - since I wrote these PRs, you should have no conflict of interest :-)

@adomani
Copy link
Copy Markdown
Contributor Author

adomani commented May 12, 2024

Michael, thank you very much for the continuing thorough reviews!

mathlib-bors bot pushed a commit that referenced this pull request May 12, 2024
@grunweg
chore: remove some stream-of-conciousness syntax for obtain (#12850)
b897a62 
Similar to #11045; discovered in #12834.
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 13, 2024
@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 May 13, 2024
@grunweg @eric-wieser
Update Mathlib/MeasureTheory/Measure/Haar/Basic.lean
98114d7 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented May 13, 2024

Thank you for writing this linter, Damiano - I would very much like to see it land!

mathlib-bors bot pushed a commit that referenced this pull request May 13, 2024
@grunweg
chore: use refine instead of refine' (#12851)
9147b87 
In three files which are modified in #12834 or #12381: in my opinion, the unprimed version makes these modifications easier to read.
jcommelin
jcommelin reviewed May 13, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 13, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 13, 2024

Canceled.

@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented May 13, 2024

bors merge

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 13, 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.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 13, 2024
@adomani @grunweg
chore: adapt to multiple goal linter 6 (#12834)
b99b683 
Another halfway split of #12381 on the way to #12352.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: adapt to multiple goal linter 6 [Merged by Bors] - chore: adapt to multiple goal linter 6 May 13, 2024
@mathlib-bors mathlib-bors bot closed this May 13, 2024
@mathlib-bors mathlib-bors bot deleted the adomani/use_cdots_6 branch May 13, 2024 09:51
mathlib-bors bot pushed a commit that referenced this pull request May 13, 2024
@adomani
chore: adapt to multiple goal linter 4 (#12381)
c551dcc 
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
callesonne pushed a commit that referenced this pull request May 16, 2024
@grunweg @callesonne
chore: remove some stream-of-conciousness syntax for obtain (#12850)
fcbd41b 
Similar to #11045; discovered in #12834.
callesonne pushed a commit that referenced this pull request May 16, 2024
@grunweg @callesonne
chore: use refine instead of refine' (#12851)
eead9a6 
In three files which are modified in #12834 or #12381: in my opinion, the unprimed version makes these modifications easier to read.
callesonne pushed a commit that referenced this pull request May 16, 2024
@adomani @grunweg @callesonne
chore: adapt to multiple goal linter 6 (#12834)
e316632 
Another halfway split of #12381 on the way to #12352.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
callesonne pushed a commit that referenced this pull request May 16, 2024
@adomani @callesonne
chore: adapt to multiple goal linter 4 (#12381)
1630513 
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
grunweg added a commit that referenced this pull request May 17, 2024
@grunweg
chore: remove some stream-of-conciousness syntax for obtain (#12850)
d37165d 
Similar to #11045; discovered in #12834.
grunweg added a commit that referenced this pull request May 17, 2024
@grunweg
chore: use refine instead of refine' (#12851)
ee3190f 
In three files which are modified in #12834 or #12381: in my opinion, the unprimed version makes these modifications easier to read.
grunweg added a commit that referenced this pull request May 17, 2024
@adomani @grunweg
chore: adapt to multiple goal linter 6 (#12834)
66a5986 
Another halfway split of #12381 on the way to #12352.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
grunweg pushed a commit that referenced this pull request May 17, 2024
@adomani @grunweg
chore: adapt to multiple goal linter 4 (#12381)
22ede76 
This PR was reduced by approximately half of its original size: the other half of this PR is now the content of #12560.

This PR was reduced by approximately half of its halved size: the other half of the halved PR is now the content of #12834.

A PR analogous to the merged PRs #12338, #12361 and #12372: reformatting proofs following the multiple goals linter of #12339.

This should be the last of the adaptations.
mathlib-bors bot pushed a commit that referenced this pull request Oct 21, 2024
@adomani @grunweg
feat: the multiGoal linter (#12339)
f738d22 
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 <rothgami@math.hu-berlin.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@grunweg grunweg grunweg approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

3 participants

@adomani @grunweg @jcommelin