Skip to content

Pull requests: leanprover/lean4

New pull request New
558 Open 10,065 Closed
558 Open 10,065 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

refactor: app elaborator refactoring and improvements changelog-language Language features and metaprograms
#13762 opened May 17, 2026 by kmill Collaborator Loading…
feat: improve performance of structure instance notation elaboration changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13760 opened May 16, 2026 by kmill Collaborator Loading…
4
chore: CI: fold Linux Lake into Linux release toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13759 opened May 16, 2026 by Kha Member Loading…
2
try disabling prefer_native for further stages as well 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 mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13757 opened May 16, 2026 by Kha Member • Draft
4
feat: apply suppressInsideQuot to meta declarations changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13756 opened May 16, 2026 by Kha Member Loading…
2
feat: implement textDocument/selectionRange LSP request toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13755 opened May 16, 2026 by dominique-unruh Loading…
4
refactor: derive LEAN_GITHASH from src/ content instead of commit SHA toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13754 opened May 16, 2026 by Kha Member • Draft
2
feat: report private inherited declaration in projection notation error changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13752 opened May 16, 2026 by Kha Member Loading…
2
feat: enter private scope when elaborating proof fields of structure instances breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13751 opened May 16, 2026 by Kha Member Loading…
2
feat: filter MePo candidates to theorems and order output by iteration breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13750 opened May 16, 2026 by kim-em Collaborator Loading…
2
fix: instantiate metavariables when collecting a goal's constants breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13748 opened May 15, 2026 by kim-em Collaborator Loading…
2
fix: drop stale .reverse in MePo premise selector breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13747 opened May 15, 2026 by kim-em Collaborator Loading…
2
perf: bump priority of zsmul 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 fast-ci Forces the use of large runners so that e.g. PR releases are created faster mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13746 opened May 15, 2026 by hargoniX Contributor Loading…
4
doc: fix case syntax in mvcgen docs toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13745 opened May 15, 2026 by frangio Loading…
2
feat: allow Lean.Linter to access the environment from before starting to elaborate the top-level command changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13744 opened May 15, 2026 by wkrozowski Contributor • Draft
2
fix: use consistent, robust instance-like check in compiler 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 changelog-no Do not include this PR in the release changelog mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13743 opened May 15, 2026 by Kha Member Loading…
4
doc: add no-line-wrapping convention for commit messages toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13742 opened May 15, 2026 by Kha Member Loading…
2
chore: remove addInfo flag from elabSetOption toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13736 opened May 14, 2026 by thorimur Contributor Loading…
3
perf: try to emit assumes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13732 opened May 14, 2026 by hargoniX Contributor • Draft
4
feat: add newDecls fields to Core.State and Command.State changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13731 opened May 14, 2026 by wkrozowski Contributor • Draft
7
experiment: reduce clangs cleverness toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13727 opened May 13, 2026 by hargoniX Contributor • Draft
4
feat: improve semantic highlighting (close #2305) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13726 opened May 13, 2026 by RIvance Loading…
1
2
[don’t merge] cherry-pick try-on-empty-by to v4.30rc2 breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13724 opened May 13, 2026 by nomeata Collaborator • Draft
2
feat: proof mode for new foundations of mvcgen 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 changelog-library Library changelog-tactics User facing tactics mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13722 opened May 13, 2026 by volodeyka Contributor Loading…
2
perf: inline assorted declarations used in match_expr toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13716 opened May 12, 2026 by hargoniX Contributor • Draft
4
ProTip! Mix and match filters to narrow down what you’re looking for.