Merge branch 'dev' into chore/version

2025-05-01 13:39:28 -04:00 · 2025-05-01 13:39:28 -04:00 · df370b0bff
parent 3653465ded 06071c1044
commit df370b0bff
14 changed files with 202 additions and 136 deletions
--- a/Pantograph/Frontend/Elab.lean
+++ b/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
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/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!

--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -113,11 +113,14 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
  }

 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume_parent]
+@[export pantograph_goal_state_immediate_resume]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
  -- Prune parents solved goals
  let mctx := state.mctx
-  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
+  let parentGoals := parent.goals.filter λ goal =>
+    let isDuplicate := state.goals.contains goal
+    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
  {
    state with
    savedState := {
@ -127,19 +130,19 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
  }

 /--
-Brings into scope a list of goals
+Brings into scope a list of goals. User must ensure `goals` is distinct.
 -/
@[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
    .error s!"Goals {invalid_goals} are not in scope"
-  else
  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let unassigned := goals.filter (λ goal =>
-      let mctx := state.mctx
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-    .ok {
+  let unassigned := goals.filter λ goal =>
+    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+    let isDuplicate := state.goals.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
+  return {
    state with
    savedState := {
      term := state.savedState.term,
@ -238,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
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
-      if m.severity == .error then
-        return .some $ ← m.toString
-      else
-        return .none
+private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
+  let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
+  let hasErrors := newMessages.any (·.severity == .error)
+  let newMessages ← newMessages.mapM λ m => m.toString
  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
@ -266,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
-    if ¬ newMessages.isEmpty then
+    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
+    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 -/
@ -341,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]

@ -378,7 +381,7 @@ protected def GoalState.convExit (state: GoalState):
      parentMVar? := .some convGoal,
      convMVar? := .none
      calcPrevRhs? := .none
-    }
+    } #[]
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

@ -456,7 +459,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
      },
      parentMVar? := .some goal,
      calcPrevRhs?
-    }
+    } #[]
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

--- a/Pantograph/Protocol.lean
+++ b/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
-  tacticErrors?: Option (Array String) := .none
+  messages? : Option (Array String) := .some #[]

  -- 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
--- a/Repl.lean
+++ b/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
@ -81,6 +87,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
    : EMainM α := do
  let scope := (← get).scope
  let context := {
+    errToSorry := false,
    isNoncomputableSection := scope.isNoncomputable,
  }
  let state := {
@ -148,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
@ -318,12 +325,10 @@ 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
-          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
-            Protocol.throw $ errorIO "Resuming known goals"
-          pure result
+          pure $ nextGoalState.immediateResume goalState
        | true, .some true => pure nextGoalState
        | true, .some false => do
          let .some (_, _, dormantGoals) := goalState.convMVar? |
@ -337,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]? |
--- a/Test/Common.lean
+++ b/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}"
--- a/Test/Integration.lean
+++ b/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))

--- a/Test/Main.lean
+++ b/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)
--- a/Test/Metavar.lean
+++ b/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 ()
--- a/Test/Proofs.lean
+++ b/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 ()
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -1,2 +1,3 @@
 import Test.Tactic.Assign
 import Test.Tactic.Prograde
+import Test.Tactic.Special
--- a/Test/Tactic/Prograde.lean
+++ b/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 ()
--- a/Test/Tactic/Special.lean
+++ b/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
--- a/doc/repl.md
+++ b/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.