Skip to content

Pull requests: leanprover/lean4

New pull request New
554 Open 10,057 Closed
554 Open 10,057 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

fix: instantiate metavariables when collecting a goal's constants 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…
1
fix: drop stale .reverse in MePo premise selector 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…
1
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: adjust dev-release preset toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13741 opened May 15, 2026 by Kha Member Loading…
4
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
chore: CI: verify lake cache step 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
#13735 opened May 14, 2026 by tydeu Member Loading…
2
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
chore: CI: build everything with Lake release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13721 opened May 13, 2026 by Kha Member • Draft
6
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
fix: do not block on async theorem bodies when iterating local consts 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-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
#13712 opened May 11, 2026 by nomeata Collaborator Loading…
1
4
restrict lazy WHNF to reducible (test) 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 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
#13702 opened May 11, 2026 by datokrat Contributor • Draft
6
chore: re-enable LLVM CI 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 changes-stage0 Contains stage0 changes, merge manually using rebase 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
#13700 opened May 11, 2026 by hargoniX Contributor • Draft
22
feat: collect diagnostic explanations into hover popup
#13697 opened May 10, 2026 by wvhulle • Draft
feat: ship lsp-probe test-equipment binary toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13696 opened May 10, 2026 by wvhulle • Draft
2
fix: Expose related information diagnostics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13695 opened May 10, 2026 by wvhulle • Draft
2
feat: verifiable whileM via ordered fixpoints for stronger specs changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13689 opened May 8, 2026 by sgraf812 Contributor • Draft
2
ProTip! Exclude everything labeled bug with -label:bug.