Pantograph.lean

@@ -54,7 +54,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
     let nGoals := state.goalStates.size
-    set { state with goalStates := Lean.HashMap.empty }
+    set { state with nextId := 0, goalStates := Lean.HashMap.empty }
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -163,8 +163,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       | .error error => return .error error
       | .ok (.success nextGoalState) =>
         let nextStateId := state.nextId
-        let goalStates := state.goalStates.insert state.nextId goalState
-        set { state with goalStates, nextId := state.nextId + 1 }
+        set { state with
+          goalStates := state.goalStates.insert state.nextId nextGoalState,
+          nextId := state.nextId + 1,
+        }
         let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
         return .ok {
           nextStateId? := .some nextStateId,

Test/Integration.lean

@@ -83,11 +83,19 @@ def test_malformed_command : IO LSpec.TestSeq :=
       Protocol.InteractionError))
   ]
 def test_tactic : IO LSpec.TestSeq :=
-  let goal: Protocol.Goal := {
+  let goal1: Protocol.Goal := {
     name := "_uniq.10",
     target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
     vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
+  let goal2: Protocol.Goal := {
+    name := "_uniq.13",
+    target := { pp? := .some "x ∨ y → y ∨ x" },
+    vars := #[
+      { name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
+      { name := "_uniq.12", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+    ],
+  }
   subroutine_runner [
     subroutine_step "goal.start"
       [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
@@ -97,7 +105,14 @@ def test_tactic : IO LSpec.TestSeq :=
       [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      (Lean.toJson ({
        nextStateId? := .some 1,
-       goals? := #[goal],
+       goals? := #[goal1],
+     }:
+      Protocol.GoalTacticResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
+     (Lean.toJson ({
+       nextStateId? := .some 2,
+       goals? := #[goal2],
      }:
       Protocol.GoalTacticResult))
   ]