-
Notifications
You must be signed in to change notification settings - Fork 23
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
neovim can freeze up / use 100% CPU when editing or navigating around Lean files #289
Comments
Oof, yeah I've seen this too. Fortunately not very frequently, but when it does happen I have to kill and restart my neovim session, so no fun. It seems to indeed be specific to this plugin, I have no idea as of yet but my guess is that we're entering an infinite loop of some kind. |
Have the problem as well, but for me it's mainly lean instead of nvim
The problem is exacerbated by importing files from Sometimes (even without importing a new file from Mathlib, just changing code quickly) nvim freezes and I have to kill nvim as well (usually only one or two lean processes are running). |
Hey, sorry about this. For the time being you can use resession.nvim to save your sessions periodically so that when it does freeze and you have to kill nvim, you can reload your most recent session. I've added a blurb to the wiki explaining how to make I'm going to look into this more, probably by sprinkling debug messages around the code to see if I can get some hints towards the suspected infinite loop. |
There's been at least 2 or 3 threads on the Zulip discussing high CPU usage in VSCode -- the most recent IIRC being https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20Mac.20OS.20Ventura.20.28Intel.29.20CPU.20usage -- so to me it's not necessarily clear yet that there's a |
I see similar behavior. |
Occasionally neovim uses 100% and stops responding.
I also notice that lean is using 0% when this happens.
This is of the jan 12 commit.
The text was updated successfully, but these errors were encountered: