Issues

• grind: kernel error when a BitVec width is defined with def

  bug
  leanprover/lean4#15857 · Filter by author Leo0506 opened on Oct 21, 2026

• LEAN ASSERTION VIOLATION File: src/library/instantiate_mvars.cpp Line: 801 !get_mvar_assignment(m_mctx, mvar_name(e))

  bug
  leanprover/lean4#15849 · Filter by author YuanchengJiang opened on Oct 21, 2026

• lake cache get resuses path for revisions mapping (regardless of scope)

  bug
  leanprover/lean4#15848 · Filter by author arajasek opened on Oct 21, 2026

• Std.Http: valid chunked request gets 400 when a read boundary falls inside a chunk extension or trailer

  leanprover/lean4#15840 · Filter by author eumemic opened on Oct 21, 2026

• RFC: lemmas relating ByteArray.foldlM to Array.foldlM

  leanprover/lean4#15834 · Filter by author ChristianMurphy opened on Oct 21, 2026

• Docstrings for well-founded recusion with multiple arguments can't refer to themselves

  bug
  leanprover/lean4#15828 · Filter by author robsimmons opened on Oct 20, 2026
  

• Lake: package dependency cycles load and build libraries, but every executable fails with "build cycle detected" — are package cycles supported?

  leanprover/lean4#15820 · Filter by author kmrasmussen opened on Oct 20, 2026

• LEAN_SCALAR_PTR_LITERAL truncates static scalar fields on 32-bit targets

  leanprover/lean4#15814 · Filter by author basvandijk opened on Oct 20, 2026

• Lake: dynamically constructed build cycle is not detected and hangs

  bug
  leanprover/lean4#15810 · Filter by author dranov opened on Oct 20, 2026

• Lake: concurrent fetch from running jobs builds the same target more than once

  bug
  leanprover/lean4#15809 · Filter by author dranov opened on Oct 20, 2026
  1

• Lake: collectArray, mixArray, collectVector, collectList, and mixList are quadratic

  bug
  leanprover/lean4#15808 · Filter by author dranov opened on Oct 20, 2026

• Windows: intermittent stack-cookie failure (0xC0000409) in uv__tcp_connect with Std.Async.TCP connect

  leanprover/lean4#15807 · Filter by author gijzelaerr opened on Oct 20, 2026

• RFC: evaluator-owned accepted statements for conditional Comparator matches

  leanprover/lean4#15800 · Filter by author kimihiro64 opened on Oct 19, 2026
  5

• Lake: transDeps misses a transitive dependency (and its extern_lib) depending on the order of requires

  bug
  leanprover/lean4#15798 · Filter by author kmrasmussen opened on Oct 19, 2026

• Partial fixpoints do not generalize arguments properly in a module

  bug
  leanprover/lean4#15777 · Filter by author hgoldstein95 opened on Oct 19, 2026
  1

• Instance search: pruning an instance-typed mvar under a binder is rejected (regression from #14624)

  bug
  leanprover/lean4#15776 · Filter by author lzy0505 opened on Oct 19, 2026
  3

• Constructor reuse regression due to JpCases change

  bug
  leanprover/lean4#15771 · Filter by author szch79 opened on Oct 19, 2026
  1

• RFC: Wait on a C library's socket in Std.Async

  leanprover/lean4#15769 · Filter by author ChristianMurphy opened on Oct 19, 2026

• initialize of a function-typed constant: initialiser is skipped in compiled code and every call reaches unreachable (or an undefined symbol)

  bug
  leanprover/lean4#15768 · Filter by author chrisdwalton opened on Oct 18, 2026

• lake update --keep-toolchain lets a dependency's manifest override the root package's own require

  bug
  leanprover/lean4#15761 · Filter by author paulbutcher opened on Oct 18, 2026

• Sym rewrite proofs re-evaluate match discriminants when preprocessing changes the rule statement

  bug
  leanprover/lean4#15759 · Filter by author Kha opened on Oct 18, 2026

• set_option trace.Elab.info true on some antiquotation leads to Error pretty printing syntax: Unknown constant ident.antiquot.

  bug
  leanprover/lean4#15757 · Filter by author user202729 opened on Oct 18, 2026

• RFC: native Windows support for lake check sandboxing

  leanprover/lean4#15756 · Filter by author Puthranps opened on Oct 18, 2026
  2

• simp generates and tries every match equation on a stuck match, which is quadratic and bloats .olean files

  leanprover/lean4#15754 · Filter by author kevaundray opened on Oct 18, 2026

• "Cannot derive functional induction principle … still depends on" when a match is wrapped in an applied lambda and recurses under >>=

  bug
  leanprover/lean4#15749 · Filter by author josevalim opened on Oct 17, 2026
  1