perf: add LEAN_ALWAYS_INLINE to some functions

[TwoFX]

Otherwise, clang refuses to inline them for large functions which leads to a performance cliff.

[TwoFX]

!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 a401368384c161e2159b0a74b32983659d3b6e36 --onto 456e6d2b791bbc560b304b28a60f35db7072c306. (2024-11-12 10:58:39)
• ✅ Mathlib branch lean-pr-testing-6045 has successfully built against this PR. (2024-11-13 13:34:18) View Log

[leanprover-bot]

Here are the benchmark results for commit b6e42f3.
There were significant changes against commit a401368:

  Benchmark             Metric          Change
  ======================================================
+ big_do                branch-misses   -21.5% (-46.2 σ)
+ big_omega.lean MT     branch-misses    -5.2% (-50.5 σ)
+ big_omega.lean MT     task-clock       -8.1% (-28.7 σ)
+ big_omega.lean MT     wall-clock       -8.2% (-25.4 σ)
+ bv_decide_mod         branch-misses    -1.0% (-10.3 σ)
+ bv_decide_mul         branch-misses    -2.6% (-44.5 σ)
+ bv_decide_realworld   branch-misses    -1.5% (-49.7 σ)
+ stdlib                type checking    -1.0% (-19.0 σ)

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit bf2e39c.
There were significant changes against commit a401368:

  Benchmark                   Metric             Change
  =================================================================
+ big_do                      branch-misses      -21.5%   (-29.7 σ)
+ big_omega.lean              branches            -1.3%   (-40.9 σ)
+ big_omega.lean MT           branch-misses       -8.4%   (-17.8 σ)
+ big_omega.lean MT           branches            -1.0%   (-33.2 σ)
+ big_omega.lean MT           task-clock          -9.2%   (-15.8 σ)
+ big_omega.lean MT           wall-clock          -9.2%   (-15.8 σ)
+ bv_decide_inequality.lean   branches            -1.0%  (-135.2 σ)
+ bv_decide_mod               branches            -1.3%   (-51.6 σ)
+ bv_decide_mul               branch-misses       -2.6%   (-44.3 σ)
+ bv_decide_mul               branches            -1.9%  (-868.7 σ)
+ bv_decide_realworld         branch-misses       -1.5%   (-36.1 σ)
+ bv_decide_realworld         branches            -1.2%  (-301.7 σ)
+ lake env                    task-clock          -8.1%   (-16.4 σ)
+ lake env                    wall-clock          -8.0%   (-19.9 σ)
- libleanshared.so            binary size          6.4%
- nat_repr                    wall-clock           5.3%    (10.2 σ)
+ rbmap_library               instructions        -3.5% (-1770.3 σ)
+ rbmap_library               task-clock         -15.3%   (-43.9 σ)
+ rbmap_library               wall-clock         -15.3%   (-41.7 σ)
+ stdlib                      fix level params    -2.8%   (-15.1 σ)
- tests/compiler              sum binary sizes     5.7%