feat: asynchronous code generation

[Kha]

This PR enables code generation to proceed in parallel to further elaboration.

It does not aim to make further refinements such as generating code for different declarations in parallel or removing the dependency on kernel checking.

[Kha]

!bench

[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 757899a7d179b3fd845d3e03031bbe360c80ef51 --onto c70f4064b4041dee70925bddbef095ebb2b36d7d. (2025-01-24 19:04:29)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 757899a7d179b3fd845d3e03031bbe360c80ef51 --onto 62788395345c7f145714157c138acd0e137ab716. (2025-01-26 20:08:50)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 757899a7d179b3fd845d3e03031bbe360c80ef51 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 13:08:18)
• ✅ Mathlib branch lean-pr-testing-6770 has successfully built against this PR. (2025-01-31 17:34:52) View Log
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-02-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2025-02-03 10:40:38)

[leanprover-bot]

Here are the benchmark results for commit 63ac64b.
There were significant changes against commit 757899a:

  Benchmark                   Metric                  Change
  ====================================================================
- Init.Prelude async          branches                  2.3% (275.1 σ)
- Init.Prelude async          instructions              1.8% (253.4 σ)
- bv_decide_inequality.lean   task-clock                1.9%  (10.2 σ)
- ilean roundtrip             parse                     3.0%  (24.3 σ)
- parser                      task-clock                4.0%  (17.9 σ)
- parser                      wall-clock                4.0%  (18.3 σ)
- stdlib                      attribute application     1.9%  (18.2 σ)
- stdlib                      type checking             2.0% (210.4 σ)

[Kha]

@zwarich FYI, you might want to take a look even though this interacts with the code generator only superficially, in compileDecls. The unification of that and compileDecl is desirable, I hope :) .

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3ace745.
There were significant changes against commit ad48761:

  Benchmark                      Metric       Change
  ============================================================
- Init.Data.List.Sublist async   task-clock     1.6%  (10.4 σ)
+ Init.Data.List.Sublist async   wall-clock    -3.1% (-14.6 σ)
- Init.Prelude async             branches       1.0% (107.1 σ)
+ big_omega.lean MT              task-clock    -2.9% (-11.6 σ)
+ big_omega.lean MT              wall-clock    -2.9% (-13.5 σ)
- stdlib                         dsimp          4.5%  (62.3 σ)

[Kha]

@leodemoura @zwarich FYI, because of how the old codegen adds these stage declarations to the environment via C++, ident elaboration will not be able to find them anymore after this PR. The old codegen itself is unaffected. I assume this is acceptable as the new codegen does not use the environment in this way anyway, thus I've removed the single test that accesses them.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 0ce68b1.
There were significant changes against commit d68c2ce:

  Benchmark                      Metric                    Change
  ==========================================================================
+ Init.Data.List.Sublist async   branches                   -1.8%  (-99.1 σ)
+ Init.Data.List.Sublist async   instructions               -1.5%  (-74.6 σ)
+ Init.Prelude async             branches                   -2.1%  (-33.8 σ)
+ Init.Prelude async             instructions               -1.7%  (-24.0 σ)
+ big_do                         task-clock                 -5.6%  (-61.5 σ)
+ big_do                         wall-clock                 -5.6%  (-64.0 σ)
- big_omega.lean MT              task-clock                  4.6%   (10.3 σ)
- big_omega.lean MT              wall-clock                  4.6%   (10.5 σ)
- binarytrees.st                 task-clock                  5.9%   (25.6 σ)
- binarytrees.st                 wall-clock                  5.9%   (25.3 σ)
- bv_decide_inequality.lean      task-clock                  4.1%   (64.3 σ)
- bv_decide_inequality.lean      wall-clock                  4.1%   (60.6 σ)
- parser                         task-clock                  5.7%   (32.4 σ)
- parser                         wall-clock                  5.7%   (31.1 σ)
- rbmap                          task-clock                  8.4%   (15.9 σ)
- rbmap                          wall-clock                  8.3%   (16.9 σ)
+ stdlib                         attribute application      -1.4%  (-20.2 σ)
+ stdlib                         process pre-definitions    -2.9%  (-17.8 σ)
+ stdlib                         tactic execution           -3.4% (-104.9 σ)
- unionfind                      task-clock                  8.5%   (12.0 σ)
- unionfind                      wall-clock                  8.5%   (12.1 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit c288ae4.
There were significant changes against commit d68c2ce:

  Benchmark                      Metric                 Change
  =======================================================================
+ Init.Data.List.Sublist async   branches                -1.9% (-191.1 σ)
+ Init.Data.List.Sublist async   instructions            -1.5% (-125.0 σ)
+ Init.Data.List.Sublist async   task-clock              -1.7%  (-11.4 σ)
+ Init.Data.List.Sublist async   wall-clock              -7.0%  (-77.1 σ)
+ Init.Prelude async             branches                -2.2% (-257.9 σ)
+ Init.Prelude async             instructions            -1.7% (-185.9 σ)
+ Init.Prelude async             wall-clock             -16.8%  (-25.3 σ)
- ilean roundtrip                compress                 6.1%   (34.0 σ)
+ ilean roundtrip                parse                   -3.8%  (-10.7 σ)
- ilean roundtrip                task-clock               3.4%   (19.8 σ)
- ilean roundtrip                wall-clock               3.4%   (19.1 σ)
- stdlib                         instantiate metavars     2.3%   (20.9 σ)