Introduce incremental processing of the commands

REPL/Frontend.lean

@@ -5,10 +5,42 @@ Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
 
-open Lean Elab
+open Lean Elab Language
 
 namespace Lean.Elab.IO
 
+partial def IO.processCommandsIncrementally' (inputCtx : Parser.InputContext)
+    (parserState : Parser.ModuleParserState) (commandState : Command.State)
+    (old? : Option IncrementalState) :
+    BaseIO (List (IncrementalState × Option InfoTree)) := do
+  let task ← Language.Lean.processCommands inputCtx parserState commandState
+    (old?.map fun old => (old.inputCtx, old.initialSnap))
+  return go task.get task #[]
+where
+  go initialSnap t commands :=
+    let snap := t.get
+    let commands := commands.push snap
+    -- Opting into reuse also enables incremental reporting, so make sure to collect messages from
+    -- all snapshots
+    let messages := toSnapshotTree initialSnap
+      |>.getAll.map (·.diagnostics.msgLog)
+      |>.foldl (· ++ ·) {}
+    -- In contrast to messages, we should collect info trees only from the top-level command
+    -- snapshots as they subsume any info trees reported incrementally by their children.
+    let trees := commands.map (·.elabSnap.infoTreeSnap.get.infoTree?) |>.filterMap id |>.toPArray'
+    let result : (IncrementalState × Option InfoTree) :=
+      ({ commandState := { snap.elabSnap.resultSnap.get.cmdState with messages, infoState.trees := trees }
+         , parserState := snap.parserState
+         , cmdPos := snap.parserState.pos
+         , commands := commands.map (·.stx)
+         , inputCtx := inputCtx
+         , initialSnap := initialSnap
+       }, snap.elabSnap.infoTreeSnap.get.infoTree?)
+    if let some next := snap.nextCmdSnap? then
+      result :: go initialSnap next.task commands
+    else
+      [result]
+
 /--
 Wrapper for `IO.processCommands` that enables info states, and returns
 * the new command state
@@ -17,41 +49,36 @@ Wrapper for `IO.processCommands` that enables info states, and returns
 -/
 def processCommandsWithInfoTrees
     (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)
-    (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
+    (commandState : Command.State) (incrementalState? : Option IncrementalState := none)
+    : IO (List (IncrementalState × Option InfoTree) × List Message) := do
   let commandState := { commandState with infoState.enabled := true }
-  let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.toList, s.infoState.trees.toList)
+  let incStates ← IO.processCommandsIncrementally' inputCtx parserState commandState incrementalState?
+  pure (incStates, (incStates.getLast?.map (·.1.commandState.messages.toList)).getD {})
 
 /--
 Process some text input, with or without an existing command state.
-If there is no existing environment, we parse the input for headers (e.g. import statements),
-and create a new environment.
-Otherwise, we add to the existing environment.
 
 Returns:
-1. The header-only command state (only useful when cmdState? is none)
-2. The resulting command state after processing the entire input
-3. List of messages
-4. List of info trees
+1. The resulting command state after processing the entire input
+2. List of messages
+3. List of info trees along with Command.State from the incremental processing
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × List (IncrementalState × Option InfoTree) × List Message) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
   let inputCtx   := Parser.mkInputContext input fileName
-
   match cmdState? with
   | none => do
     -- Split the processing into two phases to prevent self-reference in proofs in tactic mode
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
     let (env, messages) ← processHeader header opts messages inputCtx
     let headerOnlyState := Command.mkState env messages opts
-    let (cmdState, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
-    return (headerOnlyState, cmdState, messages, trees)
-
+    let incStates ← processCommandsWithInfoTrees inputCtx parserState headerOnlyState
+    return (headerOnlyState, incStates)
   | some cmdStateBefore => do
     let parserState : Parser.ModuleParserState := {}
-    let (cmdStateAfter, messages, trees) ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
-    return (cmdStateBefore, cmdStateAfter, messages, trees)
+    let incStates ← processCommandsWithInfoTrees inputCtx parserState cmdStateBefore
+    return (cmdStateBefore, incStates)

REPL/JSON.lean

@@ -47,7 +47,7 @@ deriving ToJson, FromJson
 structure Pos where
   line : Nat
   column : Nat
-deriving ToJson, FromJson
+deriving ToJson, FromJson, BEq, Hashable
 
 /-- Severity of a message. -/
 inductive Severity

REPL/Main.lean

@@ -102,11 +102,7 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
       fun ⟨ctx, g, pos, endPos⟩ => do
         let (goal, proofState) ← match g with
         | .tactic g => do
-          let lctx ← ctx.runMetaM {} do
-              match ctx.mctx.findDecl? g with
-              | some decl => return decl.lctx
-              | none => throwError "unknown metavariable '{g}'"
-          let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
+          let s ← ProofSnapshot.create ctx none env? [g] rootGoals?
           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
@@ -115,6 +111,16 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
         let proofStateId ← proofState.mapM recordProofSnapshot
         return Sorry.of goal pos endPos proofStateId
 
+def sorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment)
+(rootGoals? : Option (List MVarId))
+: M m (List Sorry) :=
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let s ← sorries infoTree?.toList prevEnv rootGoals?
+    let restSorries ← sorriesCmd rest state.commandState.env rootGoals?
+    return s ++ restSorries
+
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
     Lean.PrettyPrinter.ppTactic ⟨stx⟩
@@ -130,6 +136,14 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Tactic.of goals tactic pos endPos proofStateId ns
 
+def tacticsCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) : M m (List Tactic) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let ts ← tactics infoTree?.toList prevEnv
+    let restTactics ← tacticsCmd rest state.commandState.env
+    return ts ++ restTactics
+
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
@@ -138,6 +152,14 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Sorry.of goals pos pos proofStateId
 
+def collectRootGoalsAsSorriesCmd (treeList : List (IncrementalState × Option InfoTree)) (prevEnv : Environment) :
+    M m (List Sorry) := do
+  match treeList with
+  | [] => pure []
+  | (state, infoTree?) :: rest => do
+    let sorries ← collectRootGoalsAsSorries infoTree?.toList prevEnv
+    let restSorries ← collectRootGoalsAsSorriesCmd rest state.commandState.env
+    return sorries ++ restSorries
 
 private def collectFVarsAux : Expr → NameSet
   | .fvar fvarId => NameSet.empty.insert fvarId.name
@@ -197,7 +219,7 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             unless (← Meta.isDefEq pft expectedType) do
               return s!"Error: proof has type {pft} but root goal has type {expectedType}"
 
-            let pf ← abstractAllLambdaFVars pf
+            let pf ← abstractAllLambdaFVars pf >>= instantiateMVars
             let pft ← Meta.inferType pf >>= instantiateMVars
 
             if pf.hasExprMVar then
@@ -302,19 +324,19 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   if notFound then
     return .inr ⟨"Unknown environment."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (initialCmdState, cmdState, messages, trees) ← try
+  let (initialCmdState, incStates, messages) ← try
     IO.processInput s.cmd initialCmdState?
   catch ex =>
     return .inr ⟨ex.toString⟩
+
+  let cmdState := (incStates.getLast?.map (fun c => c.1.commandState)).getD initialCmdState
   let messages ← messages.mapM fun m => Message.of m
-  -- For debugging purposes, sometimes we print out the trees here:
-  -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees initialCmdState.env none
+  let sorries ← sorriesCmd incStates initialCmdState.env none
   let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
+  | some true => pure (sorries ++ (← collectRootGoalsAsSorriesCmd incStates initialCmdState.env))
   | _ => pure sorries
   let tactics ← match s.allTactics with
-  | some true => tactics trees initialCmdState.env
+  | some true => tacticsCmd incStates initialCmdState.env
   | _ => pure []
   let cmdSnapshot :=
   { cmdState
@@ -324,6 +346,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
+  let trees := cmdState.infoState.trees.toList
+  -- For debugging purposes, sometimes we print out the trees here:
+  -- trees.forM fun t => do IO.println (← t.format)
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.flatMap InfoTree.retainTacticInfo

REPL/Snapshots.lean

@@ -185,33 +185,44 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
+
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
-
 For convenience, we also allow a list of `Expr`s, and these are appended to the goals
 as fresh metavariables with the given types.
 -/
-def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Environment)
+def create (ctx : ContextInfo) (lctx? : Option LocalContext) (prevEnv? : Option Environment)
     (goals : List MVarId) (rootGoals? : Option (List MVarId)) (types : List Expr := [])
     : IO ProofSnapshot := do
-  ctx.runMetaM (lctx?.getD {}) do
-    let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    let s ← getThe Core.State
-    let s := match env? with
-    | none => s
-    | some env => { s with env }
-    pure <|
-    { coreState := s
-      coreContext := ← readThe Core.Context
-      metaState := ← getThe Meta.State
-      metaContext := ← readThe Meta.Context
-      termState := {}
-      termContext := {}
-      tacticState := { goals }
-      tacticContext := { elaborator := .anonymous }
-      rootGoals := match rootGoals? with
-        | none => goals
-        | some gs => gs }
+  -- Get the local context from the goals if not provided.
+  let lctx ← match lctx? with
+  | none => match goals with
+    | g :: _ => ctx.runMetaM {} do pure (← g.getDecl).lctx
+    | [] => match rootGoals? with
+      | some (g :: _) => ctx.runMetaM {} do pure (← g.getDecl).lctx
+      | _ => pure {}
+  | some lctx => pure lctx
+
+  ctx.runMetaM lctx do
+    -- update local instances, which is necessary when `types` is non-empty
+    Meta.withLocalInstances (lctx.decls.toList.filterMap id) do
+      let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+      let s ← getThe Core.State
+      let s := match prevEnv? with
+      | none => s
+      | some env => { s with env }
+      pure <|
+      { coreState := s
+        coreContext := ← readThe Core.Context
+        metaState := ← getThe Meta.State
+        metaContext := ← readThe Meta.Context
+        termState := {}
+        termContext := {}
+        tacticState := { goals }
+        tacticContext := { elaborator := .anonymous }
+        rootGoals := match rootGoals? with
+          | none => goals
+          | some gs => gs }
 
 open Lean.Core in
 /-- A copy of `Core.State` with the `Environment`, caches, and logging omitted. -/

test/in_command_dependency.expected.out

@@ -0,0 +1,45 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "info",
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 28},
+   "data": "Try this:\n  [apply] exact x"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 1,
+   "pos": {"line": 1, "column": 21},
+   "goal": "⊢ False",
+   "endPos": {"line": 1, "column": 26}},
+  {"proofState": 2,
+   "pos": {"line": 2, "column": 19},
+   "goal": "⊢ False",
+   "endPos": {"line": 2, "column": 24}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "warning",
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
+{"proofStatus": "Completed",
+ "proofState": 3,
+ "messages":
+ [{"severity": "info",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "Try this:\n  [apply] exact x"}],
+ "goals": []}
+

test/in_command_dependency.in

@@ -0,0 +1,6 @@
+{"cmd": "theorem x : False := sorry\nexample : False := by exact?"}
+
+{"cmd": "theorem x : False := sorry\nexample : False := sorry"}
+
+{"proofState": 2, "tactic": "exact?"}
+

test/local_instance_proof.expected.out

@@ -0,0 +1,62 @@
+{"env": 0}
+
+{"env": 1}
+
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 42},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 47}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 2}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"sorries":
+ [{"proofState": 2,
+   "pos": {"line": 1, "column": 45},
+   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 50}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 3}
+
+{"proofStatus": "Completed", "proofState": 3, "goals": []}
+
+{"env": 4}
+
+{"sorries":
+ [{"proofState": 4,
+   "pos": {"line": 1, "column": 17},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 22}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 5}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"sorries":
+ [{"proofState": 6,
+   "pos": {"line": 1, "column": 20},
+   "goal": "α : Type\ns : Inhabited α\n⊢ α",
+   "endPos": {"line": 1, "column": 25}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 9},
+   "data": "declaration uses 'sorry'"}],
+ "env": 6}
+
+{"proofStatus": "Completed", "proofState": 7, "goals": []}
+