Search results

shake --fix non-idempotency caused when modules are loaded via IR

bugSomething isn't workingSomething isn't working

Status: Open.

#13599 In leanprover/lean4;

· bryangingechen opened on May 1, 2026

Intermittent panic in lake build on Task.get

bugSomething isn't workingSomething isn't working

LakeLake related issueLake related issue

Status: Open.

#13598 In leanprover/lean4;

· david-christiansen opened on May 1, 2026

simp? returns unuseful lemmas

bugSomething isn't workingSomething isn't working

Status: Open.

#13592 In leanprover/lean4;

· b-mehta opened on May 1, 2026

lean --error does not result in a non-zero exit code

bugSomething isn't workingSomething isn't working

Status: Open.

#13588 In leanprover/lean4;

· eric-wieser opened on Apr 30, 2026

set_option diagnostics true fails with 'Unknown constant' on private _sparseCasesOn_* / match_* helpers in module mode

Status: Open.

#13581 In leanprover/lean4;

· kim-em opened on Apr 30, 2026

lia fails with "(kernel) application type mismatch"

bugSomething isn't workingSomething isn't working

Status: Open.

#13572 In leanprover/lean4;

· andres-erbsen opened on Apr 29, 2026

Inconsistent behavior in typeclass resolution (local vs top-level instance)

bugSomething isn't workingSomething isn't working

Status: Open.

#13571 In leanprover/lean4;

· TWal opened on Apr 29, 2026

set_option maxErrors does not work

bugSomething isn't workingSomething isn't working

Status: Open.

#13570 In leanprover/lean4;

· andres-erbsen opened on Apr 29, 2026

Unexpected ellision of constructor paramete/arguments.

bugSomething isn't workingSomething isn't working

Status: Open.

#13568 In leanprover/lean4;

· tinganho opened on Apr 29, 2026

BitVec.ofBoolListLE stack overflow for large lists

Status: Open.

#13561 In leanprover/lean4;

· adomasbaliuka opened on Apr 28, 2026

Sym.Simp.EvalGround produces kernel-rejected proofs when typeclass instances are shadowed

bugSomething isn't workingSomething isn't working

Status: Open.

#13544 In leanprover/lean4;

· wkrozowski opened on Apr 27, 2026

Please, provide a way to ensure that given function is panic-free. For example, by making panic opaque

bugSomething isn't workingSomething isn't working

Status: Open.

#13515 In leanprover/lean4;

· safinaskar opened on Apr 23, 2026