declaration has free variable with v4.25.0-rc2

Stream: general

[pandaman]

I got (kernel) declaration has free variables 'insert._proof_2' when upgrading to v4.25.0-rc2. Here is a minimized example:

#eval Lean.versionString

structure SparseSet (n : Nat) where
  count : Nat
  dense : Vector (Fin n) n
  sparse : Vector (Fin n) n
  -- sparse_dense : ∀ i : Fin n, i < count → sparse[dense[i.val].val] = i
  -- le_count : count ≤ n

def insert {n : Nat} (s : SparseSet n) (i : Fin n) : SparseSet n :=
  let ⟨count, dense, sparse⟩ := s
  have isLt : count < n := sorry
  let dense' := dense.set count i
  have sparse_dense' (j : Fin n) (h : j < count + 1) : sparse[dense'[j]] = j := by
    sorry
  ⟨count + 1, dense', sparse⟩

It seems the nightly has already fixed the issue. Will the fix get backported to v4.25.0?

[Kim Morrison]

@pandaman, could you try to identify which PR fixed your problem? Without that, there's nothing to backport.

[pandaman]

Do we have pre-built compiler artifacts? I can try bisecting them.

[Kim Morrison]

Yes, you can set the contents of lean-toolchain to e.g. leanprover/lean4:nightly-2025-10-27. These form a linear chain, so should be bisectable. (Although not out-of-the-box by git bisect.)

For individual PRs, there is usually, but not always, a toolchain available of the form leanprover/lean4-pr-releases:pr-release-10967.

[pandaman]

The issue was introduced by leanprover/lean4:nightly-2025-10-03 and fixed by leanprover/lean4:nightly-2025-10-25. I haven't investigated which commit was the culprit.

Log

Phase 1: Bisecting regression (2025-09-02 to 2025-10-10)

• [x] leanprover/lean4:nightly-2025-09-02: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-09-21: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-09-30: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-10-02: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-10-03: Build failed with (kernel) declaration has free variables 'insert._proof_2'
• [x] leanprover/lean4:nightly-2025-10-05: Build failed with (kernel) declaration has free variables 'insert._proof_2'
• [x] leanprover/lean4:nightly-2025-10-10: Build failed with (kernel) declaration has free variables 'insert._proof_2'

Phase 2: Bisecting fix (2025-10-10 to 2025-10-27)

• [x] leanprover/lean4:nightly-2025-10-18: Build failed with (kernel) declaration has free variables 'insert._proof_2'
• [x] leanprover/lean4:nightly-2025-10-22: Build failed with (kernel) declaration has free variables 'insert._proof_2'
• [x] leanprover/lean4:nightly-2025-10-24: Build failed with (kernel) declaration has free variables 'insert._proof_2'
• [x] leanprover/lean4:nightly-2025-10-25: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-10-26: Build succeeded (sorry is ok)
• [x] leanprover/lean4:nightly-2025-10-27: Build succeeded (sorry is ok)

Result

Regression introduced on: 2025-10-03 (nightly-2025-10-03)
The fix was introduced on: 2025-10-25 (nightly-2025-10-25)

[Markus Himmel]

Commits in 2025-10-03:

• 643da1e test: disable flaky tests (lean4#10665)
• 3d75c2c fix: eliminate potential source of inlay hint flakiness (lean4#10664)
• b979fa0 fix: verso docstring {name} role suggestion overload (lean4#10663)
• 288b7d2 chore: further cleanup from shaking Init (lean4#10658)
• 5c707d9 chore: rename Stream to Std.Stream (lean4#10645)
• 5a2e46b fix: equational theorem generation: avoid reducing at transparency all (lean4#10654)
• 24c86fc fix: improve error message for mstart when goal is not a Prop (lean4#10650)
• d171605 chore: module system fixes and refinements from Mathlib porting (lean4#10643)
• 89686fc refactor: replace PRange shape α with Rcc α and eight other types (lean4#10319)

Commits in 2025-10-25:

• d5ca0c7 fix: bug in cutsat model construction (lean4#10951)
• 3c2ab0f feat: model-based theory combination tactic and action (lean4#10950)
• 1643fd7 fix: finish? checks whether solver propagation steps are needed (lean4#10949)
• 53442d4 feat: finish? produces partial tactic scripts with sorry (lean4#10948)
• 96bace5 fix: run enableRealizationsForConst on sizeOf decls (lean4#10944)
• b0127e0 chore: final module system fixes and refinements for initial Mathlib porting (lean4#10869)
• e71d0ab test: test case for #10775 (lean4#10943)
• a6d50a6 fix: Meta.Closure: topologically sort abstracted vars (lean4#10926)
• dec0076 chore: fix C++ warning (lean4#10922)
• 1145498 fix: regression from ST redefinition (lean4#10940)

Out of those, lean4#10926 fixes lean4#10705, which has a similar error message.

[Markus Himmel]

Yes, the error is fixed on leanprover/lean4-pr-releases:pr-release-10926. So lean4#10926 might be a candidate for backporting to the 4.25 branch.

[Kim Morrison]

I've added the backport-v4.25 label. A bot will hopefully do the rest now!

[pandaman]

Thank you!

[Eric Wieser]

lean4#10954 might also be worth backporting