Skip to content

Pull requests: leanprover/lean4

New pull request New
631 Open 10,854 Closed
631 Open 10,854 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

test: clean up tests writing to tracked files, prevent future violations release-ci Enable all CI checks for a PR, like is done for releases
#14772 opened Aug 13, 2026 by Kha Member Loading…
fix: look up local declarations in environments built by ofKernelEnv breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14771 opened Aug 13, 2026 by Kha Member • Draft
1
6
doc: fix typo in example of SourceInfo.synthetic toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14756 opened Aug 11, 2026 by ia0 Contributor Loading…
2
doc: fix typo in IterStep.skip toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14755 opened Aug 11, 2026 by ia0 Contributor Loading…
2
doc: fix imprecision in IO.FS.Stream.getLine and IO.FS.Handle.getLine toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14754 opened Aug 11, 2026 by ia0 Contributor Loading…
2
feat: grind reads a loop's measure into any well-founded type changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14753 opened Aug 11, 2026 by sgraf812 Contributor • Draft
2
doc: fix typo in Init.Data.Repr toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14750 opened Aug 11, 2026 by ia0 Contributor Loading…
2
feat: record code quality metrics from linters changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14748 opened Aug 11, 2026 by wkrozowski Contributor Loading…
fix: enable HWASAN support in the runtime changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14742 opened Aug 10, 2026 by eric-wieser Contributor Loading…
3
perf: don't type check if no let decls are being referenced toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14741 opened Aug 10, 2026 by Rob23oba Contributor • Draft
4
feat: generalize LE, LT and the Std order-predicate classes to Sort u changelog-library Library changes-stage0 Contains stage0 changes, merge manually using rebase force-mathlib-ci needs-update-stage0 stage 0 should be updated after merging this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14737 opened Aug 10, 2026 by sgraf812 Contributor • Draft
8
fix: don't error in defeq for missing unification hints 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
#14733 opened Aug 10, 2026 by Rob23oba Contributor Loading…
1
5
feat: cbv on arrays using a tree data structure 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
#14732 opened Aug 10, 2026 by Rob23oba Contributor • Draft
7
fix: lake: retry transient artifact transfer failures toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14725 opened Aug 10, 2026 by marcelolynch Contributor Loading…
1
2
feat: lake: support package code quality checks in lake lint changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14716 opened Aug 7, 2026 by wkrozowski Contributor Loading…
2
feat: always record per-declaration heartbeat costs with no performance degradation toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14712 opened Aug 7, 2026 by dennj Loading…
2
refactor: rework the vcgen frame procedure API around a commit callback 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
#14706 opened Aug 6, 2026 by sgraf812 Contributor • Draft
2
feat: add hint to deprecated linter changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14705 opened Aug 6, 2026 by wkrozowski Contributor Loading…
2
fix: format choice nodes from duplicate syntax without uncaught backtrack toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14696 opened Aug 5, 2026 by jcreinhold Contributor Loading…
1
2
fix: measure Format.align at the column the renderer uses toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14693 opened Aug 5, 2026 by jcreinhold Contributor Loading…
2
2
fix: preserve non-finite values in Float.scaleB builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI 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
#14690 opened Aug 5, 2026 by felix314159 Loading…
6
fix: report a missing spec for an un-steppable vcgen program head toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14688 opened Aug 5, 2026 by sgraf812 Contributor Loading…
2
feat: add linter for simp arguments triggering TC synthesis at every subterm awaiting-review Waiting for someone to review the 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
#14677 opened Aug 4, 2026 by sgraf812 Contributor Loading…
6
feat: lean_initializing builds-mathlib CI has verified that Mathlib builds against this PR changelog-compiler Compiler, runtime, and FFI 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
#14676 opened Aug 4, 2026 by tydeu Member Loading…
3
feat: use a computableExt instead of a noncomputableExt toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#14674 opened Aug 4, 2026 by Rob23oba Contributor • Draft
2
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.