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")]