feat: elaborate theorem bodies in parallel

[Kha]

Draft in need of cleanups, smaller fixes, and incremental upstreaming, opened for benchmarking

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3319266.
There were significant changes against commit 07ea626:

  Benchmark     Metric                    Change
  =========================================================
- import Lean   branch-misses               4.8%   (41.6 σ)
- import Lean   branches                  323.8% (6967.6 σ)
- import Lean   instructions              234.6% (4024.9 σ)
- import Lean   task-clock                 73.0%   (17.5 σ)
- import Lean   wall-clock                 72.7%   (17.3 σ)
- stdlib        attribute application      41.1%   (25.5 σ)
- stdlib        dsimp                      53.6%   (78.9 σ)
- stdlib        instantiate metavars       57.3%   (11.4 σ)
- stdlib        instructions                3.1%  (393.6 σ)
- stdlib        maxrss                     54.2%   (77.4 σ)
- stdlib        process pre-definitions    63.3%   (31.2 σ)
- stdlib        share common exprs         52.7%   (23.4 σ)
- stdlib        tactic execution          126.0%   (63.7 σ)
- stdlib        task-clock                 18.0%  (275.8 σ)
- stdlib        type checking              96.4%  (325.3 σ)
+ stdlib size   bytes .olean               -6.2%
+ stdlib size   lines C                    -8.0%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 600b587.
There were significant changes against commit 07ea626:

  Benchmark     Metric                    Change
  =========================================================
- stdlib        attribute application      40.7%   (52.8 σ)
- stdlib        dsimp                      50.4%  (100.0 σ)
- stdlib        fix level params           36.2%   (15.0 σ)
- stdlib        instantiate metavars       57.2%   (25.3 σ)
- stdlib        maxrss                     54.5%  (159.1 σ)
- stdlib        process pre-definitions    65.3%   (99.1 σ)
- stdlib        tactic execution          127.0%   (88.2 σ)
- stdlib        task-clock                 16.4%   (41.8 σ)
- stdlib        type checking              96.6%  (364.6 σ)
+ stdlib        wall-clock                 -2.7% (-594.3 σ)
+ stdlib size   bytes .olean               -6.2%
+ stdlib size   lines C                    -8.0%

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 9727358.
There were significant changes against commit 07ea626:

  Benchmark   Metric                    Change
  ======================================================
- stdlib      attribute application      47.2%  (18.7 σ)
- stdlib      fix level params           34.9%  (38.0 σ)
- stdlib      instantiate metavars       59.9%  (29.6 σ)
- stdlib      instructions                6.7% (991.7 σ)
- stdlib      maxrss                     54.0% (135.2 σ)
- stdlib      process pre-definitions    69.0%  (21.8 σ)
- stdlib      share common exprs         56.7% (111.7 σ)
- stdlib      tactic execution          157.6% (395.3 σ)
- stdlib      task-clock                 30.0% (625.7 σ)
- stdlib      type checking             104.3%  (67.8 σ)
- stdlib      wall-clock                  6.5%  (14.6 σ)