Using withTraceNode

Stream: lean4

[Eric Wieser]

I thought I'd post here to solicit some feedback on Mathlib's #19855, and whether these seem like appropriate invocations of docs#Lean.withTraceNode. Some considerations:

1. All the trace nodes have name linarith rather than something hierarchical, since trace.linarith is not an inherited trace option (if it were, then linarith.detail wouldn't work). This of course makes the trace useless without set_option trace.profiler.output.pp true.
2. There seems to be some tension between putting data in the node message vs putting it in a trace[] within the scope. If you do the former, then the trace is easier to read, but if you do the latter, then the grouping provided by the firefox profiler is more useful
3. It's not clear to me when the cost of formatting the message is paid; is this only when writing out the profile data at the very end?
4. In one case I use a trace node just to make a long message collapsible; is this reasonable, and should there be a helper to streamline this in core?

[Eric Wieser]

I suppose the other relevant question here is how to choose between recording data with the trace.profiler and profiler machinery, and whether there should be an interface that encourages the use of both simultaneously

[Eric Wieser]

(I suspect thinking about this too long isn't a great use of FRO time, but if these things have already been thought about it would be great to build on that wisdom!)

[Henrik Böving]

Regarding

Eric Wieser said:

I suppose the other relevant question here is how to choose between recording data with the trace.profiler and profiler machinery, and whether there should be an interface that encourages the use of both simultaneously

The only situation in which I use profiler is when getting the data from trace.profiler is too expensive for some reason. For example when we run bv_decide on SMTLIB it can takes gigabytes of memory and quite some time to render the trace.profiler trace (this is tweakable with pretty pritner and threshold options and what not) and with profiler you can at least get some data as to what is slow. But apart from that profiler is just inferior to trace.profiler in every regard I'd say.

[Eric Wieser]

Henrik Böving said:

it can takes gigabytes of memory and quite some time to render the trace.profiler trace

Are you using "render" in the "React in the infoview" sense, or "serialize to json" sense?

[Eric Wieser]

IIRC, the json -> string serializer has some unpleasant quadratic behavior, which makes the latter much more expensive than it should be

[Henrik Böving]

Eric Wieser said:

Henrik Böving said:

it can takes gigabytes of memory and quite some time to render the trace.profiler trace

Are you using "render" in the "React in the infoview" sense, or "serialize to json" sense?

print to stdout

[Henrik Böving]

the expensive part is not serialisations or whatever it is pretty printing of expressions, SMTLIB contains expressiosn with megabytes up to gigabytes of text size

[Eric Wieser]

The json failure I'm thinking of is lean4#5548

import Lean

def big : List Nat := List.iota 200000

-- stack overflow
#eval (String.length <| toString <| Lean.ToJson.toJson big)

[Eric Wieser]

Henrik Böving said:

the expensive part is not serialisations or whatever it is pretty printing of expressions, SMTLIB contains expressiosn with megabytes up to gigabytes of text size

Does this suggest there should be an intermediate version of output.pp which is "assemble messages but do not interpolate Exprs? Or are the SMT objects not Exprs anyway?

[Henrik Böving]

They are exprs but there are means to reduce the size of printed expressions with the pretty printer options and threshold options already anyway. Its just an example where using profiler might even begin to make sense against trace.profiler

[Eric Wieser]

Eric Wieser said:

3. It's not clear to me when the cost of formatting the message is paid; is this only when writing out the profile data at the very end?

Can someone confirm that this understanding is correct? That is, message formatting costs are not included in the profiler results?