structured tracing

Stream: lean4

[Lukas Stevens]

Where can I find information about the structured tracing that lean4 has? Are there any suggestive examples? I am especially interested in how one could capture the tree-like structure of a simp trace.

[Daniel Selsam]

The TraceState is in CoreM https://github.com/leanprover/lean4/blob/master/src/Lean/CoreM.lean#L31 and consists of the following data: https://github.com/leanprover/lean4/blob/master/src/Lean/Util/Trace.lean#L14-L22

[Mario Carneiro]

where's the tree structure?

[Daniel Selsam]

which tree structure are you referring to?

[Sebastian Ullrich]

https://github.com/leanprover/lean4/blob/master/src/Lean/Util/Trace.lean#L89-L95

[Mario Carneiro]

Perhaps this is a better place to point to then: https://github.com/leanprover/lean4/blob/master/src/Lean/Message.lean#L38-L57

[Mario Carneiro]

that last constructor looks especially tree-like

[Daniel Selsam]

There is also a separate, static, implicit tree structure given by the hierarchical trace names, e.g.

[Meta.Tactic.simp] no lemmas found for post-rewriting x
[Meta.Tactic.simp.rewrite] <unknown>:1000, q x ==> True
[Meta.Tactic.simp] no lemmas found for pre-rewriting True

[Wojciech Nawrocki]

And there is also a tree of elaboration information: link . It is constructed similarly to the trace tree, but serves a somewhat different purpose

[Lukas Stevens]

Thanks a lot! Are there any examples on how to use that datatype?

[Wojciech Nawrocki]

I suppose the main consumer of structured traces is the format function. A MessageData is converted to a Format expressing how it should be displayed as a String at some later point. Note that MessageData has constructors lifted from Format but that it includes semantic information as well.