Skip to content

[Merged by Bors] - chore: update SHA of already forward-ported files#2181

Closed
joneugster wants to merge 4 commits intomasterfrom
forward-port-sha
Closed

[Merged by Bors] - chore: update SHA of already forward-ported files#2181
joneugster wants to merge 4 commits intomasterfrom
forward-port-sha

Conversation

@joneugster
Copy link
Copy Markdown
Contributor

@joneugster joneugster commented Feb 9, 2023 •
edited by eric-wieser
Loading

Update some SHAs of files that changed in mathlib3.

These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported.

The relevant changes are:

(haven't spent much time verifying these exactly, mostly assumed that the already merged forward ports were correct.)
Now after the reviews, I am fairly certain that all missing statements/comments have been spotted

Open in Gitpod

@joneugster joneugster added WIP Work in progress awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged and removed WIP Work in progress labels Feb 9, 2023
@joneugster joneugster changed the title chore: forward-port update SHA chore: update SHA of already forward-ported files Feb 9, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 12, 2023

I suggest we refrain from reviewing this until I've improved the tooling that those links point to.

@joneugster
Copy link
Copy Markdown
Contributor Author

joneugster commented Feb 13, 2023

That's fine by me, I'll leave it as a reference here ro test the tooling.

eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 17, 2023
View reviewed changes
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 17, 2023

Ok, the tool is mostly good enough now. Note that this PR claims to update 20 files but only actually touches 17, presumably since other PRs were merged.

I've left resolved comments on everything I think looks good, and unresolved ones on the rest.

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 17, 2023
@joneugster joneugster added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 22, 2023
eric-wieser
eric-wieser reviewed Feb 22, 2023
View reviewed changes
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 22, 2023

Thanks, just one snake_case name to fix

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Feb 22, 2023

✌️ joneugster 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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 22, 2023
@joneugster
Copy link
Copy Markdown
Contributor Author

joneugster commented Feb 22, 2023

bors r+

bors bot pushed a commit that referenced this pull request Feb 22, 2023
@joneugster @eric-wieser
chore: update SHA of already forward-ported files (#2181)
88c789e 
Update some SHAs of files that changed in mathlib3.

These 17 files need mainly only updated SHA as they've been only touched by backports or already have been forward-ported.

The relevant changes are:

* [Algebra.Group.Defs (#17884)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/defs?range=41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3..2e0975f6a25dd3fbfb9e41556a77f075f6269748)
  * #945
* [Algebra.Group.WithOne.Defs (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/group/with_one/defs?range=e574b1a4e891376b0ef974b926da39e05da12a06..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Algebra.Module.Submodule.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/algebra/module/submodule/basic?range=f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Algebra.Order.Monoid.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/monoid/with_top?range=2258b40dacd2942571c8ce136215350c702dc78f..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Algebra.Order.Ring.WithTop (#18149, #18081)](https://leanprover-community.github.io/mathlib-port-status/file/algebra/order/ring/with_top?range=550b58538991c8977703fdeb7c9d51a5aa27df11..e7e2ba8aa216a5833b5ed85a93317263711a36b5)
  * #1508
  * #1439
* [Data.Finset.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/n_ary?range=9003f28797c0664a49e4179487267c494477d853..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Option.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/option/n_ary?range=2258b40dacd2942571c8ce136215350c702dc78f..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.Set.NAry (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/data/set/n_ary?range=2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [Data.SetLike.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/data/set_like/basic?range=fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [Data.Sum.Basic (#18184)](https://leanprover-community.github.io/mathlib-port-status/file/data/sum/basic?range=d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d..f4ecb599422baaf39055d8278c7d9ef3b5b72b88)
  * #1583
* [GroupTheory.GroupAction.SubMulAction  (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/group_action/sub_mul_action?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [GroupTheory.Submonoid.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/submonoid/basic?range=207cfac9fcd06138865b5d04f7091e46d9320432..feb99064803fd3108e37c18b0f77d0a8344677a3)
* [ Logic.Basic (#18291): backport](https://leanprover-community.github.io/mathlib-port-status/file/logic/basic?range=1c521b4fb909320eca16b2bb6f8b5b0490b1cb5e..feb99064803fd3108e37c18b0f77d0a8344677a3)
  * #1509
* [Order.InitialSeg (#18198): backport](https://leanprover-community.github.io/mathlib-port-status/file/order/initial_seg?range=ee0c179cd3c8a45aa5bffbf1b41d8dbede452865..7c3269ca3fa4c0c19e4d127cd7151edbdbf99ed4)
* [Order.RelClasses (#17957)](https://leanprover-community.github.io/mathlib-port-status/file/order/rel_classes?range=c4658a649d216f57e99621708b09dcb3dcccbd23..bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e)
  * #1047
* [Order.WithBot (#18081)](https://leanprover-community.github.io/mathlib-port-status/file/order/with_bot?range=70d50ecfd4900dd6d328da39ab7ebd516abe4025..995b47e555f1b6297c7cf16855f1023e355219fb)
  * #1439
* [RingTheory.Subsemiring.Basic (#18291) : backport](https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/subsemiring/basic?range=f93c11933efbc3c2f0299e47b8ff83e9b539cbf6..feb99064803fd3108e37c18b0f77d0a8344677a3)



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Feb 22, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: update SHA of already forward-ported files [Merged by Bors] - chore: update SHA of already forward-ported files Feb 22, 2023
@bors bors bot closed this Feb 22, 2023
@bors bors bot deleted the forward-port-sha branch February 22, 2023 14:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged

Projects

No open projects
Forward ports of mathlib3
Status: Done

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@joneugster @eric-wieser