Skip to content

Pull requests: leanprover/lean4

New pull request New
483 Open 9,741 Closed
483 Open 9,741 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

feat: Runtime.hold changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13270 opened Apr 3, 2026 by tydeu Loading…
2
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 toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13260 opened Apr 2, 2026 by mhuisi • Draft
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 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
#13239 opened Apr 1, 2026 by Kha Loading…
3
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
fix: match stub signature of lean_uv_dns_get_info to real implementation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13234 opened Apr 1, 2026 by kjsdesigns Loading…
2
fix: add missing release() and adopt_lock_t to single-threaded unique_lock stub toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13233 opened Apr 1, 2026 by kjsdesigns Loading…
2
fix: add amortized checkSystem to LCNF simp changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13231 opened Apr 1, 2026 by nomeata • Draft
8
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
feat: add warning when applying global attribute using in 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 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
#13223 opened Mar 31, 2026 by wkrozowski Loading…
8
feat: add optional check_system interval monitoring 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
#13212 opened Mar 31, 2026 by nomeata • Draft
7
feat: verifiable repeat/while loops changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13209 opened Mar 31, 2026 by sgraf812 • Draft
7
feat: add try? => tac syntax and fix asTask subtask cancellation 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
#13206 opened Mar 31, 2026 by nomeata • Draft
2
feat: add List.prod, Array.prod, and Vector.prod changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13200 opened Mar 31, 2026 by kim-em Loading…
2
fix: handle numerals in non-tail positions of cutsat polynomials changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13199 opened Mar 31, 2026 by kim-em Loading…
2
fix: docstring errors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13198 opened Mar 30, 2026 by dfpetrin Loading…
3
ProTip! no:milestone will show everything without a milestone.