Issues

• decreasing_tactic fails for structure projections

  bug
  leanprover/lean4#16209 · Filter by author TwoFX opened on Nov 3, 2026
  2

• IO.FS.withTempDir segfaults when TMPDIR points to a missing directory

  leanprover/lean4#16202 · Filter by author douglaz opened on Nov 3, 2026

• With compiler.postponeCompile, leanir fails with `Unknown constant _private.Init.Data.Array.Basic.0.Array.mapMUnsafe.map on any use of Array.map`

  leanprover/lean4#16201 · Filter by author alpaylan opened on Nov 3, 2026

• PANIC "getOptions called inside a computation recording its dependencies" when logAt warns during instance synthesis (decide on BitVec.twoPow 276)

  leanprover/lean4#16197 · Filter by author alpaylan opened on Nov 2, 2026

• Confusing error when trying to derive instance for compound type

  bug
  leanprover/lean4#16189 · Filter by author FeldrinH opened on Nov 2, 2026

• Deprecations generate multiple try this: suggestions for rewrites at multiple locations

  bug
  leanprover/lean4#16184 · Filter by author grunweg opened on Nov 2, 2026

• RFC: initialise top-level constants lazily, as closed terms already are

  leanprover/lean4#16179 · Filter by author matthiasgoergens opened on Nov 2, 2026

• IO.sleep never returns while its thread is interrupted by frequent signals

  leanprover/lean4#16171 · Filter by author matthiasgoergens opened on Nov 2, 2026

• Kernel exhausts memory checking (x + BitVec.ofNat 64 C).toNat = … by rfl (the @[defeq] lemma BitVec.toNat_add), cost growing with the literal C

  leanprover/lean4#16170 · Filter by author alpaylan opened on Nov 2, 2026
  1

• Expose the logical range-loop body for kernel reduction in modules

  leanprover/lean4#16169 · Filter by author kim-em opened on Nov 2, 2026

• With compiler.extract_closed false, borrow inference treats string and big Nat literals as borrowed: use after free and wrong results

  code-generator
  leanprover/lean4#16160 · Filter by author alpaylan opened on Nov 1, 2026

• [4.34] simp rewriting of decide p = true (via core decide_eq_true_eq) changes term shape, breaking nested projections

  leanprover/lean4#16154 · Filter by author JaneConan opened on Nov 1, 2026
  1

• RFC: Improve Semantic Highlighting

  RFC
  leanprover/lean4#16150 · Filter by author RIvance opened on Nov 1, 2026
  1

• bug: String.fromUTF8Lossy does not follow the Unicode practice for U+FFFD substitution

  bug
  leanprover/lean4#16145 · Filter by author fgdorais opened on Nov 1, 2026

• RFC: re-enable the Web Assembly CI job

  leanprover/lean4#16134 · Filter by author basvandijk opened on Oct 31, 2026

• Universe approximation creates a cyclic level metavariable assignment and stack overflow

  bugelaboration
  leanprover/lean4#16125 · Filter by author kim-em opened on Oct 31, 2026
  

• Lake reuses an externally replaced .olean despite a current trace, including with --rehash

  leanprover/lean4#16123 · Filter by author VladimirMarko opened on Oct 30, 2026

• vcgen +jp: join points not shared after unfolding a definition; shared join hypotheses make discharge exponential

  bug
  leanprover/lean4#16122 · Filter by author govereau opened on Oct 30, 2026

• Std.Http: a valid UPDATEREDIRECTREF request gets 400 when a read ends inside the method name

  leanprover/lean4#16111 · Filter by author matthiasgoergens opened on Oct 30, 2026
  1

• module system: by exact h in an exposed definition leaves h in the exported body, and importers get a kernel error

  leanprover/lean4#16110 · Filter by author matthiasgoergens opened on Oct 30, 2026

• Task.bind leaks the inner task when the bind task is dropped while its function runs

  leanprover/lean4#16109 · Filter by author matthiasgoergens opened on Oct 30, 2026
  1

• decide on bounded quantifiers reaches maxRecDepth sooner since #15371

  leanprover/lean4#16108 · Filter by author matthiasgoergens opened on Oct 30, 2026

• Server: the reference index stores the parent declaration name once per usage location

  leanprover/lean4#16100 · Filter by author spitters opened on Oct 29, 2026

• Kernel performance regression checking computed projection applications (4.32.1 → 4.33.1, persists on nightly)

  leanprover/lean4#16088 · Filter by author whilo opened on Oct 29, 2026

• Lean reports a type error at a wrong source position

  bug
  leanprover/lean4#16084 · Filter by author fduxiao opened on Oct 29, 2026