Issues

Kernel: `is_def_eq` remains order-dependent via `is_def_eq_binding` right-bias and `m_eager_reduce` cache pollution

leanprover/lean4#15706 · opened

on Oct 15, 2026

Kernel: `check_recursors` uses `tcheck.infer(reduct)` (`infer_only = true`), leaving generated induction hypotheses `v` untypechecked

leanprover/lean4#15705 · opened

on Oct 15, 2026

Kernel soundness: unverified `consume_type_annotations` and parameter domain mismatch in `elim_only_at_universe_zero` allow large elimination from `Prop`

leanprover/lean4#15704 · opened

on Oct 15, 2026

`grind`: kernel error because `abstractGroundMismatches?` passes the abstracted terms in reverse order

leanprover/lean4#15700 · opened

on Oct 15, 2026

`lia`: kernel error in `eq_def_struct` with a dependent `Int` field (regression)

leanprover/lean4#15699 · opened

on Oct 15, 2026

grind: hypothesis treated as a match condition fails depending on hypothesis order (nested constructor pattern)

leanprover/lean4#15697 · opened

on Oct 14, 2026

1

autoImplicit auto-binds a name that collides with an existing out-of-scope declaration with only an editor inlay hint, no CLI/batch-visible diagnostic

leanprover/lean4#15694 · opened

on Oct 14, 2026

`IO.appPath` fails when `/proc` belongs to another PID namespace

leanprover/lean4#15692 · opened

on Oct 14, 2026

`vcgen`: unhelpful errors when migrating a `Std.Do` proof from `mvcgen`

leanprover/lean4#15691 · opened

on Oct 14, 2026

2

Kernel check slows down quadratically for `Nat` that are multiples of `2^64`

leanprover/lean4#15686 · opened

on Oct 14, 2026

2

"Bug in a `do` elaborator" in code combining conditionals and for loops

leanprover/lean4#15685 · opened

on Oct 14, 2026

`leanexport` UX

leanprover/lean4#15684 · opened

on Oct 14, 2026

`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`

leanprover/lean4#15683 · opened

on Oct 14, 2026

`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)

leanprover/lean4#15681 · opened

on Oct 14, 2026

`isExclusiveUnsafe` crashes (SIGSEGV) on scalar arguments such as a small `Nat`

leanprover/lean4#15677 · opened

on Oct 14, 2026

`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process group

leanprover/lean4#15674 · opened

on Oct 14, 2026

`IO.Process.spawn` with `inheritEnv := false` crashes the child on macOS when `env` sets a variable

leanprover/lean4#15662 · opened

on Oct 13, 2026

letToHave unifies types ignoring transparency seetings

leanprover/lean4#15661 · opened

on Oct 13, 2026

`lean --incr-save` never terminates on a file that elaborates in 3 s (`Finsupp.mk ... (fun x => by aesop)`, Mathlib)

leanprover/lean4#15660 · opened

on Oct 13, 2026

1

Diagnostics reused by `--incr-load` carry the saving file's path instead of the current file's path

leanprover/lean4#15658 · opened

on Oct 13, 2026

1

`--incr-save` on top of an `--incr-header-save` snapshot yields a snapshot that fails to load (`invalid 'import' command`) once the file has >= 3 commands

leanprover/lean4#15657 · opened

on Oct 13, 2026

1

`#print axioms` disagrees with the kept theorem body after a duplicate theorem import

leanprover/lean4#15652 · opened

on Oct 13, 2026

Parsing `.lean` and writing `.ilean` are quadratic in line length

leanprover/lean4#15646 · opened

on Oct 13, 2026

Windows: copy-on-write .olean mapping (FILE_MAP_COPY) charges the full size of all imported module files to commit (regression since v4.31.0-rc1)

leanprover/lean4#15644 · opened

on Oct 13, 2026

`leanchecker --from-export` rejects string and quotient rfl proof accepted by `Lean`

leanprover/lean4#15643 · opened

on Oct 13, 2026

1

Navigation Menu

Repository navigation

Issues

Kernel: `is_def_eq` remains order-dependent via `is_def_eq_binding` right-bias and `m_eager_reduce` cache pollution

Kernel: `check_recursors` uses `tcheck.infer(reduct)` (`infer_only = true`), leaving generated induction hypotheses `v` untypechecked

Kernel soundness: unverified `consume_type_annotations` and parameter domain mismatch in `elim_only_at_universe_zero` allow large elimination from `Prop`

`grind`: kernel error because `abstractGroundMismatches?` passes the abstracted terms in reverse order

`lia`: kernel error in `eq_def_struct` with a dependent `Int` field (regression)

grind: hypothesis treated as a match condition fails depending on hypothesis order (nested constructor pattern)

autoImplicit auto-binds a name that collides with an existing out-of-scope declaration with only an editor inlay hint, no CLI/batch-visible diagnostic

`IO.appPath` fails when `/proc` belongs to another PID namespace

`vcgen`: unhelpful errors when migrating a `Std.Do` proof from `mvcgen`

Kernel check slows down quadratically for `Nat` that are multiples of `2^64`

"Bug in a `do` elaborator" in code combining conditionals and for loops

`leanexport` UX

`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`

`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)

`isExclusiveUnsafe` crashes (SIGSEGV) on scalar arguments such as a small `Nat`

`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process group

`IO.Process.spawn` with `inheritEnv := false` crashes the child on macOS when `env` sets a variable

letToHave unifies types ignoring transparency seetings

`lean --incr-save` never terminates on a file that elaborates in 3 s (`Finsupp.mk ... (fun x => by aesop)`, Mathlib)

Diagnostics reused by `--incr-load` carry the saving file's path instead of the current file's path

`--incr-save` on top of an `--incr-header-save` snapshot yields a snapshot that fails to load (`invalid 'import' command`) once the file has >= 3 commands

`#print axioms` disagrees with the kept theorem body after a duplicate theorem import

Parsing `.lean` and writing `.ilean` are quadratic in line length

Windows: copy-on-write .olean mapping (FILE_MAP_COPY) charges the full size of all imported module files to commit (regression since v4.31.0-rc1)

`leanchecker --from-export` rejects string and quotient rfl proof accepted by `Lean`