-
Notifications
You must be signed in to change notification settings - Fork 345
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Watchdog sometimes gets stuck and stops processing requests for a file #1219
Comments
I'm also seeing this issue in the neovim plugin, so maybe this is a bug in the Lean 4 LSP implementation itself. Does the |
It does not. The only thing that seems to work is renaming the file. |
This looks like a bug in the watchdog. Transferring to the Lean 4 repo because this bug is not editor-specific. |
I'm going out on a limb here, but this could be due to this line: lean4/src/Lean/Server/Watchdog.lean Line 308 in 5896e6f
If writing the exit message to the file worker blocks, then the file worker will never be erased. In particular it won't be restarted with |
I'm not sure I've encountered this myself so far; I get plenty of hangs, but they usually seem to be Emacs' fault. We took care to make sure that the main loop of the file worker never blocks except on reading requests. Would be interesting to get stack traces from such a hung worker. |
But just to be clear, should "Restart Server" not replace the entire watchdog process? |
Oh, I confused that with "Refresh File Dependencies". Maybe something different is going on as well then.
👍 about the stack traces. We do all kinds of (potentially) blocking operations in the main loop though: printing to stdout/stderr, handle LSP requests (most handlers spawn a task for some of the work, but this is not enforced), there's also lots of potentially contended accesses to |
This issue has been plaguing me for a while in VSCode and is very unfortunate, It kills all the nice interactive features that are major positives of Lean. However, I do believe I have figured out a surefire way to exit this state once in it for a file in VSCode. Close all open Lean tabs and then execute |
I'm seeing the same thing reported here #1564 and I suspect the repro always involves editing through some invalid states. If I load good code and simply browse around, then everything is fine. So the scenario is I'm writing code, getting errors, and then I fix the code, lake build succeeds from the command line, but goto definition and hover tips are gone. And I can see goto definition working in other files, but not on the files I've been editing. So yes "watchdog stuck" is a great description. Refresh file dependencies did not fix it for me also. I didn't try restart server, I will try that next time, but close and restart vscode does fix it (except perhaps in the case Mac mentions above where VS code remembers which files you were editing and quickly goes right back into the stuck state). |
We probably need to write some async state machine proofs in the LSP, I would love to do that it would be very fun and would be related to a previous project I worked on called Coyote. The best way to handle async state machines is with an inbox actor model to ensure serialization of messages across the various async actors involved in the LSP implementation, that should include actors for IO, according to Gabriel's comments above. |
I can consistently reproduce this on my Windows machine, but I didn't manage to reproduce it yesterday on my Linux machine (both in VSCode). Here is some behavior that might suggest possible problems:
Hopefully this helps. I can share a screen recording of me performing these steps if that is useful. |
Occasionally, the extension will stop providing feedback for a given file, with the problem persisting after restarting the extension/vscode, and after removing build artifacts. The behavior goes away if I change the file name, and returns if I revert the file to the original name. I had a similar experience today, where it initially provides incorrect error/line numbers and then stops providing feedback.
I'm not sure how to trigger this or debug it through vscode so I can't provide a MWE, but this sounds like a cache issue, I can take a look if you point me in the right direction.
MacOS 11.6.6
vscode 1.67.2
extension v0.0.77
nightly-2022-05-31
The text was updated successfully, but these errors were encountered: