Skip to content

chore: further adaptations for batteries modulization #10542

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
Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

chore: further adaptations for batteries modulization #10542

wants to merge 1 commit into from

Conversation

Kha
Copy link
Member

@Kha Kha commented Sep 24, 2025

Placeholder for now

@Kha Kha force-pushed the push-kqpowsuotrwy branch from 56ad49b to e313121 Compare September 24, 2025 12:05
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 24, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Sep 24, 2025 •
edited
Loading

Mathlib CI status (docs):
Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 44a2b085c4c9fc386879973fdd6798255e29e420 --onto 0807f73171ca8f765c11ef37d69fd95e6613a878. (2025-09-24 12:56:43)

  • 💥 Mathlib branch lean-pr-testing-10542 build failed against this PR. (2025-09-24 13:06:21) View Log
    Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2c54386555f12af82f8fd89ba28d9f6590a90a22 --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. (2025-09-26 14:36:58)
  • 🟡 Mathlib branch lean-pr-testing-10542 build this PR didn't complete normally. (2025-09-26 15:35:36) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Sep 24, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 44a2b085c4c9fc386879973fdd6798255e29e420 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-24 12:56:45)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2c54386555f12af82f8fd89ba28d9f6590a90a22 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-26 14:37:00)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10542
50091bc
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10542
0fa384e
@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 24, 2025
@Kha Kha force-pushed the push-kqpowsuotrwy branch from e313121 to de9278c Compare September 26, 2025 13:05
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Sep 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10542
06bfe88
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Sep 26, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10542
64fcc17
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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Kha @leanprover-community-bot @leanprover-bot