Merge pull request 'chore: Update version' (#195) from chore/version into dev

Reviewed-on: #195

Main.lean

@@ -8,6 +8,12 @@ import Repl
 open Pantograph.Repl
 open Pantograph.Protocol
 
+/-- Print a string to stdout without buffering -/
+def printImmediate (s : String) : IO Unit := do
+  let stdout ← IO.getStdout
+  stdout.putStr (s ++ "\n")
+  stdout.flush
+
 /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
 def parseCommand (s: String): Except String Command := do
   match s.trim.get? 0 with
@@ -34,27 +40,27 @@ partial def loop : MainM Unit := do repeat do
   | .error error =>
     let error  := Lean.toJson ({ error := "command", desc := error }: InteractionError)
     -- Using `Lean.Json.compress` here to prevent newline
-    IO.println error.compress
+    printImmediate error.compress
   | .ok command =>
     try
       let ret ← execute command
       let str := match state.options.printJsonPretty with
         | true => ret.pretty
         | false => ret.compress
-      IO.println str
+      printImmediate str
     catch e =>
       let message := e.toString
       let error  := Lean.toJson ({ error := "main", desc := message }: InteractionError)
-      IO.println error.compress
+      printImmediate error.compress
 
-
-unsafe def main (args: List String): IO Unit := do
+def main (args: List String): IO Unit := do
   -- NOTE: A more sophisticated scheme of command line argument handling is needed.
   if args == ["--version"] then do
     IO.println s!"{Pantograph.version}"
     return
 
-  Pantograph.initSearch ""
+  unsafe do
+    Pantograph.initSearch ""
 
   -- Separate imports and options
   let (options, imports) := args.partition (·.startsWith "--")
@@ -62,7 +68,7 @@ unsafe def main (args: List String): IO Unit := do
   let coreState ← Pantograph.createCoreState imports.toArray
   try
     let mainM := loop.run { coreContext } |>.run' { env := coreState.env }
-    IO.println "ready."
+    printImmediate "ready."
     mainM
   catch ex =>
     let message := ex.toString

Pantograph/Delate.lean

@@ -164,7 +164,7 @@ partial def instantiateDelayedMVars (expr : Expr) : MetaM Expr :=
   self e := instantiateDelayedMVars e
 
 /--
-Convert an expression to an equiavlent form with
+Convert an expression to an equivalent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas or matchers
 3. No assigned mvars

Pantograph/Frontend/Elab.lean

@@ -154,33 +154,31 @@ 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
-        let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+  let goalsM := sorrys.mapM λ i => do
+    match i.info with
+    | .ofTermInfo termInfo  => do
+      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
+      if (← mvarId.getType).hasSorry then
+        throwError s!"Coupling is not allowed in drafting"
+      return [(mvarId, stxByteRange termInfo.stx)]
+    | .ofTacticInfo tacticInfo => do
+      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      for mvarId in mvarIds do
         if (← mvarId.getType).hasSorry then
           throwError s!"Coupling is not allowed in drafting"
-        return [(mvarId, stxByteRange termInfo.stx)]
-      | .ofTacticInfo tacticInfo => do
-        let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-        for mvarId in mvarIds do
-          if (← mvarId.getType).hasSorry then
-            throwError s!"Coupling is not allowed in drafting"
-        let range := stxByteRange tacticInfo.stx
-        return mvarIds.map (·, range)
-      | _ => panic! "Invalid info"
-    let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
-    let goals := annotatedGoals.map Prod.fst
-    let srcBoundaries := annotatedGoals.map Prod.snd
-    let root := match goals with
-      | [] => panic! "No MVars generated"
-      | [g] => g
-      | _ => { name := .anonymous }
-    let state ← GoalState.createFromMVars goals root
-    return { state, srcBoundaries }
+      let range := stxByteRange tacticInfo.stx
+      return mvarIds.map (·, range)
+    | _ => panic! "Invalid info"
+  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+  let goals := annotatedGoals.map Prod.fst
+  let srcBoundaries := annotatedGoals.map Prod.snd
+  let root := match goals with
+    | [] => panic! "No MVars generated"
+    | [g] => g
+    | _ => { name := .anonymous }
+  let state ← GoalState.createFromMVars goals root
+  return { state, srcBoundaries }
 
 
 @[export pantograph_frontend_collect_new_defined_constants_m]

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

@@ -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,25 +130,24 @@ 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 {
-      state with
-      savedState := {
-        term := state.savedState.term,
-        tactic := { goals := unassigned },
-      },
-    }
+  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+  let unassigned := goals.filter λ goal =>
+    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+    ¬ isSolved
+  return {
+    state with
+    savedState := {
+      term := state.savedState.term,
+      tactic := { goals := unassigned },
+    },
+  }
 /--
 Brings into scope all goals from `branch`
 -/
@@ -159,18 +161,18 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
     target.resume (goals := branch.goals)
 
 @[export pantograph_goal_state_root_expr]
-protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
+protected def GoalState.rootExpr? (goalState : GoalState): Option Expr := do
   if goalState.root.name == .anonymous then
     .none
   let expr ← goalState.mctx.eAssignment.find? goalState.root
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  if expr.hasExprMVar then
-    -- Must not assert that the goal state is empty here. We could be in a branch goal.
-    --assert! ¬goalState.goals.isEmpty
-    .none
-  else
-    assert! goalState.goals.isEmpty
-    return expr
+  return expr
+@[export pantograph_goal_state_is_solved]
+protected def GoalState.isSolved (goalState : GoalState) : Bool :=
+  let solvedRoot := match goalState.rootExpr? with
+    | .some e => ¬ e.hasExprMVar
+    | .none => true
+  goalState.goals.isEmpty && solvedRoot
 @[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
   let parent ← goalState.parentMVar?
@@ -238,23 +240,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 +265,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 +343,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 +380,7 @@ protected def GoalState.convExit (state: GoalState):
       parentMVar? := .some convGoal,
       convMVar? := .none
       calcPrevRhs? := .none
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
@@ -456,7 +458,7 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
       },
       parentMVar? := .some goal,
       calcPrevRhs?
-    }
+    } #[]
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 

Pantograph/Library.lean

@@ -123,8 +123,9 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
 
+  let rootExpr? := state.rootExpr?
   let root? ← if rootExpr then
-      state.rootExpr?.mapM λ expr => state.withRootContext do
+      rootExpr?.mapM λ expr => state.withRootContext do
         serializeExpression options (← instantiateAll expr)
     else
       pure .none
@@ -143,11 +144,15 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
     state.withContext mvarId do
       let .some expr ← getExprMVarAssignment? mvarId | return {}
       serializeExpression options (← instantiateAll expr)
+  let env ← getEnv
   return {
     root?,
     parent?,
     goals,
     extraMVars,
+    rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
+    rootHasUnsafe := rootExpr?.map (env.hasUnsafe ·) |>.getD false,
+    rootHasMVar := rootExpr?.map (·.hasExprMVar) |>.getD false,
   }
 
 @[export pantograph_goal_have_m]

Pantograph/Protocol.lean

@@ -268,14 +268,17 @@ 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.
-  goals?: Option (Array Goal)          := .none
+  -- 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
+
+  hasSorry : Bool := false
+  hasUnsafe : Bool := false
   deriving Lean.ToJson
 structure GoalContinue where
   -- State from which the continuation acquires the context
@@ -319,6 +322,10 @@ structure GoalPrintResult where
   parent?: Option Expression := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
+
+  rootHasSorry : Bool := false
+  rootHasUnsafe : Bool := false
+  rootHasMVar : Bool := true
   deriving Lean.ToJson
 
 -- Diagnostic Options, not available in REPL

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.3.0"
+def version := "0.3.1"
 
 end Pantograph

README.md

@@ -81,7 +81,7 @@ the environment might be setup like this:
 ``` sh
 LIB="../lib"
 LIB_MATHLIB="$LIB/mathlib4/.lake"
-export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
 
 LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
 ```

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,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? |
@@ -334,17 +338,21 @@ def execute (command: Protocol.Command): MainM Json := do
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
+      let parentExpr := nextGoalState.parentExpr?.get!
       let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
+        messages? := .some messages,
+        hasSorry := parentExpr.hasSorry,
+        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
       }
     | .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

@@ -84,12 +84,17 @@ def test_tactic : Test :=
     step "goal.tactic" ({ stateId := 0, tactic? := .some "intro x" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.print" ({ stateId := 1, parentExpr? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
-     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+     ({
+       root? := .some { pp? := "fun x => ?m.11"},
+       parent? := .some { pp? := .some "fun x => ?m.11" },
+     }: Protocol.GoalPrintResult),
     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"] }:
-      Protocol.GoalTacticResult)
+     ({ 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),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
   ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
   simp
@@ -302,6 +307,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 +355,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,20 +79,20 @@ 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 ()
   addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 root)" $ ¬ state1.isSolved
   -- 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 ()
-  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  checkTrue "(1b root)" $ ¬ state2.isSolved
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -100,7 +100,7 @@ def test_m_couple: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 3", .some "3 ≤ 5"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state1b.isSolved
 
 def test_m_couple_simp: TestM Unit := do
   let state? ← startProof "(2: Nat) ≤ 5"
@@ -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,11 +122,11 @@ 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 ()
-  addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
+  checkTrue "(1b root)" $ ¬ state2.isSolved
   let state1b ← match state2.continue state1 with
     | .error msg => do
       addTest $ assertUnreachable $ msg
@@ -134,9 +134,9 @@ def test_m_couple_simp: TestM Unit := do
     | .ok state => pure state
   addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ 2", .some "2 ≤ 5"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state1b.isSolved
   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 ()
@@ -184,27 +184,27 @@ def test_proposition_generation: TestM Unit := do
       ])
   if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
     addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
-  addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 root)" $ ¬ state1.isSolved
 
   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 ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "?m.30 x"])
-  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
+  checkTrue "(2 root)" $ ¬ state2.isSolved
 
   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 ()
   addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[])
 
-  addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
+  checkTrue "(3 root)" state3.isSolved
   return ()
 
 def test_partial_continuation: TestM Unit := do
@@ -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 ()
@@ -238,23 +238,23 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 1)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
   --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
-  let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
+  let coupled_goals := coupled_goals.map (·.name.toString)
+  let coupled_goals := coupled_goals.map ({ name := ·.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
+  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
     #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
-  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
+  checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with

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,27 +187,27 @@ 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
+  checkTrue "(1 root)" state1.rootExpr?.get!.hasExprMVar
   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 ()
   addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
-  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+  checkTrue "(2 root)" state2.rootExpr?.get!.hasExprMVar
   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 ()
   addTest $ LSpec.test tactic state3.goals.isEmpty
-  addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
+  checkTrue "(3 root)" $ ¬ state3.rootExpr?.get!.hasExprMVar
   return ()
 
 -- Two ways to write the same theorem
@@ -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 ()
@@ -257,15 +257,15 @@ def test_or_comm: TestM Unit := do
         { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
-  addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
-  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
+  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  checkTrue "(1 root)" $ ¬ state1.isSolved
 
   let state1parent ← state1.withParentContext do
     serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   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 ()
@@ -276,8 +276,8 @@ def test_or_comm: TestM Unit := do
   let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
     #[caseL, caseR])
-  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
-  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
+  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  checkTrue "(2 root)" $ ¬ state2.isSolved
 
   let state2parent ← state2.withParentContext do
     serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
@@ -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,27 +301,27 @@ 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 ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
   let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
+  checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
   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 ()
   addTest $ LSpec.check "  assumption" state4_2.goals.isEmpty
-  addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
+  checkTrue "(4_2 root)" $ ¬ state4_2.isSolved
   -- Ensure the proof can continue from `state4_2`.
   let state2b ← match state4_2.continue state2 with
     | .error msg => do
@@ -330,18 +330,18 @@ 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 ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
+  checkTrue "(4_1 root)" $ ¬ state4_1.rootExpr?.get!.hasExprMVar
 
   return ()
   where
@@ -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/rationale.md

@@ -47,11 +47,16 @@ include:
 
 - If a tactic loses track of metavariables, it will not be caught until the end
   of the proof search. This is a bug in the tactic itself.
-- Timeouts for executing tactics is not available. Maybe this will change in the
-  future.
+- Although a timeout feature exists in Pantograph, it relies on the coöperative
+  multitasking from the tactic implementation. There is nothing preventing a
+  buggy tactic from stalling Lean if it does not check for cancellation often.
+- For the same reason as above, there is no graceful way to stop a tactic which
+  leaks infinite memory. Users who wish to have this behaviour should run
+  Pantograph in a controlled environment with limited allocations. e.g.
+  Linux control groups.
 - Interceptions of parsing errors generally cannot be turned into goals (e.g.
-  `def mystery : Nat := :=`) due to Lean's parsing system.
-
+  `def mystery : Nat := :=`) due to Lean's parsing system. This question is also
+  not well-defined.
 
 ## References
 

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.