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.

opaque Lean.Server.Snapshots.dummyTacticCache : IO.Ref Lean.Elab.Tactic.Cache

structure Lean.Server.Snapshots.Snapshot : Type

• beginPos : String.Pos

  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.

• stx : Lean.Syntax
• mpState : Lean.Parser.ModuleParserState
• cmdState : Lean.Elab.Command.State
• interactiveDiags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic

  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.

• tacticCache : IO.Ref Lean.Elab.Tactic.Cache

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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.

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

Equations

• Lean.Server.Snapshots.Snapshot.isAtEnd s = Lean.Parser.isTerminalCommand s.stx

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.

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)

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)

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.

opaque Lean.Server.Snapshots.server.stderrAsMessages : Lean.Option Bool

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.

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.