Skip to content

Pull requests: leanprover/lean4

New pull request New
569 Open 10,293 Closed
569 Open 10,293 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: remove custom small allocator 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
#14149 opened Jun 22, 2026 by hargoniX Contributor Loading…
2
perf: lazy IR loading 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
#14145 opened Jun 22, 2026 by Kha Member • Draft
6
hbv/json gerät++
#14144 opened Jun 22, 2026 by hargoniX Contributor • Draft
2
chore: disable binary stripping in release configuration builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI 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
#14139 opened Jun 22, 2026 by hargoniX Contributor Loading…
4
perf: short-circuit Sym pattern matching on pointer equality changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14137 opened Jun 22, 2026 by sgraf812 Contributor • Draft
2
fix: split universe levels for le_of_forall_le lemma changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14133 opened Jun 21, 2026 by volodeyka Contributor • Draft
3
fix: handle overlapping block comment terminators in fast import parser changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14131 opened Jun 20, 2026 by leiko1337 Contributor Loading…
3
eta trick 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
#14129 opened Jun 19, 2026 by datokrat Contributor • Draft
4
test toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14124 opened Jun 19, 2026 by datokrat Contributor • Draft
2
chore: add import Lean (cold) benchmark 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
#14121 opened Jun 19, 2026 by Kha Member Loading…
8
feat: cost metrics for the grind e-matching graph 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
#14118 opened Jun 19, 2026 by hargoniX Contributor Loading…
4
fix: deadlock using Selectable.combine changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14116 opened Jun 19, 2026 by algebraic-dev Member Loading…
1
@algebraic-dev
4
feat: extensible Markdown rendering of Verso docstrings changelog-language Language features and metaprograms 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
#14115 opened Jun 18, 2026 by david-christiansen Contributor • Draft
2
fix: reject sym apply with an unresolved instance argument toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14113 opened Jun 18, 2026 by sgraf812 Contributor • Draft
2
perf: replace unordered_map/unordered_set with flat hash tables in object compactor 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
#14109 opened Jun 18, 2026 by Kha Member • Draft
6
draft: decl check 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
#14101 opened Jun 18, 2026 by datokrat Contributor • Draft
12
perf: route BitVec.flattenList through the chunked Array merge core changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14097 opened Jun 18, 2026 by kim-em Collaborator • Draft
2
fix: delete broken header file 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
#14096 opened Jun 18, 2026 by eric-wieser Contributor Loading…
2
perf: prefetch import regions via madvise 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
#14093 opened Jun 17, 2026 by Kha Member • Draft
4
perf: JSON fast path for String literal parsing changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14086 opened Jun 17, 2026 by hargoniX Contributor Loading…
4
doc: fix a typo in List.foldr toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14085 opened Jun 17, 2026 by pevogam Loading…
2
chore: improve diagnostics when thread creation fails
#14082 opened Jun 16, 2026 by eric-wieser Contributor Loading…
step 1 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14074 opened Jun 16, 2026 by hargoniX Contributor • Draft
8
test: add regression test for #13512 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14070 opened Jun 16, 2026 by TWal Contributor Loading…
3
chore: re-land "feat: expire idle task pool threads after 5 seconds (#14043)" 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
#14069 opened Jun 16, 2026 by Kha Member • Draft
2
ProTip! Mix and match filters to narrow down what you’re looking for.