Pantograph.lean

@@ -143,7 +143,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       let goalState ← GoalState.create expr
       let (goalStates, stateId) := state.goalStates.insert goalState
       set { state with goalStates }
-      return .ok { stateId }
+      return .ok { stateId, root := goalState.root.name.toString }
   goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
     let state ← get
     match state.goalStates.get? args.stateId with

Pantograph/Protocol.lean

@@ -142,6 +142,8 @@ structure GoalStart where
   deriving Lean.FromJson
 structure GoalStartResult where
   stateId: Nat := 0
+  -- Name of the root metavariable
+  root: String
   deriving Lean.ToJson
 structure GoalTactic where
   -- Identifiers for tree, state, and goal

Test/Integration.lean

@@ -91,7 +91,7 @@ def test_tactic : IO LSpec.TestSeq :=
   subroutine_runner [
     subroutine_step "goal.start"
       [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
-     (Lean.toJson ({stateId := 0}:
+     (Lean.toJson ({stateId := 0, root := "_uniq.8"}:
       Protocol.GoalStartResult)),
     subroutine_step "goal.tactic"
       [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]