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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - style: remove mathport output #13198

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - style: remove mathport output #13198

wants to merge 4 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented May 25, 2024

Open in Gitpod

@Komyyy Komyyy added awaiting-review mathlib-port This is a port of a theory file from mathlib. easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI labels May 25, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot 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 27, 2024
@Komyyy Komyyy 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 27, 2024
YaelDillies
YaelDillies previously requested changes May 28, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Can you please check that the comments are not applicable anymore?

Mathlib/Data/DFinsupp/Basic.lean Outdated
@@ -1522,7 +1522,6 @@ theorem sigmaCurry_single [∀ i, DecidableEq (α i)] [∀ i j, Zero (δ i j)]
simp [hi]
#align dfinsupp.sigma_curry_single DFinsupp.sigmaCurry_single

/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/
Copy link
Collaborator

Choose a reason for hiding this comment

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

Eg this one is still applicable since there is Π₀ (i) (j), δ i j just a few lines under.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

We can't write Π₀ (i) (j), δ i j as either Π₀ (i j), δ i j or Π₀ i j, δ i j so this is not a problem.
I also checked the other mathport output but there are no other problems.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Then shouldn't we fix the Π₀ notation? cc @eric-wieser

This PR is hiding the problem under the rug

@YaelDillies YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review mathlib-port This is a port of a theory file from mathlib. easy < 20s of review time. See the lifecycle page for guidelines. labels May 28, 2024
@Komyyy Komyyy added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 28, 2024
@Komyyy Komyyy requested a review from YaelDillies May 28, 2024 08:09
@Komyyy Komyyy dismissed YaelDillies’s stale review May 28, 2024 08:10

We can't write Π₀ (i) (j), δ i j as either Π₀ (i j), δ i j or Π₀ i j, δ i j so this is not a problem.

@Ruben-VandeVelde Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jun 4, 2024
@Ruben-VandeVelde
Copy link
Collaborator

I agree with Yaël. Please keep the binder comments

@Komyyy Komyyy changed the title style: remove all mathport output style: remove mathport output Jun 4, 2024
@Komyyy Komyyy mentioned this pull request Jun 4, 2024
Open
@Komyyy
Copy link
Collaborator Author

Komyyy commented Jun 4, 2024

@YaelDillies @Ruben-VandeVelde Sorry. I've created the issue #13496.
I reverted removing expanding binder groups, except Mathlib.Analysis.Matrix which is rewritten from ∑ k j, ‖A i j‖₊ * ‖B j k‖₊ to ∑ k, ∑ j, ‖A i j‖₊ * ‖B j k‖₊ during porting.

@Komyyy Komyyy added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 4, 2024
YaelDillies
YaelDillies reviewed Jun 4, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Great! Thanks. The remaining changes all look agreeable.

maintainer merge

@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 4, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@PatrickMassot
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 4, 2024
@Komyyy
style: remove mathport output (#13198)
aa6c69b
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title style: remove mathport output [Merged by Bors] - style: remove mathport output Jun 4, 2024
@mathlib-bors mathlib-bors bot closed this Jun 4, 2024
@mathlib-bors mathlib-bors bot deleted the Komyyy/Mathport branch June 4, 2024 19:08
callesonne pushed a commit that referenced this pull request Jun 4, 2024
@Komyyy @callesonne
style: remove mathport output (#13198)
460ca22
grunweg pushed a commit that referenced this pull request Jun 7, 2024
@Komyyy @grunweg
style: remove mathport output (#13198)
8e2e31c
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@Komyyy @AntoineChambert-Loir
style: remove mathport output (#13198)
31e46d9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees
No one assigned
Labels
maintainer-merge 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
@Komyyy @Ruben-VandeVelde @PatrickMassot @YaelDillies @leanprover-community-mathlib4-bot