Pull requests · leanprover/lean4

fix: dead locks and memory leaks in task manager finalization

#15743algebraic-dev opened

Oct 16, 2026

Member

perf: `grind` relates `(x - y).toNat` to `x.toNat` and `y.toNat` without `%`

#15739sgraf812 opened

Oct 16, 2026

Contributor

6

fix: `fun_cases` when a goal variable depends on a match discriminant

#15737sgraf812 opened

Oct 16, 2026

Contributor

2

fix: fix some typos in `BuiltinNotation` comment

#15736user202729 opened

Oct 16, 2026

Contributor

perf: populate the `Sym.simp` `grind` normalization theorems at attribute time

#15725leodemoura opened

Oct 16, 2026

Member

temp: claudified import profiling for testing

#15724thorimur opened

Oct 15, 2026

Contributor

3

refactor: drop redundant `inline` from `@[always_inline, inline]`

#15723user470750 opened

Oct 15, 2026

fix: parameterize `ST.RefPointed` to prevent unsafe cast

#15718Rob23oba opened

Oct 15, 2026

Contributor

feat: encode `a % k` as `a` in `lia` when `0 ≤ a < k`

#15716sgraf812 opened

Oct 15, 2026

Contributor

2

perf: lake: resolve a module's transitive import closure from one store snapshot

#15714zeldovich opened

Oct 15, 2026

perf: lake: read the build store without taking its ref

#15712zeldovich opened

Oct 15, 2026

2

fix: prevent order-dependent cache pollution in kernel is_def_eq

#15709gersh opened

Oct 15, 2026

1

fix: fully typecheck recursor computation rules in check_recursors

#15708gersh opened

Oct 15, 2026

1

fix: verify type annotations and parameter domains in inductive checking

#15707gersh opened

Oct 15, 2026

1

perf: alternatives to #15351

#15698arthur-adjedj opened

Oct 15, 2026

Contributor

9

fix: lake: fetch plugin and link facets on the fetching thread

#15696rbeauchamp opened

Oct 14, 2026

Contributor

1

perf: make column computations on long lines independent of the line length

#15695Kha opened

Oct 14, 2026

Member

4

perf: shard the interpreter's native symbol cache lock

#15693marcelolynch opened

Oct 14, 2026

Contributor

2

fix: `Sym.simp` reduces `match` on literal discriminants

#15690sgraf812 opened

Oct 14, 2026

Contributor

fix: make `unfold` on non-recursive definitions independent of `eq_def` realization

#15687Kha opened

Oct 14, 2026

Member

1

fix: elaborate the do continuation only once when contracting `pure ()`

#15682sgraf812 opened

Oct 14, 2026

Contributor

1

refactor: implement reference-counting deletion's cascade in Lean

#15676vincentqb opened

Oct 14, 2026

Contributor

perf: avoid the task-manager mutex when destroying pure tasks

#15673marcelolynch opened

Oct 14, 2026

Contributor

2

fix: fail libuv calls after the event loop is torn down

#15671algebraic-dev opened

Oct 14, 2026

Member

perf: reduce lock contention when unfolding imported constants

#15670marcelolynch opened

Oct 13, 2026

Contributor

4

Navigation Menu

Repository navigation

All pull requests

fix: dead locks and memory leaks in task manager finalization

perf: `grind` relates `(x - y).toNat` to `x.toNat` and `y.toNat` without `%`

fix: `fun_cases` when a goal variable depends on a match discriminant

fix: fix some typos in `BuiltinNotation` comment

perf: populate the `Sym.simp` `grind` normalization theorems at attribute time

temp: claudified import profiling for testing

refactor: drop redundant `inline` from `@[always_inline, inline]`

fix: parameterize `ST.RefPointed` to prevent unsafe cast

feat: encode `a % k` as `a` in `lia` when `0 ≤ a < k`

perf: lake: resolve a module's transitive import closure from one store snapshot

perf: lake: read the build store without taking its ref

fix: prevent order-dependent cache pollution in kernel is_def_eq

fix: fully typecheck recursor computation rules in check_recursors

fix: verify type annotations and parameter domains in inductive checking

perf: alternatives to #15351

fix: lake: fetch plugin and link facets on the fetching thread

perf: make column computations on long lines independent of the line length

perf: shard the interpreter's native symbol cache lock

fix: `Sym.simp` reduces `match` on literal discriminants

fix: make `unfold` on non-recursive definitions independent of `eq_def` realization

fix: elaborate the do continuation only once when contracting `pure ()`

refactor: implement reference-counting deletion's cascade in Lean

perf: avoid the task-manager mutex when destroying pure tasks

fix: fail libuv calls after the event loop is torn down

perf: reduce lock contention when unfolding imported constants