structure Lean.Language.Snapshot.Diagnostics : Type

MessageLog with interactive diagnostics.

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

• msgLog : Lean.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.

instance Lean.Language.Snapshot.instInhabitedDiagnostics : Inhabited Lean.Language.Snapshot.Diagnostics

Equations

• Lean.Language.Snapshot.instInhabitedDiagnostics = { default := { msgLog := default, interactiveDiagsRef? := default } }

def Lean.Language.Snapshot.Diagnostics.empty : Lean.Language.Snapshot.Diagnostics

The empty set of diagnostics.

Equations

• Lean.Language.Snapshot.Diagnostics.empty = { msgLog := Lean.MessageLog.empty, interactiveDiagsRef? := none }

structure Lean.Language.Snapshot : Type

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 : Lean.Language.Snapshot.Diagnostics

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

• infoTree? : Option Lean.Elab.InfoTree

  General elaboration metadata produced by this step.

• 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.

instance Lean.Language.instInhabitedSnapshot : Inhabited Lean.Language.Snapshot

Equations

• Lean.Language.instInhabitedSnapshot = { default := { desc := default, diagnostics := default, infoTree? := default, isFatal := default } }

structure Lean.Language.SnapshotTask (α : Type) : Type

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

• range? : 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.

• task : Task α

  Underlying task producing the snapshot.

instance Lean.Language.instNonemptySnapshotTask : ∀ {α : Type} [inst : Nonempty α], Nonempty (Lean.Language.SnapshotTask α)

Equations

• ⋯ = ⋯

instance Lean.Language.instInhabitedSnapshotTask : {a : Type} → [inst : Inhabited a] → Inhabited (Lean.Language.SnapshotTask a)

Equations

• Lean.Language.instInhabitedSnapshotTask = { default := { range? := default, task := default } }

def Lean.Language.SnapshotTask.ofIO {α : Type} (range? : Option String.Range) (act : BaseIO α) : BaseIO (Lean.Language.SnapshotTask α)

Creates a snapshot task from a reporting range and a BaseIO action.

Equations

• Lean.Language.SnapshotTask.ofIO range? act = do let __do_lift ← act.asTask pure { range? := range?, task := __do_lift }

def Lean.Language.SnapshotTask.pure {α : Type} (a : α) : Lean.Language.SnapshotTask α

Creates a finished snapshot task.

Equations

• Lean.Language.SnapshotTask.pure a = { range? := none, task := { get := a } }

def Lean.Language.SnapshotTask.cancel {α : Type} (t : Lean.Language.SnapshotTask α) : BaseIO Unit

Explicitly cancels a tasks. Like with basic Taskss, cancellation happens implicitly when the last reference to the task is dropped if it is not an I/O task.

Equations

• t.cancel = IO.cancel t.task

def Lean.Language.SnapshotTask.map {α : Type} {β : Type} (t : Lean.Language.SnapshotTask α) (f : α → β) (range? : optParam (Option String.Range) t.range?) (sync : optParam Bool false) : Lean.Language.SnapshotTask β

Transforms a task's output without changing the reporting range.

Equations

• t.map f range? sync = { range? := range?, task := Task.map f t.task Task.Priority.default sync }

def Lean.Language.SnapshotTask.bind {α : Type} {β : Type} (t : Lean.Language.SnapshotTask α) (act : α → Lean.Language.SnapshotTask β) (range? : optParam (Option String.Range) t.range?) (sync : optParam Bool false) : Lean.Language.SnapshotTask β

Chains two snapshot tasks. The range is taken from the first task if not specified; the range of the second task is discarded.

Equations

• t.bind act range? sync = { range? := range?, task := t.task.bind (fun (x : α) => (act x).task) Task.Priority.default sync }

def Lean.Language.SnapshotTask.bindIO {α : Type} {β : Type} (t : Lean.Language.SnapshotTask α) (act : α → BaseIO (Lean.Language.SnapshotTask β)) (range? : optParam (Option String.Range) t.range?) (sync : optParam Bool false) : BaseIO (Lean.Language.SnapshotTask β)

Chains two snapshot tasks. The range is taken from the first task if not specified; the range of the second task is discarded.

Equations

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

def Lean.Language.SnapshotTask.get {α : Type} (t : Lean.Language.SnapshotTask α) : α

Synchronously waits on the result of the task.

Equations

• t.get = t.task.get

def Lean.Language.SnapshotTask.get? {α : Type} (t : Lean.Language.SnapshotTask α) : BaseIO (Option α)

Returns task result if already finished or else none.

Equations

• t.get? = do let __do_lift ← IO.hasFinished t.task pure (if __do_lift = true then some t.task.get else none)

structure Lean.Language.SyntaxGuarded (α : Type) : Type

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

• stx : Lean.Syntax

  Syntax to be inspected for reuse.

• val : α

  Potentially reusable value.

structure Lean.Language.SnapshotBundle (α : Type) : Type

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.

• old? : Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))

  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.

def Lean.Language.withAlwaysResolvedPromise {m : Type → Type u_1} {α : Type} {β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α] (act : IO.Promise α → m β) : m β

Runs act with a newly created promise and finally resolves it to default if not done by act.

Always resolving promises involved in the snapshot tree is important to avoid deadlocking the language server.

Equations

• Lean.Language.withAlwaysResolvedPromise act = do let p ← liftM IO.Promise.new tryFinally (act p) (liftM (IO.Promise.resolve default p))

def Lean.Language.withAlwaysResolvedPromises {m : Type → Type u_1} {α : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] [Inhabited α] (count : Nat) (act : Array (IO.Promise α) → m Unit) : m Unit

Runs act with count newly created promises and finally resolves them to default if not done by act.

Always resolving promises involved in the snapshot tree is important to avoid deadlocking the language server.

Equations

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

inductive Lean.Language.SnapshotTree : Type

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.

• mk: Lean.Language.Snapshot → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree

  Creates a snapshot tree node.

instance Lean.Language.instInhabitedSnapshotTree : Inhabited Lean.Language.SnapshotTree

Equations

• Lean.Language.instInhabitedSnapshotTree = { default := Lean.Language.SnapshotTree.mk default default }

@[reducible, inline]

abbrev Lean.Language.SnapshotTree.element : Lean.Language.SnapshotTree → Lean.Language.Snapshot

The immediately available element of the snapshot tree node.

Equations

• (Lean.Language.SnapshotTree.mk s children).element = s

@[reducible, inline]

abbrev Lean.Language.SnapshotTree.children : Lean.Language.SnapshotTree → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)

The asynchronously available children of the snapshot tree node.

Equations

• (Lean.Language.SnapshotTree.mk s children).children = children

def Lean.Language.SnapshotTree.trace (s : Lean.Language.SnapshotTree) : Lean.CoreM Unit

Produces trace of given snapshot tree, synchronously waiting on all children.

Equations

• s.trace = Lean.Language.SnapshotTree.trace.go none s

partial def Lean.Language.SnapshotTree.trace.go (range? : Option String.Range) (s : Lean.Language.SnapshotTree) : Lean.CoreM Unit

class Lean.Language.ToSnapshotTree (α : Type) : Type

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

• toSnapshotTree : α → Lean.Language.SnapshotTree

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

instance Lean.Language.instToSnapshotTreeOption {α : Type} [Lean.Language.ToSnapshotTree α] : Lean.Language.ToSnapshotTree (Option α)

Equations

• Lean.Language.instToSnapshotTreeOption = { toSnapshotTree := fun (x : Option α) => match x with | some a => Lean.Language.toSnapshotTree a | none => default }

structure Lean.Language.SnapshotLeafextends Lean.Language.Snapshot : Type

Snapshot type without child nodes.

instance Lean.Language.instNonemptySnapshotLeaf : Nonempty Lean.Language.SnapshotLeaf

Equations

• Lean.Language.instNonemptySnapshotLeaf = ⋯

instance Lean.Language.instTypeNameSnapshotLeaf : TypeName Lean.Language.SnapshotLeaf

Equations

• Lean.Language.instTypeNameSnapshotLeaf = Lean.Language.inst✝

instance Lean.Language.instToSnapshotTreeSnapshotLeaf : Lean.Language.ToSnapshotTree Lean.Language.SnapshotLeaf

Equations

• Lean.Language.instToSnapshotTreeSnapshotLeaf = { toSnapshotTree := fun (s : Lean.Language.SnapshotLeaf) => Lean.Language.SnapshotTree.mk s.toSnapshot #[] }

structure Lean.Language.DynamicSnapshot : Type

Arbitrary snapshot type, used for extensibility.

• val : Dynamic

  Concrete snapshot value as Dynamic.

• tree : Thunk Lean.Language.SnapshotTree

  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.

instance Lean.Language.instToSnapshotTreeDynamicSnapshot : Lean.Language.ToSnapshotTree Lean.Language.DynamicSnapshot

Equations

• Lean.Language.instToSnapshotTreeDynamicSnapshot = { toSnapshotTree := fun (s : Lean.Language.DynamicSnapshot) => s.tree.get }

def Lean.Language.DynamicSnapshot.ofTyped {α : Type} [TypeName α] [Lean.Language.ToSnapshotTree α] (val : α) : Lean.Language.DynamicSnapshot

Creates a DynamicSnapshot from a typed snapshot value.

Equations

• Lean.Language.DynamicSnapshot.ofTyped val = { val := Dynamic.mk val, tree := { fn := fun (x : Unit) => Lean.Language.toSnapshotTree val } }

def Lean.Language.DynamicSnapshot.toTyped? (α : Type) [TypeName α] (snap : Lean.Language.DynamicSnapshot) : Option α

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

Equations

• Lean.Language.DynamicSnapshot.toTyped? α snap = Dynamic.get? α snap.val

instance Lean.Language.instInhabitedDynamicSnapshot : Inhabited Lean.Language.DynamicSnapshot

Equations

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

@[specialize #[]]

partial def Lean.Language.SnapshotTree.forM {m : Type u_1 → Type u_2} [Monad m] (s : Lean.Language.SnapshotTree) (f : Lean.Language.Snapshot → m PUnit) : m PUnit

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

opaque Lean.Language.printMessageEndPos : Lean.Option Bool

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 : Lean.MessageLog) (opts : Lean.Options) (json : optParam Bool false) : IO Unit

Reports messages on stdout. If json is true, prints messages as JSON (one per line).

Equations

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

def Lean.Language.SnapshotTree.runAndReport (s : Lean.Language.SnapshotTree) (opts : Lean.Options) (json : optParam Bool false) : IO Unit

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

Equations

• s.runAndReport opts json = s.forM fun (x : Lean.Language.Snapshot) => Lean.Language.reportMessages x.diagnostics.msgLog opts json

def Lean.Language.SnapshotTree.getAll (s : Lean.Language.SnapshotTree) : Array Lean.Language.Snapshot

Waits on and returns all snapshots in the tree.

Equations

• s.getAll = (StateT.run (s.forM fun (s : Lean.Language.Snapshot) => modify fun (x : Array Lean.Language.Snapshot) => x.push s) #[]).snd

structure Lean.Language.ProcessingContextextends Lean.Parser.InputContext : Type

Context of an input processing invocation.

@[reducible, inline]

abbrev Lean.Language.ProcessingT (m : Type → Type u_1) (α : Type) : Type u_1

Monad transformer holding all relevant data for processing.

Equations

• Lean.Language.ProcessingT m = ReaderT Lean.Language.ProcessingContext m

@[reducible, inline]

abbrev Lean.Language.ProcessingM (α : Type) : Type

Monad holding all relevant data for processing.

Equations

• Lean.Language.ProcessingM = Lean.Language.ProcessingT BaseIO

instance Lean.Language.instMonadLiftProcessingMProcessingTIO : MonadLift Lean.Language.ProcessingM (Lean.Language.ProcessingT IO)

Equations

• Lean.Language.instMonadLiftProcessingMProcessingTIO = { monadLift := fun {α : Type} (act : Lean.Language.ProcessingM α) (ctx : Lean.Language.ProcessingContext) => liftM (act ctx) }

def Lean.Language.Snapshot.Diagnostics.ofMessageLog (msgLog : Lean.MessageLog) : BaseIO Lean.Language.Snapshot.Diagnostics

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

• Lean.Language.Snapshot.Diagnostics.ofMessageLog msgLog = do let __do_lift ← IO.mkRef none pure { msgLog := msgLog, interactiveDiagsRef? := some __do_lift }

def Lean.Language.diagnosticsOfHeaderError (msg : String) : Lean.Language.ProcessingM Lean.Language.Snapshot.Diagnostics

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

Equations

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

def Lean.Language.withHeaderExceptions {α : Type} (ex : Lean.Language.Snapshot → α) (act : Lean.Language.ProcessingT IO α) : Lean.Language.ProcessingM α

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

Equations

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

def Lean.Language.mkIncrementalProcessor {InitSnap : Type} (process : Option InitSnap → Lean.Language.ProcessingM InitSnap) : BaseIO (Lean.Parser.InputContext → BaseIO InitSnap)

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

Equations

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