Lean.Server.Snapshots

One can think of this module as being a partial reimplementation of Lean.Elab.Frontend which also stores a snapshot of the world after each command. Importantly, we allow (re)starting compilation from any snapshot/position in the file for interactive editing purposes.

Where the command which produced this snapshot begins. Note that neighbouring snapshots are not necessarily attached beginning-to-end, since inputs outside the grammar advance the parser but do not produce snapshots.
beginPos : String.Pos
stx : Lean.Syntax
mpState : Lean.Parser.ModuleParserState
cmdState : Lean.Elab.Command.State
We cache interactive diagnostics in order not to invoke the pretty-printer again on messages from previous snapshots when publishing diagnostics for every new snapshot (this is quadratic), as well as not to invoke it once again when handling $/lean/interactiveDiagnostics.
interactiveDiags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic
tacticCache : IO.Ref Lean.Elab.Tactic.Cache

What Lean knows about the world after the header and each command.

Instances For

source

def Lean.Server.Snapshots.Snapshot.endPos (s : Lean.Server.Snapshots.Snapshot) :

String.Pos

Equations

Lean.Server.Snapshots.Snapshot.endPos s = s.mpState.pos

source

def Lean.Server.Snapshots.Snapshot.env (s : Lean.Server.Snapshots.Snapshot) :

Lean.Environment

Equations

Lean.Server.Snapshots.Snapshot.env s = s.cmdState.env

source

def Lean.Server.Snapshots.Snapshot.msgLog (s : Lean.Server.Snapshots.Snapshot) :

Lean.MessageLog

Equations

Lean.Server.Snapshots.Snapshot.msgLog s = s.cmdState.messages

source

def Lean.Server.Snapshots.Snapshot.diagnostics (s : Lean.Server.Snapshots.Snapshot) :

Lean.PersistentArray Lean.Lsp.Diagnostic

Equations

Lean.Server.Snapshots.Snapshot.diagnostics s = Lean.PersistentArray.map (fun d => Lean.Widget.InteractiveDiagnostic.toDiagnostic d) s.interactiveDiags

source

def Lean.Server.Snapshots.Snapshot.infoTree (s : Lean.Server.Snapshots.Snapshot) :

Lean.Elab.InfoTree

Equations

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

source

def Lean.Server.Snapshots.Snapshot.isAtEnd (s : Lean.Server.Snapshots.Snapshot) :

Bool

Equations

Lean.Server.Snapshots.Snapshot.isAtEnd s = (Lean.Parser.isEOI s.stx || Lean.Parser.isTerminalCommand s.stx)

source

def Lean.Server.Snapshots.Snapshot.runCommandElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.Elab.Command.CommandElabM α) :

EIO Lean.Exception α

Use the command state in the given snapshot to run a CommandElabM.

Equations

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

source

def Lean.Server.Snapshots.Snapshot.runCoreM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.CoreM α) :

EIO Lean.Exception α

Run a CoreM computation using the data in the given snapshot.

Equations

Lean.Server.Snapshots.Snapshot.runCoreM snap meta c = Lean.Server.Snapshots.Snapshot.runCommandElabM snap meta (Lean.Elab.Command.liftCoreM c)

source

def Lean.Server.Snapshots.Snapshot.runTermElabM {α : Type} (snap : Lean.Server.Snapshots.Snapshot) (meta : Lean.Server.DocumentMeta) (c : Lean.Elab.TermElabM α) :

EIO Lean.Exception α

Run a TermElabM computation using the data in the given snapshot.

Equations

Lean.Server.Snapshots.Snapshot.runTermElabM snap meta c = Lean.Server.Snapshots.Snapshot.runCommandElabM snap meta (Lean.Elab.Command.liftTermElabM c)

source

def Lean.Server.Snapshots.parseNextCmd (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) :

IO Lean.Syntax

Parses the next command occurring after the given snapshot without elaborating it.

Equations

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

source

opaque Lean.Server.Snapshots.server.stderrAsMessages :

Lean.Option Bool

source

def Lean.Server.Snapshots.compileNextCmd (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) :

IO Lean.Server.Snapshots.Snapshot

Compiles the next command occurring after the given snapshot. If there is no next command (file ended), Snapshot.isAtEnd will hold of the return value.

Equations

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

source

def Lean.Server.Snapshots.compileNextCmd.withNewInteractiveDiags (inputCtx : Lean.Parser.InputContext) (snap : Lean.Server.Snapshots.Snapshot) (hasWidgets : Bool) (msgLog : Lean.MessageLog) :

IO (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)

Compute the current interactive diagnostics log by finding a "diff" relative to the parent snapshot. We need to do this because unlike the MessageLog itself, interactive diags are not part of the command state.

Equations

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