source
structure Lean.Language.Snapshot.Diagnostics :
Type

`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

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

- Lean.Language.Snapshot.instInhabitedDiagnostics = { default := Lean.Language.Snapshot.instInhabitedDiagnostics.default }

source
def Lean.Language.Snapshot.instInhabitedDiagnostics.default :
Diagnostics
Equations

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

Instances For

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

The empty set of diagnostics.

Equations

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

Instances For

source
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 : 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

source
instance Lean.Language.instInhabitedSnapshot :
Inhabited Snapshot
Equations

- Lean.Language.instInhabitedSnapshot = { default := Lean.Language.instInhabitedSnapshot.default }

source
def Lean.Language.instInhabitedSnapshot.default :
Snapshot
Equations

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

Instances For

source
inductive Lean.Language.SnapshotTask.ReportingRange :
Type

Range that is marked as being processed by the server while a task is running.

- inherit : ReportingRange

  Inherit range from outer task if any, or else the entire file.

- some (range : String.Range) : ReportingRange

  Use given range.

- skip : ReportingRange

  Do not mark as being processed. Child nodes are still visited.

Instances For

source
def Lean.Language.SnapshotTask.instInhabitedReportingRange.default :
ReportingRange
Equations

- Lean.Language.SnapshotTask.instInhabitedReportingRange.default = Lean.Language.SnapshotTask.ReportingRange.inherit

Instances For

source
instance Lean.Language.SnapshotTask.instInhabitedReportingRange :
Inhabited ReportingRange
Equations

- Lean.Language.SnapshotTask.instInhabitedReportingRange = { default := Lean.Language.SnapshotTask.instInhabitedReportingRange.default }

source
def Lean.Language.SnapshotTask.ReportingRange.ofOptionInheriting :
Option String.Range → ReportingRange

Constructs a reporting range by replacing a missing range with `inherit`, which is a reasonable default to ensure that a range is shown in all cases.

Equations

- Lean.Language.SnapshotTask.ReportingRange.ofOptionInheriting (some range) = Lean.Language.SnapshotTask.ReportingRange.some range
- Lean.Language.SnapshotTask.ReportingRange.ofOptionInheriting none = Lean.Language.SnapshotTask.ReportingRange.inherit

Instances For

source
def Lean.Language.SnapshotTask.defaultReportingRange (stx? : Option Syntax) :
ReportingRange

Yields the default reporting range of a `Syntax`, which is just the `canonicalOnly` range of the syntax if any, or `inherit` otherwise.

Equations

- Lean.Language.SnapshotTask.defaultReportingRange stx? = Lean.Language.SnapshotTask.ReportingRange.ofOptionInheriting (stx?.bind fun (x : Lean.Syntax) => x.getRange? true)

Instances For

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

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 : ReportingRange

  Range that is marked as being processed by the server while the task is running.

- cancelTk? : Option IO.CancelToken

  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

source
instance Lean.Language.instNonemptySnapshotTask {α✝ : Type} [Nonempty α✝] :
Nonempty (SnapshotTask α✝)
source
def Lean.Language.instInhabitedSnapshotTask.default {a✝ : Type} [Inhabited a✝] :
SnapshotTask a✝
Equations

- Lean.Language.instInhabitedSnapshotTask.default = { stx? := default, reportingRange := default, cancelTk? := default, task := default }

Instances For

source
instance Lean.Language.instInhabitedSnapshotTask {a✝ : Type} [Inhabited a✝] :
Inhabited (SnapshotTask a✝)
Equations

- Lean.Language.instInhabitedSnapshotTask = { default := Lean.Language.instInhabitedSnapshotTask.default }

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

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

Equations

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

Instances For

source
def Lean.Language.SnapshotTask.finished {α : Type} (stx? : Option Syntax) (a : α) :
SnapshotTask α

Creates a finished snapshot task.

Equations

- Lean.Language.SnapshotTask.finished stx? a = { stx? := stx?, reportingRange := Lean.Language.SnapshotTask.ReportingRange.skip, cancelTk? := none, task := { get := a } }

Instances For

source
def Lean.Language.SnapshotTask.map {α β : Type} (t : SnapshotTask α) (f : α → β) (stx? : Option Syntax := t.stx?) (reportingRange : ReportingRange := t.reportingRange) (sync : Bool := false) :
SnapshotTask β

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

Equations

- t.map f stx? reportingRange sync = { stx? := stx?, reportingRange := reportingRange, cancelTk? := t.cancelTk?, task := Task.map f t.task Task.Priority.default sync }

Instances For

source
def Lean.Language.SnapshotTask.bindIO {α β : Type} (t : SnapshotTask α) (act : α → BaseIO (SnapshotTask β)) (stx? : Option Syntax := t.stx?) (reportingRange : ReportingRange := t.reportingRange) (cancelTk? : Option IO.CancelToken) (sync : Bool := false) :
BaseIO (SnapshotTask β)

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

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

Instances For

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

Synchronously waits on the result of the task.

Equations

- t.get = t.task.get

Instances For

source
def Lean.Language.SnapshotTask.get? {α : Type} (t : 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)

Instances For

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

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

source
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 (SyntaxGuarded (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.

Instances For

source
structure 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.

- element : Snapshot

  The immediately available element of the snapshot tree node.

- children : Array (SnapshotTask SnapshotTree)

  The asynchronously available children of the snapshot tree node.

Instances For

source
def Lean.Language.instInhabitedSnapshotTree.default :
SnapshotTree
Equations

- Lean.Language.instInhabitedSnapshotTree.default = { element := default, children := default }

Instances For

source
instance Lean.Language.instInhabitedSnapshotTree :
Inhabited SnapshotTree
Equations

- Lean.Language.instInhabitedSnapshotTree = { default := Lean.Language.instInhabitedSnapshotTree.default }

source
instance Lean.Language.instTypeNameSnapshotTree :
TypeName SnapshotTree
Equations

- Lean.Language.instTypeNameSnapshotTree = Lean.Language.inst✝

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

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

source
instance Lean.Language.instToSnapshotTreeSnapshotTree :
ToSnapshotTree SnapshotTree
Equations

- Lean.Language.instToSnapshotTreeSnapshotTree = { toSnapshotTree := fun (s : Lean.Language.SnapshotTree) => s }

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

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

source
partial def Lean.Language.SnapshotTask.cancelRec {α : Type} [ToSnapshotTree α] (t : SnapshotTask α) :
BaseIO Unit

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

source
structure Lean.Language.SnapshotLeaf extends Lean.Language.Snapshot :
Type

Snapshot type without child nodes.

- desc : String
- diagnostics : Diagnostics
- infoTree? : Option Elab.InfoTree
- traces : TraceState
- isFatal : Bool

Instances For

source
instance Lean.Language.instInhabitedSnapshotLeaf :
Inhabited SnapshotLeaf
Equations

- Lean.Language.instInhabitedSnapshotLeaf = { default := Lean.Language.instInhabitedSnapshotLeaf.default }

source
def Lean.Language.instInhabitedSnapshotLeaf.default :
SnapshotLeaf
Equations

- Lean.Language.instInhabitedSnapshotLeaf.default = { toSnapshot := default }

Instances For

source
instance Lean.Language.instTypeNameSnapshotLeaf :
TypeName SnapshotLeaf
Equations

- Lean.Language.instTypeNameSnapshotLeaf = Lean.Language.inst✝

source
instance Lean.Language.instToSnapshotTreeSnapshotLeaf :
ToSnapshotTree SnapshotLeaf
Equations

- Lean.Language.instToSnapshotTreeSnapshotLeaf = { toSnapshotTree := fun (s : Lean.Language.SnapshotLeaf) => { element := s.toSnapshot, children := #[] } }

source
structure Lean.Language.DynamicSnapshot :
Type

Arbitrary snapshot type, used for extensibility.

- val : Dynamic

  Concrete snapshot value as `Dynamic`.

- tree : Thunk 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.

Instances For

source
instance Lean.Language.instToSnapshotTreeDynamicSnapshot :
ToSnapshotTree DynamicSnapshot
Equations

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

source
def Lean.Language.DynamicSnapshot.ofTyped {α : Type} [TypeName α] [ToSnapshotTree α] (val : α) :
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 } }

Instances For

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

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

Equations

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

Instances For

source
instance Lean.Language.instInhabitedDynamicSnapshot :
Inhabited DynamicSnapshot
Equations

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

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

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

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

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

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

source
opaque Lean.Language.maxErrors :
Lean.Option Nat

Maximum number of errors to report.

source
def Lean.Language.SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json : Bool := false) (severityOverrides : NameMap MessageSeverity := ∅) :
IO Bool

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

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

Instances For

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

Waits on and returns all snapshots in the tree.

Equations

- s.getAll = (s.foldM (fun (x1 : Array Lean.Language.Snapshot) (x2 : Lean.Language.Snapshot) => pure (x1.push x2)) #[]).run

Instances For

source
def Lean.Language.SnapshotTree.waitAll :
SnapshotTree → BaseIO (Task Unit)

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

Equations

- { element := element, children := children }.waitAll = Lean.Language.SnapshotTree.waitAll.go✝ children.toList

Instances For

source
structure Lean.Language.ProcessingContext extends Lean.Parser.InputContext :
Type

Context of an input processing invocation.

- inputString : String
- fileName : String
- fileMap : FileMap
- endPos : String.Pos.Raw
- endPos_valid : self.endPos ≤ self.inputString.endPos

Instances For

source
@[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

Instances For

source
@[reducible, inline]
abbrev Lean.Language.ProcessingM (α : Type) :
Type

Monad holding all relevant data for processing.

Equations

- Lean.Language.ProcessingM = Lean.Language.ProcessingT BaseIO

Instances For

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

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

source
def Lean.Language.Snapshot.Diagnostics.ofMessageLog (msgLog : MessageLog) :
BaseIO 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 }

Instances For

source
def Lean.Language.diagnosticsOfHeaderError (msg : String) :
ProcessingM 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.

Instances For

source
def Lean.Language.withHeaderExceptions {α : Type} (ex : Snapshot → α) (act : ProcessingT IO α) :
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.

Instances For

source
def Lean.Language.mkIncrementalProcessor {InitSnap : Type} (process : Option InitSnap → ProcessingM InitSnap) :
BaseIO (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.

Instances For