Skip to content

Pull requests: leanprover/lean4

New pull request New
548 Open 10,018 Closed
548 Open 10,018 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

chore: re-enable Lake tests changelog-no Do not include this PR in the release changelog 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
#13692 opened May 8, 2026 by tydeu Member Loading…
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 • Draft
2
chore: align cbv tactic with SymM framework conventions 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
#13682 opened May 7, 2026 by wkrozowski Contributor Loading…
10
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
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
13
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
doc: add CLAUDE.md guidance on rebasing vs changing PR base 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
#13652 opened May 6, 2026 by kim-em Collaborator Loading…
2
feat: efficient tactic configuration elaborators and configurability 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
feat: restrict simpa using h close to reducible transparency breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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
#13636 opened May 5, 2026 by kim-em Collaborator Loading…
3
feat: add @[attribute] for registering custom attributes 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
#13629 opened May 4, 2026 by Kha Member • Draft
4
fix: apply rcases substitution before recording pattern info changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13621 opened May 3, 2026 by berberman • Draft
1
4
chore: export function needed to implement dead / unused code detection functions outside of Lean core by users toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13609 opened May 2, 2026 by wvhulle • Draft
2
feat: show live Lake LSP loading progress in status bar of editors instead of top of file toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13608 opened May 2, 2026 by wvhulle • Draft
2
Nix flake improvements toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13607 opened May 2, 2026 by wvhulle • Draft
2
Lsp formatting toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13606 opened May 2, 2026 by wvhulle • Draft
2
ProTip! Exclude everything labeled bug with -label:bug.