feat: synchronized environment extension access

[Kha]

No description provided.

[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 14:26:54)

[leanprover-bot]

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

  Benchmark                  Metric                  Change
  ===================================================================
- Init.Prelude async         branches                  1.7% (172.1 σ)
- Init.Prelude async         instructions              1.2%  (97.0 σ)
- big_do                     task-clock                7.4%  (16.2 σ)
- big_do                     wall-clock                7.4%  (16.8 σ)
- big_omega.lean             branch-misses             4.6%  (14.1 σ)
- bv_decide_mul              branch-misses             2.6%  (16.3 σ)
+ lake build no-op           instructions             -1.6% (-24.8 σ)
- simp_arith1                branch-misses             2.3%  (18.2 σ)
- stdlib                     attribute application     2.5%  (25.6 σ)
- stdlib                     dsimp                     2.4%  (58.7 σ)
- stdlib                     task-clock                1.3% (811.4 σ)
- stdlib                     wall-clock                1.7% (719.2 σ)
- tests/bench/ interpreted   task-clock                5.1%  (30.0 σ)
- tests/bench/ interpreted   wall-clock                3.1%  (33.6 σ)

[Kha]

!bench

[leanprover-bot]

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

  Benchmark            Metric                  Change
  ==============================================================
- Init.Prelude async   branches                  1.5% (1261.9 σ)
- Init.Prelude async   instructions              1.1%  (332.9 σ)
+ big_omega.lean MT    task-clock               -4.8%  (-16.6 σ)
+ big_omega.lean MT    wall-clock               -4.8%  (-16.7 σ)
+ import Lean          task-clock               -5.9%  (-15.2 σ)
+ import Lean          wall-clock               -5.9%  (-16.4 σ)
- stdlib               attribute application     2.2%   (17.9 σ)
+ stdlib               instantiate metavars     -5.3%  (-19.5 σ)
- stdlib               task-clock                1.0%   (17.0 σ)

[Kha]

!bench

[leanprover-bot]

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

[Kha]

!bench

[leanprover-bot]

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

  Benchmark                      Metric                    Change
  =========================================================================
- Init.Data.List.Sublist async   wall-clock                  6.5%  (17.8 σ)
- Init.Prelude async             branches                    1.5% (111.5 σ)
- Init.Prelude async             instructions                1.0%  (75.2 σ)
- bv_decide_inequality.lean      branch-misses               1.1%  (26.4 σ)
- bv_decide_mul                  branch-misses               2.9%  (16.6 σ)
- qsort                          task-clock                 16.5%  (44.0 σ)
- qsort                          wall-clock                 16.5%  (44.2 σ)
- rbmap_1                        task-clock                  3.5%  (11.7 σ)
- rbmap_1                        wall-clock                  3.5%  (11.2 σ)
- rbmap_fbip                     task-clock                  8.0%  (40.0 σ)
- rbmap_fbip                     wall-clock                  8.0%  (41.4 σ)
- reduceMatch                    task-clock                  6.5%  (32.7 σ)
- reduceMatch                    wall-clock                  6.5%  (32.0 σ)
+ simp_arith1                    task-clock                 -1.7% (-31.8 σ)
+ simp_arith1                    wall-clock                 -1.7% (-17.8 σ)
- stdlib                         dsimp                       1.8%  (26.9 σ)
- stdlib                         process pre-definitions     1.0%  (23.2 σ)
- stdlib                         type checking               2.8%  (30.3 σ)
- stdlib                         wall-clock                  1.6%  (11.0 σ)