# Documentation

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
• 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 :
• tacticCache :

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

Instances For
Equations
• = s.mpState.pos
Equations
• = s.cmdState.env
Equations
• = s.cmdState.messages
Equations
Equations
• One or more equations did not get rendered due to their size.

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.

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

Equations

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

Equations

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.

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.

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.