All issues

Search results

module system: public theorems added by metaprograms can mention private auxiliary proofs (_private.M.0.*._proof_N), which importing module files cannot see

Status: Open.

#15393 In leanprover/lean4;

· marcelolynch opened on Sep 28, 2026

first grind +suggestions / try? takes 12 s with import Lean and minutes with import Mathlib since v4.35.0-rc2 (#15159)

Status: Open.

#15392 In leanprover/lean4;

· marcelolynch opened on Sep 28, 2026

grind: Application type mismatch on cpop of a let-bound BitVec

bugSomething isn't workingSomething isn't working

Status: Open.

#15388 In leanprover/lean4;

· luigirinaldi opened on Sep 28, 2026

bv_decide no longer reifies a BitVec atom reached through a @[reducible] accessor over a structure field whose width is computed by a def (regression in v4.34.0)

Status: Open.

#15368 In leanprover/lean4;

· Calgooon opened on Sep 27, 2026

Compiler PANIC in ExplicitBoxing when an auto-generated SizeOf instance reaches codegen (regression since 4.28)

bugSomething isn't workingSomething isn't working

Status: Open.

#15346 In leanprover/lean4;

· rvs314 opened on Sep 26, 2026

getMainModule breaks when accessing files through URIs with #-fragments

bugSomething isn't workingSomething isn't working

Status: Open.

#15342 In leanprover/lean4;

· thorimur opened on Sep 26, 2026

The test lake/tests/cacheTransfer fails

Status: Open.

#15335 In leanprover/lean4;

· yurivict opened on Sep 25, 2026

Tests don't respect the CTEST_PARALLEL_LEVEL environment variable

Status: Open.

#15334 In leanprover/lean4;

· yurivict opened on Sep 25, 2026

Missed specialization leading to bad code

bugSomething isn't workingSomething isn't working

code-generatorThis issue is with the code generatorThis issue is with the code generator

Status: Open.

#15328 In leanprover/lean4;

· TwoFX opened on Sep 25, 2026

Inconsistency in functions handling private names

bugSomething isn't workingSomething isn't working

Status: Open.

#15308 In leanprover/lean4;

· Rob23oba opened on Sep 24, 2026

Anonymous instances are sometimes silently not created

bugSomething isn't workingSomething isn't working

Status: Open.

#15302 In leanprover/lean4;

· TwoFX opened on Sep 24, 2026

Type ascription with autoParam under ∀ᵐ times out

bugSomething isn't workingSomething isn't working

Status: Open.

#15284 In leanprover/lean4;

· liu-junming opened on Sep 23, 2026