Skip to content

Pull requests: leanprover/lean4

New pull request New
582 Open 10,088 Closed
582 Open 10,088 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

wrapInstance makes defeq checks at implicit
#13927 opened Jun 2, 2026 by datokrat Contributor • Draft
fix: dbgTraceIfShared in all non-linear situations changelog-compiler Compiler, runtime, and FFI
#13926 opened Jun 2, 2026 by hargoniX Contributor • Queued
feat: consolidate mvcgen' syntax changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13925 opened Jun 2, 2026 by sgraf812 Contributor Loading…
6
chore: extract stage2-build and ci-log-retrieval skills from CLAUDE.md 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
#13923 opened Jun 2, 2026 by Kha Member Loading…
2
test: make instance projections implicit-reducible by default toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13919 opened Jun 1, 2026 by datokrat Contributor • Draft
3
feat: add module syntax linters changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13917 opened Jun 1, 2026 by wkrozowski Contributor Loading…
2
feat: add FlattenBehavior to MessageData.group toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13914 opened Jun 1, 2026 by whxvd • Draft
2
feat: accept arbitrary doElems after ← changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13912 opened Jun 1, 2026 by sgraf812 Contributor • Draft
2
chore: deprecate Lean.Data.RBMap and Lean.Data.RBTree changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13908 opened May 31, 2026 by kim-em Collaborator Loading…
2
doc: remove circularity in #eval docstring toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13906 opened May 31, 2026 by epjnre Loading…
2
fix: recover theorem-backed grind? suggestions without regressing stable output changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13905 opened May 31, 2026 by peter941221 Loading…
4
perf: bump priority of Grind.IntModule.OfNatModule.ofNatModule 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
#13904 opened May 30, 2026 by hargoniX Contributor • Draft
6
feat: add HTTP Client changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13902 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add RedirectPlan for validating and following redirects changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13901 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
feat: add type class for replayable body types changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13900 opened May 30, 2026 by algebraic-dev Member Loading…
@algebraic-dev
2
perf: spawn child processes via libuv uv_spawn changelog-compiler Compiler, runtime, and FFI 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
#13898 opened May 30, 2026 by Kha Member • Draft
2
fix: respectTransparency (new mathlib) builds-mathlib CI has verified that Mathlib builds against this PR 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
#13895 opened May 29, 2026 by datokrat Contributor • Draft
7
feat: Void.get_mk builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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
#13894 opened May 29, 2026 by tydeu Member • Draft
5
feat: control environment linters with Lean.Option changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13893 opened May 29, 2026 by wkrozowski Contributor Loading…
9
doc: remove duplicated sentence in decide docstring 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
#13892 opened May 29, 2026 by brettkoonce Loading…
4
chore: CLAUDE.md: test failures that should be retried in stage 2 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
#13871 opened May 28, 2026 by Kha Member Loading…
2
feat: add Environment.hasExposedBody helper changelog-language Language features and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13868 opened May 28, 2026 by kim-em Collaborator Loading…
4
chore: update release scripts toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#13866 opened May 27, 2026 by Garmelon Contributor • Draft
2
feat: simp lemmas for LawfulApplicative 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
#13865 opened May 27, 2026 by frangio Contributor Loading…
3
feat: experimental cross-process jobserver via POSIX semaphore 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
#13856 opened May 26, 2026 by Kha Member • Draft
10
ProTip! no:milestone will show everything without a milestone.