profiling pure functions and tactics

Stream: lean4

[Rob Lewis]

The new simplex implementation for linarith isn't as fast as it could be. I'm trying to get a sense for where the slowdown is. One candidate is the Gaussian elimination subroutine. Is there a convenient way to get detailed profiling information on this, a pure function that's being called by a tactic?

[Rob Lewis]

And another question. For things that live in IO, it's easier to get/print timing information. But I'm not sure I'm doing it in the canonical/most convenient way, so I wanted to ask. If I want to figure out in which subroutines nlinarith is spending its time in the following code?

import Mathlib.Tactic.Linarith

example (a1 a2 a3 b1 b2 b3 c1 c2 c3 d1 d2 d3 : ℚ)
    (_ : a1 ≥ 0)
    (_ : a2 ≥ 0)
    (_ : a3 ≥ 0)
    (_ : b1 ≥ 0)
    (_ : b2 ≥ 0)
    (_ : b3 ≥ 0)
    (_ : c1 ≥ 0)
    (_ : c2 ≥ 0)
    (_ : c3 ≥ 0)
    (_ : d1 ≥ 0)
    (_ : d2 ≥ 0)
    (_ : d3 ≥ 0)
    (h1 : a1 + a2 + a3 = b1 + b2 + b3)
    (h2 : c1 + c2 + c3 = d1 + d2 + d3) :
    a1 * c1 + a2 * c1 + a3 * c1 + a1 * c2 + a2 * c2 + a3 * c2 + a1 * c3 + a2 * c3 + a3 * c3 ≤
    b1 * d1 + b2 * d1 + b3 * d1 + b1 * d2 + b2 * d2 + b3 * d2 + b1 * d3 + b2 * d3 + b3 * d3 := by
  nlinarith

[Rob Lewis]

set_option profiler true doesn't give me anything particularly detailed.

[Eric Wieser]

I wonder if optimizing the lean code here is worth it, vs pushing for getting compiled tactics working in mathlib

[Eric Wieser]

I think so far the rule has been "tactics are compiled only if they're in core"; but upstreaming all tactics to core doesn't sound sustainable

[Rob Lewis]

I'm still curious to hear advice about profiling :smile: but that's a fair point. The most recent discussion I can find of compiling mathlib tactics is here, there haven't been any more recent updates, have there?

[Henrik Böving]

If linarith did its job of putting trace nodes well you can use the trace.profiler option, otherwise you are pretty much out of luck / have to add trace nodes on your own

[Sebastian Ullrich]

(see also https://lean-lang.org/talks/lmu2024.pdf for a quick overview of the current state of profiling)

[Kevin Buzzard]

Great to see you taking an interest in presheaves of modules Sebastian!

[Rob Lewis]

Thanks for the tips. Is it the presence of trace nodes that makes ring, norm_num, and linarith (but no other tactics) show up when I lean --profile that example?

[Rob Lewis]

/ What's the relationship with profileitM?

[Sebastian Ullrich]

profileitM is for profiler, trace nodes are for trace.profiler

[Joachim Breitner]

Is there any hope in renaming set_option profiler to set_option something.profile to avoid confusion with the “other” profiler? :sweat_smile: