feat: asynchronous kernel checking #6368
Draft
Conversation
This file contains 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
Kha
force-pushed
the
async-tc
branch
6 times, most recently
from
06a6e24 to
b44a2ff
Compare
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
!bench |
|
Here are the benchmark results for commit 9b36754. |
|
!bench |
|
Here are the benchmark results for commit ed17ab3. Benchmark Metric Change
========================================================================
- big_do branches 4.0% (329.8 σ)
- big_do instructions 1.1% (63.6 σ)
- big_do maxrss 5.8% (124.1 σ)
+ big_omega.lean branch-misses -64.9% (-143.9 σ)
+ big_omega.lean branches -70.2% (-4059.2 σ)
+ big_omega.lean instructions -71.1% (-3756.4 σ)
+ big_omega.lean maxrss -54.7% (-105.7 σ)
+ big_omega.lean task-clock -74.6% (-347.4 σ)
+ big_omega.lean wall-clock -74.8% (-327.5 σ)
+ big_omega.lean MT branch-misses -69.1% (-546.0 σ)
+ big_omega.lean MT branches -72.4% (-9861.4 σ)
+ big_omega.lean MT instructions -72.9% (-13535.0 σ)
+ big_omega.lean MT maxrss -66.4% (-47.5 σ)
+ big_omega.lean MT task-clock -80.9% (-135.4 σ)
+ big_omega.lean MT wall-clock -80.9% (-135.2 σ)
+ binarytrees instructions -8.4% (-3211.4 σ)
+ binarytrees.st instructions -8.4% (-5177.1 σ)
- bv_decide_mul branches 1.5% (382.5 σ)
+ bv_decide_mul instructions -1.2% (-215.5 σ)
- bv_decide_mul maxrss 1.6% (42.3 σ)
+ bv_decide_realworld branches -1.5% (-178.8 σ)
+ bv_decide_realworld instructions -3.9% (-529.8 σ)
- bv_decide_realworld maxrss 4.1% (15.4 σ)
+ bv_decide_realworld task-clock -1.8% (-11.5 σ)
+ bv_decide_realworld wall-clock -2.1% (-15.1 σ)
+ const_fold instructions -3.5% (-82.7 σ)
+ deriv instructions -1.9% (-45.7 σ)
+ ilean roundtrip instructions -3.3% (-500.2 σ)
- import Lean branches 340.3% (6011.9 σ)
- import Lean instructions 238.0% (3468.3 σ)
- import Lean maxrss 2.9% (30.2 σ)
- import Lean task-clock 84.4% (17.1 σ)
- import Lean wall-clock 84.1% (17.1 σ)
- language server startup branches 50.5% (88.1 σ)
- language server startup instructions 38.5% (61.2 σ)
- language server startup wall-clock 19.1% (14.3 σ)
- liasolver instructions 3.5% (1661.0 σ)
+ liasolver maxrss -1.4% (-37.9 σ)
- libleanshared.so binary size 3.9%
+ nat_repr instructions -5.0% (-1756.3 σ)
+ parser instructions -4.4% (-1586.4 σ)
+ parser maxrss -1.4% (-37.9 σ)
+ qsort instructions -4.0% (-1866.2 σ)
+ qsort maxrss -1.4% (-16.6 σ)
- rbmap instructions 1.5% (184.0 σ)
+ rbmap_1 instructions -1.8% (-102.6 σ)
+ rbmap_fbip instructions -10.3% (-708.9 σ)
+ rbmap_library instructions -1.9% (-171.1 σ)
- reduceMatch instructions 17.1% (675.1 σ)
- reduceMatch maxrss 19.8% (820.9 σ)
- reduceMatch task-clock 12.8% (14.3 σ)
- reduceMatch wall-clock 12.4% (12.6 σ)
- simp_arith1 branch-misses 3.6% (12.7 σ)
- simp_arith1 branches 129.5% (4425.6 σ)
- simp_arith1 instructions 84.0% (2749.9 σ)
- simp_arith1 maxrss 3.6% (64.0 σ)
- simp_arith1 task-clock 43.7% (66.8 σ)
- simp_arith1 wall-clock 43.3% (55.9 σ)
- stdlib attribute application 199.1% (90.3 σ)
- stdlib dsimp 13.6% (20.7 σ)
- stdlib fix level params 10.8% (21.2 σ)
- stdlib instructions 13.0% (4005.3 σ)
- stdlib maxrss 39.4% (163.9 σ)
- stdlib process pre-definitions 162.7% (292.1 σ)
- stdlib share common exprs 12.5% (131.1 σ)
- stdlib tactic execution 25.2% (338.6 σ)
- stdlib task-clock 16.7% (1478.4 σ)
- stdlib type checking 38.8% (56.0 σ)
- stdlib wall-clock 14.9% (77.2 σ)
- stdlib size bytes .olean 2.7%
- stdlib size lines 2.3%
- stdlib size lines C 1.4%
- stdlib size max dynamic symbols 1.4%
- tests/bench/ interpreted instructions 3.1% (515.5 σ)
- tests/bench/ interpreted maxrss 3.6% (11.5 σ)
- tests/bench/ interpreted task-clock 32.8% (35.8 σ)
- tests/bench/ interpreted wall-clock 12.2% (21.4 σ)
- tests/compiler sum binary sizes 4.7%
+ unionfind instructions -8.2% (-2666.8 σ)
+ unionfind task-clock -11.6% (-20.6 σ)
+ unionfind wall-clock -11.6% (-20.6 σ)
- workspaceSymbols instructions 1.7% (2541.3 σ)
- workspaceSymbols maxrss 3.5% (73.0 σ) |
|
!bench |
|
Here are the benchmark results for commit ed17ab3. Benchmark Metric Change
========================================================================
- big_do branches 3.5% (293.7 σ)
- big_do instructions 2.7% (159.7 σ)
- big_do maxrss 5.6% (119.1 σ)
+ big_omega.lean branch-misses -65.2% (-145.9 σ)
+ big_omega.lean branches -70.4% (-4095.9 σ)
+ big_omega.lean instructions -70.7% (-3688.5 σ)
+ big_omega.lean maxrss -54.7% (-105.8 σ)
+ big_omega.lean task-clock -73.7% (-331.5 σ)
+ big_omega.lean wall-clock -73.9% (-312.6 σ)
+ big_omega.lean MT branch-misses -69.8% (-564.6 σ)
+ big_omega.lean MT branches -72.5% (-9938.0 σ)
+ big_omega.lean MT instructions -72.8% (-13467.7 σ)
+ big_omega.lean MT maxrss -66.4% (-47.4 σ)
+ big_omega.lean MT task-clock -80.1% (-129.2 σ)
+ big_omega.lean MT wall-clock -80.2% (-129.0 σ)
+ binarytrees task-clock -5.3% (-15.3 σ)
- bv_decide_mul branches 1.2% (317.9 σ)
- bv_decide_mul maxrss 1.4% (38.1 σ)
+ bv_decide_realworld branches -1.5% (-178.5 σ)
+ bv_decide_realworld instructions -2.6% (-350.6 σ)
- bv_decide_realworld maxrss 4.1% (15.6 σ)
- import Lean branch-misses 8.4% (125.8 σ)
- import Lean branches 349.4% (6047.4 σ)
- import Lean instructions 236.1% (3460.0 σ)
- import Lean maxrss 2.9% (30.4 σ)
- import Lean task-clock 74.1% (15.9 σ)
- import Lean wall-clock 74.0% (15.9 σ)
- language server startup branches 50.2% (87.7 σ)
- language server startup instructions 37.2% (59.7 σ)
- language server startup wall-clock 18.6% (14.0 σ)
- libleanshared.so binary size 1.9%
- parser instructions 1.0% (347.7 σ)
- reduceMatch instructions 17.6% (691.7 σ)
- reduceMatch maxrss 19.8% (821.3 σ)
- reduceMatch task-clock 16.1% (17.4 σ)
- reduceMatch wall-clock 15.7% (15.5 σ)
- simp_arith1 branch-misses 8.3% (28.3 σ)
- simp_arith1 branches 129.8% (4430.4 σ)
- simp_arith1 instructions 83.1% (2733.9 σ)
- simp_arith1 maxrss 3.5% (62.6 σ)
- simp_arith1 task-clock 40.1% (62.9 σ)
- simp_arith1 wall-clock 39.8% (52.7 σ)
- stdlib attribute application 204.4% (91.1 σ)
- stdlib dsimp 13.9% (21.0 σ)
- stdlib fix level params 10.3% (20.4 σ)
- stdlib instructions 13.8% (4219.1 σ)
- stdlib maxrss 39.4% (163.8 σ)
- stdlib process pre-definitions 164.7% (293.5 σ)
- stdlib share common exprs 12.7% (132.2 σ)
- stdlib tactic execution 26.8% (355.2 σ)
- stdlib task-clock 17.6% (1544.3 σ)
- stdlib type checking 39.0% (56.2 σ)
- stdlib wall-clock 15.7% (80.6 σ)
- stdlib size bytes .olean 2.7%
- stdlib size lines 2.3%
- stdlib size lines C 1.4%
- stdlib size max dynamic symbols 1.4%
- tests/bench/ interpreted instructions 5.5% (893.1 σ)
- tests/bench/ interpreted maxrss 3.5% (11.2 σ)
- tests/bench/ interpreted task-clock 36.9% (39.0 σ)
- tests/bench/ interpreted wall-clock 15.6% (26.5 σ)
- tests/compiler sum binary sizes 2.8%
- workspaceSymbols instructions 5.3% (7607.4 σ)
- workspaceSymbols maxrss 3.5% (72.3 σ) |
Kha
force-pushed
the
async-tc
branch
8 times, most recently
from
a8eb378 to
2ce35e9
Compare
|
!bench |
|
Here are the benchmark results for commit 2ce35e9. Benchmark Metric Change
=======================================================================
- big_do branch-misses 2.4% (11.4 σ)
- big_do branches 3.3% (103.6 σ)
- big_do instructions 2.3% (65.3 σ)
- big_omega.lean branch-misses 7.8% (102.8 σ)
- big_omega.lean branches 3.2% (271.3 σ)
- big_omega.lean instructions 2.7% (202.0 σ)
- big_omega.lean maxrss 5.6% (63.6 σ)
- big_omega.lean task-clock 4.2% (20.5 σ)
- big_omega.lean wall-clock 3.7% (13.9 σ)
- big_omega.lean MT branch-misses 5.9% (11.9 σ)
- big_omega.lean MT branches 3.2% (67.5 σ)
- big_omega.lean MT instructions 2.7% (57.5 σ)
- big_omega.lean MT maxrss 20.2% (253.3 σ)
- bv_decide_mul branches 1.3% (122.6 σ)
- bv_decide_realworld branches 3.0% (854.9 σ)
- bv_decide_realworld instructions 1.9% (483.3 σ)
- import Lean branch-misses 4.9% (33.7 σ)
- import Lean branches 377.9% (15941.3 σ)
- import Lean instructions 253.3% (12720.4 σ)
- import Lean task-clock 68.5% (16.4 σ)
- import Lean wall-clock 69.0% (16.6 σ)
- lake build clean instructions 490.8% (14373.2 σ)
- lake build clean maxrss 2.6% (40.1 σ)
- lake build clean task-clock 301.5% (185.0 σ)
- lake build clean wall-clock 180.7% (170.4 σ)
- lake build no-op instructions 31.4% (16.5 σ)
- lake build no-op wall-clock 17.8% (18.5 σ)
- lake config elab instructions 49.6% (3917.4 σ)
- lake config import instructions 120.9% (3907.2 σ)
- lake config tree instructions 117.2% (4229.6 σ)
- lake env instructions 118.4% (2122.8 σ)
- language server startup branch-misses 3.0% (24.8 σ)
- language server startup branches 53.0% (1831.8 σ)
- language server startup instructions 38.0% (1595.4 σ)
- language server startup task-clock 14.6% (10.7 σ)
- language server startup wall-clock 16.0% (14.1 σ)
- reduceMatch instructions 18.8% (4181.7 σ)
- reduceMatch maxrss 14.0% (586.6 σ)
- reduceMatch task-clock 15.9% (38.1 σ)
- reduceMatch wall-clock 16.0% (38.2 σ)
- simp_arith1 branch-misses 6.1% (23.1 σ)
- simp_arith1 branches 144.8% (4091.3 σ)
- simp_arith1 instructions 92.2% (3159.8 σ)
- simp_arith1 task-clock 40.9% (20.2 σ)
- simp_arith1 wall-clock 41.7% (20.6 σ)
- stdlib attribute application 695.8% (6680.8 σ)
- stdlib dsimp 11.0% (64.2 σ)
- stdlib fix level params 3.1% (62.3 σ)
- stdlib instantiate metavars 3.0% (14.1 σ)
- stdlib instructions 8.9% (5636.4 σ)
- stdlib process pre-definitions 138.1% (182.1 σ)
- stdlib share common exprs 5.3% (420.1 σ)
- stdlib tactic execution 15.6% (69.8 σ)
- stdlib task-clock 10.0% (218.6 σ)
- stdlib type checking 22.8% (193.7 σ)
- stdlib wall-clock 9.8% (20.5 σ)
- tests/bench/ interpreted instructions 2.6% (258.6 σ)
- workspaceSymbols instructions 3.2% (778.9 σ) |
|
!bench |
|
Here are the benchmark results for commit ad9df61. Benchmark Metric Change
========================================================================
- big_do branches 1.5% (104.3 σ)
- big_do instructions 1.1% (38.6 σ)
- big_omega.lean branches 2.0% (34.9 σ)
- big_omega.lean instructions 1.9% (26.7 σ)
- big_omega.lean task-clock 4.7% (18.4 σ)
- big_omega.lean wall-clock 4.2% (20.1 σ)
- big_omega.lean MT branches 2.1% (49.5 σ)
- big_omega.lean MT instructions 2.0% (67.0 σ)
- big_omega.lean MT maxrss 20.2% (314.9 σ)
- bv_decide_inequality.lean branch-misses 1.4% (10.2 σ)
- bv_decide_mul branch-misses 2.7% (13.9 σ)
- bv_decide_mul wall-clock 2.4% (25.5 σ)
+ import Lean task-clock -8.3% (-19.4 σ)
+ import Lean wall-clock -8.3% (-17.1 σ)
- lake config elab instructions 1.3% (56.5 σ)
- reduceMatch instructions 1.7% (175.6 σ)
- reduceMatch maxrss 14.0% (161.6 σ)
- reduceMatch task-clock 5.4% (12.5 σ)
- reduceMatch wall-clock 5.4% (12.0 σ)
- simp_arith1 branch-misses 2.6% (14.5 σ)
- simp_arith1 branches 1.5% (44.9 σ)
- stdlib attribute application 703.0% (171.8 σ)
- stdlib fix level params 4.1% (11.5 σ)
- stdlib instructions 4.0% (64325.6 σ)
- stdlib maxrss 4.0% (24.9 σ)
- stdlib process pre-definitions 139.6% (222.0 σ)
- stdlib share common exprs 8.3% (68.0 σ)
- stdlib tactic execution 16.4% (77.1 σ)
- stdlib task-clock 8.4% (27.4 σ)
- stdlib type checking 23.2% (38.5 σ)
- stdlib wall-clock 9.1% (139.3 σ) |
Kha
force-pushed
the
async-tc
branch
5 times, most recently
from
d519e08 to
46d0d13
Compare
|
!bench |
|
Here are the benchmark results for commit 46d0d13. Benchmark Metric Change
=======================================================================
- big_do branch-misses 3.8% (10.3 σ)
- big_do branches 1.1% (70.8 σ)
- big_omega.lean instructions 1.1% (99.7 σ)
- big_omega.lean maxrss 6.0% (85.7 σ)
- big_omega.lean MT branches 1.1% (63.8 σ)
- big_omega.lean MT instructions 1.2% (101.3 σ)
- big_omega.lean MT maxrss 20.3% (6675.9 σ)
- bv_decide_inequality.lean branch-misses 1.5% (23.6 σ)
- bv_decide_mul branch-misses 2.6% (18.8 σ)
- bv_decide_realworld maxrss 2.8% (23.4 σ)
- lake config tree instructions 1.0% (30.4 σ)
- reduceMatch maxrss 14.7% (293.2 σ)
- simp_arith1 branch-misses 6.1% (11.3 σ)
- simp_arith1 branches 1.4% (28.6 σ)
- stdlib attribute application 719.2% (176.0 σ)
- stdlib fix level params 10.5% (26.1 σ)
- stdlib instructions 9.1% (8388.2 σ)
- stdlib maxrss 4.0% (86.3 σ)
- stdlib process pre-definitions 137.1% (744.4 σ)
- stdlib share common exprs 9.8% (41.2 σ)
- stdlib tactic execution 52.0% (95.5 σ)
- stdlib task-clock 12.5% (77.5 σ)
- stdlib type checking 24.2% (124.0 σ)
- stdlib wall-clock 17.6% (25.6 σ)
- stdlib size bytes .olean 1.1%
- stdlib size lines 2.4%
- tests/bench/ interpreted maxrss 1.3% (40.6 σ)
- workspaceSymbols instructions 1.5% (1105.7 σ) |
Kha
force-pushed
the
async-tc
branch
2 times, most recently
from
49d5cf6 to
4a8e19c
Compare
|
!bench |
|
Here are the benchmark results for commit 4a8e19c. Benchmark Metric Change
======================================================================
- big_do branch-misses 2.1% (33.5 σ)
- big_do task-clock 7.9% (28.6 σ)
- big_do wall-clock 8.0% (28.4 σ)
- big_omega.lean maxrss 3.8% (79.2 σ)
- big_omega.lean task-clock 2.9% (13.7 σ)
- big_omega.lean MT maxrss 20.4% (200.0 σ)
+ big_omega.lean MT task-clock -8.0% (-33.0 σ)
+ big_omega.lean MT wall-clock -11.9% (-46.6 σ)
- bv_decide_realworld maxrss 2.7% (11.6 σ)
+ import Lean task-clock -8.4% (-18.2 σ)
+ import Lean wall-clock -8.4% (-18.9 σ)
- reduceMatch maxrss 14.7% (478.3 σ)
- simp_arith1 branch-misses 3.3% (19.2 σ)
- simp_arith1 branches 1.0% (140.0 σ)
- simp_arith1 maxrss 1.2% (19.4 σ)
- stdlib attribute application 60.3% (80.4 σ)
- stdlib fix level params 10.6% (13.6 σ)
- stdlib instantiate metavars 17.2% (17.2 σ)
- stdlib instructions 8.7% (9549.8 σ)
- stdlib maxrss 3.7% (120.7 σ)
- stdlib process pre-definitions 141.2% (478.3 σ)
- stdlib share common exprs 9.9% (23.6 σ)
- stdlib tactic execution 54.0% (130.1 σ)
- stdlib task-clock 12.0% (53.0 σ)
- stdlib type checking 25.0% (243.4 σ)
- stdlib wall-clock 12.1% (185.2 σ)
- stdlib size bytes .olean 1.1%
- stdlib size lines 2.4%
- tests/bench/ interpreted maxrss 1.3% (30.4 σ)
- workspaceSymbols instructions 1.5% (742.4 σ) |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jan 22, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 22, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jan 22, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 22, 2025
leanprover-community-bot
added
the
breaks-mathlib
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 implements executing kernel checking in parallel to elaboration, which is a prerequisite for parallelizing elaboration itself.
Stacked on #6214