perf: do not import non-template IR for codegen

[Kha]

This PR adjusts the experimental module system to not import the IR of non-meta declarations. It does this by replacing such IR with opaque foreign declarations on export and adjusting the new compiler accordingly.

This PR should not be merged before the new compiler.

Based on #8664.

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

  Benchmark                              Metric                  Change
  ===================================================================================
+ Init size                              bytes .olean            -10.9%
- Init size                              bytes .olean.private     13.6%
- Init.Data.BitVec.Lemmas                branch-misses             4.6%      (45.8 σ)
- Init.Data.BitVec.Lemmas                branches                  8.2%     (935.1 σ)
- Init.Data.BitVec.Lemmas                instructions              7.6%     (810.1 σ)
- Init.Data.BitVec.Lemmas                wall-clock                7.0%      (26.3 σ)
- Init.Data.BitVec.Lemmas re-elab        branches                  7.8%     (111.4 σ)
- Init.Data.BitVec.Lemmas re-elab        instructions              7.3%     (112.6 σ)
- Init.Data.List.Sublist async           branches                  8.1%     (343.4 σ)
- Init.Data.List.Sublist async           instructions              7.9%     (311.4 σ)
- Init.Data.List.Sublist re-elab -j4     branches                  7.5%     (108.5 σ)
- Init.Data.List.Sublist re-elab -j4     instructions              7.4%     (120.2 σ)
+ Init.Data.List.Sublist re-elab -j4     maxrss                   -9.3%     (-22.9 σ)
- Init.Prelude async                     branches                 20.8%    (1031.1 σ)
- Init.Prelude async                     instructions             18.7%     (819.0 σ)
- Std.Data.DHashMap.Internal.RawLemmas   branches                  7.9%     (710.6 σ)
- Std.Data.DHashMap.Internal.RawLemmas   instructions              7.8%     (621.2 σ)
- Std.Data.Internal.List.Associative     branches                  7.3%     (819.4 σ)
- Std.Data.Internal.List.Associative     instructions              7.4%     (722.5 σ)
- big_do                                 branches               9373.5%      (34.5 σ)
- big_do                                 instructions           8190.4%      (27.9 σ)
- big_do                                 maxrss                  898.8%      (66.6 σ)
- big_omega.lean                         branches                  5.3%     (684.4 σ)
- big_omega.lean                         instructions              3.7%     (631.9 σ)
- big_omega.lean MT                      branches                  5.2%     (178.5 σ)
- big_omega.lean MT                      instructions              3.8%     (188.4 σ)
- bv_decide_inequality.lean              branches                  6.5%     (165.2 σ)
- bv_decide_inequality.lean              instructions              5.1%     (117.2 σ)
+ bv_decide_large_aig.lean               branches                 -5.4%    (-161.8 σ)
+ bv_decide_large_aig.lean               instructions             -4.7%    (-128.8 σ)
- bv_decide_mod                          branches                  5.9%    (3199.9 σ)
- bv_decide_mod                          instructions              4.8%    (1483.2 σ)
- bv_decide_mod                          task-clock                5.2%      (68.2 σ)
- bv_decide_mod                          wall-clock                5.1%      (28.7 σ)
- bv_decide_mul                          branches                  8.8%     (495.8 σ)
- bv_decide_mul                          instructions              7.6%     (437.6 σ)
+ bv_decide_mul                          maxrss                   -1.5%     (-53.5 σ)
- bv_decide_realworld                    branches                  9.9%     (144.7 σ)
- bv_decide_realworld                    instructions              8.2%     (118.4 σ)
- deriv                                  instructions              5.8%    (1506.7 σ)
- identifier auto-completion             branches                  3.4%      (48.8 σ)
- identifier auto-completion             instructions              3.0%      (37.3 σ)
- ilean roundtrip                        branches                  5.7%      (37.7 σ)
- ilean roundtrip                        instructions              5.3%      (83.1 σ)
+ import Lean                            branches                -14.9%   (-1031.7 σ)
+ import Lean                            instructions            -15.4%    (-908.7 σ)
+ import Lean                            maxrss                  -14.6%    (-636.3 σ)
+ lake build clean                       instructions             -2.1%    (-325.8 σ)
+ lake build clean                       task-clock               -6.8%     (-27.2 σ)
- lake config elab                       instructions              9.6%     (464.1 σ)
+ lake config elab                       maxrss                  -11.2%    (-142.5 σ)
+ lake config import                     instructions            -13.7%    (-457.1 σ)
+ lake config import                     maxrss                  -12.6%    (-243.3 σ)
+ lake config tree                       instructions            -15.4%   (-7375.4 σ)
+ lake config tree                       maxrss                  -12.6%   (-2633.5 σ)
+ lake env                               instructions            -13.4%    (-447.9 σ)
+ lake env                               maxrss                  -12.5%    (-172.9 σ)
- lake startup                           instructions              1.6%     (118.9 σ)
- language server startup                branches                  1.0%      (23.1 σ)
- liasolver                              instructions              1.0%     (168.1 σ)
+ libleanshared.so                       binary size             -12.1%
- nat_repr                               task-clock                8.3%      (34.3 σ)
- nat_repr                               wall-clock                8.2%      (35.5 σ)
- omega_stress.lean async                branches                  6.1%     (561.1 σ)
- omega_stress.lean async                instructions              5.4%     (552.3 σ)
+ parser                                 instructions             -2.3%    (-437.6 σ)
- parser                                 maxrss                    7.7%      (36.8 σ)
- rbmap                                  instructions            210.9%   (19334.8 σ)
+ rbmap_1                                instructions            -13.8%  (-23802.0 σ)
+ rbmap_1                                task-clock               -5.3%     (-21.8 σ)
+ rbmap_1                                wall-clock               -5.3%     (-21.7 σ)
- rbmap_10                               instructions            144.7%   (19625.5 σ)
- rbmap_10                               task-clock               96.5%      (22.0 σ)
- rbmap_10                               wall-clock               96.4%      (22.0 σ)
- rbmap_library                          instructions            199.4%   (39534.9 σ)
- rbmap_library                          task-clock              196.6%      (25.7 σ)
- rbmap_library                          wall-clock              196.2%      (25.7 σ)
+ reduceMatch                            instructions             -1.7%     (-44.7 σ)
- riscv-ast.lean                         branches                  3.4%      (31.5 σ)
- riscv-ast.lean                         instructions              2.9%      (22.5 σ)
- simp_arith1                            branches                  3.0%      (43.7 σ)
+ simp_arith1                            maxrss                  -12.8%     (-61.1 σ)
+ stdlib                                 maxrss                  -14.5%   (-3833.8 σ)
- stdlib size                            bytes .olean              5.1%
- stdlib size                            bytes .olean.private     13.6%
+ stdlib size                            lines C                 -18.7%
+ stdlib size                            max dynamic symbols     -12.1%
- tests/bench/ interpreted               instructions              5.9%    (4929.5 σ)
+ tests/bench/ interpreted               maxrss                  -12.6%     (-74.8 σ)
+ tests/compiler                         sum binary sizes         -8.7%
+ unionfind                              instructions             -1.7%    (-652.5 σ)
+ workspaceSymbols                       instructions            -79.3% (-604707.1 σ)
+ workspaceSymbols                       maxrss                  -15.3%    (-107.9 σ)
+ workspaceSymbols                       task-clock              -77.5%    (-562.2 σ)
+ workspaceSymbols                       wall-clock              -77.6%    (-557.7 σ)

[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 bd16c0f87d978193d2988fdd09bf906fd424a57e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-27 16:26:49)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4f2d107b524eecd9dc1c2a00b88e7d1a5d05e3f1 --onto 0aca10b228974232cd2d77cd4575a8594458c6e4. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-28 10:42:55)

[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 bd16c0f87d978193d2988fdd09bf906fd424a57e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-06-27 16:26:50)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4f2d107b524eecd9dc1c2a00b88e7d1a5d05e3f1 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-06-28 10:42:57)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2530e08.
There were significant changes against commit 4f2d107:

  Benchmark                  Metric                 Change
  ==================================================================
+ Init size                  bytes .olean           -16.8%
- Init size                  bytes .olean.private    12.4%
- binarytrees                maxrss                   1.1%  (29.8 σ)
- bv_decide_large_aig.lean   wall-clock               3.5%  (26.7 σ)
- parser                     task-clock               7.2%  (22.6 σ)
- parser                     wall-clock               7.2%  (22.5 σ)
+ stdlib size                bytes .olean            -1.3%
- stdlib size                bytes .olean.private    12.4%
+ workspaceSymbols           task-clock              -4.7% (-46.3 σ)
+ workspaceSymbols           wall-clock              -4.7% (-46.4 σ)

[Kha]

No significant instruction changes