how to run `lake exe cache get` while in VSCode

Stream: lean4

[Scott Morrison]

This is hopefully just a question about others' workflow.

Often I'm working in VSCode, and either want to run lake build, or lake exe cache get. If I do so from a terminal within VSCode, likely there is already a Lean 4 server running, and it will "fight" with the command I'm running in the terminal (e.g. overwriting olean files).

I could close VSCode and run these commands in an outside terminal, but this is pretty annoying. Is there a way to stop the Lean 4 server from inside VSCode so I can run this command?

Perhaps beyond that I think I'd like a keyboard shortcut that:

• stops the server
• runs either lake build or lake exe cache get && lake build in a new terminal
• restarts the server...

Advice, or an explanation that I'm doing it wrong, much appreciated. :-)

[Gabriel Ebner]

Indeed, I also find it very frustrating that I have no control over when things get built. And closing a file in vscode doesn't help either, lake just keeps running in the background. :sad:

[Mario Carneiro]

having a "stop server" instead of just "restart server" would help a lot

[Mario Carneiro]

overwriting/corrupting olean files is a bug though, there should be some locking going on

[Mario Carneiro]

I usually run sleep 1; killall lean in a loop when starting up vscode to prevent it from running out of memory, and this is also useful when I want to "stop server"

[Gabriel Ebner]

I wonder if we should just disable the auto-build when opening a file.

[Gabriel Ebner]

Just make a big "dependencies not built/up-to-date" popup instead.

[Adam Topaz]

One thing I find really annoying is when vscode decides to build something for a while (usually because I was stupid and forgot to fetch the oleans before opening vscode) and even after closing vscode I have some number of lean processes running forever.

[Adam Topaz]

Gabriel Ebner said:

Indeed, I also find it very frustrating that I have no control over when things get built. And closing a file in vscode doesn't help either, lake just keeps running in the background. :sad:

Ah I guess this is the same issue :)

[Adam Topaz]

Concerning Scott's original message: there are times where I want to switch branches within mathlib4, and I found that I can do this effectively by remembering to first close all files in vscode, switch branches, use lake exe cache get! (maybe the ! is too aggressive, but whatever) in a vscode terminal, restart the server, and only then (re)open the files I want. It's not the most errorproof workflow, but it works.

[Scott Morrison]

Okay, it's great/terrible to see that everyone is having the same troubles as me. :-)

[Scott Morrison]

Here's a "Stop server" command, which works, but reports an annoying message: https://github.com/leanprover/vscode-lean4/pull/291

[Sebastian Ullrich]

That probably won't help with the issue of runaway Lake and Lean worker processes, will it?

[Sebastian Ullrich]

In theory, lake should die the next time it tries to write "Building [...]" to stderr, though that may of course take an arbitrary amount of time. Apparently there is a much better way to make sure child processes die with their parents, which we could integrate into IO.Process.spawn. Alas, Linux only. https://stackoverflow.com/a/36945270

[James Gallicchio]

If we add a (cross-platform) IO.Process.kill, could we track each thread's open processes and send them sigkill when the thread gets shut down?

[Mario Carneiro]

I think that would also have a propensity to corrupt oleans

[Sebastian Ullrich]

lean itself will never corrupt oleans because they are first written to a temporary location and then moved to the final location (assuming you FS supports atomic moves)

[Sebastian Ullrich]

...as long as you don't run two lean -o processes for the same file

[Mario Carneiro]

is that because the temp location is deterministic?

[Mario Carneiro]

two lean -o processes for the same file sounds like a very likely situation, although it is fair to argue that this should be lake's problem to prevent

[Sebastian Ullrich]

Yes, it is literally just .tmp appended. And yes, the build system should prevent that for more than just that reason.

[Trebor Huang]

Processes still running after vscode is closed should be a bug in the Lean extension right? It ought to clean everything up upon receiving the disposing signal

[Sebastian Ullrich]

I don't see why this should get an editor-specific solution

[James Gallicchio]

Mario Carneiro said:

two lean -o processes for the same file sounds like a very likely situation, although it is fair to argue that this should be lake's problem to prevent

Since we don't have an API for getting temp file handles yet, it's not really a fixable problem...

[James Gallicchio]

and it looks like windows doesnt even have an API for atomically getting a unique temp file

[James Gallicchio]

(made a separate topic for that discussion https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Temp.20file.20utilities)

[Gabriel Ebner]

FWIW, I have written up a preliminary RFC at lean4#2154

[Eric Wieser]

Adam Topaz said:

Concerning Scott's original message: there are times where I want to switch branches within mathlib4, and I found that I can do this effectively by remembering to first close all files in vscode, switch branches, use lake exe cache get! (maybe the ! is too aggressive, but whatever) in a vscode terminal, restart the server, and only then (re)open the files I want. It's not the most errorproof workflow, but it works.

How do you restart the server when no files are open?

[Eric Wieser]

I think that command is only available if you have a lean file open

[Scott Morrison]

I'd love to see progress on this one. I am still regularly having to close VSCode / logout and login / pkill lean etc. I change branches a lot!

In particular, the thing I want most is to prevent opening a new file in VSCode starting to rewrite oleans on the disk!