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] - feat: synchronize with mathlib3 #17905 #1280

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat: synchronize with mathlib3 #17905 #1280

wants to merge 7 commits into from

Conversation

alreadydone
Copy link
Contributor

@alreadydone alreadydone commented Dec 31, 2022 •
edited

mathlib3 SHA: 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff

mathlib#17905 has been approved, so I think reviewers don't need to check the mathematical content.

@alreadydone alreadydone added the awaiting-review The author would like community review of the PR label Dec 31, 2022
@alreadydone alreadydone changed the title feat: three lemmas in Order/Directed feat: add three lemmas in Order/Directed Dec 31, 2022
@alreadydone alreadydone mentioned this pull request Dec 31, 2022
Closed
1 task
@alreadydone alreadydone changed the title feat: add three lemmas in Order/Directed feat: synchronize with mathlib#17905 Jan 2, 2023
@alreadydone alreadydone changed the title feat: synchronize with mathlib#17905 feat: synchronize with mathlib3 #17905 Jan 2, 2023
@alreadydone alreadydone added the easy < 20s of review time. See the lifecycle page for guidelines. label Jan 2, 2023
@riccardobrasca
Copy link
Member

There is a bunch of modifications to lake-manifest.json that are probably unwanted.

@alreadydone
Copy link
Contributor Author

There is a bunch of modifications to lake-manifest.json that are probably unwanted.

Hmm, thanks for noticing! I noticed the changes and made sure not to include the file in the first commit, but forgot about it in the second commit. They're probably generated by some "lake update" command.

@hrmacbeth hrmacbeth added the mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged label Jan 2, 2023
@riccardobrasca
Copy link
Member

Just wait for the mathlib3 PR to be merged.

bors d+

@bors
Copy link

bors bot commented Jan 3, 2023

✌️ alreadydone 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 and removed awaiting-review The author would like community review of the PR labels Jan 3, 2023
@riccardobrasca
Copy link
Member

Even better, if this is the correct thing to do (I am not 100% sure), you can update the sha of Order/Directed directly in this PR.

@alreadydone
Copy link
Contributor Author

Even better, if this is the correct thing to do (I am not 100% sure), you can update the sha of Order/Directed directly in this PR.

Is that required (not yet automated), or can I simply bors r+ now?

@riccardobrasca
Copy link
Member

Even better, if this is the correct thing to do (I am not 100% sure), you can update the sha of Order/Directed directly in this PR.

Is that required (not yet automated), or can I simply bors r+ now?

Just change the has to the latest mathlib3 hash (double check that nobody else had made any modification to the relevant file) and then merge this.

I don't think this can be automatized, since someone has to check that the modification are in sync, but I can be wrong.

@alreadydone
Copy link
Contributor Author

alreadydone commented Jan 5, 2023 •
edited

I copied the SHA of the latest commit of the file in mathlib3 to the PR description. That's what I'm supposed to do right? I'll wait a bit for a confirmation before merging. This is my first mathlib4 PR and I'm not following all the recent changes in procedure ...

@riccardobrasca
Copy link
Member

I copied the SHA of the latest commit of the file in mathlib3 to the PR description. That's what I'm supposed to do right? I'll wait a bit for a confirmation before merging. This is my first mathlib4 PR and I'm not following all the recent changes in procedure ...

I think that's OK, let's merge this, thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 5, 2023
bors bot pushed a commit that referenced this pull request Jan 5, 2023
@alreadydone
feat: synchronize with mathlib3 #17905 (#1280)
fea2634 
mathlib3 SHA: 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff

________

[mathlib#17905](https://github.com/leanprover-community/mathlib/pull/17905/files#diff-deb01ba12632f4703c3dc29a10a34bd3a7d2a1c02dcf8b44d3e561fe3bde06fe) has been approved, so I think reviewers don't need to check the mathematical content.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@bors
Copy link

bors bot commented Jan 5, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: synchronize with mathlib3 #17905 [Merged by Bors] - feat: synchronize with mathlib3 #17905 Jan 5, 2023
@bors bors bot closed this Jan 5, 2023
@bors bors bot deleted the directedOn_range branch January 5, 2023 03:24
@alreadydone
Copy link
Contributor Author

alreadydone commented Jan 5, 2023 •
edited

Maybe I need to modify line 7 as well? It now refers to an earlier hash:

! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9

@riccardobrasca
Copy link
Member

Yes sorry, this we should modify this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ChrisHughes24 ChrisHughes24 ChrisHughes24 left review comments

Assignees
No one assigned
Labels
delegated easy < 20s of review time. See the lifecycle page for guidelines. mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged 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.

None yet
4 participants
@alreadydone @riccardobrasca @ChrisHughes24 @hrmacbeth