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.

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

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

      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.
      Instances For

        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.
        Instances For

          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.
          Instances For

            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.
            Instances For