Zulip Chat Archive

Stream: lean4

Topic: structured tracing


view this post on Zulip Lukas Stevens (Feb 03 2021 at 20:39):

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.

view this post on Zulip Daniel Selsam (Feb 03 2021 at 20:49):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 20:50):

where's the tree structure?

view this post on Zulip Daniel Selsam (Feb 03 2021 at 20:50):

which tree structure are you referring to?

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 20:52):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 20:54):

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

view this post on Zulip Mario Carneiro (Feb 03 2021 at 20:54):

that last constructor looks especially tree-like

view this post on Zulip Daniel Selsam (Feb 03 2021 at 21:00):

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

view this post on Zulip Wojciech Nawrocki (Feb 03 2021 at 23:31):

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

view this post on Zulip Lukas Stevens (Feb 04 2021 at 10:39):

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

view this post on Zulip Wojciech Nawrocki (Feb 04 2021 at 20:07):

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.


Last updated: May 18 2021 at 23:14 UTC