maybe a cache bug?

Stream: general

[fonqL]

Lean version: 4.9.0-rc1
System: wsl, ubuntu 22.04
Vscode version: 1.84.2
mwe (update: a smaller example is in the following reply.)

def Vect (n: Nat) (A: Type u) := {l: List A // l.length = n}

def Vect.rep (n: Nat): Vect n Nat := ⟨List.replicate n 0, by simp⟩

def Vect.get (v: Vect n A) (i: Fin n): A :=
  let ⟨v, h⟩ := v
  v.get (h ▸ i)

set_option pp.proofs true in
theorem Vect.rep_zero: (Vect.rep (n+1)).get 0 = 0 := by
  simp [get, rep]
  show _ = 0
  show _ = 0
  -- ↑ just copy and paste
  generalize get.proof_1 (0 :: List.replicate n 0) (by simp; rfl) = h
  revert h
  -- apoidsfpoiasqhwe
  generalize hb: List.replicate n 0 = b
  replace hb := congrArg List.length hb
  simp at hb
  rw [hb]
  simp

Snipaste_2024-06-07_18-19-47.png

Note that the bug behavior is related to the comment in code, and it doesn't seem to be 100% triggered.

I speculate the bug is related to cache. If I change the code(just press Enter) before the theorem, InfoView will only show one goal. But I'm not sure whether the bug is related to vscode-extension or lean's incrementality.

[Kevin Buzzard]

(I can't reproduce on v4.8.0 BTW)

[Sebastian Ullrich]

Thanks, I can reproduce on master

[fonqL]

Now I find a smaller example. It is definitely trigger now, and is less relevant to the comments.

example: True := by
  show True
  -- ↑ just copy and paste
  -- It seems that the more lines of comments
  --  the more targets can be generated.
  -- It seems that the more lines of comments
  --  the more targets can be generated.
  -- It seems that the more lines of comments
  --  the more targets can be generated.

screen shot

[Sebastian Ullrich]

There is a fix up at lean#4395. Note that this is purely a UI issue, subsequent tactics are not affected by these ghost goals.