feat: zero cost BaseIO #10625
Draft
feat: zero cost BaseIO #10625
+631,329
−578,473
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
|
!bench |
|
(I expect a performance regression from this, just want to see by how much) |
|
Here are the benchmark results for commit 9088219. Benchmark Metric Change
==================================================================================
- Init.Data.List.Sublist async branches 5.7% (40.2 σ)
- Init.Data.List.Sublist async instructions 5.1% (33.0 σ)
- Init.Prelude async branches 5.0% (27.1 σ)
- Init.Prelude async instructions 4.6% (22.9 σ)
- Std.Data.DHashMap.Internal.RawLemmas branch-misses 8.3% (25.8 σ)
- Std.Data.DHashMap.Internal.RawLemmas branches 4.6% (39.1 σ)
- Std.Data.DHashMap.Internal.RawLemmas instructions 4.3% (33.6 σ)
- Std.Data.Internal.List.Associative wall-clock 3.7% (28.4 σ)
- big_beq branch-misses 6.8% (31.7 σ)
- big_beq branches 4.7% (234.9 σ)
- big_beq instructions 4.3% (233.1 σ)
- big_beq maxrss 1.6% (26.1 σ)
- big_beq_rec branch-misses 7.4% (37.5 σ)
- big_beq_rec branches 3.3% (235.7 σ)
- big_beq_rec instructions 3.1% (219.5 σ)
- big_deceq branch-misses 5.9% (25.0 σ)
- big_deceq branches 5.8% (118.9 σ)
- big_deceq instructions 5.4% (107.1 σ)
- big_deceq_rec branch-misses 6.8% (129.7 σ)
- big_deceq_rec branches 5.7% (294.3 σ)
- big_deceq_rec instructions 5.2% (297.1 σ)
- big_do branches 6.1% (816.0 σ)
- big_do instructions 5.7% (721.7 σ)
- big_match branch-misses 6.8% (25.3 σ)
- big_match branches 5.8% (3470.6 σ)
- big_match instructions 5.3% (3023.6 σ)
- big_match maxrss 1.5% (144.4 σ)
- big_omega.lean branches 5.5% (1069.0 σ)
- big_omega.lean instructions 4.6% (255.3 σ)
- big_omega.lean MT branches 5.4% (479.8 σ)
- big_omega.lean MT instructions 4.6% (444.5 σ)
- bv_decide_mul maxrss 1.6% (28.2 σ)
- bv_decide_rewriter.lean branch-misses 21.0% (44.5 σ)
- bv_decide_rewriter.lean branches 8.0% (1192.9 σ)
- bv_decide_rewriter.lean instructions 7.5% (968.8 σ)
- bv_decide_rewriter.lean task-clock 14.3% (67.0 σ)
- bv_decide_rewriter.lean wall-clock 14.3% (35.8 σ)
- grind_bitvec2.lean branch-misses 10.3% (21.2 σ)
- grind_bitvec2.lean branches 7.2% (32.2 σ)
- grind_bitvec2.lean instructions 6.5% (27.7 σ)
- grind_list2.lean branch-misses 11.2% (32.6 σ)
- grind_list2.lean branches 8.6% (90.2 σ)
- grind_list2.lean instructions 7.9% (74.6 σ)
- grind_ring_5.lean branch-misses 5.5% (46.4 σ)
- grind_ring_5.lean branches 1.4% (215.2 σ)
- grind_ring_5.lean instructions 1.0% (159.2 σ)
- hashmap.lean branches 4.6% (2595.1 σ)
- hashmap.lean instructions 4.9% (2314.1 σ)
- identifier auto-completion branches 1.1% (47.2 σ)
- identifier auto-completion instructions 1.1% (40.2 σ)
- import Lean branches 1.6% (29.8 σ)
- import Lean instructions 1.5% (23.6 σ)
- iterators (elab) branch-misses 12.0% (40.5 σ)
- iterators (elab) branches 11.2% (502.9 σ)
- iterators (elab) instructions 11.3% (421.8 σ)
- iterators (interpreted) branches 1.6% (355.7 σ)
- iterators (interpreted) instructions 1.2% (297.9 σ)
- lake build clean instructions 1.6% (326.5 σ)
- lake config elab instructions 11.2% (571.9 σ)
- lake config elab maxrss 1.4% (38.7 σ)
- lake config import instructions 1.6% (38.9 σ)
- lake config tree instructions 1.7% (190.4 σ)
- lake env instructions 1.7% (32.3 σ)
- language server startup branches 5.2% (107.8 σ)
- language server startup instructions 5.0% (83.5 σ)
- libleanshared.so binary size 13.1%
- mut_rec_wf branch-misses 9.5% (48.6 σ)
- mut_rec_wf branches 5.8% (494.8 σ)
- mut_rec_wf instructions 5.3% (405.0 σ)
- mut_rec_wf maxrss 1.8% (21.2 σ)
- omega_stress.lean async branches 4.8% (135.6 σ)
- omega_stress.lean async instructions 4.2% (106.9 σ)
- omega_stress.lean async maxrss 2.6% (36.8 σ)
- phashmap.lean branches 2.5% (398.5 σ)
- phashmap.lean instructions 2.5% (318.1 σ)
- qsort instructions 2.2% (749.7 σ)
- reduceMatch instructions 3.4% (87.1 σ)
- riscv-ast.lean branch-misses 13.6% (68.4 σ)
- riscv-ast.lean branches 7.3% (1228.2 σ)
- riscv-ast.lean instructions 6.8% (948.7 σ)
- riscv-ast.lean task-clock 10.1% (46.8 σ)
- riscv-ast.lean wall-clock 10.9% (71.4 σ)
- simp_arith1 branches 4.6% (58.0 σ)
- simp_arith1 instructions 4.1% (38.3 σ)
- simp_bubblesort_256 branch-misses 47.1% (75.3 σ)
- simp_bubblesort_256 branches 10.9% (633.2 σ)
- simp_bubblesort_256 instructions 10.2% (611.5 σ)
- simp_congr branch-misses 14.7% (40.0 σ)
- simp_congr branches 3.4% (92.3 σ)
- simp_congr instructions 3.0% (78.6 σ)
- simp_local branch-misses 77.0% (37.0 σ)
- simp_local branches 14.1% (1085.4 σ)
- simp_local instructions 13.6% (835.1 σ)
- simp_subexpr branch-misses 44.7% (31.1 σ)
- simp_subexpr branches 10.8% (165.2 σ)
- simp_subexpr instructions 10.1% (132.7 σ)
- stdlib compilation (LCNF base) 30.2% (48.7 σ)
- stdlib compilation (LCNF mono) 24.0% (20.8 σ)
- stdlib congr simp thm 7.1% (22.5 σ)
- stdlib grind ac 48.0% (24.3 σ)
- stdlib grind ring 31.7% (27.0 σ)
- stdlib instructions 8.7% (300.3 σ)
- stdlib longest build path 11.8% (36.8 σ)
- stdlib longest rebuild path 10.8% (39.4 σ)
- stdlib process pre-definitions 3.5% (23.6 σ)
- stdlib task-clock 6.8% (35.2 σ)
- stdlib wall-clock 12.3% (80.7 σ)
- stdlib size bytes .ir 10.9%
- stdlib size bytes .olean.private 2.9%
- stdlib size lines C 15.4%
- tests/bench/ interpreted maxrss 1.5% (67.0 σ)
- tests/compiler sum binary sizes 11.6%
- treemap.lean branches 1.1% (1530.3 σ)
- treemap.lean iterate 53.1% (78.3 σ)
- workspaceSymbols maxrss 1.6% (23.0 σ)
+ workspaceSymbols with new ranges instructions -1.2% (-62.4 σ) |
hargoniX
force-pushed
the
hbv/baseio_zero
branch
4 times, most recently
from
8dc7ac4 to
3a10225
Compare
|
!bench |
|
Here are the benchmark results for commit 3a10225. Benchmark Metric Change
======================================================================================
- Init.Data.BitVec.Lemmas maxrss 71.5% (29.8 σ)
- Init.Data.BitVec.Lemmas re-elab maxrss 20.5% (74.2 σ)
- Init.Data.List.Sublist re-elab -j4 maxrss 175.3% (291.8 σ)
- Std.Data.DHashMap.Internal.RawLemmas maxrss 141.1% (21.8 σ)
- Std.Data.Internal.List.Associative maxrss 98.0% (98.1 σ)
+ big_beq branches -1.1% (-69.6 σ)
- big_beq maxrss 17.4% (349.9 σ)
- big_beq_rec maxrss 22.2% (240.0 σ)
- big_deceq maxrss 7.3% (78.7 σ)
- big_deceq_rec maxrss 10.3% (263.5 σ)
+ big_do branches -2.0% (-105.6 σ)
+ big_do instructions -2.0% (-84.3 σ)
- big_do maxrss 30.9% (119.7 σ)
- big_match maxrss 13.8% (199.9 σ)
- big_omega.lean maxrss 5.0% (24.6 σ)
- big_omega.lean MT maxrss 4.7% (87.4 σ)
- binarytrees maxrss 13.2% (285.9 σ)
+ bv_decide_mod maxrss -1.1% (-86.7 σ)
- bv_decide_rewriter.lean maxrss 8.1% (24.6 σ)
- grind_bitvec2.lean maxrss 97.9% (104.5 σ)
- grind_list2.lean maxrss 39.7% (32.5 σ)
+ iterators (elab) branches -7.8% (-547.2 σ)
+ iterators (elab) instructions -5.0% (-297.4 σ)
- iterators (elab) maxrss 103.6% (309.8 σ)
+ iterators (interpreted) branches -1.1% (-527.8 σ)
- iterators (interpreted) maxrss 102.7% (1360.2 σ)
- lake config elab instructions 1.9% (21.2 σ)
- lake config elab maxrss 15.5% (157.7 σ)
+ libleanshared.so binary size -5.2%
- mut_rec_wf maxrss 17.6% (144.0 σ)
+ nat_repr wall-clock -5.3% (-23.8 σ)
+ omega_stress.lean async branch-misses -2.5% (-36.1 σ)
- phashmap.lean branches 1.9% (191.1 σ)
- phashmap.lean instructions 1.9% (155.0 σ)
- phashmap.lean iterate 22.6% (31.5 σ)
- qsort instructions 2.1% (825.2 σ)
+ rbmap_library instructions -1.2% (-814.4 σ)
+ riscv-ast.lean branches -1.1% (-80.0 σ)
- riscv-ast.lean maxrss 114.5% (171.4 σ)
+ simp_arith1 branches -1.8% (-299.1 σ)
- simp_arith1 maxrss 13.8% (38.1 σ)
+ simp_bubblesort_256 branches -1.2% (-27.1 σ)
+ simp_bubblesort_256 instructions -1.6% (-28.7 σ)
+ simp_local branches -3.6% (-202.7 σ)
+ simp_local instructions -4.4% (-184.4 σ)
- simp_local maxrss 21.9% (124.0 σ)
+ simp_subexpr branch-misses -9.7% (-21.1 σ)
+ simp_subexpr branches -1.2% (-57.7 σ)
+ simp_subexpr instructions -1.7% (-69.5 σ)
- stdlib compilation (IR) 6.1% (76.2 σ)
- stdlib compilation (LCNF base) 26.5% (37.7 σ)
- stdlib compilation (LCNF mono) 13.7% (49.2 σ)
+ stdlib grind ematch -3.0% (-98.5 σ)
- stdlib instantiate metavars 14.7% (42.6 σ)
- stdlib let-to-have transformation 6.8% (23.9 σ)
- stdlib maxrss 723.6% (43831.4 σ)
- stdlib wall-clock 8.3% (39.0 σ)
+ stdlib size bytes .ir -7.3%
- stdlib size bytes .olean.private 2.9%
+ stdlib size lines C -7.2%
+ tests/compiler sum binary sizes -4.6%
- workspaceSymbols maxrss 1.8% (22.2 σ) |
|
!radar |
|
Benchmarking finished, results. |
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
3a10225 to
0e5100c
Compare
|
!bench |
|
Benchmark results for 0e5100c against 663d4d2 are in! @hargoniX |
|
Here are the benchmark results for commit 0e5100c. Benchmark Metric Change
================================================================================
- Init.Data.BitVec.Lemmas maxrss 72.9% (65.3 σ)
- Init.Data.List.Sublist re-elab -j4 maxrss 172.3% (430.4 σ)
- Init.Prelude async maxrss 67.9% (31.0 σ)
- Std.Data.Internal.List.Associative maxrss 99.2% (41.1 σ)
+ big_beq branches -1.6% (-72.6 σ)
- big_beq maxrss 16.1% (89.9 σ)
- big_beq_rec maxrss 20.7% (160.5 σ)
+ big_deceq branches -1.6% (-113.9 σ)
+ big_deceq instructions -1.1% (-82.3 σ)
- big_deceq maxrss 6.4% (36.9 σ)
+ big_deceq_rec branches -1.6% (-218.6 σ)
+ big_deceq_rec instructions -1.1% (-144.4 σ)
- big_deceq_rec maxrss 9.0% (44.1 σ)
- big_do maxrss 30.2% (101.3 σ)
- big_do task-clock 4.2% (23.2 σ)
- big_do wall-clock 4.3% (21.1 σ)
- big_match maxrss 10.5% (128.4 σ)
- big_omega.lean maxrss 5.3% (35.9 σ)
- binarytrees maxrss 13.2% (148.2 σ)
- bv_decide_rewriter.lean maxrss 8.4% (577.7 σ)
- grind_bitvec2.lean maxrss 97.1% (44.3 σ)
- grind_list2.lean maxrss 38.7% (39.6 σ)
- identifier auto-completion maxrss 5.6% (173.0 σ)
+ iterators (elab) branches -9.9% (-490.2 σ)
+ iterators (elab) instructions -7.2% (-274.6 σ)
- iterators (elab) maxrss 102.1% (504.7 σ)
+ iterators (interpreted) branches -1.5% (-548.6 σ)
- iterators (interpreted) maxrss 100.9% (213.4 σ)
+ lake config elab instructions -3.0% (-257.2 σ)
- lake config elab maxrss 14.6% (459.4 σ)
+ libleanshared.so binary size -2.2%
- mut_rec_wf maxrss 15.0% (55.6 σ)
- riscv-ast.lean maxrss 114.2% (321.8 σ)
+ simp_arith1 branches -2.8% (-96.3 σ)
+ simp_arith1 instructions -1.8% (-36.5 σ)
- simp_arith1 maxrss 13.6% (40.6 σ)
+ simp_bubblesort_256 branches -1.0% (-41.8 σ)
+ simp_bubblesort_256 instructions -1.4% (-36.7 σ)
+ simp_local branches -2.6% (-587.1 σ)
+ simp_local instructions -3.2% (-964.5 σ)
- simp_local maxrss 23.3% (221.4 σ)
+ simp_subexpr branches -1.1% (-35.1 σ)
+ simp_subexpr instructions -1.5% (-40.5 σ)
- stdlib compilation (LCNF base) 8.3% (86.8 σ)
- stdlib compilation (LCNF mono) 7.9% (22.8 σ)
+ stdlib instructions -2.0% (-28.6 σ)
- stdlib maxrss 682.1% (2310.9 σ)
- stdlib process pre-definitions 5.7% (32.9 σ)
- stdlib task-clock 2.3% (24.6 σ)
+ stdlib size bytes .ir -2.1%
+ stdlib size lines C -2.2%
+ tests/compiler sum binary sizes -2.0%
+ treemap.lean iterate -11.6% (-23.8 σ)
- workspaceSymbols maxrss 1.2% (52.5 σ) |
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
0e5100c to
4afc85f
Compare
|
!radar |
|
Benchmark results for 4afc85f against 663d4d2 are in! @hargoniX |
Rob23oba
reviewed
Oct 3, 2025
Rob23oba
reviewed
Oct 3, 2025
Rob23oba
reviewed
Oct 3, 2025
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
4afc85f to
751ea5a
Compare
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
751ea5a to
b45e7fb
Compare
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
b45e7fb to
d4830d3
Compare
|
!radar |
|
Benchmark results for d4830d3 against 663d4d2 are in! @hargoniX |
hargoniX
force-pushed
the
hbv/baseio_zero
branch
from
d4830d3 to
4b8007e
Compare
|
!radar |
|
Benchmark results for 4b8007e against 663d4d2 are in! @hargoniX |
|
!bench |
|
Benchmark results for 4b8007e against 663d4d2 are in! @hargoniX |
|
Here are the benchmark results for commit 4b8007e. Benchmark Metric Change
======================================================================================
+ Init.Data.List.Sublist async branches -4.4% (-26.9 σ)
+ Init.Data.List.Sublist async instructions -3.9% (-20.5 σ)
+ Init.Prelude async branches -4.3% (-66.0 σ)
+ Init.Prelude async instructions -3.8% (-44.9 σ)
+ Std.Data.DHashMap.Internal.RawLemmas branches -3.3% (-35.2 σ)
+ Std.Data.DHashMap.Internal.RawLemmas instructions -3.1% (-29.7 σ)
+ big_beq branches -3.0% (-73.0 σ)
+ big_beq instructions -2.6% (-69.6 σ)
+ big_beq_rec branch-misses -4.7% (-24.6 σ)
+ big_beq_rec branches -2.2% (-395.9 σ)
+ big_beq_rec instructions -2.0% (-269.0 σ)
+ big_deceq branches -3.0% (-228.2 σ)
+ big_deceq instructions -2.6% (-174.7 σ)
+ big_deceq_rec branch-misses -4.1% (-55.9 σ)
+ big_deceq_rec branches -3.3% (-177.3 σ)
+ big_deceq_rec instructions -2.9% (-171.5 σ)
+ big_do branches -6.2% (-2484.0 σ)
+ big_do instructions -5.8% (-1489.7 σ)
+ big_match branches -3.3% (-335.1 σ)
+ big_match instructions -2.8% (-258.8 σ)
+ big_omega.lean branches -3.6% (-190.9 σ)
+ big_omega.lean instructions -3.1% (-198.0 σ)
+ big_omega.lean MT branches -3.6% (-301.7 σ)
+ big_omega.lean MT instructions -3.0% (-292.8 σ)
- binarytrees maxrss 13.0% (30.4 σ)
+ bv_decide_rewriter.lean branch-misses -10.5% (-104.4 σ)
+ bv_decide_rewriter.lean branches -4.5% (-461.2 σ)
+ bv_decide_rewriter.lean instructions -4.2% (-757.2 σ)
+ grind_list2.lean branch-misses -6.2% (-29.9 σ)
+ grind_list2.lean branches -6.0% (-65.2 σ)
+ grind_list2.lean instructions -5.5% (-55.4 σ)
+ grind_ring_5.lean branches -3.0% (-39.2 σ)
+ grind_ring_5.lean instructions -2.5% (-30.3 σ)
+ iterators (elab) branches -6.2% (-801.1 σ)
+ iterators (elab) instructions -6.1% (-661.1 σ)
+ lake config elab instructions -4.4% (-327.9 σ)
+ language server startup branches -2.0% (-96.6 σ)
+ language server startup instructions -1.9% (-69.3 σ)
+ libleanshared.so binary size -4.4%
+ mut_rec_wf branches -3.3% (-577.8 σ)
+ mut_rec_wf instructions -2.9% (-308.2 σ)
+ omega_stress.lean async branch-misses -4.8% (-37.8 σ)
+ omega_stress.lean async branches -4.0% (-338.2 σ)
+ omega_stress.lean async instructions -3.5% (-201.2 σ)
+ reduceMatch instructions -1.9% (-93.1 σ)
+ riscv-ast.lean branches -4.9% (-637.2 σ)
+ riscv-ast.lean instructions -4.5% (-953.3 σ)
+ riscv-ast.lean wall-clock -4.5% (-23.0 σ)
+ simp_arith1 branches -2.8% (-63.9 σ)
+ simp_arith1 instructions -2.4% (-36.2 σ)
+ simp_bubblesort_256 branches -7.3% (-199.9 σ)
+ simp_bubblesort_256 instructions -7.0% (-174.5 σ)
+ simp_congr branches -2.8% (-551.6 σ)
+ simp_congr instructions -2.4% (-499.6 σ)
+ simp_local branches -8.4% (-425.2 σ)
+ simp_local instructions -8.4% (-318.4 σ)
+ simp_subexpr branches -7.3% (-272.2 σ)
+ simp_subexpr instructions -7.0% (-201.8 σ)
+ stdlib attribute application -4.9% (-43.1 σ)
+ stdlib blocked (unaccounted) -5.1% (-43.6 σ)
+ stdlib compilation (LCNF base) -8.8% (-30.9 σ)
+ stdlib dsimp -2.3% (-586.0 σ)
+ stdlib grind -6.1% (-21.5 σ)
+ stdlib grind ac -34.4% (-21.0 σ)
+ stdlib grind linarith -10.8% (-77.8 σ)
+ stdlib grind ring -16.5% (-109.3 σ)
+ stdlib grind simp -5.7% (-137.1 σ)
+ stdlib instantiate metavars -2.6% (-20.1 σ)
+ stdlib instructions -5.1% (-120.8 σ)
+ stdlib let-to-have transformation -4.7% (-130.2 σ)
+ stdlib longest build path -3.5% (-43.8 σ)
+ stdlib size bytes .ir -5.7%
+ stdlib size lines C -5.1%
+ tests/compiler sum binary sizes -3.8% |
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.
No description provided.