chore: re-enable Elab.async on the cmdline

[Kha]

Benchmarking PR that I intend to rebase from time to time to observe parallelism perf on the stdlib

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d0cfd88.
There were significant changes against commit b01ca8e:

  Benchmark                   Metric                    Change
  =======================================================================
- big_do                      branches                    1.1%  (222.8 σ)
- big_do                      maxrss                      5.1%   (82.3 σ)
- big_omega.lean              branches                    3.8%  (982.4 σ)
- big_omega.lean              instructions                4.1% (1878.1 σ)
- big_omega.lean              maxrss                      8.0%  (111.9 σ)
- big_omega.lean              task-clock                  5.8%   (14.0 σ)
- big_omega.lean MT           branches                    1.7%   (96.0 σ)
- big_omega.lean MT           instructions                1.8%  (210.3 σ)
- big_omega.lean MT           maxrss                     10.8%  (216.8 σ)
- bv_decide_inequality.lean   maxrss                      1.7%   (54.8 σ)
- lake build clean            task-clock                  3.8%   (14.7 σ)
- libleanshared.so            binary size                24.4%
- reduceMatch                 task-clock                  9.3%   (11.6 σ)
+ reduceMatch                 wall-clock                -36.7%  (-78.1 σ)
- simp_arith1                 branches                    1.4%   (54.7 σ)
- simp_arith1                 instructions                1.1%   (57.1 σ)
- simp_arith1                 maxrss                      1.8%   (61.0 σ)
- stdlib                      attribute application     726.5%   (73.3 σ)
- stdlib                      fix level params            4.9%   (29.6 σ)
- stdlib                      instructions                3.4%  (430.2 σ)
- stdlib                      maxrss                     26.4%   (41.0 σ)
- stdlib                      process pre-definitions    41.6%  (173.2 σ)
- stdlib                      tactic execution           21.9%   (30.5 σ)
- stdlib                      task-clock                 17.6%   (46.9 σ)
- stdlib                      type checking             238.5%  (129.7 σ)
+ stdlib                      wall-clock                 -8.3%  (-39.7 σ)
- stdlib size                 bytes .olean                2.8%
- stdlib size                 lines C                    15.2%
- stdlib size                 max dynamic symbols         2.7%
- tests/bench/ interpreted    maxrss                      3.0%   (10.6 σ)
- unionfind                   instructions                2.6% (1033.7 σ)
- workspaceSymbols            maxrss                      1.0%   (39.5 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❌ Mathlib branch lean-pr-testing-6985 built against this PR, but testing failed. (2025-02-07 11:24:52) View Log
• ❗ 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 12:26:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1248a55d32f5fc64c7a26cd606fdf4c2908ce09c --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-10 10:36:44)

[Kha]

!bench

[Kha]

!bench

[leanprover-bot]

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

  Benchmark                    Metric                    Change
  ========================================================================
- big_do                       branches                    1.2%  (108.2 σ)
- big_do                       maxrss                      6.1%  (809.0 σ)
- big_omega.lean               branches                    3.8%  (113.9 σ)
- big_omega.lean               instructions                4.1%  (169.5 σ)
- big_omega.lean               maxrss                      8.2%   (93.9 σ)
- big_omega.lean MT            branches                    1.7%   (38.0 σ)
- big_omega.lean MT            instructions                1.8%   (46.0 σ)
- big_omega.lean MT            maxrss                     11.4%  (273.2 σ)
- bv_decide_inequality.lean    maxrss                      1.5%   (12.2 σ)
+ bv_decide_inequality.lean    task-clock                 -3.6%  (-27.2 σ)
+ bv_decide_inequality.lean    wall-clock                 -4.0%  (-27.6 σ)
- identifier auto-completion   maxrss                      2.2%   (65.9 σ)
+ lake config tree             task-clock                 -8.2%  (-18.3 σ)
+ lake config tree             wall-clock                 -8.3%  (-19.0 σ)
- language server startup      branches                    1.9%   (34.8 σ)
- language server startup      instructions                2.0%   (31.4 σ)
- language server startup      maxrss                      3.9%   (24.3 σ)
- libleanshared.so             binary size                24.4%
+ parser                       task-clock                 -5.9%  (-23.7 σ)
+ parser                       wall-clock                 -5.9%  (-23.2 σ)
+ rbmap                        task-clock                 -5.0%  (-15.4 σ)
+ rbmap                        wall-clock                 -5.0%  (-13.7 σ)
+ rbmap_1                      task-clock                 -3.8%  (-20.8 σ)
+ rbmap_1                      wall-clock                 -3.8%  (-20.9 σ)
+ reduceMatch                  wall-clock                -37.8%  (-45.5 σ)
- simp_arith1                  branches                    1.5%  (129.9 σ)
- simp_arith1                  instructions                1.2%  (177.2 σ)
- simp_arith1                  maxrss                      2.2%   (32.9 σ)
- stdlib                       attribute application     734.9%  (317.8 σ)
- stdlib                       dsimp                      29.2%   (38.0 σ)
- stdlib                       instantiate metavars       10.1%   (56.2 σ)
- stdlib                       instructions                3.5% (1060.7 σ)
- stdlib                       maxrss                     27.3%   (25.4 σ)
- stdlib                       process pre-definitions    41.7%   (20.6 σ)
- stdlib                       share common exprs         13.4%   (67.2 σ)
- stdlib                       tactic execution           24.4%   (38.9 σ)
- stdlib                       task-clock                 18.5%   (62.9 σ)
- stdlib                       type checking             244.5%  (249.6 σ)
+ stdlib                       wall-clock                 -7.5%  (-51.8 σ)
- stdlib size                  bytes .olean                2.8%
- stdlib size                  lines C                    15.2%
- stdlib size                  max dynamic symbols         2.7%
- unionfind                    instructions                2.6% (1096.2 σ)
- workspaceSymbols             maxrss                      1.6%   (17.2 σ)
- workspaceSymbols             task-clock                  7.4%   (32.4 σ)
- workspaceSymbols             wall-clock                  7.1%   (31.3 σ)

[leanprover-bot]

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

  Benchmark                    Metric                    Change
  ========================================================================
- big_do                       branches                    1.2%   (53.6 σ)
- big_do                       maxrss                      6.1%   (44.3 σ)
- big_omega.lean               branches                    3.8%  (169.7 σ)
- big_omega.lean               instructions                4.1%  (204.9 σ)
- big_omega.lean               maxrss                      8.2%  (131.9 σ)
- big_omega.lean MT            branches                    1.7%  (173.6 σ)
- big_omega.lean MT            instructions                1.8%  (246.4 σ)
- big_omega.lean MT            maxrss                     11.4%  (170.4 σ)
- bv_decide_inequality.lean    maxrss                      1.6%   (52.6 σ)
- bv_decide_realworld          maxrss                      4.1%   (44.2 σ)
- deriv                        instructions                1.0%   (17.4 σ)
- identifier auto-completion   maxrss                      2.1%   (30.3 σ)
- language server startup      branches                    2.0%   (24.2 σ)
- language server startup      instructions                2.0%   (21.9 σ)
- language server startup      maxrss                      4.0%   (55.6 σ)
+ liasolver                    task-clock                 -6.2%  (-37.8 σ)
+ liasolver                    wall-clock                 -6.2%  (-29.2 σ)
- libleanshared.so             binary size                24.4%
+ nat_repr                     task-clock                 -7.9%  (-20.5 σ)
+ nat_repr                     wall-clock                 -8.0%  (-20.1 σ)
+ qsort                        task-clock                 -5.4%  (-14.7 σ)
+ qsort                        wall-clock                 -5.5%  (-14.8 σ)
+ rbmap_fbip                   task-clock                 -6.1%  (-14.0 σ)
+ rbmap_fbip                   wall-clock                 -6.1%  (-14.0 σ)
+ reduceMatch                  wall-clock                -37.8% (-146.8 σ)
- simp_arith1                  branches                    1.5%  (200.3 σ)
- simp_arith1                  instructions                1.2%  (200.2 σ)
- simp_arith1                  maxrss                      2.2%   (35.2 σ)
- stdlib                       attribute application     730.2%  (212.9 σ)
- stdlib                       dsimp                      26.4%   (10.9 σ)
- stdlib                       fix level params            5.2%  (170.7 σ)
- stdlib                       instructions                3.5% (4776.4 σ)
- stdlib                       maxrss                     26.1%  (888.6 σ)
- stdlib                       process pre-definitions    41.8%  (275.8 σ)
- stdlib                       share common exprs         13.3%   (36.5 σ)
- stdlib                       tactic execution           24.4%   (53.6 σ)
- stdlib                       task-clock                 18.9%  (141.8 σ)
- stdlib                       type checking             245.8%  (105.1 σ)
+ stdlib                       wall-clock                 -7.5% (-262.0 σ)
- stdlib size                  bytes .olean                2.8%
- stdlib size                  lines C                    15.2%
- stdlib size                  max dynamic symbols         2.7%
- tests/bench/ interpreted     maxrss                      2.2%  (192.6 σ)
- unionfind                    instructions                2.6%  (892.2 σ)
- workspaceSymbols             maxrss                      1.6%   (28.8 σ)

[Kha]

!bench

[leanprover-bot]

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

  Benchmark                    Metric                    Change
  ========================================================================
- big_do                       branches                    1.2%   (80.5 σ)
- big_do                       maxrss                      6.1%  (113.3 σ)
- big_omega.lean               branches                    3.8%  (140.4 σ)
- big_omega.lean               instructions                4.1%  (166.3 σ)
- big_omega.lean               maxrss                      8.2%   (81.9 σ)
- big_omega.lean MT            branches                    1.8%   (12.1 σ)
- big_omega.lean MT            instructions                1.9%   (10.8 σ)
- big_omega.lean MT            maxrss                     11.4%  (193.8 σ)
- bv_decide_inequality.lean    maxrss                      1.5%   (20.0 σ)
- bv_decide_realworld          maxrss                      4.3%   (70.7 σ)
- identifier auto-completion   maxrss                      2.2%   (37.9 σ)
- language server startup      branches                    1.9%   (33.1 σ)
- language server startup      instructions                2.0%   (30.3 σ)
- language server startup      maxrss                      4.0%   (34.5 σ)
- libleanshared.so             binary size                24.4%
+ parser                       task-clock                 -6.3%  (-18.8 σ)
+ parser                       wall-clock                 -6.3%  (-18.7 σ)
- reduceMatch                  maxrss                      8.6%  (222.8 σ)
- reduceMatch                  task-clock                  7.0%   (12.1 σ)
+ reduceMatch                  wall-clock                -38.4%  (-66.6 σ)
- simp_arith1                  branches                    1.5%   (62.2 σ)
- simp_arith1                  instructions                1.2%   (77.4 σ)
- simp_arith1                  maxrss                      2.3%  (109.5 σ)
- stdlib                       attribute application     742.0%  (285.4 σ)
- stdlib                       dsimp                      25.4%   (41.6 σ)
- stdlib                       fix level params            6.2%   (17.6 σ)
- stdlib                       instructions                3.5% (1414.6 σ)
- stdlib                       maxrss                     26.7%   (90.7 σ)
- stdlib                       process pre-definitions   400.6%  (299.7 σ)
- stdlib                       share common exprs         10.7%   (31.7 σ)
- stdlib                       tactic execution           24.4%  (894.5 σ)
- stdlib                       task-clock                 19.0%  (791.6 σ)
- stdlib                       type checking              38.6%  (167.0 σ)
+ stdlib                       wall-clock                 -7.6% (-280.9 σ)
- stdlib size                  bytes .olean                2.8%
- stdlib size                  lines C                    15.2%
- stdlib size                  max dynamic symbols         2.7%
- tests/bench/ interpreted     task-clock                 23.3%   (17.6 σ)
- unionfind                    instructions                2.6% (2814.7 σ)
+ unionfind                    task-clock                -10.0%  (-40.2 σ)
+ unionfind                    wall-clock                -10.0%  (-42.4 σ)
- workspaceSymbols             maxrss                      1.7%   (58.2 σ)