RFC: Move the error message earlier on incomplete-tactic-followed-by-deindentation

[hrmacbeth]

This is intended as a proposal for discussion. When there is an incomplete tactic call, Lean considers the error as occurring in the first place afterwards where new text appears to make it malformed. This is done even in examples like the following, when the incomplete tactic call is followed by de-indentation, so the user's intention was very likely that the new (de-indented) text be unrelated to that tactic call.

theorem lem1 : True := by
  exact

theorem lem2 : True := sorry -- red underline ("expected term") on the word `theorem`

This is the same behaviour as in Lean 3, but the situation arose much more rarely there because usually there was a begin/end block or a comma to contain the error to a single line.

Proposal: if there is text following an incomplete tactic call which is the same or a lower indentation level, then Lean could treat the error as being located on the exact itself or in the space after it. (So in this case we are assuming that that later text wasn't supposed to be part of the tactic call.)

This proposal comes from Mario in a Zulip discussion; he notes there that this would seem to require a change within the core parser infrastructure / somewhere around the withPosition parser combinator.

[PatrickMassot]

This also goes wrong when you go in the other direction, supplying too many arguments to tactics. The simplest case could arise from mixing up exact and assumption:

example (P : Prop) (h : P) : P := by
  assumption P

which gives the error expected command since the proof is over after assumption and Lean tries to process whatever comes after this proof.

A nasty variation if you add an extraneous argument in a calc block:

example : 1 + 1 = 2 := by
  calc 1 + 1 = 1 + 1 := by rfl
  _ = 2 := by rfl [h]

example (P : Prop) (h : P) : P := by
  exact h

Here the error comes on line 5 and is expected :=.

[PatrickMassot]

Note that in my example everything would be much clearer if we simply went back to delimiting tactic proofs by begin/end.

[kbuzzard]

Here's an example in the wild of an experienced user being totally confused by this.

[Kha]

@kbuzzard It is not clear to me that this is the same class of error. Could you distill an MWE from that?

[kbuzzard]

Yes you're right, the thing I linked to is confusing but perhaps for a different reason.

Re this issue: I have just been telling my students to write by ... done and this seems to make the problem go away.

[PatrickMassot]

@hrmacbeth do you consider this issue is solved by #2393?

[PatrickMassot]

Both my examples from #1971 (comment) now have better error messages. The first one now says: unexpected identifier; expected command and the second one unexpected token '['; expected command. Maybe it would be even better to add "Maybe the previous command was completed earlier than you expected". But I'm not 100% sure this is better and, depending on all the situations this error can appear, it could be sometimes misleading.