Performance in Small Projects

Stream: new members

[Robert Maxton]

Trying to debug a painfully slow lean setup; right now it's taking on the order of ten minutes to finish updating after making minor changes to a single, small file (150 lines). One thing I notice is that Lean is actually using much _less_ of my computer resources than I'd prefer; lean is taking about 0.5 GB of RAM and less than 10% of my CPU time, and I really wouldn't mind tripling or quadrupling both of those numbers. Unfortunately, Lean 4 doesn't seem to have a memory limit setting like Lean 3 did. Any other ideas or debugging advice?

[Robert Maxton]

... Restarting the server fixed the issue; I had forgotten I'd left it open for several hours. Somewhat strange that that matters but oh well.

[Marc Huisinga]

Please let me know if you encounter this issue again. When you do, please also include the state of the file around the time when it suddenly started getting slow.