Merge pull request 'fix: Shield tactics from the environment generated by `frontend.process`' (#199) from bug/exact-question-mark into dev

Reviewed-on: #199

Pantograph/Frontend/Elab.lean

@@ -154,9 +154,7 @@ the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
-  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
-  withEnv env do
   let goalsM := sorrys.mapM λ i => do
     match i.info with
     | .ofTermInfo termInfo  => do

Pantograph/Frontend/MetaTranslate.lean

@@ -118,6 +118,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
 
 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
   if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
+    trace[Pantograph.Frontend.MetaTranslate] "Existing mvar id {srcMVarId.name} → {mvarId'.name}"
     return mvarId'
   let mvarId' ← Meta.withLCtx .empty #[] do
     let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
@@ -134,6 +135,7 @@ partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
           let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
           assignDelayedMVar mvarId' fvars' mvarIdPending'
         pure mvarId'
+  trace[Pantograph.Frontend.MetaTranslate] "Translated {srcMVarId.name} → {mvarId'.name}"
   addTranslatedMVar srcMVarId mvarId'
   return mvarId'
 end
@@ -148,6 +150,7 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
     let lctx' ← translateLCtx
     let mvar ← Meta.withLCtx lctx' #[] do
       let type' ← translateExpr type
+      trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'
     return mvar.mvarId!
 

Pantograph/Goal.lean

@@ -241,23 +241,20 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
-  | success (state: GoalState)
+  | success (state : GoalState) (messages : Array String)
   -- Tactic failed with messages
-  | failure (messages: Array String)
+  | failure (messages : Array String)
   -- Could not parse tactic
-  | parseError (message: String)
+  | parseError (message : String)
   -- The given action cannot be executed in the state
-  | invalidAction (message: String)
+  | invalidAction (message : String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
+  let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
+  let hasErrors := newMessages.any (·.severity == .error)
-      if m.severity == .error then
+  let newMessages ← newMessages.mapM λ m => m.toString
-        return .some $ ← m.toString
-      else
-        return .none
   Core.resetMessageLog
-  return newMessages.toArray
+  return (hasErrors, newMessages.toArray)
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
@@ -269,13 +266,16 @@ protected def GoalState.tryTacticM
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
-    let newMessages ← dumpMessageLog prevMessageLength
+    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
-    if ¬ newMessages.isEmpty then
+    if hasError then
       return .failure newMessages
-    return .success nextState
+    else
+      return .success nextState newMessages
   catch exception =>
     match exception with
-    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
+    | .internal _ =>
+      let (_, messages) ← dumpMessageLog prevMessageLength
+      return .failure messages
     | _ => return .failure #[← exception.toMessageData.toString]
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
@@ -344,7 +344,7 @@ protected def GoalState.conv (state: GoalState) (goal: MVarId):
       parentMVar? := .some goal,
       convMVar? := .some (convRhs, goal, otherGoals),
       calcPrevRhs? := .none
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -381,7 +381,7 @@ protected def GoalState.convExit (state: GoalState):
       parentMVar? := .some convGoal,
       convMVar? := .none
       calcPrevRhs? := .none
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -459,7 +459,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       },
       parentMVar? := .some goal,
       calcPrevRhs?
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 

Pantograph/Protocol.lean

@@ -268,14 +268,14 @@ structure GoalTactic where
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
   nextStateId?: Option Nat          := .none
-  -- If the array is empty, it shows the goals have been fully resolved.
+  -- If the array is empty, it shows the goals have been fully resolved. If this
+  -- is .none, there has been a tactic error.
   goals?: Option (Array Goal)       := .none
 
-  -- Existence of this field shows tactic execution failure
+  messages? : Option (Array String) := .some #[]
-  tacticErrors?: Option (Array String) := .none
 
   -- Existence of this field shows the tactic parsing has failed
-  parseError?: Option String := .none
+  parseError? : Option String       := .none
   deriving Lean.ToJson
 structure GoalContinue where
   -- State from which the continuation acquires the context

Repl.lean

@@ -5,6 +5,8 @@ namespace Pantograph.Repl
 
 open Lean
 
+set_option trace.Pantograph.Frontend.MetaTranslate true
+
 structure Context where
   coreContext : Core.Context
 
@@ -61,6 +63,10 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
     catch ex =>
       let desc ← ex.toMessageData.toString
       return Except.error $ ({ error := "exception", desc } : Protocol.InteractionError)
+    finally
+      for {msg, ..} in (← getTraceState).traces do
+        IO.eprintln (← msg.format.toIO)
+      resetTraceState
   if let .some token := cancelTk? then
     runCancelTokenWithTimeout token (timeout := .ofBitVec options.timeout)
   let (result, state') ← match ← (coreM'.run coreCtx coreState).toIO' with
@@ -149,7 +155,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): EMainM Protocol.Fro
         .some $ step.newConstants.toArray.map λ name => name.toString
       else
         .none
-    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then do
+    let (goalStateId?, goals?, goalSrcBoundaries?) ← if step.sorrys.isEmpty then
         pure (.none, .none, .none)
       else do
         let ({ state, srcBoundaries }, goals) ← liftMetaM do
@@ -319,7 +325,7 @@ def execute (command: Protocol.Command): MainM Json := do
         pure $ .error error
     match nextGoalState? with
     | .error error => Protocol.throw error
-    | .ok (.success nextGoalState) => do
+    | .ok (.success nextGoalState messages) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
           pure $ nextGoalState.immediateResume goalState
@@ -336,13 +342,14 @@ def execute (command: Protocol.Command): MainM Json := do
       return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
+        messages? := .some messages,
       }
     | .ok (.parseError message) =>
-      return { parseError? := .some message }
+      return { messages? := .none, parseError? := .some message }
     | .ok (.invalidAction message) =>
       Protocol.throw $ errorI "invalid" message
     | .ok (.failure messages) =>
-      return { tacticErrors? := .some messages }
+      return { messages? := .some messages }
   goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
     let state ← getMainState
     let .some target := state.goalStates[args.target]? |

Test/Common.lean

@@ -71,7 +71,7 @@ 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 TacticResult.toString : TacticResult → String
-  | .success state => s!".success ({state.goals.length} goals)"
+  | .success state _messages => s!".success ({state.goals.length} goals)"
   | .failure messages =>
     let messages := "\n".intercalate messages.toList
     s!".failure {messages}"

Test/Integration.lean

@@ -88,7 +88,7 @@ def test_tactic : Test :=
     step "goal.tactic" ({ stateId := 1, tactic? := .some "intro y" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
-     ({ tacticErrors? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
+     ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
       Protocol.GoalTacticResult)
   ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
@@ -302,6 +302,34 @@ def test_import_open : Test :=
      ({ stateId := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
   ]
 
+/-- Ensure there cannot be circular references -/
+def test_frontend_process_circular : Test :=
+  let withSorry := "theorem mystery : 1 + 2 = 2 + 3 := sorry"
+  [
+    let goal1: Protocol.Goal := {
+      name := "_uniq.2",
+      target := { pp? := .some "1 + 2 = 2 + 3" },
+      vars := #[],
+    }
+    step "frontend.process"
+      ({
+        file? := .some withSorry,
+        sorrys := true,
+      }: Protocol.FrontendProcess)
+     ({
+       units := [{
+         boundary := (0, withSorry.utf8ByteSize),
+         goalStateId? := .some 0,
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(35, 40)],
+         messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
+       }],
+     }: Protocol.FrontendProcessResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "exact?" }: Protocol.GoalTactic)
+     ({ messages? := .some #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."] }
+     : Protocol.GoalTacticResult),
+  ]
+
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
   let coreContext ← createCoreContext #[]
@@ -322,6 +350,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),
     ("frontend.process import", test_import_open),
+    ("frontend.process circular", test_frontend_process_circular),
   ]
   tests.map (fun (name, test) => (name, runTest env test))
 

Test/Main.lean

@@ -55,6 +55,7 @@ def main (args: List String) := do
     ("Serial", Serial.suite env_default),
     ("Tactic/Assign", Tactic.Assign.suite env_default),
     ("Tactic/Prograde", Tactic.Prograde.suite env_default),
+    ("Tactic/Special", Tactic.Special.suite env_default),
   ]
   let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
   LSpec.lspecEachIO [()] (λ () => runTestGroup nameFilter? tests)

Test/Metavar.lean

@@ -79,7 +79,7 @@ def test_m_couple: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -88,7 +88,7 @@ def test_m_couple: TestM Unit := do
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   -- Set m to 3
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -111,7 +111,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -122,7 +122,7 @@ def test_m_couple_simp: TestM Unit := do
     #[#["_uniq.38"], #["_uniq.38"], #[]])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -136,7 +136,7 @@ def test_m_couple_simp: TestM Unit := do
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
   addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
   let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -146,7 +146,7 @@ def test_m_couple_simp: TestM Unit := do
       return ()
     | .ok state => pure state
   let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -173,7 +173,7 @@ def test_proposition_generation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -187,7 +187,7 @@ def test_proposition_generation: TestM Unit := do
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
 
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -197,7 +197,7 @@ def test_proposition_generation: TestM Unit := do
 
   let assign := "Eq.refl x"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -216,7 +216,7 @@ def test_partial_continuation: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -224,7 +224,7 @@ def test_partial_continuation: TestM Unit := do
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()

Test/Proofs.lean

@@ -89,7 +89,7 @@ def test_identity: TestM Unit := do
 
   let tactic := "intro p h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -116,7 +116,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn 0 "intro n m" with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -130,7 +130,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
     addTest $ assertUnreachable $ other.toString
 
   let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -148,14 +148,14 @@ def test_delta_variable: TestM Unit := do
       return ()
 
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
     #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -187,14 +187,14 @@ def test_arith: TestM Unit := do
 
   let tactic := "intros"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic (state1.goals.length = 1)
   addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -202,7 +202,7 @@ def test_arith: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
   let tactic := "assumption"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -237,7 +237,7 @@ def test_or_comm: TestM Unit := do
 
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -265,7 +265,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -291,7 +291,7 @@ def test_or_comm: TestM Unit := do
     s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
 
   let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -301,7 +301,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv {state3_1goal0}))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -310,13 +310,13 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
   let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -330,13 +330,13 @@ def test_or_comm: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals[0]!])
   let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -375,7 +375,7 @@ def test_conv: TestM Unit := do
 
   let tactic := "intro a b c1 c2 h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -383,7 +383,7 @@ def test_conv: TestM Unit := do
     #[interiorGoal [] "a + b + c1 = b + a + c2"])
 
   let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -392,7 +392,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rhs"
   let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -401,7 +401,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "lhs"
   let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -410,7 +410,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "congr"
   let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -422,7 +422,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rw [Nat.add_comm]"
   let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -431,7 +431,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -446,7 +446,7 @@ def test_conv: TestM Unit := do
 
   let convTactic := "rfl"
   let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -454,14 +454,14 @@ def test_conv: TestM Unit := do
     #[])
 
   let state1_1 ← match ← state6.convExit with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
 
   let tactic := "exact h"
   let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -488,7 +488,7 @@ def test_calc: TestM Unit := do
       return ()
   let tactic := "intro a b c d h1 h2"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -496,7 +496,7 @@ def test_calc: TestM Unit := do
     #[interiorGoal [] "a + b = c + d"])
   let pred := "a + b = b + c"
   let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -510,7 +510,7 @@ def test_calc: TestM Unit := do
 
   let tactic := "apply h1"
   let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -521,7 +521,7 @@ def test_calc: TestM Unit := do
       return ()
   let pred := "_ = c + d"
   let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -532,7 +532,7 @@ def test_calc: TestM Unit := do
   addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
   let tactic := "apply h2"
   let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -553,7 +553,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
 
   let tactic := "intro p"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -572,7 +572,7 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
 
   let tactic := "intro p q r h"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -604,7 +604,7 @@ def test_deconstruct : TestM Unit := do
 
   let tactic := "intro p q ⟨hp, hq⟩"
   let state1 ← match ← state0.tacticOn 0 tactic with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       fail other.toString
       return ()

Test/Tactic.lean

@@ -1,2 +1,3 @@
 import Test.Tactic.Assign
 import Test.Tactic.Prograde
+import Test.Tactic.Special

Test/Tactic/Prograde.lean

@@ -56,7 +56,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -65,7 +65,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -75,7 +75,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
   let evalBind := "y"
   let evalExpr := "Or.inl h"
   let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -95,7 +95,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl y"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
 def test_define_root_expr : TestT Elab.TermElabM Unit := do
   --let rootExpr ← parseSentence "Nat"
   --let state0 ← GoalState.create rootExpr
-  --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
+  --let .success state1 _ ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
   --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
   --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
   let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p x"
-  let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state1 _ ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let binderName := `binder
   let value := "x.fst"
   let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
   let tacticM := Tactic.evalDefine binderName expr
-  let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
+  let .success state2 _ ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
   let tactic := s!"apply {binderName}"
-  let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state3 _ ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let tactic := s!"exact 5"
-  let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
+  let .success state4 _ ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
@@ -140,7 +140,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -149,7 +149,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl (Or.inl h)"
   let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -159,7 +159,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
   let haveBind := "y"
   let haveType := "p ∨ q"
   let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -171,7 +171,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
 
   let expr := "Or.inl h"
   let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -185,7 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
       return ()
   let expr := "Or.inl y"
   let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -200,7 +200,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let state0 ← GoalState.create rootExpr
   let tactic := "intro a p h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -216,7 +216,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
     | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
     | false => state1.tryAssign (state1.get! 0) (expr := expr)
   let state2 ← match result2 with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -241,7 +241,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact 1"
   let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
@@ -274,7 +274,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
 
   let tactic := "exact Or.inl (Or.inl h)"
   let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
+    | .success state _ => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()

Test/Tactic/Special.lean

@@ -0,0 +1,23 @@
+import LSpec
+import Lean
+import Test.Common
+
+open Lean
+open Pantograph
+
+namespace Pantograph.Test.Tactic.Special
+
+def test_exact_q : TestT Elab.TermElabM Unit := do
+  let rootExpr ← parseSentence "1 + 2 = 2 + 3"
+  let state0 ← GoalState.create rootExpr
+  let tactic := "exact?"
+  let state1? ← state0.tacticOn (goalId := 0) (tactic := tactic)
+  let .failure messages := state1? | fail "Must fail"
+  checkEq "messages" messages #["`exact?` could not close the goal. Try `apply?` to see partial suggestions."]
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("exact?", test_exact_q),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Special

doc/repl.md

@@ -39,6 +39,8 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   - `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
     exit, the goal id is ignored.
   - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
+  If the `goals` field does not exist, the tactic execution has failed. Read
+  `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
   Execute continuation/resumption
   - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.