Expandable trace API

Stream: lean4

[Gabriel Ebner]

The new expandable traces are really cool. I've been trying to create such a trace. Is traceCtx the correct API to use? With traceCtx I can only create nodes without text:

▶ 5:27-5:27: information:
[Tactic.librarySearch] proving 0 ≠ 1 + 1
  [Tactic.librarySearch] ▶
  [Tactic.librarySearch] ▶
  [Tactic.librarySearch] ▶

Ideally, I'd like to add some more text like this:

▶ 5:27-5:27: information:
[Tactic.librarySearch] proving 0 ≠ 1 + 1
  [Tactic.librarySearch] trying ne_of_gt ▶
  [Tactic.librarySearch] trying List.ne_of_not_mem_cons ▶
  [Tactic.librarySearch] trying ne_of_lt ▶

[Gabriel Ebner]

(As a side note: it is mildly infuriating that the "clickable area" does not begin at the start of the line, which means I can't just move the cursor up and down in the first column to explore traces. But this should ideally be resolved by sending more structured traces to the editor instead of just strings with markup, then I can make the hitbox as large as I want.)

[Leonardo de Moura]

@Gabriel Ebner We want to improve the tracing API. The suggestion above is great. Any other features/improvements?

[Gabriel Ebner]

Great!

• I think it would even make sense to have the expandable behavior available for all nested traces (right now you can only collapse traces created with traceCtx).
• A very boring but helpful improvement would be to add docstrings to the set_option completion.
• API-wise it would be nice to have the trace[...] macro check that the trace class has actually been declared (I believe there are a few trace calls in core that use undeclared classes).
• If you do e.g. set_option trace.Meta.synthInstance true, then this also enables all subclasses. Some of those subclasses have important information, others are just noise. It would be good if we could set a reasonable default here (i.e., that only some subclasses are enabled). (I've run into a similar issue in Lean 3 quite often. set_option trace.simplify true produces an enormous amount of information, and I usually want set_option trace.simplify.failure false as well.)
• (There could also be a toggle in the UI that allows you to enable the extra disabled-by-default subclasses.)
• It is also important to improve the actual traces to make use of the new features. For example about the set_option trace.Meta.synthInstance true: by default I don't want to see the implementation details, I want to see which goals were generated and which instances were applied (and in as few lines as possible, with as few extra words as possible). If an instance failed, I want to see a :cross_mark: right at the first line containing the instance name and not a "failure" message twenty lines below in a collapsed trace.

[Leonardo de Moura]

Thanks for sharing!

[Tomas Skrivan]

I would also be interested for some kind of tracing for debugging simp tactic. I have bunch of theorems for simplification but they are usually conditioned on existence of some typeclass instances. Quite often I'm confused why simp is not simplifying and it would be really helpful to list all the theorems that could simplify but cannot because of the lack of some typeclass instance.

[Leonardo de Moura]

@Tomas Skrivan Any suggestions?
We want to improve the trace messages. Right now, they are a bit messy. Messages for debugging Lean (developer feature) are mixed with messages for diagnosing (tactic) failures (user feature).

[Tomas Skrivan]

@Leonardo de Moura I do not have a suggestion right now. But next time I again debug simp, I will pay closer attention to what went wrong and what information could have been presented to me.

[Tomas Skrivan]

An example of what I'm dealing with:

I have these two theorems how to differentiate a function: chain rule and differential of linear function:

@[simp] def comp.differential_3 (f : Y → Z) (g : X → Y) (x dx : X) [IsDiff f] [IsDiff g] : δ (comp f g) x dx = δ f (g x) (δ g x dx) := sorry
@[simp] def differential_of_linear (f : X → Y) (x dx : X) [IsLin f] : δ f x dx = f dx := sorry

Now when I want to simplify δ (comp f g) x dx there are two paths. Either show that comp f g is linear or that f and g are differentiable.

If g is differentiable but f is not. I would like a report that comp.differential_3 could have been used but failed to find IsDiff f.

When g is linear the situation is a little bit more interesting(because linearity implies differentiability). Most probably, I would like to have two messages:

1. failed to use comp.differential_3 because failed to find IsDiff f
2. failed to use differential_of_linear because failed to find IsLin (comp f g) and that failed because could not find IsLin f (there is also theorem that composition of linear is linear)

So attempting to find some pattern from this, I would say that if there are different paths simp could take prefer to report the path that 'digged the deepest' (what ever that means :D )

[Sebastian Ullrich]

@Tomas Skrivan Have you tried set_option trace.Meta.Tactic.simp.discharge true? Does it show too much, or not enough information?

[Tomas Skrivan]

@Sebastian Ullrich I didn't try that, but I will :)

[Tomas Skrivan]

@Sebastian Ullrich Looks like I'm requesting feature that already exists but I just do not know about :face_palm: Seems to work quite nice, the only issue that for some reason the option trace.Meta.Tactic.simp.discharge does not exists for me and I have to set trace.Meta.Tactic.simp, then I get bunch of unify and rewrite traces as well.

[Sebastian Ullrich]

Thanks for the feedback! I'll fix that one :) .

[Wojciech Nawrocki]

Gabriel Ebner said:

But this should ideally be resolved by sending more structured traces to the editor instead of just strings with markup, then I can make the hitbox as large as I want.

The choice to send already-formatted text directly is a bit strange but has a very good reason behind it. Namely, it is borderline impossible to reproduce the Lean Format layout algorithm with CSS. With the only other option being to port it exactly to JS, I went with formatting on the server.

[Gabriel Ebner]

And I completely agree for expressions (and other syntax-formattable stuff). For traces the situation is a bit less clear (though we might still want to take indentation in account). Even if we require a specific formatting of traces, it is still possible to send the tree structure (so that we can do at least something in the editor: think highlighting subtrees, color-coded vertical lines like in email replies, etc.). I'm thinking of something like this:

interface Trace {
  line: CodeWithInfos;
  nested: LazyTrace | Trace[];
}

[Gabriel Ebner]

borderline impossible to reproduce the Lean Format layout algorithm

It is a bit unfortunate that Lean.Format does not follow the standard Wadler-Leijen API (the group behavior is nonstandard). Otherwise it should be fairly easy to reproduce it on the JS/Lua side (and also future-proof).

[Wojciech Nawrocki]

Gabriel Ebner said:

And I completely agree for expressions (and other syntax-formattable stuff). For traces the situation is a bit less clear (though we might still want to take indentation in account). Even if we require a specific formatting of traces, it is still possible to send the tree structure (so that we can do at least something in the editor: think highlighting subtrees, color-coded vertical lines like in email replies, etc.). I'm thinking of something like this:

interface Trace {
  line: CodeWithInfos;
  nested: LazyTrace | Trace[];
}

Could you please start a discussion on GitHub so we remember to do this at some point?

[Gabriel Ebner]

I've put a comment on the existing discussion at https://github.com/leanprover/lean4/issues/591#issuecomment-945738033