Skip to content

Pull requests: leanprover/lean4

New pull request New
586 Open 10,435 Closed
586 Open 10,435 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

perf: cache inside matcher WHNFs at reducible/instances/implicit 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
#14323 opened Jul 8, 2026 by datokrat Contributor • Draft
4
perf: type class experiment 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
#14318 opened Jul 8, 2026 by leodemoura Member • Draft
6
fix: unsafeCast should not be inlined changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14317 opened Jul 7, 2026 by hargoniX Contributor Loading…
1
4
experiment: persist type class resolution cache across commands 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
#14316 opened Jul 7, 2026 by Kha Member • Draft
6
chore: change UnusedSimpArgs hint 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
#14313 opened Jul 7, 2026 by wkrozowski Contributor • Draft
2
feat: add forward_type_reference% for negative type occurrences changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14311 opened Jul 7, 2026 by sgraf812 Contributor • Draft
2
chore: fix namespaceing in DeprecatedModule 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
#14310 opened Jul 7, 2026 by wkrozowski Contributor Loading…
1
feat: add a warning for adding a deprecated attribute to register_option 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
#14309 opened Jul 7, 2026 by wkrozowski Contributor Loading…
2
chore: reduce namespace pollution changelog-no Do not include this PR in the release changelog
#14308 opened Jul 7, 2026 by TwoFX Member Loading…
feat: lake: content-stable module archives via leantar hash stripping (backport releases/v4.32.0) 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
#14301 opened Jul 7, 2026 by marcelolynch Contributor • Draft
2
feat: lake: presetup module facet breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-lake Lake 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
#14300 opened Jul 7, 2026 by tydeu Member • Draft
2
perf: share depth-invariant type class cache entries across synthPendingDepth 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
#14298 opened Jul 6, 2026 by Kha Member • Draft
14
String.toList semireducible toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14294 opened Jul 6, 2026 by datokrat Contributor • Draft
4
test: cross-check integer @[extern] implementations with test_extern 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
#14288 opened Jul 6, 2026 by kim-em Collaborator Loading…
3
fix: borrow Nat arguments to ByteArray.copySlice changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14286 opened Jul 5, 2026 by kim-em Collaborator Loading…
4
fix: prevent size_t overflow in object_compactor doubling changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14283 opened Jul 5, 2026 by kim-em Collaborator Loading…
3
fix: guard string growth paths against size_t overflow changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14282 opened Jul 5, 2026 by kim-em Collaborator Loading…
3
fix: respect pp.instantiateMVars while pretty-printing goals 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
#14276 opened Jul 4, 2026 by Rob23oba Contributor • Draft
1
2
fix: prevent size_t overflow in lean_sarray_ensure_capacity changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14274 opened Jul 4, 2026 by kim-em Collaborator • Draft
5
fix: guard against size_t overflow in lean_byte_array_copy_slice changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14273 opened Jul 4, 2026 by kim-em Collaborator • Draft
5
fix: plug Nat argument leak in lean_byte_array_copy_slice changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14271 opened Jul 4, 2026 by kim-em Collaborator Loading…
5
feat: add HTTP Server benchmark changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14268 opened Jul 4, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add hint to unusedVariables linter 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 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
#14259 opened Jul 3, 2026 by wkrozowski Contributor Loading…
2
fix: handle errors in Selectable.one and simplify Selectable helpers changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14253 opened Jul 3, 2026 by algebraic-dev Member Loading…
@algebraic-dev
4
9077, other attempt 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
#14248 opened Jul 2, 2026 by datokrat Contributor • Draft
6
ProTip! Adding no:label will show everything without a label.