search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

neovim can freeze up / use 100% CPU when editing or navigating around Lean files #289

Closed Karthik-Dulam closed 6 months ago

Karthik-Dulam commented 1 year ago

Occasionally neovim uses 100% and stops responding. I also notice that lean is using 0% when this happens.

NVIM v0.8.2
Build type: Release
LuaJIT 2.1.0-beta3
Compiled by builduser

lean.nvim
Commit af5ac626ffac9af956eedda1f5b31bf36572708e

This is of the jan 12 commit.

rish987 commented 1 year ago

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.

n-0 commented 1 year ago

Have the problem as well, but for me it's mainly lean instead of nvim Here the output of top on my machine (~ 4.00 GHz x 8 cores)

top - 10:55:05 up  2:02,  1 user,  load average: 8.54, 8.71, 7.14
Tasks: 349 total,  12 running, 336 sleeping,   0 stopped,   1 zombie
%Cpu(s): 94.3 us,  3.8 sy,  0.0 ni,  0.0 id,  0.0 wa,  1.8 hi,  0.1 si,  0.0 st
MiB Mem :  15691.9 total,   1275.2 free,   6675.0 used,   7741.7 buff/cache
MiB Swap:  16108.0 total,  16088.0 free,     20.0 used.   7770.9 avail Mem

    PID USER      PR  NI    VIRT    RES    SHR S  %CPU  %MEM     TIME+ COMMAND
 156358 no        20   0 1607660   1.4g 995.1m R 100.0   9.2   5:12.63 lean
 156792 no        20   0 1345732   1.2g   1.0g R 100.0   7.6   0:47.99 lean
 157105 no        20   0 1020564 887416 811892 R  98.7   5.5   0:09.58 lean
 157122 no        20   0 1291780   1.1g   1.0g R  95.7   7.2   0:07.97 lean
 156697 no        20   0 1306232   1.1g   1.0g R  94.0   7.3   1:28.97 lean
 156839 no        20   0 1356152   1.2g   1.0g R  90.0   7.6   0:26.33 lean
 157107 no        20   0 1300008   1.1g   1.0g R  88.4   7.2   0:08.99 lean
 156692 no        20   0 1343164   1.2g   1.0g R  87.0   7.5   1:49.73 lean

The problem is exacerbated by importing files from Mathlib. Oddly the resource usage is kept small by running lake build upfront (reasonable runtime), then nvim still builds a few files from Mathlib, but finishes quickly.

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).

rish987 commented 1 year ago

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 resession.nvim work with this plugin.

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.

Julian commented 1 year ago

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 lean.nvim-specific issue to fix, but I haven't played around much myself recently obviously :/

mattrobball commented 1 year ago

I see similar behavior. nvim reports 100% CPU on its thread and lean reports 0. I mentioned this on Zulip to see if others might have this issue. I don't think the cause is this extension but felt this might be a good place to record information.