repeat tactic: hover after `repeat` is confusing

Consider this example

partial def whileSome (f : α → Option α) (x : α) : α :=
  match f x with
  | none => x
  | some x' => whileSome f x'

axiom whileSome_eq.{u_1} {α : Type u_1} (f : α → Option α) (x : α) :
  whileSome f x =
    match f x with
    | none => x
    | some x' => whileSome f x'

example : whileSome (fun x => do guard (x < 10); pure (x+1)) 1 = 10 := by
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  rw [whileSome_eq]; simp [guard, failure] 
  done

example : whileSome (fun x => do guard (x < 10); pure (x+1)) 1 = 10 := by
  repeat (rw [whileSome_eq]; simp [guard, failure])

I first wrote the example with the repeated lines, and thought I could simplify it with repeat. Abut when I did that, the info view showed

mathlib-demo.lean:26:51
Tactic state
9 goals
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 2 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 3 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 4 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 5 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 6 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 7 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 8 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 9 = 10
⊢ whileSome (fun x => (if x < 10 then some () else none).bind fun x_1 => some (x + 1)) 10 = 10

and I thought I wasn’t done, and it left me very confused.

I tried repeat', tried minimizing the example, only to notice that indeed I was done! It’s just that while my cursor was on the last character of that line, the closing parens, it showed the intermediary goals.

With other tactics one is used to seeing the goal after the full tactic when the cursor is at the end of the line, even those that show something different and interesting in between (like rw […]).

I am not sure what, if anything, can be done here, maybe this is by design and consistent and just something that one has to learn when using repeat. But now that I debugged this I wonder if this was the reason for all the other times I used repeat and thought it didn’t work as expected.

Maybe repeat (…) could be special-cased (i.e. the parentheses).

Maybe this UX confusion will go away once we have more a clear “your proof is incomplete here” markers that would leave me in no doubt about whether the proof is done (e.g. discussed in https://github.com/leanprover/lean4/issues/4190#issuecomment-2114840176).

Versions

Lean 4.16.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the repeat (rw [whileSome_eq]; simp [guard, failure]) example and inspect the info view while the cursor is at the end of the tactic. Trace how intermediate goals are selected for hover display; done means a completed proof shows its final state rather than misleading intermediary goals.