chore: build Lean with Elab.async

[Kha]

No description provided.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1543a1a.
There were significant changes against commit 1248a55:

  Benchmark                      Metric                    Change
  ==========================================================================
- Init.Data.List.Sublist async   branches                    1.1%  (141.5 σ)
- Init.Data.List.Sublist async   maxrss                      9.4%   (43.5 σ)
- Init.Prelude async             maxrss                      5.7%   (12.7 σ)
- big_do                         maxrss                      4.7%   (42.7 σ)
- big_omega.lean                 maxrss                      4.2%  (132.9 σ)
- big_omega.lean MT              maxrss                      3.9%   (61.8 σ)
- binarytrees                    wall-clock                  5.0%   (13.8 σ)
- bv_decide_inequality.lean      maxrss                      1.7%   (35.9 σ)
- bv_decide_mod                  maxrss                      2.0%   (96.0 σ)
- bv_decide_mul                  maxrss                      2.8%   (59.3 σ)
- bv_decide_realworld            maxrss                      4.7%   (59.5 σ)
- identifier auto-completion     maxrss                      3.5%   (61.0 σ)
- import Lean                    branches                    7.7%  (172.6 σ)
- import Lean                    instructions                7.8%  (201.2 σ)
- import Lean                    maxrss                      4.9%  (165.3 σ)
- lake build clean               instructions                5.2%   (42.5 σ)
- lake build clean               task-clock                 11.4%   (10.3 σ)
- lake config elab               instructions                3.7%  (119.1 σ)
- lake config elab               maxrss                      7.1%  (110.4 σ)
- lake config import             instructions                8.3%  (126.0 σ)
- lake config import             maxrss                      7.3%   (65.2 σ)
- lake config tree               instructions                8.0%  (126.8 σ)
- lake config tree               maxrss                      7.4%  (108.8 σ)
- lake env                       instructions                8.4%  (370.1 σ)
- lake env                       maxrss                      7.2%   (63.3 σ)
- lake env                       task-clock                 14.9%   (15.2 σ)
- lake env                       wall-clock                 14.8%   (14.6 σ)
- lake startup                   instructions               11.2%  (421.9 σ)
- lake startup                   maxrss                     15.2%   (77.2 σ)
- language server startup        branches                    5.6%   (67.6 σ)
- language server startup        instructions                5.9%   (66.1 σ)
- language server startup        maxrss                      6.6%   (76.0 σ)
- libleanshared.so               binary size                24.4%
- qsort                          task-clock                  2.7%   (42.7 σ)
- qsort                          wall-clock                  2.7%   (35.4 σ)
- rbmap_library                  maxrss                      5.1%   (13.4 σ)
- reduceMatch                    maxrss                      4.7%  (448.5 σ)
- simp_arith1                    branches                    3.1%  (167.2 σ)
- simp_arith1                    instructions                2.9%  (193.9 σ)
- simp_arith1                    maxrss                      4.6%   (70.8 σ)
- stdlib                         attribute application     737.9%  (101.1 σ)
- stdlib                         fix level params            7.2%   (25.9 σ)
- stdlib                         instantiate metavars       12.4%   (10.1 σ)
- stdlib                         instructions                4.1% (4152.9 σ)
- stdlib                         maxrss                     28.4%  (378.9 σ)
- stdlib                         process pre-definitions    44.1%   (84.1 σ)
- stdlib                         share common exprs         12.3%  (210.7 σ)
- stdlib                         tactic execution           26.0%   (69.1 σ)
- stdlib                         task-clock                 21.4%  (181.6 σ)
- stdlib                         type checking             244.9%  (265.2 σ)
+ stdlib                         wall-clock                 -5.8%  (-24.2 σ)
- stdlib size                    bytes .olean                2.8%
- stdlib size                    lines C                    15.2%
- stdlib size                    max dynamic symbols         2.7%
- tests/bench/ interpreted       maxrss                      4.7%   (82.8 σ)
- tests/compiler                 sum binary sizes           15.1%
- workspaceSymbols               instructions               27.7% (7583.1 σ)
- workspaceSymbols               maxrss                      5.2%  (301.3 σ)

[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 1248a55d32f5fc64c7a26cd606fdf4c2908ce09c --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 15:03:00)
• ✅ Mathlib branch lean-pr-testing-6989 has successfully built against this PR. (2025-02-10 11:34:46) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 46ae4c0d7c05f5b4492278edb882ee9d137647f7 --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-10 12:40:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase feb8cc2d4ad32a5df123222565317c2103814233 --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-10 16:58:38)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 638d5ba.
There were significant changes against commit d61f506:

  Benchmark                      Metric                    Change
  ===========================================================================
- Init.Data.List.Sublist async   branches                    1.1%   (136.9 σ)
- Init.Data.List.Sublist async   maxrss                      8.3%    (13.1 σ)
- Init.Prelude async             maxrss                      5.5%    (22.3 σ)
- big_do                         maxrss                      4.5%    (83.8 σ)
- big_omega.lean                 maxrss                      3.9%    (29.8 σ)
- big_omega.lean MT              maxrss                      3.5%    (65.7 σ)
- bv_decide_inequality.lean      maxrss                      1.5%    (23.0 σ)
- bv_decide_mod                  maxrss                      2.0%   (176.5 σ)
- bv_decide_mul                  maxrss                      2.8%    (52.9 σ)
- bv_decide_realworld            maxrss                      4.7%    (40.7 σ)
- identifier auto-completion     maxrss                      3.5%   (135.2 σ)
- import Lean                    branches                    7.7%   (127.2 σ)
- import Lean                    instructions                7.8%   (148.4 σ)
- import Lean                    maxrss                      4.9%    (91.0 σ)
- lake build clean               instructions                5.3%    (44.6 σ)
- lake build clean               task-clock                  8.8%    (19.6 σ)
- lake config elab               instructions                3.7%    (97.4 σ)
- lake config elab               maxrss                      6.9%   (135.1 σ)
- lake config import             instructions                8.5%   (113.3 σ)
- lake config import             maxrss                      7.2%   (302.3 σ)
- lake config tree               instructions                8.0%   (166.8 σ)
- lake config tree               maxrss                      7.2%   (184.6 σ)
- lake env                       instructions                8.4%   (239.1 σ)
- lake env                       maxrss                      7.1%  (1309.6 σ)
- lake startup                   instructions               10.9%  (1121.6 σ)
- lake startup                   maxrss                     14.5%    (73.8 σ)
- language server startup        branches                    5.7%   (119.6 σ)
- language server startup        instructions                6.0%   (121.1 σ)
- language server startup        maxrss                      6.3%    (27.4 σ)
- libleanshared.so               binary size                24.4%
- rbmap_library                  maxrss                      5.0%    (30.3 σ)
- reduceMatch                    maxrss                      4.7%   (130.8 σ)
- simp_arith1                    branches                    3.2%    (80.4 σ)
- simp_arith1                    instructions                3.0%    (88.4 σ)
- simp_arith1                    maxrss                      4.6%   (176.0 σ)
- stdlib                         attribute application      24.6%    (27.6 σ)
- stdlib                         dsimp                      29.8%    (13.2 σ)
- stdlib                         fix level params            6.8%    (40.4 σ)
- stdlib                         instructions                4.2%  (7801.2 σ)
- stdlib                         maxrss                     28.2%   (196.9 σ)
- stdlib                         process pre-definitions    42.5%    (43.5 σ)
- stdlib                         share common exprs         12.1%    (20.2 σ)
- stdlib                         tactic execution           13.3%    (19.8 σ)
- stdlib                         task-clock                 21.4%  (2469.8 σ)
- stdlib                         type checking              37.1%    (89.8 σ)
+ stdlib                         wall-clock                 -5.4%   (-32.1 σ)
- stdlib size                    bytes .olean                2.8%
- stdlib size                    lines C                    15.1%
- stdlib size                    max dynamic symbols         2.8%
- tests/bench/ interpreted       maxrss                      4.7%   (220.2 σ)
- tests/compiler                 sum binary sizes           15.1%
- workspaceSymbols               instructions               27.3% (10994.1 σ)
- workspaceSymbols               maxrss                      5.1%    (90.4 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1a70bea.Found no runs to compare against.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1a70bea.
There were significant changes against commit 46ae4c0:

  Benchmark                      Metric                    Change
  ==========================================================================
- Init.Data.List.Sublist async   branches                    1.1%  (378.9 σ)
- Init.Data.List.Sublist async   maxrss                      8.4%   (53.2 σ)
- Init.Prelude async             maxrss                      5.5%   (22.7 σ)
- big_do                         maxrss                      4.9%   (67.8 σ)
- big_omega.lean                 maxrss                      4.1%   (84.3 σ)
- big_omega.lean MT              maxrss                      3.8%   (84.6 σ)
- bv_decide_inequality.lean      maxrss                      1.6%  (157.3 σ)
- bv_decide_mod                  maxrss                      2.1%  (119.4 σ)
- bv_decide_mul                  maxrss                      2.9%   (24.5 σ)
- bv_decide_realworld            maxrss                      4.6%   (28.0 σ)
- identifier auto-completion     maxrss                      3.6%   (60.5 σ)
- import Lean                    branches                    7.7%  (118.5 σ)
- import Lean                    instructions                7.8%  (169.2 σ)
- import Lean                    maxrss                      5.0%  (209.9 σ)
- import Lean                    task-clock                 23.2%   (34.2 σ)
- import Lean                    wall-clock                 23.2%   (34.1 σ)
- lake build clean               instructions                5.3%   (41.3 σ)
- lake build clean               task-clock                  8.9%   (25.5 σ)
- lake config elab               instructions                3.8%   (81.0 σ)
- lake config elab               maxrss                      6.9%   (98.4 σ)
- lake config import             instructions                8.6%  (370.2 σ)
- lake config import             maxrss                      7.3%  (109.6 σ)
- lake config tree               instructions                8.1%  (149.7 σ)
- lake config tree               maxrss                      7.3%   (65.2 σ)
- lake env                       instructions                8.4%  (127.8 σ)
- lake env                       maxrss                      7.3%  (133.7 σ)
- lake startup                   instructions               11.1%  (326.3 σ)
- lake startup                   maxrss                     15.0%
- lake startup                   wall-clock                 15.2%   (10.2 σ)
- language server startup        branches                    5.8%   (53.8 σ)
- language server startup        instructions                6.2%   (49.2 σ)
- language server startup        maxrss                      6.8%   (80.5 σ)
- language server startup        task-clock                  8.0%   (11.0 σ)
- parser                         maxrss                      4.1%   (12.1 σ)
- rbmap_fbip                     maxrss                      1.2%
- rbmap_library                  maxrss                      4.7%   (25.1 σ)
- reduceMatch                    maxrss                      4.7%   (44.9 σ)
- simp_arith1                    branches                    3.2%  (101.4 σ)
- simp_arith1                    instructions                3.0%  (107.2 σ)
- simp_arith1                    maxrss                      4.7%  (453.4 σ)
- stdlib                         attribute application      20.9%   (48.5 σ)
- stdlib                         dsimp                      23.4%   (22.6 σ)
- stdlib                         fix level params            7.8%   (29.5 σ)
- stdlib                         instantiate metavars        8.0%  (209.9 σ)
- stdlib                         instructions                3.1% (1554.5 σ)
- stdlib                         maxrss                     27.6%   (29.3 σ)
- stdlib                         process pre-definitions    43.9%   (21.5 σ)
- stdlib                         share common exprs          9.7%   (14.8 σ)
- stdlib                         tactic execution           13.8%   (15.8 σ)
- stdlib                         task-clock                 19.5%   (69.2 σ)
- stdlib                         type checking              39.1%   (58.8 σ)
+ stdlib                         wall-clock                 -7.1%  (-40.5 σ)
- tests/bench/ interpreted       maxrss                      4.8%  (131.3 σ)
- tests/compiler                 sum binary sizes           15.1%
- workspaceSymbols               instructions               27.4% (5996.7 σ)
- workspaceSymbols               maxrss                      5.3%  (153.6 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2c510e7.Found no runs to compare against.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2c510e7.
There were significant changes against commit feb8cc2:

  Benchmark   Metric                    Change
  =======================================================
+ liasolver   wall-clock                 -2.9%  (-11.0 σ)
- stdlib      attribute application      18.6%   (32.5 σ)
- stdlib      fix level params            7.2%   (11.7 σ)
- stdlib      instructions                2.4% (1342.2 σ)
- stdlib      maxrss                     25.1%   (69.9 σ)
- stdlib      process pre-definitions    42.7%   (30.2 σ)
- stdlib      share common exprs         11.1%   (30.1 σ)
- stdlib      tactic execution           11.7%   (30.0 σ)
- stdlib      task-clock                 17.8%  (186.4 σ)
- stdlib      type checking              39.6%  (159.3 σ)
+ stdlib      wall-clock                 -8.4%  (-57.1 σ)