chore: add import Lean (cold) benchmark

[Kha]

No description provided.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-19 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-19 13:52:52)

[Kha]

!bench

[leanprover-radar]

Benchmark results for f834803 against bc5f89f are in. There are significant results. @Kha

• ✅ build//instructions: -175.1M (-0.00%)
• 🟥 other exited with code 1

Small changes (2🟥)

• 🟥 build//task-clock: +42s (+2.00%)
• 🟥 build/profile/compilation (LCNF impure)//wall-clock: +1s (+3.58%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-14121 has successfully built against this PR. (2026-06-19 14:49:08) View Log
• ✅ Mathlib branch lean-pr-testing-14121 has successfully built against this PR. (2026-06-19 19:36:06) View Log
• ✅ Mathlib branch lean-pr-testing-14121 has successfully built against this PR. (2026-06-22 14:41:00) View Log

[Garmelon]

!bench

[leanprover-radar]

Benchmark results for 9da5dad against bc5f89f are in. There are significant results. @Garmelon

• 🟥 build//instructions: +241.2M (+0.00%)

Large changes (2✅)

• ✅ misc/import Lean//maxrss: -13MiB (-2.50%)
• ✅ misc/leanchecker --fresh Init//maxrss: -10MiB (-1.84%)

Medium changes (1✅)

• ✅ misc/re-elab Init.Data.List.Basic//maxrss: -54MiB (-7.64%)

Small changes (1✅, 4🟥)

• 🟥 build/profile/grind ring//wall-clock: +7ms (+55.33%)
• 🟥 misc/import Lean//instructions: +24.2M (+2.10%)
• 🟥 misc/import Lean//task-clock: +14ms (+8.85%)
• 🟥 misc/import Lean//wall-clock: +14ms (+9.06%)
• ✅ misc/re-elab Init.Data.List.Sublist//maxrss: -44MiB (-6.27%)

[Garmelon]

The cache eviction logic is not really related to the measure logic, so there's no need for it to live in measure.py (which is manually kept in sync across different bench suites). Instead, it should just be its own script (or part of the benchmark, until we need it in more than one place).

[Kha]

Yes a separate Python script would be fine. We'll need it in Mathlib as well. The bash script takes 54 SECONDS to run for me...