VSCode cross file synchronization

Stream: lean4

[Joe Hendrix]

When I move a definition from one Lean file to another that imports it in VSCode, I find I have to restart the server for it to find the definition.

Is this expected behavior?

[Wojciech Nawrocki]

For definitions in the same file, you should never need to restart. For changes in an imported module A (including the locations of symbols one may jump to) to be observable in a module B that imports A, you need to execute the "Lean 4: Refresh File Dependencies" command in B. Does this help?

[Joe Hendrix]

@Wojciech Nawrocki Thanks, I somehow overlooked your reply. I'll try the refresh file dependencies command.
At least on the Mac, I've gotten into the habit of frequently restarting Lean and reloading the Window (Does Lean restart when I reload the window?). Otherwise, I can run into massive slowdowns that necessitate a reboot It seems to be more of a problem in a devcontainer. At one point it seemed like VSCode kept spawning Lean processes.
I may be out of date with respect to the Lean VSCode extension, but if this is completely unexpected I can try to find a way to reproduce issues.

[Wojciech Nawrocki]

@Joe Hendrix Yeah, I think the whole server should restart when VSCode is reloaded. But there is also a Lean 4: Restart Server command.

At one point it seemed like VSCode kept spawning Lean processes. Imay be out of date with respect to the Lean VSCode extension, but if this is completely unexpected I can try to find a way to reproduce issues.

The server is meant to spawn a worker process for each open file, but these processes should close when you close the file tab so the total running process count should be the number of open tabs + 1 (for the main process). If it's not that, then it's an issue. Also a worker process sleeps until there is something to be done, though it will initially compile the file on open. This could cause a significant slowdown if a lot of files are suddenly opened, but it shouldn't persist.

[Joe Hendrix]

@Wojciech Nawrocki In the case I'm thinking of I had a little over 3000 lean instances running before I killed docker (and less than 10 Lean files open). I'll try to generate a useful error report if I encounter the issue again.

[Wojciech Nawrocki]

That's definitely a bug! And yeah, if it happens again a report (maybe noting the particular container image in case its specifics break something) would be useful.

[Sebastian Reichelt]

Joe Hendrix said:

Wojciech Nawrocki Thanks, I somehow overlooked your reply. I'll try the refresh file dependencies command.
At least on the Mac, I've gotten into the habit of frequently restarting Lean and reloading the Window (Does Lean restart when I reload the window?). Otherwise, I can run into massive slowdowns that necessitate a reboot It seems to be more of a problem in a devcontainer. At one point it seemed like VSCode kept spawning Lean processes.

I wonder if this is the same problem that I regularly run into. For me, it is leanpkg running amok on Ubuntu, and respawning new processes faster than they finish. Sometimes this happens suddenly after an hour, sometimes in intervals of a minute or so. Unfortunately, I haven't been able to reproduce it, though I've noticed that Copy&Paste seems to be involved nearly every time it happens. Here's a screenshot: https://i.imgur.com/XJjUyhE.png. If I manage to reproduce it reliably in some way, I'll file a bug report.

[Joe Hendrix]

@Sebastian Reichelt It may be. It happened to me this morning, and I noticed a mix of leanpkg and lean in the OSX Activity Monitor. So far it's pretty irregular, and I haven't reproduced it.

[Sebastian Reichelt]

I've found out that it's triggered by Ctrl+hover (without clicking). That's why I thought it was copy&paste - pressing Ctrl is sufficient if the mouse is in a bad spot. Actually, now I can reproduce it in a very minimal file, so I wonder if there are any necessary conditions.

[Sebastian Reichelt]

Filed a bug report: https://github.com/leanprover/lean4/issues/367