Skip to content

Pull requests: leanprover/lean4

New pull request New
589 Open 10,392 Closed
589 Open 10,392 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: 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
3
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
3
fix: pass the message to dbgTraceIfShared borrowed changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14272 opened Jul 4, 2026 by kim-em Collaborator Loading…
3
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 • Draft
4
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
chore: reduce namespace pollution changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14265 opened Jul 3, 2026 by TwoFX Member Loading…
4
feat: add hint to unusedVariables linter 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-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
chore: remove dead module Lean.Data.Lsp.Window 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
#14257 opened Jul 3, 2026 by TwoFX Member Loading…
2
chore: rename Int.Linear to Int.Internal.Linear changelog-library Library 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
#14255 opened Jul 3, 2026 by TwoFX Member • Draft
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
chore: CI: bump softprops/action-gh-release from 3.0.0 to 3.0.1 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14239 opened Jul 1, 2026 by dependabot Bot Loading…
2
chore: CI: bump msys2/setup-msys2 from 2.31.1 to 2.32.0 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14238 opened Jul 1, 2026 by dependabot Bot Loading…
2
chore: CI: bump actions/cache from 5 to 6 dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14237 opened Jul 1, 2026 by dependabot Bot Loading…
2
draft: don't unify instance-implicit args during instance synthesis 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 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
#14236 opened Jul 1, 2026 by datokrat Contributor • Draft
10
feat: lake: add revDiscovery policy to cache services changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14230 opened Jun 30, 2026 by marcelolynch Contributor Loading…
1
13
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
4
fix: fix vcgen frames feature for monads with multiple StateT transformers 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
#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 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
#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
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: support libuv finalization before task_manager changelog-library Library 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
#14202 opened Jun 27, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
ProTip! Follow long discussions with comments:>50.