feat: async kernel checking for theorems

[Kha]

PoC based on #3106 and #4460

[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 b07384acbb67ca43e58d4f5d78ec8ea81a5ad36e --onto ee430b6c80f7fbd80c3cae1804e634cb4318d147. (2024-08-02 17:34:52)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b07384acbb67ca43e58d4f5d78ec8ea81a5ad36e --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-05 16:26:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30cf3bb3bfdac33a7ab385b25e0d262e0e3d8599 --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 18:25:05)
• 💥 Mathlib branch lean-pr-testing-4902 build failed against this PR. (2024-08-16 12:52:25) View Log

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit cc66581.
There were significant changes against commit b07384a:

  Benchmark                  Metric                    Change
  =====================================================================
- import Lean                branches                    1.1%  (27.1 σ)
- import Lean                instructions                1.1%  (29.9 σ)
- lake build clean           instructions                4.9% (100.0 σ)
- lake build clean           task-clock                 33.3%  (26.9 σ)
- lake build clean           wall-clock                  8.9%  (13.6 σ)
- lake config elab           instructions                2.6%  (32.0 σ)
- lake config elab           maxrss                      4.9%  (12.7 σ)
- reduceMatch                instructions                5.5% (240.5 σ)
- reduceMatch                maxrss                      5.4%  (10.6 σ)
- stdlib                     fix level params            3.5%  (20.1 σ)
- stdlib                     instructions                1.4% (303.4 σ)
- stdlib                     maxrss                      3.6% (356.2 σ)
- stdlib                     process pre-definitions     3.7%  (41.5 σ)
- stdlib                     share common exprs          2.3%  (20.9 σ)
- stdlib                     tactic execution            3.7%  (14.6 σ)
- stdlib                     task-clock                  8.0%  (17.5 σ)
- tests/bench/ interpreted   maxrss                      4.6% (565.7 σ)
+ tests/bench/ interpreted   task-clock                -33.4% (-61.7 σ)
+ tests/bench/ interpreted   wall-clock                 -8.1% (-10.1 σ)
- workspaceSymbols           maxrss                      3.6%  (11.3 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3f3a03e.
There were significant changes against commit b07384a:

  Benchmark                  Metric                  Change
  ===================================================================
- import Lean                branches                  1.1%  (29.6 σ)
- import Lean                instructions              1.1%  (28.1 σ)
- lake build clean           instructions              5.0%  (35.7 σ)
- lake build clean           task-clock               31.6%  (19.2 σ)
- lake config elab           instructions              2.6%  (31.5 σ)
- lake config elab           maxrss                    4.9%  (13.0 σ)
- language server startup    branch-misses             4.5%  (10.3 σ)
- language server startup    maxrss                   10.1%  (11.2 σ)
- reduceMatch                instructions              5.5% (336.5 σ)
- reduceMatch                maxrss                    5.5%  (18.2 σ)
- stdlib                     attribute application     3.7%  (18.4 σ)
- stdlib                     instructions              1.4% (397.0 σ)
- stdlib                     maxrss                    3.5% (556.4 σ)
- stdlib                     share common exprs        4.1%  (10.7 σ)
- stdlib                     task-clock                8.4%  (16.6 σ)
+ stdlib                     type checking           -32.0% (-45.7 σ)
- stdlib                     wall-clock                1.6%  (10.3 σ)
- tests/bench/ interpreted   maxrss                    4.5%  (14.8 σ)
+ tests/bench/ interpreted   task-clock              -33.2% (-92.3 σ)
+ tests/bench/ interpreted   wall-clock               -7.8% (-13.5 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 23f61d1.
There were significant changes against commit b07384a:

  Benchmark                  Metric                    Change
  ======================================================================
- lake build clean           instructions                3.0%   (27.4 σ)
- lake build clean           task-clock                 14.2%   (14.2 σ)
- lake config elab           instructions                1.8%   (83.5 σ)
- lake config elab           maxrss                      1.1%   (84.6 σ)
- language server startup    maxrss                      6.2%  (453.5 σ)
- reduceMatch                instructions                5.6%  (606.4 σ)
- reduceMatch                maxrss                      1.9%  (233.9 σ)
- stdlib                     fix level params            2.1%   (55.4 σ)
- stdlib                     maxrss                      2.0%  (225.4 σ)
- stdlib                     process pre-definitions     2.5%  (108.0 σ)
- stdlib                     share common exprs          1.8%  (164.2 σ)
- stdlib                     task-clock                  3.3%   (46.5 σ)
+ stdlib                     type checking             -33.8% (-148.7 σ)
- tests/bench/ interpreted   instructions                1.8% (2225.1 σ)
- tests/bench/ interpreted   maxrss                      3.1%  (422.9 σ)
+ tests/bench/ interpreted   task-clock                -14.0%  (-18.0 σ)
- workspaceSymbols           maxrss                      2.2%  (215.9 σ)

[Kha]

!bench

[leanprover-bot]

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

[Kha]

#5864 has diverged quite a bit from this approach