trace profiler is missing more than 99% of the time

Stream: lean4

[Jason Gross]

Running time lean on test_33_extra.lean gives 138.28s user 9.81s system 95% cpu 2:34.67 total. Running grep '^\[' | grep -o '\[[0-9][^]]*\]' | grep -o '[0-9\.]*' | awk '{s+=$1} END {print s}' on the output gives 0.500827, which is much smaller. Where is all the time going? (And how do I make Lean faster on this?). (I'm using Lean (version 4.18.0, arm64-apple-darwin23.6.0, commit 11ccbced7964, Release))

[Jason Gross]

I guess lean --profile shows that most of the time is spent parsing...

[Jason Gross]

It seems that 40 min spent on parsing (on a larger version of this file) is a bit egregious. What's the complicated thing the parser is doing?

[Mario Carneiro]

there used to be an issue with exponential parsing due to backtracking. This was fixed using a cache, but my guess is that your example is somehow foiling the cache strategy

[Jason Gross]

The example is basically one big S-expression (a bunch of nested applications), cf also https://github.com/leanprover/lean4/issues/8038. What's the backtracking that would be going on? / how would you debug whether it's due to cache misses?

[Mario Carneiro]

There is also an issue that I think was never properly fixed where if you do not manually factor your grammar, e.g. using "(" term (":" term)? ")" instead of "(" term ")" and "(" term ":" term")" as separate productions, then backtracking is triggered. Most of these cases were solved in lean by manually factoring, but this is no help if a lean syntax looks similar to a user syntax. If it's two user syntaxes then there is hope you can do the factoring yourself

[Jason Gross]

The code is just

import Std.Tactic
section Test

variable {α : Type}

variable (f : α → α) (g : α → α) (h : α → α → α)
variable (a b c : α)
variable (eq_haa_a : ∀ x y : α, (h x y) = c)

set_option maxRecDepth 150000 in
example : (((h (((h ((( {more stuff here ...}  := by sorry
end Test

Is there conflicting user syntax in Std.Tactic?

[Mario Carneiro]

no, Std is in core too

[Mario Carneiro]

all core syntax is defined in one place

[Mario Carneiro]

so this is the app elaborator indeed

[Henrik Böving]

You don't even need to import Std.Tactic for this right?

[Mario Carneiro]

As for how to debug, I guess you should look at a trace message for the parser-category parser, not sure if one exists

[Mario Carneiro]

:this: even if the declarations don't exist it would presumably take forever parsing before realizing this

[Jason Gross]

I tried

set_option trace.profiler true
set_option trace.profiler.threshold 0
set_option trace.Elab.command true

but this does not include parsing. (Does this bit require Std.Tactic?) --profile shows time spent parsing, but does not give details.

[Mario Carneiro]

you can't #time parsing, because by the time you know you are timing you've already parsed

[Henrik Böving]

Yeah I don't think the parsing was ever hooked up to the verbose profiler unfortunately, but I think it definitely should be.

[Jason Gross]

sure, but even if I call the set_options above the section start, parsing still does not show up

[Henrik Böving]

The entries in trace.profiler are manually created by the meta programs with withTraceNode and the parser is presumably lacking such a trace node right now

[Mario Carneiro]

actually you might have trouble doing that, it looks like withTraceNode requires an IO extending monad and I think the parser monad is pure

[Mario Carneiro]

actually there isn't even a monad

[Mario Carneiro]

it's all explicit state passing