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

source
opaque Lean.Server.Snapshots.dummyTacticCache :
IO.Ref Lean.Elab.Tactic.Cache
source
structure Lean.Server.Snapshots.Snapshot :
Type

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
    • s.endPos = s.mpState.pos
    Instances For
      source
      def Lean.Server.Snapshots.Snapshot.env (s : Lean.Server.Snapshots.Snapshot) :
      Lean.Environment
      Equations
      • s.env = s.cmdState.env
      Instances For
        source
        def Lean.Server.Snapshots.Snapshot.msgLog (s : Lean.Server.Snapshots.Snapshot) :
        Lean.MessageLog
        Equations
        • s.msgLog = s.cmdState.messages
        Instances For
          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.
          Instances For
            source
            def Lean.Server.Snapshots.Snapshot.isAtEnd (s : Lean.Server.Snapshots.Snapshot) :
            Bool
            Equations
            Instances For
              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.
              Instances For
                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
                Instances For
                  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
                  Instances For