Potential mathlib scalability issues

Stream: lean4 dev

[Gabriel Ebner]

As we're getting closer to move mathlib to Lean 4, we will probably run into quite a few performance problems because we've never done projects that size in Lean 4 before. It would be great to get a head-start on fixes these issues now, so if you have a hunch that some things will scale badly, please feel free to complain with concrete, reproducible, and realistic test cases.

I'm thinking of issues like https://github.com/leanprover/lake/issues/130 There's probably lots of other scalability issues like that.

[Gabriel Ebner]

BTW, could somebody try https://github.com/gebner/inundation on Windows and Mac? I'm interested whether there's any performance difference between platforms. It would also be great to verify that we don't get any "argument list too long" errors on other platforms.

[Scott Morrison]

lake print-paths Inundation  10.95s user 21.31s system 305% cpu 10.543 total

on a 2.3 GHz 18-Core Intel Xeon W running Big Sur.

[Matthew Ballard]

lake print-paths Inundation 7.88s user 3.09s system 142% cpu 7.687 total
on a MacBook Pro with an M1 Max running Monterey

[Matthew Ballard]

I also tried it with a Windows laptop. It kept throwing errors with lake build suggesting I needed to open a workspace. After 5-6 rounds, I got idempotent behavior: no output. After that, timing the lake print-paths returned about the same numbers as on the linux partition.