Skip to content

perf: sparse case splitting in match compilation #10823

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 20 commits into
base: master
Choose a base branch
from
Draft

perf: sparse case splitting in match compilation #10823

wants to merge 20 commits into from

Conversation

@nomeata
Copy link
Collaborator

@nomeata nomeata commented Oct 17, 2025 •
edited
Loading

(WIP)

@nomeata nomeata added the changelog-language Language features and metaprograms label Oct 17, 2025
@nomeata nomeata changed the title joachim/selective cases perf: sparse case splitting in match compilation Oct 17, 2025
@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 17, 2025
@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ 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-17 16:00:47)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10823
450eb09
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 17, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10823
5b7037d
@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 Oct 17, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

@nomeata nomeata mentioned this pull request Oct 22, 2025
Open
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 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features and metaprograms 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.

4 participants

@nomeata @leanprover-bot @leanprover-community-bot