Skip to content

Pull requests: leanprover/lean4

New pull request New
459 Open 9,515 Closed
459 Open 9,515 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: theorems are opaque 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
#12973 opened Mar 18, 2026 by nomeata • Draft
1
5
refactor: remove Lean.Environment.replay from core builds-mathlib CI has verified that Mathlib 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
#12972 opened Mar 18, 2026 by nomeata • Queued
1
2
feat: increase default stack size from 8MB to 1GB 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 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
#12971 opened Mar 18, 2026 by Kha Loading…
4
chore: speed up test suite slightly toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12969 opened Mar 18, 2026 by Garmelon Loading…
8
feat: New foundations for mvcgen tactic
#12965 opened Mar 18, 2026 by volodeyka Loading…
feat: add cbv annotations to iterators and strings 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
#12961 opened Mar 18, 2026 by wkrozowski • Draft
4
doc: fix a collection of docstring errors toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12959 opened Mar 18, 2026 by dfpetrin • Draft
2
feat: TR35 compatible format toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12958 opened Mar 18, 2026 by algebraic-dev • Draft
2
chore: check for empty PRs in CI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12956 opened Mar 17, 2026 by kim-em Loading…
2
fix: prevent induction/cases from swallowing diagnostics when using clause contains by toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12953 opened Mar 17, 2026 by Kha Loading…
1
2
demo
#12951 opened Mar 17, 2026 by datokrat • Draft
perf: remove simp annotation from imp_or_left_iff_true changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12949 opened Mar 17, 2026 by TwoFX • Draft
8
fix: record tasks from Command.logSnapshotTasks in snapshot tree 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
#12946 opened Mar 17, 2026 by Kha • Draft
4
perf: mark ReaderT context argument as borrow fast-ci Forces the use of large runners so that e.g. PR releases are created faster 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
#12942 opened Mar 17, 2026 by hargoniX • Draft
2
fix: add missing null check in olean loader; improve error messages changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12933 opened Mar 16, 2026 by martin-harmonic Loading…
3
perf: reduce no-op rebuild overhead toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12922 opened Mar 14, 2026 by Th0rgal Loading…
19
fix: make name (de)mangling more reliable builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-compiler Compiler, runtime, and FFI toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12916 opened Mar 13, 2026 by Rob23oba Loading…
2
feat: add rfl lemmas about ExceptCpsT.runK changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12912 opened Mar 13, 2026 by eric-wieser Loading…
3
fix: remove unused argument from ExceptCpsT.runK changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12911 opened Mar 13, 2026 by eric-wieser Loading…
3
experiment: normalize all instances 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
#12899 opened Mar 12, 2026 by Kha • Draft
4
experiment: normalize instances from def deriving 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
#12897 opened Mar 12, 2026 by Kha • Draft
11
experiment: normalize instances in inferInstanceAs 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
#12895 opened Mar 12, 2026 by Kha • Draft
20
feat: make Nat.strongRecOn and Nat.caseStrongRecOn computable 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
#12894 opened Mar 12, 2026 by Parcly-Taxel Loading…
15
test: add mvcgen' with <tac> and mvcgen' with grind to sym-based VCGen builds-manual CI has verified that the Lean Language Reference builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12893 opened Mar 11, 2026 by sgraf812 • Draft
2
chore: mark Pure.pure as match_pattern toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#12892 opened Mar 11, 2026 by eric-wieser Loading…
2
ProTip! Add no:assignee to see everything that’s not assigned.