Small UX issue: cursor at `· |` doesn't display focused goal

Stream: lean4

[Thomas Murrills]

I notice often that when writing a tactic proof, if I focus a goal with ·, I don't see the goal I've just focused. Inspecting the situation more closely, if | represents my text cursor, I find that ·| does display the goal, but · | doesn't—or, worse, it displays the wrong goal (the next one).

This whitespace issue generally wouldn't matter, except that typing \.<space> is an extremely common way to enter ·, and it leaves your cursor in the latter, un- or misinformative state (· |). So this "broken" state is one that users encounter quite frequently (well, at least, assuming I'm not alone in typing characters like this in VS code!).

Examples:

theorem foo (A B : Prop) (a : A) (b : B) : A ∧ B := by
  constructor
  · -- displays next goal (`B`)

theorem foo (A B : Prop) (a : A) (b : B) : A ∧ B := by
  constructor
  · exact a
  · --displays 'no goals' above a list of unsolved goals

I'm not expecting this to even be able to be changed soon given that core isn't moving, but thought I'd bring it up here for the record and see if people think this is solvable.

(Note: a similar issue (though possibly different in cause) occurs when typing (by ) to fill in an argument in a term.)

[Mario Carneiro]

yes this is a known issue, it is caused by the fact that a tacticSeq can't be empty

[Kevin Buzzard]

Did someone file an issue? I think this is confusing for users (it was certainly confusing for me).

[Mario Carneiro]

no issue AFAIK

[Mario Carneiro]

but @Sebastian Ullrich and I have discussed this on previous zulip threads

[Mario Carneiro]

the earlier version of the issue was something like

example : A := by
  have : B := by
    |
  simp

showing A as the goal at the | rather than B

[Mario Carneiro]

I think this was fixed, but not by making empty tactic sequences legal so minor variations on the example are still broken, like

example : A := by
  have : B := by

  have : C := by
    |
  simp

[Mario Carneiro]

Also empty · has some surprising parse behavior:

example : 0 = 0 ∧ 1 = 1 := by -- 1 = 1 goal unsolved
  constructor
  ·
  · exact Eq.refl 1 -- expected proof of 0 = 0

[James Gallicchio]

I wonder if we can make the UI for parse errors a bit more annoying/loud, to encourage people always writing sorry in places where a tactic is expected to go. I almost feel like parse error should lead to no goal state output, to kinda indicate to people "you wrote a thing that is malformed, give me good syntax first"

[James Gallicchio]

and that also would incentivize better autocompletion/hole management stuff in the VS Code plugin :P

[Mario Carneiro]

James Gallicchio said:

I wonder if we can make the UI for parse errors a bit more annoying/loud, to encourage people always writing sorry in places where a tactic is expected to go. I almost feel like parse error should lead to no goal state output, to kinda indicate to people "you wrote a thing that is malformed, give me good syntax first"

That's what lean 3 did and it was horrible

[Mario Carneiro]

it didn't help that the error message was something really obscure sounding like "sync failed"

[Mario Carneiro]

Note that my last example is not even a parse error. The reason there are those errors is because it is actually well formed and was interpreted as

example : 0 = 0 ∧ 1 = 1 := by -- 1 = 1 goal unsolved
  constructor
  · · exact Eq.refl 1 -- expected proof of 0 = 0

[James Gallicchio]

the lean4 messages are .. I guess slightly more specific, but stuff like this is not very helpful: image.png

[Mario Carneiro]

it's hard to give better parse errors than that

[Mario Carneiro]

at least generically

[James Gallicchio]

Mario Carneiro said:

Note that my last example is not even a parse error

I'm guessing we'd want that to be a parse error, and there should probably be a way to make it a parse error

[Mario Carneiro]

I would like it to be interpreted as two blocks

[Mario Carneiro]

not doing so is what causes the error that Thomas noted

[Sebastian Ullrich]

Mario Carneiro said:

it's hard to give better parse errors than that

Replacing "strict indentation" with "indented tactic sequence" or something like that at least would not be hard

[Sebastian Ullrich]

It looks like · is missing that very indentation check -- otherwise it should not be able to coalesce two cdots like that

[Sebastian Ullrich]

With both fixed, the second cdot becomes this parse error image.png

[Sebastian Ullrich]

I pushed these two small fixes, the original issue with the space after cdot turned out to be a bit more complicated

[Sebastian Ullrich]

@Mario Carneiro As shown in the screenshot, we use a token antiquotation to show the focused state on the cdot. This works fine if the cursor is adjacent to the token. Usually the language server also shows the same goal when you are inside the whitespace trailing a tactic info. But the canonical info created by the antiquotation does not possess trailing information, only original does! I really don't know whether adding (leading and?) trailing whitespace (or only length) to synthetic is the right solution. If it is an issue quite specific to cdot, it would probably be better to convert it to an elaborator and apply the info manually.

[Mario Carneiro]

Maybe the lookup just needs to be adjusted? If you are in a trailing whitespace, you should still be able to find the original token it trails in the tree, and then you can report tactic info for that position, including synthetic nodes

[Sebastian Ullrich]

That could work... but InfoTree.goalsAt? is alreay more complicated than I'd like