Documentation

Lean.Language.Basic

MessageLog with interactive diagnostics.

Can be created using Diagnostics.empty or Diagnostics.ofMessageLog.

  • msgLog : MessageLog

    Non-interactive message log.

  • interactiveDiagsRef? : Option (IO.Ref (Option Dynamic))

    Dynamic mutable slot usable by the language server for memorizing interactive diagnostics. If none, interactive diagnostics are not remembered, which should only be used for messages not containing any interactive elements as client-side state will be lost on recreating a diagnostic.

    See also section "Communication" in Lean/Server/README.md.

Instances For

    The empty set of diagnostics.

    Equations
      Instances For

        The base class of all snapshots: all the generic information the language server needs about a snapshot.

        • desc : String

          Debug description shown by trace.Elab.snapshotTree, defaults to the caller's decl name.

        • diagnostics : Diagnostics

          The messages produced by this step. The union of message logs of all finished snapshots is reported to the user.

        • infoTree? : Option Elab.InfoTree

          General elaboration metadata produced by this step.

        • traces : TraceState

          Trace data produced by this step. Currently used only by trace.profiler.output, otherwise we depend on the elaborator adding traces to diagnostics eventually.

        • isFatal : Bool

          Whether it should be indicated to the user that a fatal error (which should be part of diagnostics) occurred that prevents processing of the remainder of the file.

        Instances For

          Yields the default reporting range of a Syntax, which is just the canonicalOnly range of the syntax.

          Equations
            Instances For

              A task producing some snapshot type (usually a subclass of Snapshot).

              • stx? : Option Syntax

                Syntax processed by this SnapshotTask. The Syntax is used by the language server to determine whether to force this SnapshotTask when a request is made. In general, the elaborator retains the following invariant: If stx? is none, then this snapshot task (and all of its children) do not contain InfoTree information that can be used in the language server, and so the language server will ignore it when it is looking for an InfoTree. Nonetheless, if stx? is none, then this snapshot task (and any of its children) may still contain message log information.

              • reportingRange? : Option String.Range

                Range that is marked as being processed by the server while the task is running. If none, the range of the outer task if some or else the entire file is reported.

              • Cancellation token that can be set by the server to cancel the task when it detects the results are not needed anymore.

              • task : Task α

                Underlying task producing the snapshot.

              Instances For
                def Lean.Language.SnapshotTask.ofIO {α : Type} (stx? : Option Syntax) (cancelTk? : Option IO.CancelToken) (reportingRange? : Option String.Range := defaultReportingRange? stx?) (act : BaseIO α) :

                Creates a snapshot task from the syntax processed by the task and a BaseIO action.

                Equations
                  Instances For

                    Creates a finished snapshot task.

                    Equations
                      Instances For
                        def Lean.Language.SnapshotTask.map {α β : Type} (t : SnapshotTask α) (f : αβ) (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?) (sync : Bool := false) :

                        Transforms a task's output without changing the processed syntax.

                        Equations
                          Instances For
                            def Lean.Language.SnapshotTask.bindIO {α β : Type} (t : SnapshotTask α) (act : αBaseIO (SnapshotTask β)) (stx? : Option Syntax := t.stx?) (reportingRange? : Option String.Range := t.reportingRange?) (cancelTk? : Option IO.CancelToken) (sync : Bool := false) :

                            Chains two snapshot tasks. The processed syntax and the reporting range are taken from the first task if not specified; the processed syntax and the reporting range of the second task are discarded. The cancellation tokens of both tasks are discarded. They are replaced with the given token if any.

                            Equations
                              Instances For

                                Synchronously waits on the result of the task.

                                Equations
                                  Instances For

                                    Returns task result if already finished or else none.

                                    Equations
                                      Instances For

                                        Arbitrary value paired with a syntax that should be inspected when considering the value for reuse.

                                        • stx : Syntax

                                          Syntax to be inspected for reuse.

                                        • val : α

                                          Potentially reusable value.

                                        Instances For

                                          Pair of (optional) old snapshot task usable for incremental reuse and new snapshot promise for incremental reporting. Inside the elaborator, we build snapshots by carrying such bundles and then checking if we can reuse old? if set or else redoing the corresponding elaboration step. In either case, we derive new bundles for nested snapshots, if any, and finally resolve new to the result.

                                          Note that failing to resolve a created promise will block the language server indefinitely! We use withAlwaysResolvedPromise/withAlwaysResolvedPromises to ensure this doesn't happen.

                                          In the future, the 1-element history old? may be replaced with a global cache indexed by strong hashes but the promise will still need to be passed through the elaborator.

                                          • Snapshot task of corresponding elaboration in previous document version if any, paired with its old syntax to be considered for reuse. Should be set to none as soon as reuse can be ruled out.

                                          • new : IO.Promise α

                                            Promise of snapshot value for the current document. When resolved, the language server will report its result even before the current elaborator invocation has finished.

                                          Instances For

                                            Tree of snapshots where each snapshot comes with an array of asynchronous further subtrees. Used for asynchronously collecting information about the entirety of snapshots in the language server. The involved tasks may form a DAG on the Task dependency level but this is not captured by this data structure.

                                            • element : Snapshot

                                              The immediately available element of the snapshot tree node.

                                            • The asynchronously available children of the snapshot tree node.

                                            Instances For

                                              Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous representation.

                                              • toSnapshotTree : αSnapshotTree

                                                Transforms a language-specific snapshot to a homogeneous snapshot tree.

                                              Instances

                                                Recursively triggers all SnapshotTask.cancelTk? in the reachable tree, asynchronously.

                                                Arbitrary snapshot type, used for extensibility.

                                                • val : Dynamic

                                                  Concrete snapshot value as Dynamic.

                                                • Snapshot tree retrieved from val before erasure. We do thunk even the first level as accessing it too early can create some unnecessary tasks from toSnapshotTree that are otherwise avoided by (sync := true) when accessing only after elaboration has finished. Early access can even lead to deadlocks when later forcing these unnecessary tasks on a starved thread pool.

                                                Instances For

                                                  Creates a DynamicSnapshot from a typed snapshot value.

                                                  Equations
                                                    Instances For

                                                      Returns the original snapshot value if it is of the given type.

                                                      Equations
                                                        Instances For
                                                          @[specialize #[]]
                                                          partial def Lean.Language.SnapshotTree.forM {m : Type u_1 → Type u_2} [Monad m] (s : SnapshotTree) (f : Snapshotm PUnit) :

                                                          Runs a tree of snapshots to conclusion, incrementally performing f on each snapshot in tree preorder.

                                                          @[specialize #[]]
                                                          partial def Lean.Language.SnapshotTree.foldM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (s : SnapshotTree) (f : αSnapshotm α) (init : α) :
                                                          m α

                                                          Runs a tree of snapshots to conclusion, folding the function f over each snapshot in tree preorder.

                                                          Option for printing end position of each message in addition to start position. Used for testing message ranges in the test suite.

                                                          def Lean.Language.reportMessages (msgLog : MessageLog) (opts : Options) (json : Bool := false) (severityOverrides : NameMap MessageSeverity := ) :

                                                          Reports messages on stdout and returns whether an error was reported. If json is true, prints messages as JSON (one per line). If a message's kind is in severityOverrides, it will be reported with the specified severity.

                                                          Equations
                                                            Instances For
                                                              def Lean.Language.SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json : Bool := false) (severityOverrides : NameMap MessageSeverity := ) :

                                                              Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are reported in tree preorder. Returns whether any errors were reported. This function is used by the cmdline driver; see Lean.Server.FileWorker.reportSnapshots for how the language server reports snapshots asynchronously.

                                                              Equations
                                                                Instances For

                                                                  Waits on and returns all snapshots in the tree.

                                                                  Equations
                                                                    Instances For

                                                                      Returns a task that waits on all snapshots in the tree.

                                                                      Equations
                                                                        Instances For

                                                                          Context of an input processing invocation.

                                                                          Instances For
                                                                            @[reducible, inline]
                                                                            abbrev Lean.Language.ProcessingT (m : TypeType u_1) (α : Type) :
                                                                            Type u_1

                                                                            Monad transformer holding all relevant data for processing.

                                                                            Equations
                                                                              Instances For
                                                                                @[reducible, inline]

                                                                                Monad holding all relevant data for processing.

                                                                                Equations
                                                                                  Instances For

                                                                                    Creates snapshot message log from non-interactive message log, also allocating a mutable cell that can be used by the server to memorize interactive diagnostics derived from the log.

                                                                                    Equations
                                                                                      Instances For

                                                                                        Creates diagnostics from a single error message that should span the whole file.

                                                                                        Equations
                                                                                          Instances For

                                                                                            Adds unexpected exceptions from header processing to the message log as a last resort; standard errors should already have been caught earlier.

                                                                                            Equations
                                                                                              Instances For
                                                                                                def Lean.Language.mkIncrementalProcessor {InitSnap : Type} (process : Option InitSnapProcessingM InitSnap) :

                                                                                                Builds a function for processing a language using incremental snapshots by passing the previous snapshot to Language.process on subsequent invocations.

                                                                                                Equations
                                                                                                  Instances For