Skip to content

[Merged by Bors] - chore: bump to nightly-2023-07-01#5409

Closed
kim-em wants to merge 52 commits intomasterfrom
bump-nightly-2023-06-22
Closed

[Merged by Bors] - chore: bump to nightly-2023-07-01#5409
kim-em wants to merge 52 commits intomasterfrom
bump-nightly-2023-06-22

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Jun 23, 2023 •
edited by jcommelin
Loading

@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 23, 2023
@kim-em kim-em mentioned this pull request Jun 23, 2023
Closed
@kim-em kim-em added help-wanted The author needs attention to resolve issues and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) help-wanted The author needs attention to resolve issues labels Jun 23, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jun 23, 2023 •
edited
Loading

Changes in Lean4 have caused a regression that I think we should fix upstream first, so this bump is on hold for now.

EDIT: the regression has been fixed, and now we're waiting on Std4.

@kim-em kim-em mentioned this pull request Jun 23, 2023
Closed
1 task
@kim-em kim-em changed the title chore: bump to nightly-2023-06-22 chore: bump to nightly-2023-06-28 Jun 28, 2023
@kim-em kim-em added help-wanted The author needs attention to resolve issues blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jun 29, 2023
@Komyyy Komyyy mentioned this pull request Jun 29, 2023
Closed
2 tasks
@kim-em kim-em added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jul 4, 2023
@Ruben-VandeVelde Ruben-VandeVelde mentioned this pull request Jul 4, 2023
Closed
3 tasks
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 4, 2023
@kim-em kim-em mentioned this pull request Jul 4, 2023
Merged
1 task
@kim-em kim-em changed the title chore: bump to nightly-2023-06-28 chore: bump to nightly-2023-07-01 Jul 5, 2023
@kim-em kim-em added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jul 5, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jul 6, 2023

This PR/issue depends on:

@Komyyy Komyyy added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed help-wanted The author needs attention to resolve issues WIP Work in progress labels Jul 12, 2023
@Komyyy
Copy link
Copy Markdown
Contributor

Komyyy commented Jul 12, 2023

If recent commits doesn't conflict with this branch, it will pass the CI.
This bump PR was quite a heavy job, I nearly went mad.

By the way, look! a lot of Goofy are over there.

🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!
🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck! 🐶<ah-hyuck!

kim-em
kim-em commented Jul 12, 2023
View reviewed changes
kim-em
kim-em commented Jul 12, 2023
View reviewed changes
kim-em
kim-em commented Jul 12, 2023
View reviewed changes
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 12, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jul 13, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 13, 2023
bors bot pushed a commit that referenced this pull request Jul 13, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
57e81ae 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jul 13, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Jul 13, 2023

bors merge

bors bot pushed a commit that referenced this pull request Jul 13, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
906f722 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jul 13, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: bump to nightly-2023-07-01 [Merged by Bors] - chore: bump to nightly-2023-07-01 Jul 13, 2023
@bors bors bot closed this Jul 13, 2023
@bors bors bot deleted the bump-nightly-2023-06-22 branch July 13, 2023 02:24
kim-em added a commit that referenced this pull request Aug 14, 2023
@kim-em @Komyyy
@Ruben-VandeVelde @digama0
chore: bump to nightly-2023-07-01 (#5409)
f587581 
- [x] depends on: leanprover-community/batteries#163
- [x] depends on: #5584
- [x] depends on: #5715
- [x] depends on: #5729
- [x] depends on: leanprover-community/batteries#173

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Komyyy <pol_tta@outlook.jp>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@dwrensha dwrensha mentioned this pull request Nov 12, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Komyyy Komyyy Komyyy left review comments

Assignees

No one assigned

Labels

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.

4 participants

@kim-em @Komyyy @Ruben-VandeVelde @digama0