bug with spacing

Stream: lean4

[Kenny Lau]

theorem foo (L : List Nat) : True := by
  induction L with
  | nil => trivial -- start here

1. delete the comment -- start here
2. add a newline
3. type | cons => trivial
4. observe that lean complains that cons hasn't been provided
5. add a space before | cons and then delete the space
6. it's now magically fixed

[Kenny Lau]

image.png

[Kenny Lau]

(tested on live lean)

[Aaron Liu]

I had the same problem which sometimes I encounter it and sometimes it's fine, didn't think it was serious enough to report

[Kim Morrison]

@Kenny Lau, can you please open an issue?

[Kenny Lau]

Kim Morrison said:

Kenny Lau, can you please open an issue?

lean4#10847

[Robin Arnez]

That was lean4#10679, wasn't it?

[Kenny Lau]

but i tested it against a version after that date

[Kenny Lau]

the description is different, the one you linked is saying that the error message stays after removing the alternative, mine says that the error message appears after adding the alternative

[Kenny Lau]

which, if you think about it, how can there be an error message in the first place if there is an "offending alternative"?? that's my bug i think

[Robin Arnez]

I've had this problem before but I can't seem to reproduce it with your steps. You're probably right that this is still a problem but maybe there is a better way to reproduce it?

[Kenny Lau]

did you delete the comment?

[Sebastian Ullrich]

I have a reproducer

[Robin Arnez]

Maybe I misunderstood something but:

1. open in Lean 4 playground
2. put | cons => trivial into the clipboard
3. select -- start here
4. backspace
5. enter
6. paste

causes no error to occur. I think a better repro is:

theorem foo (L : List Nat) : True := by
  induction L with
  | nil => trivial

1. Type a single | at the end of the last line.
2. Wait until the error appears.
3. Write cons => trivial => The error is still there
4. Add a space before the | => The error disappears

[Sebastian Ullrich]

lean#10848, a partial oversight from lean#10679