refactor: omega: avoid MVar machinery

[nomeata]

This PR simplifies the implementation of omega.

When constructing the proof, omega is using MVars only for the purpose of doing case analysis on Or. We can simplify the implementation a fair bit if we just produce the proof directly using Or.elim.

While it didn’t yield the performance benefits I was hoping for, this still seems a worthwhile simplification, now that we already have it.

[nomeata]

!bench

[leanprover-bot]

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

  Benchmark           Metric                 Change
  =============================================================
+ big_omega.lean      branch-misses           -5.2%   (-21.2 σ)
+ big_omega.lean      branches                -9.1%  (-829.7 σ)
+ big_omega.lean      instructions           -10.4% (-1068.9 σ)
+ big_omega.lean MT   branches               -11.4%  (-528.6 σ)
+ big_omega.lean MT   instructions           -10.9%  (-666.8 σ)
- nat_repr            task-clock               8.0%    (11.6 σ)
- nat_repr            wall-clock               7.9%    (12.3 σ)
- stdlib              instantiate metavars    12.1%    (17.7 σ)
- stdlib              share common exprs       1.7%    (10.9 σ)

[nomeata]

Mixed benchmark results, it seems. In particular instantiate metavars to show up more is strange.

[nomeata]

Especially the nat_repr benchmark showing up is strange, I did not expect any omega in

~/build/lean/lean4 $ cat ./tests/bench/nat_repr.lean
def main : List String → IO Unit
| [n] => do
  let mut s := 0
  for i in [0:n.toNat!] do
    for j in [:i] do
      s := s + j.repr.length
  IO.println s
| _ => throw $ IO.userError "give upper bound"

[nomeata]

And the mathlib perf changes are essentially empty:
http://speed.lean-fro.org/mathlib4/compare/9aa8a0ce-0c12-4365-b1be-6012a7c2698c/to/ea453449-19e9-424e-860e-2ead229239a0

Is omega used that little in mathlib?

I’m inclined to merge anyways, given the big impact on @TwoFX’s work. Any objections?

[nomeata]

I made a mistake while testing, and there is no performance gain after all. Was too good to be true in the first place.

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit c3d4f27.
There were significant changes against commit 456e6d2:

  Benchmark           Metric         Change
  =====================================================
+ big_omega.lean      branches        -9.0% (-1467.6 σ)
+ big_omega.lean      instructions   -10.4% (-1882.4 σ)
+ big_omega.lean      task-clock      -8.0%   (-10.2 σ)
+ big_omega.lean      wall-clock      -8.0%   (-10.2 σ)
+ big_omega.lean MT   branches       -11.3%  (-302.2 σ)
+ big_omega.lean MT   instructions   -10.8%  (-221.0 σ)
+ import Lean         task-clock      -7.6%   (-25.6 σ)
+ import Lean         wall-clock      -7.5%   (-25.5 σ)
+ nat_repr            task-clock      -3.8%   (-10.1 σ)
+ nat_repr            wall-clock      -3.8%   (-10.6 σ)
+ stdlib              maxrss          -1.4%   (-60.2 σ)

[nomeata]

This benchmark report looks better, although it makes me wonder if something is amiss with our benchmarks here, because I just pulled in the latest master, and didn’t change anything else. Oh well.

[nomeata]

@kim-em, do you want to have a brief look if you are ok with this change?

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5991 has successfully built against this PR. (2024-11-12 11:38:03) View Log