feat: async linting

[Kha]

A proof of concept for parallelism in the elaborator in a simple-to-parallelize but ultimately not significant component (<1% in both core and Mathlib, which is easily eaten up by increased synchronization overhead).

Enabling #4363 would require further thought with this.

[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)

[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 σ)