Info View frequent updates

Stream: new members

[Josh Cohen]

Hello, I have a lot of experience with Coq/Rocq but I am brand new to Lean, and I am working through "Theorem Proving in Lean 4". In Coq, one typically proceeds tactic-by-tactic and can see the proof state at each step. When I am using Lean in VSCode, the info view is constantly changing as I type, including sometimes disappearing entirely in the middle of writing a tactic. This is very difficult to manage, as I find myself having to move the cursor just to remember hypothesis names and the goal shape. Is there a setting or way to make the display update less frequently, either on command or when a tactic is applied (like in the Natural Number Game)? I know about the pin/pause/unpause button in the VSCode proof view window, but that doesn't seem like a practical thing to do regularly. Thanks!

[Weiyi Wang]

Second this. It didn't bother me that much, but sometimes I needed to move my cursor back to see the info I wanted

[Shreyas Srinivas]

There is a setting in vscode called Elaboration Delay

[Shreyas Srinivas]

The default value appears to be 500 ms. You can set it to a higher value.

[Shreyas Srinivas]

but this is not going to help with the situation you mention @Weiyi

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Maybe the closest approximation you can have right now is to bind a keyboard shortcut to the 'Lean 4: InfoView: Toggle Updating' command, then at least you don't have to use your mouse. Many people have asked about this, so it might be something worth making more usable in the extension.

[Kevin Buzzard]

To a certain extent this can be mitigated against with judicious use of _ -- a lot of people just starting don't realise that once the right holes are there, the error is on the holes and the infoview reports the expected type.

[Damiano Testa]

I often write --[what I actually want] and then erase the --.

[Riccardo Brasca]

Damiano Testa said:

I often write --[what I actually want] and then erase the --.

I do the same. It's nice to see that we have similar tricks :D

[suhr]

Josh Cohen said:

This is very difficult to manage, as I find myself having to move the cursor just to remember hypothesis names and the goal shape.

Consider adding some type annotations into your proof. You can also use show to set up proof goal.

[suhr]

NNG teaches a very unreadable proof style, but you can do better in Lean.

[Josh Cohen]

Damiano Testa said:

I often write --[what I actually want] and then erase the --.

What does this do?

[Josh Cohen]

suhr said:

Josh Cohen said:

This is very difficult to manage, as I find myself having to move the cursor just to remember hypothesis names and the goal shape.

Consider adding some type annotations into your proof. You can also use show to set up proof goal.

Thanks, do you know if there are any resources for proof style/best practices in Lean?

[Aaron Liu]

Josh Cohen said:

Damiano Testa said:

I often write --[what I actually want] and then erase the --.

What does this do?

-- this is a comment so Lean won't try to evaluate it before you're finished typing