cleanup and doc-strings

REPL/Main.lean

@@ -95,29 +95,35 @@ def recordProofState (proofState : ProofState) : M m Nat := do
   modify fun s => { s with proofStates := s.proofStates.push proofState }
   return id
 
+/-- Record a `ProofState` and generate a JSON response for it. -/
 def createProofStepReponse (p : ProofState): M m ProofStepResponse := do
   let id ← recordProofState p
   return { proofState := id, goals := (← p.ppGoals).map fun s => s!"{s}" }
 
+/-- Pickle an `Environment`, generating a JSON response. -/
 def pickleEnvironment (n : PickleEnvironment) : M m (CommandResponse ⊕ Error) := do
   match (← get).environments[n.env]? with
   | none => return .inr ⟨"Unknown environment."⟩
   | some env =>
     discard <| env.pickle n.pickleTo
     return .inl { env := n.env }
 
+/-- Unpickle an `Environment`, generating a JSON response. -/
 def unpickleEnvironment (n : UnpickleEnvironment) : M IO CommandResponse := do
   let (env, _) ← Environment.unpickle n.unpickleEnvFrom
   let env ← recordEnvironment env
   return { env }
 
+/-- Pickle a `ProofState`, generating a JSON response. -/
+-- This generates a new identifier, which perhaps is not what we want?
 def pickleProofState (n : PickleProofState) : M m (ProofStepResponse ⊕ Error) := do
   match (← get).proofStates[n.proofState]? with
   | none => return .inr ⟨"Unknown proof State."⟩
   | some proofState =>
     discard <| proofState.pickle n.pickleTo
     return .inl (← createProofStepReponse proofState)
 
+/-- Unpickle a `ProofState`, generating a JSON response. -/
 def unpickleProofState (n : UnpickleProofState) : M IO ProofStepResponse := do
   let (proofState, _) ← ProofState.unpickle n.unpickleProofStateFrom
   createProofStepReponse proofState
@@ -176,6 +182,7 @@ instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
   | .inl a => toJson a
   | .inr b => toJson b
 
+/-- Commands accepted by the REPL. -/
 inductive Input
 | command : REPL.Command → Input
 | proofStep : REPL.ProofStep → Input
@@ -184,6 +191,7 @@ inductive Input
 | pickleProofState : REPL.PickleProofState → Input
 | unpickleProofState : REPL.UnpickleProofState → Input
 
+/-- Parse a user input string to an input command. -/
 def parse (query : String) : IO Input := do
   let json := Json.parse query
   match json with

REPL/ProofState.lean

@@ -94,13 +94,16 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext)
       tacticContext := { elaborator := .anonymous } }
 
 open Lean.Meta in
+/-- A copy of `Meta.Context` with closures omitted. -/
 structure CompactableMetaContext where
   config            : Config               := {}
   lctx              : LocalContext         := {}
   localInstances    : LocalInstances       := #[]
   defEqCtx?         : Option DefEqContext  := none
   synthPendingDepth : Nat                  := 0
+  -- canUnfold?        : Option (Config → ConstantInfo → CoreM Bool) := none
 
+/-- A copy of `Term.Context` with closures and a cache omitted. -/
 structure CompactableTermContext where
   declName? : Option Name := none
   auxDeclToFullName : FVarIdMap Name  := {}
@@ -116,11 +119,12 @@ structure CompactableTermContext where
   isNoncomputableSection : Bool        := false
   ignoreTCFailures : Bool := false
   inPattern        : Bool := false
-  tacticCache?     : Option (IO.Ref Tactic.Cache) := none
+  -- tacticCache?     : Option (IO.Ref Tactic.Cache) := none
   saveRecAppSyntax : Bool := true
   holesAsSyntheticOpaque : Bool := false
 
 open Lean.Core in
+/-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/
 structure CompactableCoreState where
   -- env             : Environment
   nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1
@@ -132,6 +136,11 @@ structure CompactableCoreState where
 
 open System (FilePath)
 
+/--
+Pickle a `ProofState`, discarding closures and non-essential caches.
+
+When pickling the `Environment`, we do so relative to its imports.
+-/
 def pickle (p : ProofState) (path : FilePath) : IO Unit := do
   let env := p.coreState.env
   let p' := { p with coreState := { p.coreState with env := ← mkEmptyEnvironment }}
@@ -147,9 +156,15 @@ def pickle (p : ProofState) (path : FilePath) : IO Unit := do
      p'.tacticState,
      p'.tacticContext)
 
+/--
+Unpickle a `ProofState`.
+-/
 def unpickle (path : FilePath) : IO (ProofState × CompactedRegion) := unsafe do
-  let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext, tacticState, tacticContext), region) ←
-    _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState × Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext × Tactic.State × Tactic.Context) path
+  let ((imports, map₂, coreState, coreContext, metaState, metaContext, termState, termContext,
+    tacticState, tacticContext), region) ←
+    _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCoreState ×
+      Core.Context × Meta.State × CompactableMetaContext × Term.State × CompactableTermContext ×
+      Tactic.State × Tactic.Context) path
   let env ← importModules imports {} 0
   let env := { env with constants := { env.constants with map₂ }}
   let p' :=