Lean is unusably slow

Stream: lean4

[Damiano Testa]

Today, when using lean, I find that I constantly have to forcibly quit VSCode and restart. Sometimes my computer crashes, other times it does not. Has anyone else been experiencing something similar?

[Damiano Testa]

In particular, this is what I see when I open VSCode and type top:

 282531 damiano   20   0 4413960  46424   1392 S  25.0   0.6   0:03.72 lean
    106 root      20   0       0      0      0 R  22.5   0.0  11:41.42 kswapd0
 282379 damiano   20   0 3912496 174148  73992 S  20.0   2.2   0:05.03 lean
 282399 damiano   20   0 4397920 122836  39104 S  17.5   1.6   0:05.43 lean
 282433 damiano   20   0 3913980 161996  56432 S  17.5   2.1   0:04.83 lean
 281705 damiano   20   0 4221012 167464  50780 S  15.0   2.1   0:04.79 lean
 281821 damiano   20   0 3991560 244728  86612 S  15.0   3.1   0:03.10 lean
 281927 damiano   20   0 3975560 242852  84412 S  15.0   3.1   0:03.33 lean
 282229 damiano   20   0 4074024 133184  42000 S  15.0   1.7   0:05.95 lean
 282259 damiano   20   0 3871848 168720  54672 S  15.0   2.1   0:04.67 lean
 282471 damiano   20   0 3963780 160588  61724 S  15.0   2.0   0:04.79 lean
 282624 damiano   20   0 3753952 172632  54440 S  15.0   2.2   0:04.58 lean
 282690 damiano   20   0 3694800 153168  57708 S  15.0   1.9   0:04.71 lean
 282727 damiano   20   0 3070916 141756  38244 S  15.0   1.8   0:03.97 lean
 281941 damiano   20   0 3949696 221496  62636 S  12.5   2.8   0:03.37 lean
 281978 damiano   20   0 3711596 201352  78872 S  12.5   2.5   0:02.60 lean
 282094 damiano   20   0 3894756 221728  62696 S  12.5   2.8   0:03.65 lean
 282198 damiano   20   0 3645408 199548  76756 S  12.5   2.5   0:02.56 lean
 282209 damiano   20   0 3633236 195312  75748 S  12.5   2.5   0:02.99 lean
 233539 root      20   0 1407852  17676   7856 R  10.0   0.2   0:20.01 Xorg
 279880 damiano   20   0 1392.5g 473528  78436 D  10.0   6.0   0:54.20 chrome
 280432 damiano   20   0   32.4g   5340   3268 R  10.0   0.1   0:02.02 code
 280688 damiano   20   0 4529452 197056    724 S  10.0   2.5   0:04.78 lean
 282047 damiano   20   0 3849564 239276  82628 S  10.0   3.0   0:02.56 lean
 282181 damiano   20   0 3815616 153092  29688 S  10.0   1.9   0:04.21 lean
 282282 damiano   20   0 3369412 195344  74428 S  10.0   2.5   0:02.92 lean
 281931 damiano   20   0 3676972 198872  76856 S   7.5   2.5   0:02.71 lean
 285938 damiano   20   0 1709132  92852  26948 D   7.5   1.2   0:03.65 lake
 285985 damiano   20   0   16332   1604    640 R   7.5   0.0   0:00.07 top

Below that, there are no more leans.

[Damiano Testa]

Is this normal?

[Damiano Testa]

In case you are wondering, I think that my computer has 4 CPUs, not 23.

[Kenny Lau]

do you have the mathlib4 cache?

[Damiano Testa]

Yes, and lake build works without problems.

[Damiano Testa]

(And takes a couple of seconds, like always)

[Julian Berman]

What does pstree -s lean and/or pstree -s lake look like, which maybe says a bit more about who's related to who in the lean family tree.

[Kevin Buzzard]

What OS? You're opening mathlib? Which commit?

[Damiano Testa]

I also tried rm -rf .lake and re-downloading, but it keeps happening.

[Damiano Testa]

I am on Linux and I am looking at the current master.

[Damiano Testa]

Julian, they both say

$ pstree -s lake
No such user name: lake

[Damiano Testa]

With damiano, which is my username, it prints out quite a lot of stuff, though.

[Damiano Testa]

Should I paste the output here?

[Damiano Testa]

Will I reveal all my darkest secrets if I do?

[Julian Berman]

Huh. You have some different pstree than I do (which is strange because there's no BSD/Linux variance there AFAIK), -s on my pstree is substring match (and the point was just to double check whether any of those leans were orphaned which is unlikely (especially given the CPU usage numbers), so no probably no need to share the output for all your processes.

[Damiano Testa]

Ok, although, contrary to what I said before, it seems that on master things are fine. The issue may therefore be due to the branch where I was. Can someone try and see if they also get weird behaviour downloading the cache for branch#adomani/lint_empty_line ?

[Damiano Testa]

Basically, opening any file and starting to type any command consumes all the resource of my neighbourhood.

[Damiano Testa]

The sizes of the oleans in the branch are just a very small amount smaller than the ones on master, but it is somewhat comforting that the issue is on a branch, rather than on master. Maybe the oleans are corrupted, either by random fluke or because of what the branch contains. I am going to push a change and try again with newer oleans to see what happens.

[Damiano Testa]

Ok, editing the file (not in VSCode!) with the root modifications on the branch and opening another file that imports it seems to work. For whatever reason the downloaded oleans had some issue. I'll try to figure out whether the issue was in my code or not.

[Damiano Testa]

In case it is ever useful, this is the commit that seems to have poisoned the oleans: https://github.com/leanprover-community/mathlib4/pull/25236/commits/088a08defece807b601dd9cd5f92c54f2e216bf1.