Pantograph/Goal.lean

@@ -260,7 +260,6 @@ protected def GoalState.tryTacticM
     (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
     (guardMVarErrors : Bool := false)
     : Elab.TermElabM TacticResult := do
-  assert! ¬ (← goal.isAssigned)
   let prevMessageLength := state.coreState.messages.toList.length
   try
     let nextState ← state.step goal tacticM guardMVarErrors
@@ -290,6 +289,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
+  assert! ¬ (← goal.isAssigned)
   state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):

Test/Common.lean

@@ -69,8 +69,6 @@ end Condensed
 
 def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
-def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
-  state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
 
 def TacticResult.toString : TacticResult → String
   | .success state _messages => s!".success ({state.goals.length} goals)"

Test/Proofs.lean

@@ -66,15 +66,15 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
     return a
 
 def test_identity: TestM Unit := do
-  let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
+  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
-  let state0 ← GoalState.create (expr := rootTarget)
+  let tactic := "intro p h"
-  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
+  let state1 ← match ← state0.tacticOn 0 tactic with
     | .success state _ => pure state
     | other => do
       fail other.toString
       return ()
   let inner := "_uniq.11"
-  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)