slow proof state update

Stream: new members

[Joachim Breitner]

Sometimes I get lean/vscode into a state where it updates the state view not just very slowly, but it seems it doesn’t “skip ahead”, and instead shows the state after each character I inputted.

For example, while I type a keyword, I can see unknown identifier 'r' and then unknown identifier 're' etc. for each character that I typed, although I have long finished typing refine.

But only sometimes – usually it only processes the latest state, and I have no idea yet what’s causing this. Do others observe this as well?

[Yaël Dillies]

Happens to me as well. I assume it's a memory leak. The only thing that seems to solve it is restart the Lean server.

[Alex J. Best]

Yeah this happens to me fairly often to me, would be a nice issue to track down once and for all, but maybe another one of those things that we live with as it will likely not be the same in lean 4.
Usually this happens when editing a file deep in the import heierachy in mathlib.
My solution is to have a keybind to restart lean, which normally is faster than waiting for it to finish typing one character at a time.

[Yaël Dillies]

Ctrl + < + P + Enter on VScode

[Yakov Pechersky]

It happens for me mostly when I'm editing a deep file, when I also have a lot of other tabs open with other files that depend on it. If I don't have those depend files open, I'm fine

[Joachim Breitner]

I do restart lean from time to time and know the keybinding, but so far it didn’t fix this issue reliably, I thought.
Deep file with other tabs open might be it, but shouln’t “check visible file” or “check visible lines” prevent that? (but that may just be how it should be, not how it is)

[Yakov Pechersky]

"how it should, not how it is" is my understanding too.

[Alex J. Best]

You can also assign a specific keybind to restart lean though, which is a bit more convenient if the computer response time is lagging, I use cmd+shift+L .
Indeed this is not how it should be, but a convenient way to reproduce this issue, and a lot of motivation for someone who knows leans internals well are prerequisites for fixing it!

[Eric Rodriguez]

as far as I know, Yakov's experience is mine too

[Eric Rodriguez]

a well placed #exit after and . before mitigates it, but isn't great. another thing I do is close all other files and restart, but this isn't ideal

[Eric Rodriguez]

it's kinda hard to diagnose, because it's to do with performance - my new laptop gets it a lot less than my 10 year old desktop, but it still can sometimes happen

[Julian Berman]

FWIW I see this in neovim occasionally, so I think it's something totally unrelated to VSCode specifically, it's on the Lean server side.