fix: Level name capture

Pantograph/Library.lean

@@ -116,17 +116,9 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Arr
   liftExcept e
 
 @[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) (levels: Array String): Protocol.FallibleT CoreM GoalState := do
-  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabType expr |>.run with
-      | .error e => return .error e
-      | .ok expr => pure $ expr
-    return .ok $ .ok $ ← GoalState.create expr
-  liftExcept e
-
-@[export pantograph_goal_resume]
-def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
-  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do
+  let t ← parseElabType expr
+  GoalState.create t
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
@@ -164,48 +156,27 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
     extraMVars,
   }
 
-@[export pantograph_goal_tactic_m]
-def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
-  runTermElabM <| state.tryTactic goal tactic
-@[export pantograph_goal_assign_m]
-def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
-  runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
 @[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal (Tactic.evalDraft expr)
-@[export pantograph_goal_let_m]
-def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
-  runTermElabM <| state.tryLet goal binderName type
-@[export pantograph_goal_conv_m]
-def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
-  runTermElabM <| state.conv goal
-@[export pantograph_goal_conv_exit_m]
-def goalConvExit (state: GoalState): CoreM TacticResult :=
-  runTermElabM <| state.convExit
-@[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goal pred
 
 -- Cancel the token after a timeout.
 @[export pantograph_run_cancel_token_with_timeout_m]

Repl.lean

@@ -77,13 +77,14 @@ def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
 
 def liftMetaM { α } (metaM : MetaM α): EMainM α :=
   runCoreM metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) : EMainM α := do
+def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name := [])
+    : EMainM α := do
   let scope := (← get).scope
   let context := {
     isNoncomputableSection := scope.isNoncomputable,
   }
   let state := {
-    levelNames := scope.levelNames,
+    levelNames := scope.levelNames ++ levelNames,
   }
   runCoreM $ termElabM.run' context state |>.run'
 
@@ -268,14 +269,16 @@ def execute (command: Protocol.Command): MainM Json := do
   options_print (_: Protocol.OptionsPrint): EMainM Protocol.Options := do
     return (← getMainState).options
   goal_start (args: Protocol.GoalStart): EMainM Protocol.GoalStartResult := do
-    let expr?: Except _ GoalState ← liftTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr (args.levels?.getD #[]) |>.run
+    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    let expr?: Except _ GoalState ← liftTermElabM (levelNames := levelNames) do
+      match args.expr, args.copyFrom with
+      | .some expr, .none => goalStartExpr expr |>.run
       | .none, .some copyFrom => do
         (match (← getEnv).find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
     match expr? with
     | .error error => Protocol.throw error
     | .ok goalState =>
@@ -349,7 +352,8 @@ def execute (command: Protocol.Command): MainM Json := do
         | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
-        pure $ goalResume target goals
+        let goals := goals.toList.map (λ n => { name := n.toName })
+        pure $ target.resume goals
       | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {branch, goals} must be supplied"
     match nextGoalState? with
     | .error error => Protocol.throw $ errorI "structure" error

Test/Integration.lean

@@ -299,7 +299,7 @@ def test_import_open : Test :=
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
     step "goal.start" ({ expr := "∀ (x : Sort u), Sort (u + 1)"} : Protocol.GoalStart)
-     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
+     ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
   ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do