Skip to content

Pull requests: leanprover/lean4

New pull request New
490 Open 9,765 Closed
490 Open 9,765 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: make delta-derived Prop-valued instances theorems changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13304 opened Apr 7, 2026 by kim-em Loading…
1
2
refactor: make CancelToken Promise-based merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13303 opened Apr 7, 2026 by nomeata • Draft
2
fix: handle flattened inheritance in wrapInstance 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
#13302 opened Apr 7, 2026 by Kha • Draft
3
feat: add try? => tac syntax and parallel cancellation test 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
#13301 opened Apr 7, 2026 by nomeata Loading…
2
fix: guard libuv symbols in io.cpp for Emscripten WASM builds (#6817) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13298 opened Apr 7, 2026 by kjsdesigns Loading…
1
2
fix: add missing release() to single-thread unique_lock stub toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13297 opened Apr 7, 2026 by kjsdesigns Loading…
3
chore: use --wfail for core CI build 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
#13294 opened Apr 7, 2026 by tydeu Loading…
2
chore: debug mismatch w/ CI lake cache 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
#13292 opened Apr 6, 2026 by tydeu • Draft
3
feat: enable backward.isDefEq.respectTransparency.types by default 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
#13283 opened Apr 5, 2026 by leodemoura Loading…
5
chore: preparatory changes for removing defeq transparency bump 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-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
#13279 opened Apr 4, 2026 by leodemoura Loading…
2
feat: new, continuation-based, repeat loop with verification potential toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13278 opened Apr 4, 2026 by Rob23oba • Draft
4
feat: use functions for match motives changelog-language Language features and metaprograms
#13264 opened Apr 2, 2026 by kmill Loading…
1
1
feat: allow field notation to use explicit universe levels changelog-language Language features and metaprograms
#13262 opened Apr 2, 2026 by kmill Loading…
1
feat: server-side support for incremental diagnostics 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
#13260 opened Apr 2, 2026 by mhuisi Loading…
2
feat: guard against variables in head positions of lhs of simp theorems changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13259 opened Apr 2, 2026 by wkrozowski • Draft
2
perf: replace global task_finished_cv with per-task waiter notifications 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
#13256 opened Apr 2, 2026 by Kha • Draft
4
perf: skip mutex in deactivate_task for finished tasks 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
#13254 opened Apr 2, 2026 by Kha • Draft
7
fix: make Name.cmp sort lexicographically from the beginning 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
#13251 opened Apr 2, 2026 by Kha • Draft
4
chore: CI: bump dawidd6/action-download-artifact from 11 to 19 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
#13248 opened Apr 2, 2026 by dependabot bot Loading…
2
chore: CI: bump actions/create-github-app-token from 2.0.2 to 3.0.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
#13247 opened Apr 2, 2026 by dependabot bot Loading…
2
chore: CI: bump marocchino/sticky-pull-request-comment from 2 to 3 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
#13246 opened Apr 2, 2026 by dependabot bot Loading…
2
feat: make Function generalized field notation more usable 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 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
#13244 opened Apr 1, 2026 by kmill Loading…
4
fix: respect visibility in initialize/builtin_initialize 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 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
#13239 opened Apr 1, 2026 by Kha Loading…
4
feat: check if addInstance target type is class 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 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
#13237 opened Apr 1, 2026 by wkrozowski Loading…
4
feat: require indentation in commands, allow empty tactic sequences builds-mathlib CI has verified that Mathlib builds against this PR 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
#13229 opened Apr 1, 2026 by nomeata Loading…
9
ProTip! Filter pull requests by the default branch with base:master.