incrementality

Author: kim-em

REPL/Frontend.lean

@@ -17,10 +17,12 @@ 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 (Command.State × IncrementalState × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
-  let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.msgs.toList, s.infoState.trees.toList)
+  let r ← IO.processCommandsIncrementally inputCtx parserState commandState incrementalState?
+  let s := r.commandState
+  pure (s, r, s.messages.msgs.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.
@@ -31,8 +33,9 @@ Otherwise, we add to the existing environment.
 Returns the resulting command state, along with a list of messages and info trees.
 -/
 def processInput (input : String) (cmdState? : Option Command.State)
+     (incrementalState? : Option IncrementalState := none)
     (opts : Options := {}) (fileName : Option String := none) :
-    IO (Command.State × List Message × List InfoTree) := unsafe do
+    IO (Command.State × IncrementalState × List Message × List InfoTree) := unsafe do
   Lean.initSearchPath (← Lean.findSysroot)
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
@@ -44,4 +47,4 @@ def processInput (input : String) (cmdState? : Option Command.State)
     pure (parserState, (Command.mkState env messages opts))
   | some cmdState => do
     pure ({ : Parser.ModuleParserState }, cmdState)
-  processCommandsWithInfoTrees inputCtx parserState commandState
+  processCommandsWithInfoTrees inputCtx parserState commandState incrementalState?

REPL/JSON.lean

@@ -17,6 +17,7 @@ If `env = some n`, builds on the existing environment `n`.
 -/
 structure Command where
   env : Option Nat
+  incr : Option Nat
   cmd : String
   allTactics : Option Bool := none
   /--
@@ -112,6 +113,7 @@ A response to a Lean command.
 -/
 structure CommandResponse where
   env : Nat
+  incr : Option Nat := none
   messages : List Message := []
   sorries : List Sorry := []
   tactics : List Tactic := []
@@ -125,6 +127,7 @@ def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Jso
 instance : ToJson CommandResponse where
   toJson r := Json.mkObj <| .join [
     [("env", r.env)],
+    match r.incr with | some i => [("incr", i)] | none => [],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "tactics" r.tactics,
@@ -166,6 +169,15 @@ structure UnpickleEnvironment where
   unpickleEnvFrom : System.FilePath
 deriving ToJson, FromJson
 
+structure PickleIncrementalState where
+  incr : Nat
+  pickleTo : System.FilePath
+deriving ToJson, FromJson
+
+structure UnpickleIncrementalState where
+  unpickleIncrFrom : System.FilePath
+deriving ToJson, FromJson
+
 structure PickleProofState where
   proofState : Nat
   pickleTo : System.FilePath

REPL/Main.lean

@@ -65,7 +65,8 @@ structure State where
   The user can run a declaration in a given environment using `{"cmd": "def f := 37", "env": 17}`.
   -/
   cmdStates : Array CommandSnapshot := #[]
-  latestIncrementalitySnapshot : HashMap Nat Nat := {}
+  incrementalStates : Array IncrementalState := #[]
+  latestIncrementalState : HashMap Nat Nat := {}
   /--
   Proof states after individual tactics.
   The user can run a tactic in a given proof state using `{"tactic": "exact 42", "proofState": 5}`.
@@ -89,6 +90,11 @@ def recordCommandSnapshot (state : CommandSnapshot) : M m Nat := do
   modify fun s => { s with cmdStates := s.cmdStates.push state }
   return id
 
+def recordIncrementalState (state : IncrementalState) : M m Nat := do
+  let id := (← get).incrementalStates.size
+  modify fun s => { s with incrementalStates := s.incrementalStates.push state }
+  return id
+
 /-- Record a `ProofSnapshot` into the REPL state, returning its index for future use. -/
 def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   let id := (← get).proofStates.size
@@ -194,9 +200,24 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     | none => pure (none, true)
   if notFound then
     return .inr ⟨"Unknown environment."⟩
+  let (incrementalStateBefore?, notFound) ← do
+    let j? ← match s.incr with
+    | none => match s.env with
+      | none => pure none
+      | some i => match (← get).latestIncrementalState.find? i with
+        | none => pure none
+        | j => pure j
+    | some j => pure j
+    match j? with
+    | none => pure (none, false)
+    | some j => do match (← get).incrementalStates[j]? with
+      | some s => pure (some s, false)
+      | none => pure (none, true)
+  if notFound then
+    return .inr ⟨"Unknown incremental state."⟩
   let initialCmdState? := cmdSnapshot?.map fun c => c.cmdState
-  let (cmdState, messages, trees) ← try
-    IO.processInput s.cmd initialCmdState?
+  let (cmdState, incrementalState, messages, trees) ← try
+    IO.processInput s.cmd initialCmdState? incrementalStateBefore?
   catch ex =>
     return .inr ⟨ex.toString⟩
   let messages ← messages.mapM fun m => Message.of m
@@ -211,6 +232,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
       { fileName := "", fileMap := default, tacticCache? := none, snap? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
+  let incr ← recordIncrementalState incrementalState
+  if let some i := s.env then
+    modify fun c => { c with latestIncrementalState := c.latestIncrementalState.insert i incr }
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.bind InfoTree.retainTacticInfo
@@ -223,6 +247,7 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     some <| Json.arr (← jsonTrees.toArray.mapM fun t => t.toJson none)
   return .inl
     { env,
+      incr,
       messages,
       sorries,
       tactics

test.sh

@@ -22,7 +22,7 @@ for infile in $IN_DIR/*.in; do
 
     # Run the command and store its output in a temporary file
     tmpfile=$(mktemp)
-    .lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
+    stdbuf -oL .lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
 
     # Compare the output with the expected output
     if diff "$tmpfile" "$expectedfile"; then

test/all_tactics.expected.out

@@ -9,5 +9,6 @@
    "pos": {"line": 1, "column": 32},
    "goals": "t : Nat ⊢ Nat",
    "endPos": {"line": 1, "column": 39}}],
+ "incr": 0,
  "env": 0}
 

test/by_cases.expected.out

@@ -8,6 +8,7 @@
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
    "data": "declaration uses 'sorry'"}],
+ "incr": 0,
  "env": 0}
 
 {"proofState": 1,

test/calc.expected.out

@@ -28,5 +28,6 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
+ "incr": 0,
  "env": 0}
 

test/def_eval.expected.out

@@ -1,9 +1,10 @@
-{"env": 0}
+{"incr": 0, "env": 0}
 
 {"messages":
  [{"severity": "info",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 6},
    "data": "rfl : f = f"}],
+ "incr": 1,
  "env": 1}
 

test/enableInitializersExecution.expected.out

@@ -1,2 +1,2 @@
-{"env": 0}
+{"incr": 0, "env": 0}
 

test/have_by_sorry.expected.out

@@ -7,7 +7,12 @@
  [{"severity": "error",
    "pos": {"line": 1, "column": 33},
    "endPos": {"line": 2, "column": 28},
-   "data": "unsolved goals\nx : Int\nh : x = 1\n⊢ x = x"}],
+   "data": "unsolved goals\nx : Int\nh : x = 1\n⊢ x = x"},
+  {"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 11},
+   "data": "declaration uses 'sorry'"}],
+ "incr": 0,
  "env": 0}
 
 {"sorries":
@@ -20,6 +25,7 @@
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
    "data": "declaration uses 'sorry'"}],
+ "incr": 1,
  "env": 1}
 
 {"sorries": [{"proofState": 2, "goal": "x : Int\n⊢ x = 1"}],