typeclass inference in linarith

Stream: mathlib4

[Heather Macbeth]

I noticed that a typical linarith call seems to spend a lot of time on typeclass inference of things like docs#AddRightStrictMono. For example, inspect the output of

import Mathlib.Tactic.Linarith
variable {K : Type*} [LinearOrderedField K] {x y : K}

set_option profiler true in
set_option profiler.threshold 10 in
example (h : x + y = 10) (h' : x + 2 * y = 18) : x = 2 := by linarith

[Heather Macbeth]

In #18714 I experimented with "hard-coding" typeclass inference, by duplicating lemmas to linarith-specific versions which assume at least the bare-minimum linarith typeclass, namely OrderedSemiring. (This was already done on most lemmas which get used in linarith, but a few had been missed.)

I'm trying to see how this affects performance.

• Do I read correctly from the output of "!bench" that the speedcenter is down again?
• Do I read correctly from the message after that that this change decreases instruction count by 0.8%? Is that good?

[Jireh Loreaux]

That's quite good!

[Frédéric Dupuis]

I think that's very good for such a small change.

[Heather Macbeth]

OK, but am I actually reading that message correctly? :)

[Frédéric Dupuis]

I think so, but let's wait for someone who actually knows something about benchmarks to chime in!

[Heather Macbeth]

File	Instructions	%
build	-111.850⬝10⁹	(-0.8%)
Mathlib.Tactic.Linarith.Lemmas	+2.82⬝10⁹	(+36.53%)

[Kim Morrison]

It looks like the benchmark bot is munging decimals here, and misrepresenting the actual result, which on the speedcenter is only -0.08%.

[Kim Morrison]

We really need to fix that. Could someone ping whoever wrote the summary bot?

[Kim Morrison]

Unfortunately, @Heather Macbeth, -0.08% is probably noise.

[Kim Morrison]

Even if there is no library-wide performance improvement, this is still a good change to make!

[Heather Macbeth]

Thanks for the explanation! Is there any chance of the speedcenter coming back soon? That would give more fine-grained performance information, right?

[Heather Macbeth]

A similar change in the linear-combination-for-inequalities code gave a 50% performance improvement (for a certain choice of denominator).

[Heather Macbeth]

Heather Macbeth said:

Is there any chance of the speedcenter coming back soon?

I think I was clicking in the wrong place -- I see it now. But I had half-remembered that the speedcenter shows time spend on broad classes of task, like "typeclass inference" -- that's not the case? It just shows per-file times?

[Heather Macbeth]

It does seem to be the case that, with this change, a few dozen analysis files get around 2% faster, which is suggestive of a genuine speedup in linarith.

[Heather Macbeth]

I wonder what the right approach would be here. Should we have special "performance" test suites for each of the major algebraic tactics?

[Eric Wieser]

I did some profiling myself in the past (for compiled rather than interpreted linarith), and also concluded that typeclass search was significant. Rewriting linarith to use Qq like ring would make (almost) all of this search happen when building Linarith.lean, rather than each time the tactic is used.

[Heather Macbeth]

I experimented a bit more and I believe the linarith speedup this change gives is real, even if it is modest on the scale of the whole library (but after all, half the library doesn't even import linarith!):

I added a performance test to the test file, eliminating the "verification" step (done by ring) so as to test just the linarith part. This example takes 3318 heartbeats on current mathlib, and 1647 heartbeats when linarith is tweaked to reduce typeclass inference.

I looked at the list of files where the summary bot reports an order-10^9 improvement in instruction count: they indeed seem to be files which are actually heavy users of linarith.

I looked at the linarith calls in the file which sees the biggest improvement: the linarith calls are all in the theorem docs#Finset.small_alternating_pow_of_small_tripling, and this theorem speeds up (on my laptop) from 3.648s to 3.264s.

[Heather Macbeth]

Given this, I think it's worth considering #18714 as a serious PR, not just an experiment. I've cleaned it up and it's ready for review.

[Yaël Dillies]

Heather Macbeth said:

I looked at the linarith calls in the file which sees the biggest improvement: the linarith calls are all in the theorem docs#Finset.small_alternating_pow_of_small_tripling, and this theorem speeds up (on my laptop) from 3.648s to 3.264s.

That's very good news! These calculations are all supposed to be trivial, but became weirdly slow on my laptop after I implemented Bhavik's suggestion to use nlinarith rather than calc

[Eric Wieser]

How easy is it to use the newish flame graph profiling tools to see where the other time is spent in linarith?

[Bhavik Mehta]

Yaël Dillies said:

Bhavik's suggestion to use nlinarith rather than calc

(to be clear, this was a suggestion to use nlinarith to solve an easy nonlinear system rather than giving a 4-line calc proof! Except it's actually 8 lots of nlinarith)

[Heather Macbeth]

For nlinarith, there's more optimization which could be done: the same process I just carried out for the lemmas used in core linarith could also be carried out for the nlinarith-preprocessor lemmas.

[Heather Macbeth]

Eric Wieser said:

How easy is it to use the newish flame graph profiling tools to see where the other time is spent in linarith?

This a tool for exploring specific examples, right? Do you have an example in mind to look at?

[Eric Wieser]

I was thinking the one you discussed above would be fine

[Heather Macbeth]

@Eric Wieser Here are profiler outputs before and
after the suggested typeclass-inference change (#18714), on the following example:

import Mathlib.Tactic.Linarith

open Lean.Elab.Tactic in
def testSorryTac : TacticM Unit := do
  let e ← getMainTarget
  let t ← `(sorryAx _)
  closeMainGoalUsing `sorry fun _ _ => elabTerm t e

example {K : Type*} [LinearOrderedField K] {x y : K}
    (h : x + y = 10) (h' : x + 2 * y ≤ 18) (h : x < 2) : False := by
  linarith (config := {discharger := testSorryTac})

[Heather Macbeth]

Anything in particular you wanted to know from the flame graph? On my laptop the timing before and after is ~107 ms, ~59ms respectively.

[Eric Wieser]

The aim behind the flame graph suggestion was to track down other key contributors to the runtime, not to evaluate your PR which I'm already sold on the premise of

[Eric Wieser]

(for instance, in my own profiling on some very large problems, I found https://github.com/leanprover-community/batteries/pull/1036 to have a significant effect)