InfoView hides goal/hypotheses when tactic incomplete

Stream: new members

[James Pollard]

Hi, I'm using Lean4 through VS Code, and I'm finding that the InfoView is too "eager" to hide the goal/hypotheses when I have an error. Trivial example:

example : 1 = 1 := by
  apply rfl

If I remove the final l of rfl, I get this:
image.png

Note that it considers there to be "no goal".

Strangely, this only occurs for some categories of error: an unknown tactic won't hide the goal/hypothesis.

For a more complicated proof state this is quite unhelpful since it usually manifests when I'm trying to remember the name of a hypothesis or variable to type.

I'm aware that I can pause the InfoView, but this is a bit annoying to have to do manually. Are there any knobs I can use to change this behaviour?

[Aaron Liu]

you can pause the infoview

[James Pollard]

Yup, I've tried this (mentioned in the original message), but it's quite annoying to have to do this ~continuously.

[James Pollard]

I'm not sure why Lean considers there to be no goal when I have a "broken" instance of a tactic?

[Aaron Liu]

the reason there is no goal

[Aaron Liu]

is that the tactic elaborates parses successfully

[Aaron Liu]

and the error handling inserts a synthetic sorry

[Aaron Liu]

and apply uses this to close the goal

[Aaron Liu]

even though there is an error

[Aaron Liu]

you can try looking at the expected type window instead maybe?

[James Pollard]

and the error handling inserts a synthetic sorry

Ah I see, thanks

[James Pollard]

you can try looking at the expected type window instead maybe?

I think this helps for the goal, but not the hypotheses.

[Aaron Liu]

it should show the entire context

[James Pollard]

Checking

[James Pollard]

Ah yes I see. Unfortunately it disappears when the error appears :/

[James Pollard]

Ok, I guess I can get used to the pause approach

[James Pollard]

From memory Proof General + Roqc was "better" at this, but I haven't touched it for a while.

[James Pollard]

Possibly because it required you to manually advance to a particular part of the proof-script rather than following the cursor?

[Marc Huisinga]

This is lean4#4181 (or more specifically, lean4#7136). I've added your example to the issue.

[Mirek Olšák]

James Pollard said:

Possibly because it required you to manually advance to a particular part of the proof-script rather than following the cursor?

Absolutely! Despite all other Rocq's inconveniences, the proof state is so much more under control there.

[Mirek Olšák]

Actually, could Lean do the same as Rocq? That is

• Obvious syntax highlight of where the current proofstate is (iirc, it slightly changes the background color of the entire document before proofstate).
• Shortcuts for user-controlled moving of this point, independent of the cursor (move one tactic forward, one tactic backward, jump to the cursor).

[Mirek Olšák]

It should be just a matter of keeping two cursors in VS Code, with a specific display of one, and jumping with it according to the tactic goal data already stored along the document. No?

[Mirek Olšák]

The pinned view is actually kind of a cursor / marker, so all we need is just display nicely the position of the pin in the editor, and move it conveniently. I can try to hack the VS Code extension with some AI :-).

[Marc Huisinga]

I would really prefer to see whether we can make some progress on lean4#4181 before we add another mode of interaction to the Lean VS Code extension.

[Mirek Olšák]

In the end, I don't think it is another mode, just a better pin :-).

[Mirek Olšák]

Visible & movable -- reasonable expectations I would say.

[Mirek Olšák]

I see the effort of stabilizing tactic output less principled than giving user more control over which state to see. When a user is typing a tactic, he is not expecting the tactic being executed in the middle of writing, and seeing the outcome -- most of the time, this is undesired (with interactive tactics being exceptions).

[Mirek Olšák]

In an ideal world, the partial text is not even sent to Lean but I understand this is not really possible with the "watching compiler" setup.

[Michael Rothgang]

I agree with you on the desired outcome - but let me disagree that having two kinds of cursors (with one behaving intuitively, and the other being never shown and implicitly updated) is intuitive :-)

[Mirek Olšák]

I am not sure if we understand each other, we already have two cursors like that when you click "pin". My proposal is

• Make the pin clearly visible (Rocq would highlight the full document before the pin meaning that that part was processed). Of course, this means that the "pin" would align with the end of a tactic rather than arbitrary position in the document.
• Make it easy to move the pin one tactic forward / backward.
• Experiment with sometimes automatically moving the pin, for example pressing enter.
  I am not yet certain how I will feel about it, and I understand Lean has this "red / green" highlight which doesn't fit very well into this pin workflow but I would be curious to try. It feels like a task that could be simple enough to be vibe-coded (because I know currently nothing about how the VS Code extension works).

[Mirek Olšák]

I started playing with moving the pin between tactics but detecting the tactic boundaries might be tricky. I kind of understand the behavior of rw but this goal change in the middle of a comment was a bit too much :sweat_smile:

example : True := by
  have : 1 = 1 := by rfl

  -- Move your curso!r around this exclamation mark
  trivial

[Jakub Nowak]

Mirek Olšák said:

I started playing with moving the pin between tactics but detecting the tactic boundaries might be tricky. I kind of understand the behavior of rw but this goal change in the middle of a comment was a bit too much :sweat_smile:

example : True := by
  have : 1 = 1 := by rfl

  -- Move your curso!r around this exclamation mark
  trivial

I think it's because it enters this second nested by. And because it's past rfl it's "No goals".

[Jakub Nowak]

It would be useful if Lean highlighted inside which by you're currently in.

[Mirek Olšák]

I tried but it seems too challenging to do it only on editor side with pins:

• The editor doesn't get from Lean cleanly the position of a next tactic. There are some way of searching for it but many exchanges with Lean server about different positions take time.
• Nested goals are tricky. Consider

theorem main := by
  have lem1 : ... := by
    tac1
    have lem2 : ... := by
      tac2

The natural proofstate after these steps depend on whether tac2 solves lem2, or not. If it does, we should be inside the proofstate for lem1, if it doesn't, we should be inside the proofstate for lem2. However, the cursor position for lem1 (after have lem2) doesn't even have to have any position in the document.

[Mirek Olšák]

I still think that visible & controlable pin would improve user's control significantly but given it would require editing not only the vscode extension but also Lean server, and given the reluctance of the community, I am not very motivated to do that...