simp? suggestion creates broken code

Stream: lean4

[Ruben Van de Velde]

In vs code, given

def foo (a : Nat) : Nat := a + 1

@[simp]
theorem foo_______________________________________________________________________________ : foo 1 = 2 := rfl

example (h : foo 1 = 2) : True := by
  simp? at h
  trivial

gives

Try this: simp only [foo_______________________________________________________________________________] at h

but when clicking it, I get

  simp only [foo_______________________________________________________________________________] at
    h

and expected '*' or checkColGt. Only

  simp only [foo_______________________________________________________________________________]
    at h

with at on the next line works. Is this:

1. A bug in lean for not supporting at at the end of a line
2. A bug in lean for suggesting code that doesn't work
3. A bug outside of lean for reformatting the output badly

?

[Damiano Testa]

4. a bug in your theorem name.

[Eric Wieser]

A simpler repro:

import Lean

run_cmd do
  let stx ← `(tactic|
    simp only [__________________________________________________________________________________________________] at h)
  Lean.logInfo m!"Got: {stx}"

[Eric Wieser]

So the issue is that the formatter for the simp syntax doesn't round-trip with the parser

[Damiano Testa]

Maybe at and the targets should not be separable.

[Eric Wieser]

Weirdly, it's fine with *

[Eric Wieser]

import Lean

theorem _____________________________________________________________________________________________________________ : True = True := sorry

example (h : True) : True := by
  rw [_____________________________________________________________________________________________________________] at
    * -- ok

example (h : True) : True := by
  rw [_____________________________________________________________________________________________________________] at
    h -- not ok

example (h : True) : True := by
  rw [_____________________________________________________________________________________________________________]
    at h -- ok

[Eric Wieser]

So I think the parser/formatter for at is just screwy

[Ruben Van de Velde]

Damiano Testa said:

4. a bug in your theorem name.

(It also happens if you have multiple theorems that happen to combine to the right length)