feat: async linting

[Kha]

This PR runs all linters for a single command (together) on a separate thread from further elaboration, making a first step towards parallelizing the elaborator.

[Kha]

!bench

[leanprover-community-mathlib4-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 237f392cc1a022ab710e388cc877e02cbcbfdd56 --onto bedcbfcfeed429428c3e7f008b6984fc8c2b2b76. (2024-06-14 14:48:40)

[leanprover-bot]

Here are the benchmark results for commit aa161a6.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit aa161a6.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4ce509b.
There were significant changes against commit 62c5bc5:

  Benchmark                  Metric                  Change
  ====================================================================
- import Lean                branch-misses             2.4%   (11.4 σ)
- import Lean                branches                  1.7%   (15.7 σ)
- import Lean                instructions              1.7%   (15.1 σ)
- lake build clean           instructions              8.1%   (81.0 σ)
- lake build clean           task-clock               54.8%   (39.0 σ)
- lake build clean           wall-clock               15.7%   (17.2 σ)
- language server startup    branch-misses            10.6%   (15.1 σ)
- language server startup    maxrss                   31.9% (1184.3 σ)
- language server startup    task-clock               34.6%   (10.5 σ)
- reduceMatch                instructions              3.5%   (41.7 σ)
- reduceMatch                maxrss                   20.7%   (12.8 σ)
- stdlib                     attribute application    17.0%   (20.8 σ)
- stdlib                     dsimp                    18.1%   (37.8 σ)
- stdlib                     instructions              5.5%  (232.5 σ)
- stdlib                     maxrss                   28.3%   (33.6 σ)
- stdlib                     tactic execution         23.9%  (194.3 σ)
- stdlib                     task-clock               31.4%   (49.1 σ)
- stdlib                     type checking            18.4%   (55.6 σ)
- stdlib                     wall-clock               14.3%   (32.8 σ)
- tests/bench/ interpreted   instructions              1.9%  (181.9 σ)
- tests/bench/ interpreted   maxrss                   12.3%   (99.1 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 656ff8f.
There were significant changes against commit 88e3a2b:

  Benchmark                  Metric                  Change
  =====================================================================
- big_do                     branches                  2.0%   (231.0 σ)
- big_do                     instructions              1.8%   (200.9 σ)
- big_do                     maxrss                    2.7%   (345.6 σ)
- big_do                     task-clock               10.0%    (42.7 σ)
- big_do                     wall-clock                9.4%    (38.2 σ)
+ big_omega.lean             branch-misses            -1.8%   (-39.5 σ)
- big_omega.lean             branches                  4.3%   (295.2 σ)
- big_omega.lean             instructions              4.3%   (282.9 σ)
- big_omega.lean             maxrss                    4.4%  (1723.6 σ)
+ bv_decide_realworld        task-clock               -3.0%   (-17.2 σ)
+ bv_decide_realworld        wall-clock               -3.0%   (-19.9 σ)
- lake config elab           maxrss                    1.7%  (1682.7 σ)
- language server startup    branch-misses             2.2%    (38.5 σ)
- language server startup    maxrss                    1.6%    (70.4 σ)
- reduceMatch                maxrss                    1.7%   (342.7 σ)
- stdlib                     attribute application     3.5%    (12.5 σ)
+ stdlib                     instantiate metavars    -10.2%   (-33.7 σ)
- stdlib                     instructions              1.7%  (3183.7 σ)
- stdlib                     maxrss                   28.3% (17764.5 σ)
- stdlib                     task-clock                5.2%    (39.3 σ)
- stdlib                     wall-clock                2.5%    (12.0 σ)
- tests/bench/ interpreted   instructions              1.9%   (399.2 σ)
- tests/bench/ interpreted   wall-clock               10.7%    (27.4 σ)

[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 88e3a2b1ab287020d5a393dc53c9441aa868681f --onto 9a17919ef11c2dba824498229633b8333a0b53d9. (2024-11-27 16:32:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 88e3a2b1ab287020d5a393dc53c9441aa868681f --onto 609346f5e03f3f2d559e7cc905f72e950c3ed8c4. (2024-11-28 10:36:30)
• 💥 Mathlib branch lean-pr-testing-4460 build failed against this PR. (2024-11-28 14:24:10) View Log
• ✅ Mathlib branch lean-pr-testing-4460 has successfully built against this PR. (2024-11-28 15:15:21) View Log
• 💥 Mathlib branch lean-pr-testing-4460 build failed against this PR. (2024-11-29 13:58:33) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 86f303774a7fbf38406ae13bd4b66f2753643a45 --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 16:18:28)
• ✅ Mathlib branch lean-pr-testing-4460 has successfully built against this PR. (2024-11-30 12:40:50) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1890ae5.
There were significant changes against commit 88e3a2b:

  Benchmark                  Metric                  Change
  ====================================================================
- big_omega.lean             branch-misses             6.0%   (51.4 σ)
- big_omega.lean             branches                  2.9%  (146.9 σ)
- big_omega.lean             instructions              3.1%  (214.8 σ)
- big_omega.lean             maxrss                    4.5% (1090.8 σ)
- big_omega.lean             task-clock                6.7%   (11.0 σ)
- big_omega.lean             wall-clock                6.7%   (11.0 σ)
+ big_omega.lean MT          branches                 -1.1%  (-48.5 σ)
- reduceMatch                maxrss                    1.8%  (886.2 σ)
- stdlib                     attribute application     3.7%   (20.0 σ)
- stdlib                     instructions              1.4%  (211.7 σ)
- stdlib                     maxrss                   28.4% (5084.2 σ)
- stdlib                     task-clock                4.5%   (34.5 σ)
- tests/bench/ interpreted   instructions              1.9%  (285.5 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7fc4163.
The entire run failed.
Found no significant differences.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit e369c3e.
There were significant changes against commit 86f3037:

  Benchmark           Metric                    Change
  ================================================================
+ big_do              branches                   -1.4%   (-92.7 σ)
+ big_do              instructions               -1.3%   (-77.9 σ)
- big_do              maxrss                      2.7%   (167.6 σ)
- big_omega.lean      branch-misses              10.8%    (12.8 σ)
- big_omega.lean      branches                    1.3%    (37.4 σ)
- big_omega.lean      instructions                1.6%    (62.5 σ)
- big_omega.lean      maxrss                      4.5%  (6452.9 σ)
+ big_omega.lean MT   branches                   -1.2%   (-72.0 σ)
+ big_omega.lean MT   instructions               -1.1%   (-45.9 σ)
- lake build clean    task-clock                  7.0%    (13.0 σ)
- lake config elab    maxrss                      1.8%   (475.0 σ)
- reduceMatch         maxrss                      1.7%   (418.8 σ)
- stdlib              fix level params            1.9%    (11.9 σ)
- stdlib              maxrss                     28.3% (71098.9 σ)
- stdlib              process pre-definitions     2.4%    (13.0 σ)
- stdlib              task-clock                  3.3%    (23.8 σ)