Documentation

Lean.Message

def Lean.mkErrorStringWithPos (fileName : String) (pos : Lean.Position) (msg : String) (endPos : optParam (Option Lean.Position) none) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A naming context is the information needed to shorten names in pretty printing.

    It gives the current namespace and the list of open declarations.

    Instances For
      structure Lean.TraceData :
      • cls : Lake.Name

        Trace class, e.g. Elab.step.

      • startTime : Float

        Start time in seconds; 0 if unknown to avoid Option allocation.

      • stopTime : Float

        Stop time in seconds; 0 if unknown to avoid Option allocation.

      • collapsed : Bool

        Whether trace node defaults to collapsed in the infoview.

      • tag : String

        Optional tag shown in trace.profiler.output output after the trace class name.

      Instances For

        Structured message data. We use it for reporting errors, trace messages, etc.

        Instances For

          Eagerly formatted text.

          Equations
          Instances For

            Lazy message data production, with access to the context as given by a surrounding MessageData.withContext (which is expected to exist).

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

              Returns true when the message contains a MessageData.tagged tag .. constructor where p tag is true.

              This does not descend into lazily generated subtress (.ofLazy); message tags of interest (like those added by logLinter) are expected to be near the root of the MessageData, and not hidden inside .ofLazy.

              Equations
              • Lean.MessageData.mkPPContext nCtx ctx = { env := ctx.env, mctx := ctx.mctx, lctx := ctx.lctx, opts := ctx.opts, currNamespace := nCtx.currNamespace, openDecls := nCtx.openDecls }
              Instances For
                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
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          • msgData.toString = do let __do_liftmsgData.format pure (toString __do_lift)
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.

                            Wrap the given message in l and r. See also Format.bracket.

                            Equations
                            Instances For

                              Wrap the given message in parentheses ().

                              Equations
                              Instances For

                                Wrap the given message in square brackets [].

                                Equations
                                Instances For

                                  Write the given list of messages as a list, separating each item with ,\n and surrounding with square brackets.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    structure Lean.BaseMessage (α : Type u) :

                                    A BaseMessage is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows. There are two varieties in the Lean core:

                                    Instances For
                                      instance Lean.instInhabitedBaseMessage :
                                      {a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.BaseMessage a)
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      instance Lean.instToJsonBaseMessage :
                                      {α : Type u_1} → [inst : Lean.ToJson α] → Lean.ToJson (Lean.BaseMessage α)
                                      Equations
                                      • Lean.instToJsonBaseMessage = { toJson := Lean.toJsonBaseMessage✝ }
                                      Equations
                                      • Lean.instFromJsonBaseMessage = { fromJson? := Lean.fromJsonBaseMessage✝ }
                                      @[reducible, inline]

                                      A Message is a richly formatted piece of information emitted by Lean. They are rendered by client editors in the infoview and in diagnostic windows.

                                      Equations
                                      Instances For
                                        @[reducible, inline]

                                        A SerialMessage is a Message whose MessageData has been eagerly serialized and is thus appropriate for use in pure contexts where the effectful MessageData.toString cannot be used.

                                        Equations
                                        Instances For
                                          @[inline]
                                          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
                                              @[inline]
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • msg.toString includeEndPos = do let __do_liftmsg.serialize pure (inline (__do_lift.toString includeEndPos))
                                                Instances For
                                                  Equations
                                                  Instances For

                                                    A persistent array of messages.

                                                    In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at various points inside a command, which will empty unreported and updated hadErrors accordingly (see CoreM.getAndEmptyMessageLog).

                                                    • hadErrors : Bool

                                                      If true, there was an error in the log previously that has already been reported to the user and removed from the log. Thus we say that in the current context (usually the current command), we "have errors" if either this flag is set or there is an error in msgs; see MessageLog.hasErrors. If we have errors, we suppress some error messages that are often the result of a previous error.

                                                    • The list of messages not already reported, in insertion order.

                                                    Instances For
                                                      Equations
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        • log.hasUnreported = !log.unreported.isEmpty
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • l₁.append l₂ = { hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported }
                                                            Instances For
                                                              Equations
                                                              Instances For
                                                                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.MessageLog.forM {m : TypeType} [Monad m] (log : Lean.MessageLog) (f : Lean.Messagem Unit) :
                                                                    Equations
                                                                    • log.forM f = log.unreported.forM f
                                                                    Instances For

                                                                      Converts the unreported messages to a list, oldest message first.

                                                                      Equations
                                                                      • log.toList = log.unreported.toList
                                                                      Instances For

                                                                        Converts the unreported messages to an array, oldest message first.

                                                                        Equations
                                                                        • log.toArray = log.unreported.toArray
                                                                        Instances For
                                                                          Instances
                                                                            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
                                                                                Instances
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    Equations
                                                                                    Equations
                                                                                    Equations
                                                                                    Equations
                                                                                    Equations
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    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