Skip to content

Pull requests: leanprover/lean4

New pull request New
278 Open 6,079 Closed
278 Open 6,079 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

docs(readme): update README.md toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8679 opened Jun 8, 2025 by 007vasy Loading…
2
feat: strengthen finIdxOf? lemmas changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8678 opened Jun 8, 2025 by eric-wieser Loading…
2
feat: allow structures to have non-bracketed binders awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8671 opened Jun 7, 2025 by cppio Loading…
3
fix: make unsafeBaseIO noinline changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8669 opened Jun 6, 2025 by zwarich Loading…
1
fix: make kabstract unify types before unifying terms breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8667 opened Jun 6, 2025 by kmill • Draft
1
perf: do not import non-meta IR changelog-language Language features, tactics, and metaprograms
#8666 opened Jun 6, 2025 by Kha • Draft
3
chore: do not expose imported non-meta IR to interpreter 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
#8664 opened Jun 6, 2025 by Kha • Draft
3
feat: warn.sorry option awaiting-review Waiting for someone to review the PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8662 opened Jun 6, 2025 by kmill Loading…
1
2
perf: update free_sized declaration to be compatible with glibc toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8661 opened Jun 6, 2025 by jcking Loading…
1
feat: meta phase restrictions changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8660 opened Jun 6, 2025 by Kha Loading…
1
feat: enable auto-implicits in lake math template changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8656 opened Jun 6, 2025 by mhuisi Loading…
2
feat: server-side for module hierarchy 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
#8654 opened Jun 6, 2025 by mhuisi Loading…
1
refactor: environment extension state splitting builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8653 opened Jun 6, 2025 by Kha Loading…
5
feat: pre-stage0 groundwork for error explanations builds-mathlib CI has verified that Mathlib builds against this PR 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
#8651 opened Jun 6, 2025 by jrr6 Loading…
2
feat: pre-stage0 groundwork for named error messages builds-mathlib CI has verified that Mathlib builds against this PR 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
#8649 opened Jun 6, 2025 by jrr6 Loading…
7
feat: Add getElem_unzip lemmas
#8644 opened Jun 5, 2025 by linesthatinterlace • Draft
3
chore: begin development cycle for v4.22.0 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
#8642 opened Jun 5, 2025 by Vierkantor Loading…
1
feat: add lean_setup_libuv for initializing required LIBUV components changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8636 opened Jun 4, 2025 by algebraic-dev Loading…
@algebraic-dev
2
feat: polymorphic ranges and slices changelog-library Library
#8632 opened Jun 4, 2025 by datokrat • Draft
2
fix: apply newlines before and after comments when formatting syntax changelog-pp Pretty printing
#8626 opened Jun 4, 2025 by kmill Loading…
1
chore: cleanup notes about grind in LRAT
#8623 opened Jun 4, 2025 by kim-em Loading…
1
fix: IO.Process.spawn on windows awaiting-review Waiting for someone to review the PR 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
#8612 opened Jun 3, 2025 by Rob23oba Loading…
2
1
chore: clarifications to release_checklist.md changelog-no Do not include this PR in the release changelog documentation Documentation improvement toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8586 opened Jun 2, 2025 by Vierkantor • Draft
1
fix: lake: test flakiness builds-mathlib CI has verified that Mathlib builds against this PR 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
#8580 opened Jun 1, 2025 by tydeu • Draft
1
feat: enable the new compiler by default changelog-compiler Compiler, runtime, and FFI force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#8577 opened Jun 1, 2025 by zwarich • Draft
4
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.