perf: do not import non-template IR for codegen #8666
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
awson
reviewed
Jun 7, 2025
a669013 to
bcf3155
Compare
|
!bench |
|
Here are the benchmark results for commit bcf3155. |
c31c468 to
7bf15df
Compare
meta IR|
!bench |
|
Here are the benchmark results for commit 7bf15df. |
|
!bench |
|
Here are the benchmark results for commit c360b04. |
|
!bench |
|
Here are the benchmark results for commit 2927dd2. 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 σ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adjusts the experimental module system to not import the IR of non-
metadeclarations. 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.< 8000 /p>
Based on #8664.