perf: avoid negative environment lookup

[Kha]

Avoids some Environment.find? lookup misses that become especially expensive on the async branch

[Kha]

!bench

[leanprover-bot]

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

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5429 has successfully built against this PR. (2024-09-23 18:30:48) View Log

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7347fd5.
There were significant changes against commit e551a36:

  Benchmark          Metric       Change
  ================================================
+ lake build clean   task-clock    -2.7% (-30.3 σ)

[leodemoura]

This is a good change, and we should merge it as a 'fix' in a separate PR. Using getUnfoldedConstNoEx? here looks very strange, so I decided to trace its origin. It originates from Lean 3, where a function for retrieving a constant without throwing an exception was used. Since then, the code has been modified and refactored a few times, but this line was never addressed and has become increasingly odd.

[leodemoura]

The name of this function is strange. It is currently called getUnfoldableConst? but some of the cases do not even have something to unfold (e.g., recInfo).
I found two use cases for this function:

• isDeltaCandidate?: This one immediately checks whether the info has a value or not. We can optimize this for this case and have clean code.
• matchConstAux: which is used to handle orthogonal cases using the same API. We should cleanup this one. This function looks odd to me.

I prefer to cleanup and ensure the function names make sense. If we decide to not cleanup, we should add comments explaining why the function implementation is counterintuitive.

[Kha]

@leodemoura Thanks for the additional context, I reduced this PR to the reordering of operations and will rework getUnfoldableConst? in a separate PR

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7fa7c46.
There were significant changes against commit e551a36:

  Benchmark                 Metric               Change
  ===============================================================
- bv_decide_mul             branch-misses          8.1% (662.4 σ)
- bv_decide_realworld       branch-misses          7.6%  (75.8 σ)
- ilean roundtrip           branch-misses        212.9% (122.8 σ)
- import Lean               branch-misses        349.9% (757.0 σ)
- import Lean               branches               3.2%  (67.4 σ)
- import Lean               instructions           1.6%  (28.6 σ)
- lake build clean          instructions           1.7%  (55.3 σ)
- lake config import        instructions           1.4%  (21.8 σ)
- lake config tree          instructions           1.3%  (32.1 σ)
- lake env                  instructions           1.4%  (80.6 σ)
- language server startup   branch-misses        157.8% (280.5 σ)
- language server startup   task-clock            12.2%  (29.6 σ)
- language server startup   wall-clock            10.7% (767.2 σ)
- nat_repr                  branch-misses        264.2% (140.2 σ)
- rbmap_fbip                task-clock             5.6%  (10.5 σ)
- rbmap_fbip                wall-clock             5.7%  (10.2 σ)
+ reduceMatch               task-clock            -2.6% (-44.6 σ)
+ reduceMatch               wall-clock            -2.7% (-35.5 σ)
+ stdlib                    dsimp                 -2.0% (-60.6 σ)
- stdlib                    share common exprs     1.6%  (13.7 σ)
+ stdlib                    tactic execution      -1.2% (-11.8 σ)
- stdlib                    task-clock             3.1%  (50.9 σ)
+ workspaceSymbols          task-clock            -5.1% (-36.7 σ)
+ workspaceSymbols          wall-clock            -5.1% (-36.2 σ)

[Kha]

!bench

[leanprover-bot]

Here are the benchmark results for commit 489c87a.
There were significant changes against commit c779f3a:

  Benchmark             Metric       Change
  ===================================================
+ bv_decide_realworld   task-clock    -2.6% (-18.8 σ)
- rbmap_10              task-clock     2.8%  (10.8 σ)
- rbmap_10              wall-clock     2.8%  (10.5 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5429 has successfully built against this PR. (2024-11-07 15:22:02) View Log

[Kha]

Apparently this change is neutral until parallelism comes in, but I believe it is harmless enough now to go ahead with merging it