From 245e76b2f1b5f0938989850e9a979250133ef651 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 6 Nov 2023 11:51:31 -0800
Subject: [PATCH] feat: Print the root mvar name

---
 Pantograph.lean          | 2 +-
 Pantograph/Protocol.lean | 2 ++
 Test/Integration.lean    | 2 +-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index fb4cc41..6ec4ac1 100644
--- a/Pantograph.lean
+++ b/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
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 2469a6c..ce42d9d 100644
--- a/Pantograph/Protocol.lean
+++ b/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
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 0420a29..d8570b0 100644
--- a/Test/Integration.lean
+++ b/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")]