Skip to content

chore: even more module system fixes and refinements from Mathlib porting #10726

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
Kha merged 15 commits into from
Oct 15, 2025
Merged

chore: even more module system fixes and refinements from Mathlib porting #10726

Kha merged 15 commits into from
Oct 15, 2025

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 9, 2025

No description provided.

@Kha Kha force-pushed the push-molqytxmnzzp branch from 44540e0 to d75f1f8 Compare October 9, 2025 15:36
@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 Oct 9, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10726
26e97c4
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10726
30aef1a
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Oct 9, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#10726
b4edca0
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Oct 9, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 9, 2025 •
edited
Loading

Reference manual CI status:

  • ✅ Reference manual branch lean-pr-testing-10726 has successfully built against this PR. (2025-10-09 17:11:09) View Log
  • 🟡 Reference manual branch lean-pr-testing-10726 build against this PR didn't complete normally. (2025-10-09 17:11:15) View Log
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-10-13 14:50:53)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7632cefa8791817df6c27e0b04ee39cd45330eaf --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-14 17:03:19)

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 9, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 9, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-10726 has successfully built against this PR. (2025-10-09 18:08:41) View Log
  • ✅ Mathlib branch lean-pr-testing-10726 has successfully built against this PR. (2025-10-13 15:58:15) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7632cefa8791817df6c27e0b04ee39cd45330eaf --onto 14ff08db6f651775ead432d367b6b083878bb0f9. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-14 17:03:16)

@zwarich zwarich removed their request for review October 10, 2025 04:54
@Kha Kha force-pushed the push-molqytxmnzzp branch from 0df1249 to 8f1ee72 Compare October 13, 2025 13:50
@Kha Kha requested a review from hargoniX as a code owner October 13, 2025 13:50
@Kha Kha enabled auto-merge October 13, 2025 13:51
@Kha Kha added this pull request to the merge queue Oct 13, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 13, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 13, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10726
b51e241
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 13, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10726
d3b8dc4
@Kha Kha enabled auto-merge October 14, 2025 16:03
@Kha Kha added this pull request to the merge queue Oct 14, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 14, 2025
@Kha Kha force-pushed the push-molqytxmnzzp branch from 17d0322 to e434766 Compare October 14, 2025 19:03
@Kha Kha enabled auto-merge October 14, 2025 19:03
@Kha Kha added this pull request to the merge queue Oct 14, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 14, 2025
@Kha Kha enabled auto-merge October 15, 2025 13:41
@Kha Kha force-pushed the push-molqytxmnzzp branch from 211877a to 22664d0 Compare October 15, 2025 13:59
@Kha Kha added this pull request to the merge queue Oct 15, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Oct 15, 2025
@Kha Kha force-pushed the push-molqytxmnzzp branch from 22664d0 to e3043fa Compare October 15, 2025 14:34
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Oct 15, 2025
@Kha Kha enabled auto-merge October 15, 2025 14:34
@Kha Kha added this pull request to the merge queue Oct 15, 2025
Merged via the queue into leanprover:master with commit 419982b Oct 15, 2025
20 of 25 checks passed
@Kha Kha deleted the push-molqytxmnzzp branch October 15, 2025 15:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@Vtec234 Vtec234 Awaiting requested review from Vtec234 Vtec234 is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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-bot @leanprover-community-bot