perf: parallel pre-read of import regions with --setup

[Kha]

This PR parallelizes parts of the .olean loading process under e.g. lake build, accelerating importing whenever a significant amount of time is spent in the OS kernel and can be parallelized there as well.

Before importModulesCore traverses the import graph, preReadArtifacts reads every module's main .olean across a small number of striped worker tasks. Only the main .olean is pre-read: it is loaded for every module in the transitive closure (the traversal needs each header to recurse), so there is no over-read, while the pruned .olean.server/.olean.private/.ir parts stay on the sequential path. The traversal then consults the pre-read cache. The worker count is capped low to bound mmap address-space lock contention.

[Kha]

!bench

[leanprover-radar]

Benchmark results for bfe1987 against 60967a7 are in. There are significant results. @Kha

• 🟥 build//instructions: +14.4G (+0.13%)

New metrics (6✅, 5🟥)

• 🟥 compiled/incr_header_load//cycles: +92.7M (+11.08%)
• ✅ compiled/incr_header_load//instructions: -1.9M (-0.18%)
• ✅ compiled/incr_header_load//maxrss: -8MiB (-1.28%)
• 🟥 compiled/incr_header_load//task-clock: +20ms (+13.09%)
• 🟥 compiled/incr_header_load//wall-clock: +12ms (+9.29%)
• ✅ compiled/incr_header_save//cycles: -106.0M (-1.22%)
• ✅ compiled/incr_header_save//instructions: -7.5M (-0.13%)
• 🟥 compiled/incr_header_save//maxrss: +426kiB (+0.02%)
• 🟥 compiled/incr_header_save//snap-size: +1kiB (+0.00%)
• ✅ compiled/incr_header_save//task-clock: -16ms (-1.08%)
• ✅ compiled/incr_header_save//wall-clock: -17ms (-1.07%)

Medium changes (2🟥)

• 🟥 build/module/LeanChecker//instructions: +1.9G (+82.80%) (reduced significance based on absolute threshold)
• 🟥 build/module/Leanc//instructions: +1.4G (+127.36%) (reduced significance based on absolute threshold)

Small changes (1✅, 49🟥)

Too many entries to display here. View the full report on radar instead.

[Kha]

!bench

[leanprover-radar]

Benchmark results for 105935e against 60967a7 are in. There are significant results. @Kha

• 🟥 build//instructions: +8.9G (+0.08%)

New metrics (5✅, 6🟥)

• 🟥 compiled/incr_header_load//cycles: +84.3M (+10.08%)
• 🟥 compiled/incr_header_load//instructions: +6.7M (+0.64%)
• ✅ compiled/incr_header_load//maxrss: -6MiB (-0.99%)
• 🟥 compiled/incr_header_load//task-clock: +18ms (+11.98%)
• 🟥 compiled/incr_header_load//wall-clock: +8ms (+5.83%)
• ✅ compiled/incr_header_save//cycles: -68.9M (-0.79%)
• ✅ compiled/incr_header_save//instructions: -21.5M (-0.37%)
• 🟥 compiled/incr_header_save//maxrss: +512kiB (+0.02%)
• 🟥 compiled/incr_header_save//snap-size: +2kiB (+0.00%)
• ✅ compiled/incr_header_save//task-clock: -12ms (-0.81%)
• ✅ compiled/incr_header_save//wall-clock: -13ms (-0.81%)

Large changes (2🟥)

• 🟥 compiled/nat_repr//task-clock: +958ms (+79.85%)
• 🟥 compiled/nat_repr//wall-clock: +958ms (+79.87%)

Medium changes (1🟥)

• 🟥 compiled/nat_repr//instructions: +13.6M (+0.03%)

Small changes (2✅, 38🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 60967a7b9523a11c19a13dc8f460ed5bd0d20249 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-12 13:51:38)
• ✅ Mathlib branch lean-pr-testing-14032 has successfully built against this PR. (2026-06-16 11:27:05) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 60967a7b9523a11c19a13dc8f460ed5bd0d20249 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-12 13:51:39)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-16 10:31:15)

[Kha]

!bench mathlib

[leanprover-radar]

Benchmark results for leanprover-community/mathlib4-nightly-testing@0c6e99b against leanprover-community/mathlib4-nightly-testing@d09d04c are in. No significant results found. @Kha

• ✅ build//instructions: -8.1G (-0.01%)

Small changes (1✅, 1🟥)

• 🟥 build/profile/blocked (unaccounted)//wall-clock: +2m 11s (+3.60%)
• ✅ build/profile/interpretation//wall-clock: -4m 14s (-2.52%)