Skip to content

chore: final module system fixes and refinements for initial Mathlib porting #10869

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 3 commits into from
Oct 24, 2025
Merged

chore: final module system fixes and refinements for initial Mathlib porting #10869

Kha merged 3 commits into from
Oct 24, 2025

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 21, 2025

No description provided.

@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 21, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 21, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-20 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-21 10:33:50)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-10-21 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-23 13:21:37)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10869
203de44
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10869
ca97953
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 21, 2025
@leanprover-community-bot
Copy link
Collaborator

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

Mathlib CI status (docs):

@Kha Kha force-pushed the push-qyzktxwszuwp branch from 49049cc to 98a4b6a Compare October 23, 2025 08:22
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
74c2f4b
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
b496dba
@Kha Kha added the fast-ci Forces the use of large runners so that e.g. PR releases are created faster label Oct 23, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
2b043b5
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 23, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
1f495be
@Kha Kha force-pushed the push-qyzktxwszuwp branch from 18060f2 to e3055c5 Compare October 24, 2025 15:39
Kha
Kha commented Oct 24, 2025
View reviewed changes
src/Lean/Meta/Tactic/Rfl.lean

/-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
Copy link
Member Author

@Kha Kha Oct 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kim-em We should probably find a better home for this theorem, this will break if the module is meta-imported indirectly only, i.e. available only as .ir

@Kha Kha enabled auto-merge October 24, 2025 15:48
@Kha Kha changed the title chore: final module system fixes and refinements for Mathlib porting chore: final module system fixes and refinements for initial Mathlib porting Oct 24, 2025
@Kha Kha added this pull request to the merge queue Oct 24, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
6e6b7f7
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 24, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10869
43cd675
Merged via the queue into leanprover:master with commit b0127e0 Oct 24, 2025
19 checks passed
@Kha Kha deleted the push-qyzktxwszuwp branch October 24, 2025 16:58
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Oct 27, 2025
@Kha @wkrozowski
chore: final module system fixes and refinements for initial Mathlib …
763e6ce 
…porting (leanprover#10869)
kim-em pushed a commit that referenced this pull request Oct 27, 2025
@Kha @kim-em
chore: final module system fixes and refinements for initial Mathlib …
eb3739e 
…porting (#10869)
@nomeata nomeata mentioned this pull request Oct 29, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@digama0 digama0 Awaiting requested review from digama0

@kmill kmill Awaiting requested review from kmill

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

@hargoniX hargoniX Awaiting requested review from hargoniX

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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