`import Mathlib` does 80K-150K `stat` (and other I/O) calls and can stall on HDD or networked drives driving wall clock time from 2 seconds to 20 minutes

Adding it as an issue to not lose if it's not relevant for that PR

Originally posted in:

• https://github.com/leanprover/lean4/pull/8024#issuecomment-2825566422
• https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Lean's.20I.2FO.20usage.20while.20using.20Mathlib/with/513864617

with strace like (I posted more straces in Zulip thread and posted the I/O call counts there):

24664 stat("././.lake/packages/batteries/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/batteries/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/Qq/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/Qq/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/aesop/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/aesop/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/proofwidgets/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/proofwidgets/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/Cli/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/Cli/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/importGraph/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/importGraph/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/REPL/.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/packages/REPL/.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/build/lib/Lake", 0x7ffc739e8408) = -1 ENOENT (No such file or directory)
24664 stat("././.lake/build/lib/Lake.olean", 0x7ffc739e8418) = -1 ENOENT (No such file or directory)
24664 stat("/home/verifier/.elan/toolchains/leanprover--lean4---v4.9.0-rc1/lib/lean/Lake", {st_mode=S_IFDIR|0755, st_size=4096, ...}) = 0
24664 stat("/home/verifier/.elan/toolchains/leanprover--lean4---v4.9.0-rc1/lib/lean/Lake/Toml/Grammar.olean", {st_mode=S_IFREG|0644, st_size=853832, ...}) = 0
24664 openat(AT_FDCWD, "/home/verifier/.elan/toolchains/leanprover--lean4---v4.9.0-rc1/lib/lean/Lake/Toml/Grammar.olean", O_RDONLY) = 3
24664 newfstatat(3, "", {st_mode=S_IFREG|0644, st_size=853832, ...}, AT_EMPTY_PATH) = 0

so it does a lot of failing stat calls before accessing an olean, and these many stat calls can be costly on HDD and even networked SSDs, so maybe some call sequence could be changed or a file index can be built so that no syscalls (and also user mode <> kernel mode switches are needed)

Even if the SSD/drive is not slow itself, if the system is busy and kernel syscalls become slow for some reason (e.g. happens when running hundreds of lean4 instances on a big-cpu server), this can stall imports because of these hundreds of thousands of useless stat calls

(for large packages, maybe a way forward could be supporting importing packages from zipballs (e.g. mathlib.zip). Indexing can be done to enable replacement for stat calls - e.g. mathlib.zip.json, and then it would be looked up instead of stat calls)