Mode for automatically updating downstream files?

Stream: general

[Harry Goldstein]

Hi all, in VSCode, is there a way to _always_ "Restart Lean server for file" in open editor tabs when their dependencies change? Sometimes I'm working on one file Foo.lean with a library function/tactic and another Bar.lean that calls that function/tactic. It'd be nice if I could have a mode where I didn't need to manually open Bar.lean and run the "Restart Lean server for file" action to see if my change in Foo actually had the intended effect.

This has been a frustration for me for a while, but it's especially annoying for me now that I'm playing around with using an AI agent to edit code — the agent often reads LSP output from a file I haven't reloaded in a while and concludes that a change it made didn't work, even though the issue is really just that the file needs to be reloaded.

[Kim Morrison]

@Harry Goldstein , could you please open an issue against the vscode extension repository asking for this feature?

[Junyan Xu]

By the way is there currently a setting to prevent Lean from automatically starting when I open the editor (VSCode)? I have 8 windows of Lean repos in VSCode and every time I open VSCode I need to manually kill all lean processes in Task Manager, otherwise they'll eat up too much resource.

[Aaron Liu]

When I open VSCode I have to wait for Lean to start before I can kill it to prevent it from messing with lake exe cache get, so the option to not have it start automatically would be useful

[Harry Goldstein]

@Kim Morrison Yes, happy to open an issue on the VSCode extension. I’m guessing the other question here about the lean server should also be a separate issue there?

[Junyan Xu]

Aaron Liu said:

When I open VSCode I have to wait for Lean to start before I can kill it to prevent it from messing with lake exe cache get, so the option to not have it start automatically would be useful

Yes, if I run lake exe cache get (or unpack) on Windows without stopping the server I frequently get messages like these:

...
C:\Users\xujys\.cache\mathlib\00c02fda1f066809.ltar: The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)
C:\Users\xujys\.cache\mathlib\4cb013cffafd46a7.ltar: The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)
C:\Users\xujys\.cache\mathlib\9b446276c801ca6a.ltar: The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)
uncaught exception: leantar failed with error code 1

and it's a waste of time to stop and restart the server manually. I guess this is something to report to the lean4 repo, since lake is a part of it.

[Junyan Xu]

It's now also very easy to randomly trigger these pop-ups in VSCode (not sure which key combination triggers it):
image.png
This should be handled by lake so why is it necessary to spam the user like this? It's not like I can randomly update Lean version when working on mathlib.

Sorry for hijacking the topic, just found this a good opportunity to summarize some recently encountered issues.

[Harry Goldstein]

Couldn't you fix this by just pinning your Lean version to a particular Lean release, rather than stable? It seems reasonable that Lean might update its notion of "stable" before a compatible version of Mathlib is released.