Skip to content

Pull requests: leanprover/lean4

New pull request New
223 Open 5,488 Closed
223 Open 5,488 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore: CI: limit CCACHE_SIZE to 400MB release-ci Enable all CI checks for a PR, like is done for releases
#7922 opened Apr 11, 2025 by Kha Loading…
chore: move test 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
#7921 opened Apr 11, 2025 by leodemoura Loading…
1
feat: enable experimental module system in Init changelog-no Do not include this PR in the release changelog 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
#7919 opened Apr 11, 2025 by Kha Loading…
5
chore: stop taking constants from kernel env in synchronous case as well awaiting-mathlib We should not merge this until we have a successful Mathlib build force-mathlib-ci toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7915 opened Apr 11, 2025 by Kha Loading…
1
feat: lake: build by source path breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7909 opened Apr 11, 2025 by tydeu • Draft
1
1
feat: lake: track trace inputs & related fixes builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7906 opened Apr 10, 2025 by tydeu • Draft
1
feat: always show nat_lit, simpler hovers for OfNat literals breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7896 opened Apr 10, 2025 by kmill • Draft
1
feat: (experiment) use low priority for parent instances 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
#7894 opened Apr 10, 2025 by kmill • Draft
1
perf: use mimalloc with important C++ hash maps 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
#7868 opened Apr 8, 2025 by Kha Loading…
7
feat: add fast circuit for unsigned multiplication overflow detection fastUmulOverflow_eq and definitions
#7858 opened Apr 7, 2025 by luisacicolini • Draft
chore: adjust BEq classes awaiting-author Waiting for PR author to address issues breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7855 opened Apr 7, 2025 by Rob23oba Loading…
@TwoFX
16
feat: basic premise selection algorithm based on MePo toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7844 opened Apr 7, 2025 by kim-em • Draft
1
feat: allow omission of => ?_ in induction/cases tactics builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features, tactics, and metaprograms changes-stage0 Contains stage0 changes, merge manually using rebase toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7830 opened Apr 5, 2025 by kmill Loading…
1
feat: Add sorried lemmas about unions of Raw₀ awaiting-author Waiting for PR author to address issues
#7823 opened Apr 4, 2025 by Paul-Lez • Draft
@TwoFX
13
feat: some Option.filter lemmas builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7820 opened Apr 4, 2025 by TwoFX • Draft
1
refactor: more complete channel implementation for Std.Channel builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7819 opened Apr 4, 2025 by hargoniX Loading…
11
perf: avoid duplicate work in simp when there are bound variables builds-mathlib CI has verified that Mathlib builds against this PR P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7804 opened Apr 3, 2025 by JovanGerb Loading…
1
perf: missing (sync := true) toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7792 opened Apr 2, 2025 by Kha Loading…
3
chore: update to mimalloc 3.0.3 beta toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7786 opened Apr 2, 2025 by Kha • Draft
9
chore: add docstring to Simp.Methods.discharge? P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7779 opened Apr 1, 2025 by Paul-Lez Loading…
2
feat: Constructions for splitting and merging vectors of bitvectors changelog-library Library P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet.
#7754 opened Mar 31, 2025 by javra Loading…
10
fix: finalize libuv toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7752 opened Mar 31, 2025 by eric-wieser • Draft
1
5
feat: lake: builtin facet memoize toggle builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
#7738 opened Mar 30, 2025 by tydeu Loading…
3
perf: make isRfl lazy 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
#7719 opened Mar 29, 2025 by Kha Loading…
7
perf: add a bitblasting cache for bv_decide's substructure on top of the bvexpr one changelog-language Language features, tactics, and metaprograms
#7707 opened Mar 28, 2025 by hargoniX • Draft
ProTip! Updated in the last three days: updated:>2025-04-08.