Stream: lean4

Topic: VSCode cross file synchronization

Joe Hendrix (Mar 13 2021 at 22:28):

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 (Mar 14 2021 at 00:12):

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 (Mar 21 2021 at 18:54):

@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 (Mar 21 2021 at 19:11):

@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 (Mar 21 2021 at 19:16):

@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 (Mar 21 2021 at 19:19):

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 (Mar 22 2021 at 20:58):

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 (Mar 22 2021 at 21:49):

@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 (Mar 22 2021 at 22:29):

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 (Mar 22 2021 at 23:06):

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

Last updated: May 07 2021 at 11:09 UTC