LSP CPU usage

Stream: general

[Michael George]

I'm using lean with nvim, and I noticed that even when I'm not using the editor, there are several lean processes eating up a ton of CPU time (and killing my battery!). I'm surprised that lean is doing much while I'm not typing, I wonder if I have some kind of configuration error or something. Any thoughts?

[Henrik Böving]

Lean alwys attempts to elaborate the file(s) you are working on until the end after an edit to see if some proof or definition doesn't work out anymore or something like that. If you have big files (or files that generally take long to compile) and edit them at the top it is likely that they are being re-elaborated all the time as you finish typing.

You can address things like that by splitting it up into more files or placing a #exit below the point you wish to check until now.

Alternatively there might also be a deeper issue but you will have to provide more detail on your setup.

[Shreyas Srinivas]

I wish there was a synchronous "update on save" elaboration. I still get this runaway thread issue on macOS

[Henrik Böving]

Write an issue for it and it will end up on the FROs queue eventually^^

[Julian Berman]

@Michael George just to rule it out, if you're working on Mathlib, or something depending on it, and you see it's Mathlib that Lean is compiling, you should double check something isn't wrong with your Mathlib cache. (If you see that's what it is, i.e. Mathlib, say so and we can elaborate -- oh god pun not intended).

[Shreyas Srinivas]

@Henrik Böving : https://github.com/leanprover/vscode-lean4/issues/305

[Shreyas Srinivas]

I have given up hope. In the bigger scheme of things I can see that this won't be a priority any time soon.

[Michael George]

This seems to have resolved itself for now for me, so maybe whatever it was doing is done now. The problem wasn't caused by a large file, because I've only been editing small files. I was editing files from multiple different projects simultaneously, so I wonder if some build artifacts weren't being found and so were being rebuilt.

If my laptop starts getting hot again I'll try to do some more investigation and let you know!