Skip to content

Pull requests: leanprover/lean4

New pull request New
550 Open 10,032 Closed
550 Open 10,032 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: 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 • Draft
1
3
fix: abort IPC test runner promptly on file worker fatal error changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13710 opened May 11, 2026 by nomeata Collaborator Loading…
2
refactor: turn dupNamespace into a Lean.Linter changelog-no Do not include this PR in the release changelog lake-ci Run all Lake tests toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13708 opened May 11, 2026 by wkrozowski Contributor Loading…
2
test: avoid deadlock in cancellation_empty_by 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
#13707 opened May 11, 2026 by nomeata Collaborator • Draft
2
test: always clean full .lake 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 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
#13703 opened May 11, 2026 by Kha Member Loading…
2
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-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
2
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
chore: performance of lake builtin-lint (experiment) 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 force-mathlib-ci 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
#13690 opened May 8, 2026 by wkrozowski Contributor • 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
feat: upstream unusedDecidableInType linter 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
#13688 opened May 8, 2026 by wkrozowski Contributor Loading…
4
feat: support mvcgen' inside sym => … blocks changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13680 opened May 7, 2026 by sgraf812 Contributor • Draft
2
[REBASED] fix: codegen should not inspect private ctor of public type 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
#13679 opened May 7, 2026 by Kha Member • Draft
2
feat: add WallTime and simplify Timestamp API changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13675 opened May 7, 2026 by algebraic-dev Member Loading…
@algebraic-dev
14
feat: more semantic tokens for Markdown/Verso changelog-server Language server, widgets, and IDE extensions toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13674 opened May 7, 2026 by david-christiansen Contributor Loading…
3
test 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
#13660 opened May 6, 2026 by datokrat Contributor • Draft
2
chore: rebase #13283 to nightly-with-mathlib 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
#13658 opened May 6, 2026 by datokrat Contributor • Draft
2
feat: add Dyadic.divAtPrec for round-down dyadic division at given precision 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 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
#13654 opened May 6, 2026 by kim-em Collaborator Loading…
1
2
feat: efficient tactic configuration elaborators and configurability breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13651 opened May 5, 2026 by kmill Collaborator Loading…
4
feat: precompiled tactic elaboration configurations (draft, for mathlib testing) changelog-language Language features and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13650 opened May 5, 2026 by kmill Collaborator • Draft
1
[Backport releases/v4.30.0] fix: record instances unfolded by wrapInstance as shake dependencies
#13648 opened May 5, 2026 by github-actions Bot Loading…
feat: add requiresModuleSystem package option in Lake 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
#13646 opened May 5, 2026 by Kha Member • Draft
2
feat: split [implicit_reducible] into [instance_reducible] and [implicit_reducible] tiers breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13637 opened May 5, 2026 by kim-em Collaborator • Draft
2
ProTip! Exclude everything labeled bug with -label:bug.