feat: async modes for environment access

[Kha]

This PR allows environment extensions to opt into access modes that do not block on the entire environment up to this point as a necessary prerequisite for parallel proof elaboration.

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8f4253e.
There were significant changes against commit 6865329:

  Benchmark                   Metric          Change
  ============================================================
+ big_do                      branch-misses    -1.6% (-11.7 σ)
+ big_omega.lean MT           branch-misses    -2.0% (-10.8 σ)
+ bv_decide_inequality.lean   branch-misses    -1.3% (-47.9 σ)
+ bv_decide_mul               branch-misses    -2.3% (-33.6 σ)
+ bv_decide_realworld         branch-misses    -1.4% (-19.2 σ)
+ simp_arith1                 branch-misses    -2.1% (-12.6 σ)

[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 68653297d16392f72aaf54024e06a95d355b6120 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 15:51:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68653297d16392f72aaf54024e06a95d355b6120 --onto e922edfc218090ab2e54092336c67fe3b970dfc2. (2025-01-30 15:12:13)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68653297d16392f72aaf54024e06a95d355b6120 --onto ad48761032c5750e51289f3885967c1b6f8edde5. (2025-01-31 12:16:38)
• ✅ Mathlib branch lean-pr-testing-6852 has successfully built against this PR. (2025-01-31 14:06:05) View Log
• ✅ Mathlib branch lean-pr-testing-6852 has successfully built against this PR. (2025-01-31 17:24:28) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 8f4253e.
There were significant changes against commit 6865329:

  Benchmark                   Metric          Change
  ============================================================
+ big_do                      branch-misses    -1.6% (-11.7 σ)
+ big_omega.lean MT           branch-misses    -2.0% (-10.8 σ)
+ bv_decide_inequality.lean   branch-misses    -1.3% (-47.9 σ)
+ bv_decide_mul               branch-misses    -2.3% (-33.6 σ)
+ bv_decide_realworld         branch-misses    -1.4% (-19.2 σ)
+ simp_arith1                 branch-misses    -2.1% (-12.6 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 3573efd.
There were significant changes against commit 6865329:

  Benchmark                      Metric          Change
  ===============================================================
+ Init.Data.List.Sublist async   branch-misses    -1.5% (-32.7 σ)
- Init.Data.List.Sublist async   wall-clock        7.2%  (19.6 σ)
- Init.Prelude async             wall-clock        3.1%  (14.0 σ)
- big_omega.lean MT              task-clock       10.8%  (16.8 σ)
- big_omega.lean MT              wall-clock       10.9%  (17.7 σ)
- nat_repr                       wall-clock        4.3%  (10.8 σ)
+ tests/bench/ interpreted       task-clock       -1.8% (-10.2 σ)

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 630378f.
There were significant changes against commit 6865329:

  Benchmark                      Metric         Change
  ==============================================================
- Init.Data.List.Sublist async   wall-clock       7.5%  (40.3 σ)
- Init.Prelude async             branches         1.6% (125.6 σ)
- Init.Prelude async             instructions     1.4%  (96.9 σ)
- import Lean                    task-clock      11.1%  (26.7 σ)
- import Lean                    wall-clock      11.0%  (26.3 σ)
- lake config tree               instructions     1.0%  (34.5 σ)
+ rbmap_fbip                     task-clock     -10.1% (-30.5 σ)
+ rbmap_fbip                     wall-clock     -10.1% (-33.1 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit c2a80b2.
There were significant changes against commit 6865329:

  Benchmark            Metric                 Change
  ============================================================
+ Init.Prelude async   task-clock              -3.2% (-11.3 σ)
+ Init.Prelude async   wall-clock              -2.9% (-93.7 σ)
- bv_decide_mod        task-clock               1.3%  (19.1 σ)
- bv_decide_mod        wall-clock               1.3%  (10.5 σ)
- import Lean          task-clock              12.1%  (66.3 σ)
- import Lean          wall-clock              12.1%  (57.8 σ)
- stdlib               instantiate metavars     7.1%  (43.0 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d171691.
There were significant changes against commit 6865329:

  Benchmark     Metric       Change
  ==========================================
- binarytrees   wall-clock     5.3% (15.6 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit d7ed395.
There were significant changes against commit 6865329:

  Benchmark                 Metric       Change
  =======================================================
+ language server startup   wall-clock    -1.2% (-11.4 σ)