perf: avoid double-open per .olean file

[Kha]

This PR optimizes the filesystem accesses during importing for a ~3% win on Linux, potentially more on other platforms.

[Kha]

!bench

[Kha]

!bench

[leanprover-radar]

Benchmark results for bd1339d against 0173444 are in! @Kha

Major changes (13)

• ✅ big_beq//instructions: -138.4M (-1.2%)
• ✅ big_deceq//instructions: -139.2M (-2.6%)
• ✅ big_deceq_rec//instructions: -141.3M (-1.9%)
• ✅ big_match//instructions: -141.4M (-1.1%)
• ✅ import Lean//instructions: -112.3M (-5.7%)
• ✅ iterators (elab)//instructions: -42.1M (-1.1%)
• ✅ lake build clean//instructions: -84.1G (-3.8%)
• ✅ lake build no-op//instructions: -76.9M (-1.2%)
• ✅ lake config elab//instructions: -82.1M (-2.6%)
• ✅ lake config import//instructions: -89.6M (-5.7%)
• ✅ lake config tree//instructions: -79.4M (-4.9%)
• ✅ lake env//instructions: -81.6M (-5.1%)
• ✅ simp_arith1//instructions: -62.0M (-1.9%)

Minor changes (5)

• ✅ big_beq_rec//instructions: -138.2M (-0.6%)
• ✅ big_match_partial//instructions: -135.2M (-0.8%)
• ✅ build//instructions: -18.3G (-0.1%)
• ✅ omega_stress.lean async//instructions: -37.9M (-0.7%)
• ✅ reduceMatch//instructions: -132.2M (-0.7%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-03 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. (2025-12-04 13:59:59)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-11507 has successfully built against this PR. (2025-12-04 15:02:44) View Log
• ✅ Mathlib branch lean-pr-testing-11507 has successfully built against this PR. (2025-12-04 18:35:15) View Log