Documentation

Lean.Util.Trace

Trace messages #

Trace messages explain to the user what problem Lean solved and what steps it took. Think of trace messages like a figure in a paper.

They are shown in the editor as a collapsible tree, usually as [class.name] message ▸. Every trace node has a class name, a message, and an array of children. This module provides the API to produce trace messages, the key entry points are:

Users can enable trace options for a class using set_option trace.class.name true. This only enables trace messages for the class.name trace class as well as child classes that are explicitly marked as inherited (see registerTraceClass).

Internally, trace messages are stored as MessageData: .trace cls msg #[.trace .., .trace ..]

When writing trace messages, try to follow these guidelines:

  1. Expansion progressively increases detail. Each level of expansion (of the trace node in the editor) should reveal more details. For example, the unexpanded node should show the top-level goal. Expanding it should show a list of steps. Expanding one of the steps then shows what happens during that step.
  2. One trace message per step. The [trace.class] marker functions as a visual bullet point, making it easy to identify the different steps at a glance.
  3. Outcome first. The top-level trace message should already show whether the action failed or succeeded, as opposed to a "success" trace message that comes pages later.
  4. Be concise. Keep messages short. Avoid repetitive text. (This is also why the editor plugins abbreviate the common prefixes.)
  5. Emoji are concisest. Several helper functions in this module help with a consistent emoji language.
  6. Good defaults. Setting set_option trace.Meta.synthInstance true (etc.) should produce great trace messages out-of-the-box, without needing extra options to tweak it.
structure Lean.TraceElem :
Instances For
    Equations
    Equations
    class Lean.MonadTrace (m : TypeType) :
    Instances
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Instances For
            @[inline]
            Equations
            • Lean.getTraces = do let s ← Lean.getTraceState pure s.traces
            Instances For
              @[inline]
              Equations
              Instances For
                @[inline]
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline]
                      Equations
                      Instances For
                        @[inline]
                        Equations
                        Instances For
                          def Lean.withSeconds {α : Type} {m : TypeType} [Monad m] [MonadLiftT BaseIO m] (act : m α) :
                          m (α × Float)
                          Equations
                          Instances For
                            @[inline]
                            Equations
                            Instances For
                              @[inline]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Lean.withTraceNode {α : Type} {m : TypeType} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] {ε : Type} [MonadExcept ε m] [MonadLiftT BaseIO m] (cls : Lake.Name) (msg : Except ε αm Lean.MessageData) (k : m α) (collapsed : optParam Bool true) :
                                m α
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.registerTraceClass (traceClassName : Lake.Name) (inherited : optParam Bool false) (ref : autoParam Lake.Name _auto✝) :

                                    Registers a trace class.

                                    By default, trace classes are not inherited; that is, set_option trace.foo true does not imply set_option trace.foo.bar true. Calling registerTraceClass `foo.bar (inherited := true) enables this inheritance on an opt-in basis.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For
                                              def Lean.exceptBoolEmoji {ε : Type u_1} :
                                              Equations
                                              Instances For
                                                def Lean.exceptOptionEmoji {α : Type} {ε : Type u_1} :
                                                Except ε (Option α)String
                                                Equations
                                                Instances For
                                                  class Lean.ExceptToEmoji (ε : Type) (α : Type) :
                                                  Instances
                                                    Equations
                                                    • Lean.instExceptToEmojiBool = { toEmoji := Lean.exceptBoolEmoji }
                                                    Equations
                                                    • Lean.instExceptToEmojiOption = { toEmoji := Lean.exceptOptionEmoji }
                                                    def Lean.withTraceNodeBefore {α : Type} {m : TypeType} [Monad m] [Lean.MonadTrace m] [MonadLiftT IO m] {ε : Type} [Lean.MonadRef m] [Lean.AddMessageContext m] [Lean.MonadOptions m] [MonadExcept ε m] [MonadLiftT BaseIO m] [Lean.ExceptToEmoji ε α] (cls : Lake.Name) (msg : m Lean.MessageData) (k : m α) (collapsed : optParam Bool true) :
                                                    m α

                                                    Similar to withTraceNode, but msg is constructed before executing k. This is important when debugging methods such as isDefEq, and we want to generate the message before k updates the metavariable assignment. The class ExceptToEmoji is used to convert the result produced by k into an emoji (e.g., 💥, , ).

                                                    TODO: find better name for this function.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For