Skip to content

Pull requests: leanprover/lean4

New pull request New
584 Open 10,348 Closed
584 Open 10,348 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: ci: update adaptation PR CI options
#14228 opened Jun 30, 2026 by Garmelon Contributor Loading…
refactor: USize/ISize handling in bv_decide builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14227 opened Jun 30, 2026 by hargoniX Contributor Loading…
5
refactor: bv_decide pre-processing API to hypothesis based.
#14226 opened Jun 30, 2026 by hargoniX Contributor • Draft
feat: add stateful linters changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14225 opened Jun 30, 2026 by wkrozowski Contributor • Draft
2
perf: map Array.mapFinIdx/mapIdx in place builds-manual CI has verified that the Lean Language Reference builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14224 opened Jun 30, 2026 by kim-em Collaborator Loading…
2
doc: remove circularity from #eval docstring builds-manual CI has verified that the Lean Language Reference builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14223 opened Jun 30, 2026 by david-christiansen Contributor Loading…
1
3
doc: convert pre-declaration comments into docstrings builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-doc Documentation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14222 opened Jun 30, 2026 by david-christiansen Contributor Loading…
2
fix: fix vcgen frames feature for monads with multiple StateT transformers toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14217 opened Jun 29, 2026 by volodeyka Contributor • Draft
2
refactor: port bv_decide reflection to SymM builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14215 opened Jun 29, 2026 by hargoniX Contributor • Draft
6
doc: improve error message for unknown attributes toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14213 opened Jun 29, 2026 by 0rca Loading…
1
2
perf: compile Bool.not and Bool.toNat without branches toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14207 opened Jun 29, 2026 by JJYYY-JJY Loading…
6
feat: use linter framework for deferred docstring checks changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14206 opened Jun 28, 2026 by david-christiansen Contributor Loading…
2
fix: detect failures when flushing module oleans toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14204 opened Jun 28, 2026 by eric-wieser Contributor • Draft
2
chore: delete unused C++ code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14203 opened Jun 28, 2026 by eric-wieser Contributor Loading…
4
feat: track libuv request refs to support thread finalization changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14202 opened Jun 27, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
fix: generalize equality @[spec] rules over their explicit arguments changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14197 opened Jun 26, 2026 by sgraf812 Contributor • Draft
2
feat: clarify warning for semireducible definitions of class type 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 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
#14196 opened Jun 26, 2026 by datokrat Contributor • Draft
2
feat: extensible frame inference for vcgen via @[frameproc] changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14195 opened Jun 26, 2026 by sgraf812 Contributor • Draft
2
perf: optimize ToJson derive handler 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
#14186 opened Jun 25, 2026 by Kha Member • Draft
4
perf: avoid spawning a new thread per worker output message toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14185 opened Jun 25, 2026 by Kha Member Loading…
6
[DO NOT MERGE] Backport incremental snapshots to v4.28 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14179 opened Jun 25, 2026 by Kha Member • Draft
chore: Claude: document the CI stage2 trigger in the stage2-olean-test skill 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
#14176 opened Jun 25, 2026 by Kha Member Loading…
2
fix: repair dead lean-manual:// links (Closes #14163) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14171 opened Jun 24, 2026 by attilavjda Loading…
1
4
chore: test adaptation PR CI builds-mathlib CI has verified that Mathlib builds against this PR downstream Request a downstream-lean4 adaptation 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
#14170 opened Jun 24, 2026 by Garmelon Contributor • Draft
3
fix: make Hoare Triple universe-polymorphic in its assertion type 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
#14168 opened Jun 24, 2026 by sgraf812 Contributor • Draft
2
ProTip! Filter pull requests by the default branch with base:master.