perf: restrict imported IR

[Kha]

This PR adjusts the experimental module system such that on the IR level (Lean.IR.declMapExt), we import full IR with bodies only for meta defs, meta imports, or in the language server. Otherwise, only declaration signatures are imported for use in codegen.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0eae3b879089c6455bcd6c68d3561d0f4c36e15 --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-07 13:10:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d46188de54f86c64cef85aaba800f4171ccffcd5 --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-07 15:36:03)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c2876a1a6a42e6df458ffb37abbc3868632beb58 --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. (2025-06-13 14:10:50)
  Forcing Mathlib CI because the force-mathlib-ci label is present, despite problem: - ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fe1b40703131756bb6af786f4c2c131a09bf0a01 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. (2025-06-27 13:29:58)
• ✅ Mathlib branch lean-pr-testing-8664 has successfully built against this PR. (2025-06-27 14:17:10) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5baee9d.
There were significant changes against commit f0eae3b:

  Benchmark                      Metric                Change
  ======================================================================
+ Init size                      bytes .olean           -6.6%
+ Init size                      bytes .olean.server   -99.5%
- Init.Data.List.Sublist async   branches                1.0%   (45.4 σ)
- Init.Data.List.Sublist async   instructions            1.0%   (41.0 σ)
+ bv_decide_inequality.lean      task-clock             -1.2%  (-25.8 σ)
- import Lean                    branches                7.7% (2133.9 σ)
- import Lean                    instructions            7.1% (1315.9 σ)
- lake build clean               instructions           11.9%  (786.5 σ)
- lake build clean               task-clock              6.9%   (51.1 σ)
- lake config elab               instructions            3.3%  (719.6 σ)
- language server startup        branches                5.0%  (143.3 σ)
- language server startup        instructions            5.0%  (119.0 σ)
+ riscv-ast.lean                 task-clock            -10.9%  (-39.0 σ)
+ riscv-ast.lean                 wall-clock             -9.3%  (-21.7 σ)
- simp_arith1                    branches                4.1%   (70.8 σ)
- simp_arith1                    instructions            3.6%   (54.7 σ)
+ stdlib                         dsimp                  -2.8%  (-35.8 σ)
- stdlib                         grind                   1.9%  (190.9 σ)
- stdlib                         instructions            1.1%  (539.1 σ)
+ stdlib size                    bytes .olean.server   -99.5%
- workspaceSymbols               task-clock              8.1%  (568.3 σ)
- workspaceSymbols               wall-clock              8.1%  (750.2 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 13e0309.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5920be2.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5920be2.
The entire run failed.
Found no significant differences.

[leanprover-bot]

Here are the benchmark results for commit 5920be2.
There were significant changes against commit d46188d:

  Benchmark                 Metric                Change
  ================================================================
+ Init size                 bytes .olean           -6.6%
+ Init size                 bytes .olean.server   -99.5%
- import Lean               branches                7.8% (285.1 σ)
- import Lean               instructions            7.2% (250.7 σ)
- lake build clean          instructions           12.1% (203.7 σ)
- lake build clean          task-clock              6.1%  (84.7 σ)
- lake build clean          wall-clock              5.9%  (29.2 σ)
- lake config elab          instructions            3.6% (468.2 σ)
- language server startup   branches                4.9% (194.3 σ)
- language server startup   instructions            4.9% (155.6 σ)
- riscv-ast.lean            maxrss                  3.0%  (30.4 σ)
- simp_arith1               branches                4.2%  (49.5 σ)
- simp_arith1               instructions            3.7%  (38.4 σ)
+ stdlib                    blocked                -1.7% (-24.1 σ)
- stdlib                    instructions            1.2% (549.8 σ)
+ stdlib size               bytes .olean.server   -99.5%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d7cc85d.
There were significant changes against commit d46188d:

  Benchmark                 Metric          Change
  ==========================================================
+ Init size                 bytes .olean     -6.6%
+ bv_decide_mod             task-clock       -1.2% (-20.3 σ)
- import Lean               branches          7.8% (978.8 σ)
- import Lean               instructions      7.2% (712.7 σ)
- lake build clean          instructions     12.0% (340.1 σ)
- lake build clean          task-clock        7.5%  (28.6 σ)
- lake config elab          instructions      3.6% (408.4 σ)
- lake env                  instructions      7.3% (359.9 σ)
- language server startup   branches          5.0% (381.9 σ)
- language server startup   instructions      5.0% (254.7 σ)
- language server startup   wall-clock        5.7%  (21.4 σ)
- omega_stress.lean async   branch-misses     3.0%  (26.6 σ)
- simp_arith1               branches          4.3%  (56.6 σ)
- simp_arith1               instructions      3.8%  (38.6 σ)
- stdlib                    instructions      1.2% (340.2 σ)
- workspaceSymbols          task-clock        4.3%  (66.2 σ)
- workspaceSymbols          wall-clock        4.3%  (67.7 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d779f12.
There were significant changes against commit c2876a1:

  Benchmark                            Metric                     Change
  =================================================================================
+ Init size                            bytes .olean                -4.7%
- Init size                            bytes .olean.server         82.3%
- Init.Data.List.Sublist re-elab -j4   maxrss                       1.4%   (21.4 σ)
- import Lean                          branches                     7.2% (1948.8 σ)
- import Lean                          instructions                 6.7% (1163.2 σ)
- lake build clean                     instructions                10.8%  (210.4 σ)
- lake build clean                     task-clock                   9.2%   (62.8 σ)
- lake build no-op                     instructions                 1.2%   (28.8 σ)
- lake config elab                     maxrss                       1.1%   (44.8 σ)
- lake config import                   instructions                 6.3%   (80.6 σ)
- lake config tree                     instructions                 5.8%   (90.0 σ)
- lake config tree                     maxrss                       1.3%   (21.5 σ)
- lake env                             instructions                 6.2%  (100.6 σ)
- lake env                             maxrss                       1.5%   (55.5 σ)
- language server startup              branches                     3.9%  (118.0 σ)
- language server startup              instructions                 3.9%  (102.2 σ)
- simp_arith1                          branches                     3.8%  (887.1 σ)
- simp_arith1                          instructions                 3.3%  (526.6 σ)
+ stdlib                               grind dsimp                 -9.0%  (-38.9 σ)
- stdlib                               number of imported bytes     2.5%
- stdlib size                          bytes .olean.server         82.3%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit a508e01.
There were significant changes against commit c2876a1:

  Benchmark                   Metric                     Change
  =======================================================================
+ Init size                   bytes .olean                -4.7%
+ bv_decide_inequality.lean   task-clock                  -3.5% (-44.8 σ)
- bv_decide_mod               task-clock                   2.9%  (62.3 σ)
- bv_decide_mod               wall-clock                   2.9% (135.5 σ)
- bv_decide_mul               maxrss                       1.2%  (35.7 σ)
+ channel.lean                unbounded_seq               -5.4%
- import Lean                 branches                     8.3% (475.2 σ)
- import Lean                 instructions                 8.2% (568.2 σ)
- import Lean                 maxrss                       1.2%  (43.7 σ)
- lake build clean            instructions                14.8% (145.3 σ)
- lake build clean            task-clock                  16.4%  (52.4 σ)
- lake build clean            wall-clock                  15.0% (515.5 σ)
- lake config elab            maxrss                       1.5% (189.9 σ)
- lake config import          instructions                 8.5% (234.6 σ)
- lake config import          maxrss                       2.1%  (49.4 σ)
- lake config tree            instructions                 7.9% (299.8 σ)
- lake config tree            maxrss                       2.0%  (79.3 σ)
- lake env                    instructions                 8.5% (107.2 σ)
- lake env                    maxrss                       2.1% (140.3 σ)
- language server startup     branches                     5.4% (182.7 σ)
- language server startup     instructions                 6.0% (162.6 σ)
- omega_stress.lean async     branch-misses                4.9%  (57.9 σ)
- omega_stress.lean async     branches                     1.1% (158.0 σ)
- omega_stress.lean async     instructions                 1.2% (212.2 σ)
- simp_arith1                 branches                     4.3% (280.3 σ)
- simp_arith1                 instructions                 4.1% (278.8 σ)
- stdlib                      number of imported bytes     2.7%
- stdlib                      tactic execution             1.2%  (65.7 σ)
- tests/bench/ interpreted    wall-clock                   2.9%  (45.0 σ)

[Kha]

@tydeu FYI, this is just a copy-paste for now but I assume will be relevant for landing the full --setup

[Kha]

@tydeu I think I'll actually move these to a separate PR for reviewing purposes since nothing should break in the meantime in practice even with USE_LAKE