Better support for browsing traces

[leodemoura]

This issue is a placeholder for collecting ideas and features for visualizing and filtering traces. @dselsam @Kha @Vtec234

[dselsam]

I wrote a proposal a few months back for organizing the trace messages which is germane to this discussion: https://github.com/leanprover/lean4/issues/400#issuecomment-819752356 I still think this proposal is basically right and that proper message organization and query support is an important foundation for visualization. Ideally, when we hover on a position that has trace info, there is a button to enter the "trace explorer", which is a little app in VScode that lets you add filters to the query, and then interactively click on the parts you want to expand.

[Vtec234]

Another observation in support of a "trace explorer" is that often the traces that come up are too large to reasonably print. That is, we can do it with optimized enough code, but it takes a few seconds because it is bottlenecked by delaboration, and then the resulting dump is hard to leaf through. Visualizing them interactively would solve the former issue as well since we could use the RPC mechanism to delay delaboration until it is actually needed and only invoke it on the subtraces that you expand.

[dselsam]

Yes, this could be a big win. I hope the trace explorer will let us be less conservative in collecting trace messages in the first place. Thanks to filtering and dynamic expansion, there may not be much cost in tracing every module at once (so we don't need to re-run the program to toggle a trace class).

[gebner]

As requested by Wojciech, I'm reposting here what I wrote about interactive traces on Zulip.

We should make all nested traces collapsible, and not just the nodes added using traceCtx. Concretely, the Lean API should look something like this:

withNestedTraces (cls : Name) (msg : MessageData) (k : m α) (collapsed := false) : m α

On the editor side it would be useful to have the tree structure of the traces available. This would allow us to highlight trace subtrees on hover and draw vertical guidelines to clarify the indentation for example. A minimal version of the protocol could look like this (traces are always block elements and should be rendered on new lines, therefore the indentation should be clear from nesting):

type MsgEmbed = ...
  | { trace: Trace };

interface Trace {
  indent: number; // not sure if necessary
  class: string;
  message: MessageData;
  children: Trace[] | RpcRef<Trace[]>;
}

As a remark, I'm not particularly happy about the trace classes being included on every line. They take up a lot of space. With the proposed protocol we could at least gray them out in the editor (visible but not a distraction from the actual content).

---

Some issues here are because of the design decision to do the formatting server side; the server needs to know the line width and the first line's indentation (and the RPC queries take these as arguments---though it's only the indentation atm). I think it would be completely feasible to port Lean.Format to javascript/lua and do the formatting on the client side (and would of course also do the implementation). For the stability of the protocol it might be a good idea to drop the non-standard Format.group behavior though (or to document and specify it).

[Vtec234]

withNestedTraces (cls : Name) (msg : MessageData) (k : m α) (collapsed := false) : m α

Is the intended usage the same as traceCtx? That is, we could write

def frobnicate (n : Nat) : M Unit :=
  withNestedTraces `frobnicate m!"{n}" do
    ...

and see something like

[frobnicate] 200 (click to expand)

in the trace? The fact that traceCtx cannot store a message is really annoying since we have to expand the subtrace to see what argument the function was called with, so this would be really cool.

therefore the indentation should be clear from nesting

It would be nice if we could remove the indent RPC argument. The only thing is, when indent is given, Lean will format the line up to width defaultWidth - indent. Maybe we should just pass width as an argument.

[Vtec234]

I think it would be completely feasible to port Lean.Format to javascript/lua and do the formatting on the client side (and would of course also do the implementation).

Btw, another reason why I didn't put the formatter in the client is that Lean.Format JSONs are actually several times larger than the formatted String, and this was causing noticeable lag. However the lag was on very large traces/goal states. If the trace explorer becomes very nice, and perhaps we also get the ability to hide by default + lazily expand large expressions in InteractiveCode, it would be less of an issue.

[gebner]

withNestedTraces (cls : Name) (msg : MessageData) (k : m α) (collapsed := false) : m α

Is the intended usage the same as traceCtx? That is, we could write

def frobnicate (n : Nat) : M Unit :=
  withNestedTraces `frobnicate m!"{n}" do
    ...

and see something like

[frobnicate] 200 (click to expand)

in the trace? The fact that traceCtx cannot store a message is really annoying since we have to expand the subtrace to see what argument the function was called with, so this would be really cool.

Indeed, that is exactly the plan here. This is also the motivation behind #1312. For withNestedTraces I want to put TaggedText inside MsgEmbed.

inductive MsgEmbed where
  | expr : CodeWithInfos → MsgEmbed
  | goal : InteractiveGoal → MsgEmbed
  | collapsedTrace : Name → TaggedText MsgEmbed → Nat → WithRpcRef Array_MessageData → MsgEmbed
  | trace : Name → TaggedText MsgEmbed → Array (TaggedText MsgEmbed) → MsgEmbed
  deriving Inhabited, RpcEncoding

is that Lean.Format JSONs are actually several times larger than the formatted String

We can try to use a better JSON encoding. For example encode text "foo" as "foo", or append a (append b c) as [a,b,c], or fill a as "fill": a.

[gebner]

Another cool feature would be to select which "branch" of the trace tree to open by default. This would be very useful for elaboration traces where you typically have a deep tree and want to see a specific trace deep inside the tree.

(Contrast to simp or TC synthesis, which has a shallow tree with lots of steps, and you want to see the list of steps rather than a specific one.)