Stop server in VSCode?

Stream: lean4

[Mac]

Is there a way to stop the Lean server altogether in VS Code? When rebuilding the Lean sources in VS Code, the build can fail because the previously built Lean is already running in as the Lean server for VS Code (and thus it can't overwrite the executable). Thus, if I could start the server before building and then start it again after, I could get around this issue.

[Mario Carneiro]

Does the server build the executable? I would have assumed not

[Sebastian Ullrich]

Wow, I assume you're on Windows?

[Gabriel Ebner]

See also this change in Lean 3: https://github.com/leanprover-community/lean/commit/667e1e138162ef6d65a2041abfe760a7aa79c2c5

[Mac]

Sebastian Ullrich said:

Wow, I assume you're on Windows?

Yep, I'm on Windows.

[Sebastian Ullrich]

Ok, then we should use something like the commit linked by Gabriel so that the server doesn't have to be stopped at all

[Mac]

Sounds great! That would be even more convient!

[Sebastian Ullrich]

If anyone wants to figure this out and test it, please go ahead :big_smile:

[Mac]

Fyi, in addition to this problem appearing while building a new Lean while the server is running, it also appears if one runs elan update on a toolchain while the toolchain server is running.

[Mac]

That is, the issue is also (Lean 4) user-facing in addition to (Lean 4) developer-facing.

[Aaron Liu]

Is there a way to stop the server in VSCode? When I'm actively editing a file and I don't want to see the infoview or anything, the server is still running, and that slows down other stuff I want to happen (like replacing \a with α). I'd be great if I could just stop the server while I'm editing and resume it once I'm done. The "pause" button in the infoview only seems to pause the infoview state, it doesn't actually stop the server.

[Kevin Buzzard]

I just type killall lean in a terminal

[Aaron Liu]

I'm on windows sometimes and stop-process -name "lean" is more characters than I want to type.

[Aaron Liu]

Also I have to start it up again when I'm done typing

[Aaron Liu]

I'd be great if I could just use a keyboard shortcut or something

[Kevin Buzzard]

To start it again I just click the "lean has stopped, click here to start it again" button

[Aaron Liu]

Kevin Buzzard said:

To start it again I just click the "lean has stopped, click here to start it again" button

That's two more clicks than I want, and that still doesn't solve the problem with stopping Lean.

[Michael Stoll]

Maybe a nearly ideal solution would be to pause the server while typing (i.e., have a configurable time interval that the server waits after the user has typed something that is restarted with every keystroke). This way, one does not have to always click/type twice (to stop and then restart the server) in addition to the actual typing.

[Michael Stoll]

And maybe all threads the server is running should be killed when I type something.

[Sebastian Ullrich]

Any significant computation outliving a text edit is a bug and should be reported

[Michael Stoll]

My impression is that this is happening all the time. At least, I experience that VSCode becomes sluggish when typing in a (not very short) file; for example (as mentioned above), after typing \N or similar, it takes a while until ℕ appears, and in some cases, it even doesn't, and I have to delete \N and re-type it.

[Yaël Dillies]

That sounds a lot like what I reported months ago

[Kevin Buzzard]

I don't think I have ever experienced this. What OS are you on and how much memory do you have? When I am killing the server it's for reasons such as "I am running lake exe cache get or lake build on the command line and my gut feeling is that it's safer to restart" rather than "I am having problems"

[Yaël Dillies]

cf #general > v4.19.0-rc2 @ 💬

[Michael Stoll]

I'm on Linux and have a reasonably fast laptop. When I type near the beginning of a Lean file with ~500 lines or so, I can see yellow bars all the way down while typing, and the system monitor shows that the server spawns a whole bunch of threads. Depending on the situation, this can max out the number of available cores, which is when I experience the sluggishness mentioned above.

I would argue that while I'm typing, there is no need for the server to check all subsequent code in the file; this can be done once I have stopped typing (for something like maybe half a second), as it is pretty unlikely that the intermediate states of the text while I'm typing are in any way meaningful.

[Robin Carlier]

I asked something similar but for neovim here
It looks like for now there's no good way of doing this.

[Kevin Buzzard]

Oh interesting! My workflow is different -- I always dump an #exit after the declaration I'm working on if I'm hacking in the middle of a file.

[Justin Asher]

Michael Stoll said:

I would argue that while I'm typing, there is no need for the server to check all subsequent code in the file; this can be done once I have stopped typing (for something like maybe half a second), as it is pretty unlikely that the intermediate states of the text while I'm typing are in any way meaningful.

This is fairly standard for search engines. Does the LSP not do this?

[Michael Stoll]

Kevin Buzzard said:

Oh interesting! My workflow is different -- I always dump an #exit after the declaration I'm working on if I'm hacking in the middle of a file.

I resort to that when it gets too bad, but it would be better if that weren't necessary.

[Kevin Buzzard]

I feel like it's cruel to keep making the server try and make sense of code which is temporarily junk because there's a declaration missing (as it's being refactored or whatever) :-)

[Aaron Liu]

Michael Stoll said:

Maybe a nearly ideal solution would be to pause the server while typing (i.e., have a configurable time interval that the server waits after the user has typed something that is restarted with every keystroke).

I'm pretty sure this already exists, but my typing times vary and I don't want to have to wait 10 seconds for the server to restart after I'm done typing and I also don't want the server to start up again while I'm in a 10 second pause to figure out what to type next

[Justin Asher]

@Aaron Liu Do you want a stop / run button then that appears on the LSP console? I do not think that should be very hard to add.