feat: support incrementality in command mode

Author: kim-em

REPL/Main.lean

@@ -66,6 +66,7 @@ structure State where
   -/
   cmdStates : Array CommandSnapshot := #[]
   incrementalStates : Array IncrementalState := #[]
+  latestInitialIncrementalState : Option Nat := none
   latestIncrementalState : HashMap Nat Nat := {}
   /--
   Proof states after individual tactics.
@@ -203,7 +204,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let (incrementalStateBefore?, notFound) ← do
     let j? ← match s.incr with
     | none => match s.env with
-      | none => pure none
+      | none => match (← get).latestInitialIncrementalState with
+        | none => pure none
+        | j => pure j
       | some i => match (← get).latestIncrementalState.find? i with
         | none => pure none
         | j => pure j
@@ -235,6 +238,8 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let incr ← recordIncrementalState incrementalState
   if let some i := s.env then
     modify fun c => { c with latestIncrementalState := c.latestIncrementalState.insert i incr }
+  else
+    modify fun c => { c with latestInitialIncrementalState := some incr }
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.bind InfoTree.retainTacticInfo

lean-toolchain

@@ -1 +1 @@
-lean4
+leanprover/lean4-pr-releases:pr-release-3636

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-lean4
+leanprover/lean4-pr-releases:pr-release-3636

test/incrementality.expected.out

@@ -1,5 +1,3 @@
-{"incr": 0, "env": 0}
-
 !
 {"sorries":
  [{"proofState": 0,
@@ -11,8 +9,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 1,
- "env": 1}
+ "incr": 0,
+ "env": 0}
 
 {"sorries":
  [{"proofState": 1,
@@ -24,8 +22,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 2,
- "env": 2}
+ "incr": 1,
+ "env": 1}
 
 {"sorries":
  [{"proofState": 2,
@@ -37,8 +35,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 3,
- "env": 3}
+ "incr": 2,
+ "env": 2}
 
 {"message": "Unknown incremental state."}
 

test/incrementality.in

@@ -1,10 +1,8 @@
-{"cmd": "import Lean\nopen Lean"}
+{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry"}
 
-{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "env": 0}
+{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry"}
 
-{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "env": 0}
+{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "incr": 1}
 
-{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "env": 0, "incr": 1}
-
-{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "env": 0, "incr": 37}
+{"cmd": "example : True := by\n  dbg_trace \"!\"\n  sorry", "incr": 37}
 

test/incrementality.lean

@@ -1,7 +1,3 @@
-import Lean
-
-open Lean
-
 example : True := by
   dbg_trace "!"
   sorry

test/incrementality_2.expected.out

@@ -1,5 +1,3 @@
-{"incr": 0, "env": 0}
-
 !1
 !2
 {"messages":
@@ -11,8 +9,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 1,
- "env": 1}
+ "incr": 0,
+ "env": 0}
 
 {"sorries":
  [{"proofState": 0,
@@ -24,8 +22,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 2,
- "env": 2}
+ "incr": 1,
+ "env": 1}
 
 {"messages":
  [{"severity": "error",
@@ -36,8 +34,8 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 3,
- "env": 3}
+ "incr": 2,
+ "env": 2}
 
 !2
 {"messages":
@@ -49,6 +47,6 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "incr": 4,
- "env": 4}
+ "incr": 3,
+ "env": 3}
 

test/incrementality_2.in

@@ -1,9 +1,7 @@
-{"cmd": "import Lean\nopen Lean"}
+{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\""}
 
-{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\"", "env": 0}
+{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  sorry"}
 
-{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  sorry", "env": 0}
+{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\"", "incr": 0}
 
-{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\"", "env": 0, "incr": 1}
-
-{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\"", "env": 0, "incr": 2}
+{"cmd": "example : True := by\n  dbg_trace \"!1\"\n  dbg_trace \"!2\"", "incr": 1}