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

chore: upstream Zero and NeZero #5231

Merged
merged 4 commits into from
Sep 10, 2024
Merged

chore: upstream Zero and NeZero #5231

merged 4 commits into from
Sep 10, 2024

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Sep 2, 2024 •
edited
Loading

No description provided.

@github-actions github-actions bot added changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Sep 2, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5231
35d7051
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5231
3a15460
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 2, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@kim-em
remove Zero for leanprover/lean4#5231
b8ab5d8
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@kim-em
remove assert_not_exists about NeZero for leanprover/lean4#5231
5dc4481
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@kim-em
fixes for leanprover/lean4#5231
b1139c8
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@kim-em
fixes for leanprover/lean4#5231
7d1eb3d
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@kim-em
fixes for leanprover/lean4#5231
2b30be1
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5231
a3e0c61
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 2, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5231
da7396e
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Sep 2, 2024
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 3, 2024 05:05 Inactive
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 3, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5231
10e3f3e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 3, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5231
07ef194
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@kim-em kim-em marked this pull request as ready for review September 9, 2024 11:46
@kim-em kim-em added awaiting-review Waiting for someone to review the PR will-merge-soon …unless someone speaks up labels Sep 9, 2024
@kim-em kim-em force-pushed the nezero branch 3 times, most recently from ca3eacd to 331c703 Compare September 10, 2024 07:08
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7a5a08960a30420a9a2524dcab76c331c72c7764 --onto c96fbdda44c14c7c256f046fb2b71fae25ea968e. (2024-09-10 07:28:04)

@kim-em kim-em enabled auto-merge September 10, 2024 08:02
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc September 10, 2024 08:11 Inactive
@kim-em kim-em added this pull request to the merge queue Sep 10, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 10, 2024
@kim-em kim-em merged commit c1da100 into master Sep 10, 2024
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kim-em @leanprover-community-bot @leanprover-community-mathlib4-bot