Merge pull request 'test(frontend): Circular sorry' (#244) from frontend/circular into dev

Reviewed-on: #244

Pantograph/Delate.lean

@@ -63,12 +63,16 @@ def exprProjToApp (env : Environment) (e : Expr) : Expr :=
       (List.range numFields)
     mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
 
-def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
+def isAuxLemma (n : Name) : Bool :=
+  match n with
+  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
+  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
+  | _ => false
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
 @[export pantograph_unfold_aux_lemmas_m]
-def unfoldAuxLemmas : Expr → CoreM Expr :=
-  (Meta.deltaExpand · Lean.Name.isAuxLemma)
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
+  Meta.deltaExpand e isAuxLemma
 /-- Unfold all matcher applications -/
 @[export pantograph_unfold_matchers_m]
 def unfoldMatchers (expr : Expr) : CoreM Expr :=
@@ -451,7 +455,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
-
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
       : MetaM Protocol.Goal := do
@@ -517,7 +520,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
     return {
       name := goal.name.toString,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
-      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
@@ -527,17 +529,20 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
 
 protected def GoalState.serializeGoals
       (state: GoalState)
-      (parent: Option GoalState := .none)
       (options: @&Protocol.Options := {}):
     MetaM (Array Protocol.Goal):= do
   state.restoreMetaM
   let goals := state.goals.toArray
-  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
   goals.mapM fun goal => do
+    let fragment := match state.fragments[goal]? with
+      | .none => .tactic
+      | .some $ .calc .. => .calc
+      | .some $ .conv .. => .conv
+      | .some $ .convSentinel .. => .conv
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
-      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
-      pure serializedGoal
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
+      pure { serializedGoal with fragment }
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
@@ -603,7 +608,9 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
     userNameToString : Name → String
       | .anonymous => ""
       | other => s!"[{other}]"
-    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
+    parentHasMVar (mvarId: MVarId): Bool := match parent? with
+      | .some state => state.mctx.decls.contains mvarId
+      | .none => true
 
 initialize
   registerTraceClass `Pantograph.Delate

Pantograph/Environment.lean

@@ -4,6 +4,7 @@ import Pantograph.Protocol
 import Pantograph.Serial
 import Lean.Environment
 import Lean.Replay
+import Lean.Util.Path
 
 open Lean
 open Pantograph
@@ -13,7 +14,7 @@ namespace Pantograph.Environment
 @[export pantograph_is_name_internal]
 def isNameInternal (n: Name): Bool :=
   -- Returns true if the name is an implementation detail which should not be shown to the user.
-  n.isAuxLemma ∨ n.hasMacroScopes
+  isAuxLemma n ∨ n.hasMacroScopes
 
 /-- Catalog all the non-internal and safe names -/
 @[export pantograph_environment_catalog]
@@ -130,17 +131,19 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
       } }
     | _ => pure core
   let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
+      try
+        let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
         let declRange? ← findDeclarationRanges? name
         let sourceStart? := declRange?.map (·.range.pos)
         let sourceEnd? := declRange?.map (·.range.endPos)
         .pure {
           result with
-        sourceUri?,
+          sourceUri? := sourceUri?.map (toString ·),
           sourceStart?,
           sourceEnd?,
         }
+      catch _e =>
+        .pure result
     else
       .pure result
   return result

Pantograph/Frontend/Basic.lean

@@ -6,8 +6,6 @@ open Lean
 namespace Lean.FileMap
 
 /-- Extract the range of a `Syntax` expressed as lines and columns. -/
--- Extracted from the private declaration `Lean.Elab.formatStxRange`,
--- in `Lean.Elab.InfoTree.Main`.
 @[export pantograph_frontend_stx_range]
 protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
   let pos    := stx.getPos?.getD 0
@@ -19,9 +17,10 @@ namespace Lean.PersistentArray
 
 /--
 Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`.
+
+We can't remove the `[Inhabited α]` hypotheses here until
+`PersistentArray`'s `GetElem` instance also does.
 -/
--- We can't remove the `[Inhabited α]` hypotheses here until
--- `PersistentArray`'s `GetElem` instance also does.
 protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :=
   List.range (t.size - n) |>.map fun i => t.get! (n + i)
 
@@ -36,8 +35,11 @@ def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
   let endPos := stx.getTailPos?.getD 0
   (pos, endPos)
 
+structure Context where
+  cancelTk? : Option IO.CancelToken := .none
 
-abbrev FrontendM := Elab.Frontend.FrontendM
+/-- This `FrontendM` comes with more options. -/
+abbrev FrontendM := ReaderT Context Elab.Frontend.FrontendM
 
 structure CompilationStep where
   scope : Elab.Command.Scope
@@ -50,14 +52,44 @@ structure CompilationStep where
   msgs : List Message
   trees : List Elab.InfoTree
 
-namespace CompilationStep
+/-- Like `Elab.Frontend.runCommandElabM`, but taking `cancelTk?` into account. -/
+@[inline] def runCommandElabM (x : Elab.Command.CommandElabM α) : FrontendM α := do
+  let config ← read
+  let ctx ← readThe Elab.Frontend.Context
+  let s ← get
+  let cmdCtx : Elab.Command.Context := {
+    cmdPos       := s.cmdPos
+    fileName     := ctx.inputCtx.fileName
+    fileMap      := ctx.inputCtx.fileMap
+    snap?        := none
+    cancelTk?    := config.cancelTk?
+  }
+  match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
+  | Except.error e      => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
+  | Except.ok (a, sNew) => Elab.Frontend.setCommandState sNew; return a
 
-@[export pantograph_frontend_compilation_step_message_strings_m]
-def messageStrings (step: CompilationStep) : IO (Array String) := do
-  List.toArray <$> step.msgs.mapM (·.toString)
-
-end CompilationStep
+def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
+  runCommandElabM do
+    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+    Elab.Command.elabCommandTopLevel stx
+    let mut msgs := (← get).messages
+    modify ({ · with messages := initMsgs ++ msgs })
 
+open Elab.Frontend in
+def processCommand : FrontendM Bool := do
+  updateCmdPos
+  let cmdState ← getCommandState
+  let ictx ← getInputContext
+  let pstate ← getParserState
+  let scope := cmdState.scopes.head!
+  let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+  match profileit "parsing" scope.opts fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
+  | (cmd, ps, messages) =>
+    modify fun s => { s with commands := s.commands.push cmd }
+    setParserState ps
+    setMessages messages
+    elabCommandAtFrontend cmd
+    pure (Parser.isTerminalCommand cmd)
 
 /--
 Process one command, returning a `CompilationStep` and
@@ -67,17 +99,19 @@ Process one command, returning a `CompilationStep` and
 def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
-  let done ← Elab.Frontend.processCommand
+  let done ← processCommand
   let stx := (← get).commands.back!
-  let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
+  let src := (← readThe Elab.Frontend.Context).inputCtx.input.toSubstring.extract
+    (← get).cmdPos
+    (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env
   let msgs := s'.messages.toList.drop s.messages.toList.length
   let trees := s'.infoState.trees.drop s.infoState.trees.size
-  let ⟨_, fileName, fileMap⟩  := (← read).inputCtx
+  let ⟨_, fileName, fileMap⟩  := (← readThe Elab.Frontend.Context).inputCtx
   return ({ scope := s.scopes.head!, fileName, fileMap, src, stx, before, after, msgs, trees }, done)
 
-partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
+partial def mapCompilationSteps { α } (f: CompilationStep → FrontendM α) : FrontendM (List α) := do
   let (cmd, done) ← processOneCommand
   if done then
     if cmd.src.isEmpty then
@@ -110,10 +144,11 @@ def createContextStateFromFile
   --let file ← IO.FS.readFile (← findSourcePath module)
   let inputCtx := Parser.mkInputContext file fileName
 
+  let (header, parserState, messages) ← Parser.parseHeader inputCtx
   let (env, parserState, messages) ← match env? with
     | .some env => pure (env, {}, .empty)
     | .none =>
-      let (header, parserState, messages) ← Parser.parseHeader inputCtx
+      -- Only process the header if we don't have an environment.
       let (env, messages) ← Elab.processHeader header opts messages inputCtx
       pure (env, parserState, messages)
   let commandState := Elab.Command.mkState env messages opts

Pantograph/Frontend/InfoTree.lean

@@ -10,7 +10,7 @@ namespace Lean.Elab
 private def elaboratorToString : Name → String
   | .anonymous => ""
   | n => s!"⟨{n}⟩ "
-private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
+private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("  " ++ .)
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 protected def Info.stx? : Info → Option Syntax
@@ -131,16 +131,16 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
   | .node info children =>
     if let some ctx := ctx? then
       let node : String ← match info with
-      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
-      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
-      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
+      | .ofTermInfo    info => pure s!"[term] {info.stx}"
+      | .ofCommandInfo info => pure s!"[command] {info.stx}"
+      | .ofTacticInfo  info => pure s!"[tactic] {info.stx}"
       | .ofMacroExpansionInfo _ => pure "[macro_exp]"
-      | .ofOptionInfo _ => pure "[option]"
+      | .ofOptionInfo info => pure s!"[option] {info.stx}"
       | .ofFieldInfo _ => pure "[field]"
-      | .ofCompletionInfo _ => pure "[completion]"
+      | .ofCompletionInfo info => pure s!"[completion] {info.stx}"
       | .ofUserWidgetInfo _ => pure "[user_widget]"
       | .ofCustomInfo _ => pure "[custom]"
-      | .ofFVarAliasInfo _ => pure "[fvar]"
+      | .ofFVarAliasInfo _ => pure "[fvar_alias]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"

Pantograph/Frontend/MetaTranslate.lean

@@ -111,7 +111,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
   let lctx ← MonadLCtx.getLCtx
   assert! lctx.isEmpty
   (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do
+    let localDecl ← Meta.withLCtx' lctx do
       translateLocalDecl srcLocalDecl
     pure $ lctx.addDecl localDecl
   ) lctx
@@ -149,6 +149,7 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
     let type := termInfo.expectedType?.get!
     let lctx' ← translateLCtx
     let mvar ← Meta.withLCtx lctx' #[] do
+      Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
       let type' ← translateExpr type
       trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'

Pantograph/Goal.lean

@@ -6,28 +6,75 @@ All the functions starting with `try` resume their inner monadic state.
 import Pantograph.Tactic
 import Lean
 
-
 namespace Pantograph
 open Lean
 
+/-- The acting area of a tactic -/
+inductive Site where
+  -- Dormant all other goals
+  | focus (goal : MVarId)
+  -- Move the goal to the first in the list
+  | prefer (goal : MVarId)
+  -- Execute as-is, no goals go dormant
+  | unfocus
+  deriving BEq, Inhabited
+
+instance : Coe MVarId Site where
+  coe := .focus
+instance : ToString Site where
+  toString
+    | .focus { name } => s!"[{name}]"
+    | .prefer { name } => s!"[{name},...]"
+    | .unfocus => "[*]"
+
+/-- Executes a `TacticM` on a site and return affected goals -/
+protected def Site.runTacticM (site : Site)
+  { m } [Monad m] [MonadLiftT Elab.Tactic.TacticM m] [MonadControlT Elab.Tactic.TacticM m] [MonadMCtx m] [MonadError m]
+  (f : m α) : m (α × List MVarId) :=
+  match site with
+  | .focus goal => do
+    Elab.Tactic.setGoals [goal]
+    let a ← f
+    return (a, [goal])
+  | .prefer goal => do
+    let before ← Elab.Tactic.getUnsolvedGoals
+    let otherGoals := before.filter (· != goal)
+    Elab.Tactic.setGoals (goal :: otherGoals)
+    let a ← f
+    let after ← Elab.Tactic.getUnsolvedGoals
+    let parents := before.filter (¬ after.contains ·)
+    Elab.Tactic.pruneSolvedGoals
+    return (a, parents)
+  | .unfocus => do
+    let before ← Elab.Tactic.getUnsolvedGoals
+    let a ← f
+    let after ← Elab.Tactic.getUnsolvedGoals
+    let parents := before.filter (¬ after.contains ·)
+    Elab.Tactic.pruneSolvedGoals
+    return (a, parents)
+
 /--
-Represents an interconnected set of metavariables, or a state in proof search
+Kernel view of the state of a proof
  -/
 structure GoalState where
+  -- Captured `TacticM` state
   savedState : Elab.Tactic.SavedState
 
-  -- The root hole which is the search target
+  -- The root goal which is the search target
   root: MVarId
 
-  -- Parent state metavariable source
-  parentMVar?: Option MVarId
+  /--
+  Parent goals which became assigned or fragmented to produce this state.
+  Note that due to the existence of tactic fragments, parent goals do not
+  necessarily have an expression assignment.
+  -/
+  parentMVars : List MVarId := []
 
-  -- Existence of this field shows that we are currently in `conv` mode.
-  -- (convRhs, goal, dormant)
-  convMVar?: Option (MVarId × MVarId × List MVarId) := .none
-  -- Previous RHS for calc, so we don't have to repeat it every time
-  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
-  calcPrevRhs?: Option (MVarId × Expr) := .none
+  -- Any goal associated with a fragment has a partial tactic which has not
+  -- finished executing.
+  fragments : FragmentMap := .empty
+
+def throwNoGoals { m α } [Monad m] [MonadError m] : m α := throwError "no goals to be solved"
 
 @[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@@ -42,7 +89,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
   return {
     root := root.mvarId!,
     savedState,
-    parentMVar? := .none,
   }
 @[export pantograph_goal_state_create_from_mvars_m]
 protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
@@ -51,13 +97,19 @@ protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): Met
   return {
     root,
     savedState,
-    parentMVar? := .none,
   }
-@[export pantograph_goal_state_is_conv]
-protected def GoalState.isConv (state: GoalState): Bool :=
-  state.convMVar?.isSome
+@[always_inline]
 protected def GoalState.goals (state: GoalState): List MVarId :=
   state.savedState.tactic.goals
+@[always_inline]
+protected def GoalState.mainGoal? (state : GoalState) : Option MVarId :=
+  state.goals.head?
+@[always_inline]
+protected def GoalState.actingGoal? (state : GoalState) (site : Site) : Option MVarId := do
+  match site with
+  | .focus goal | .prefer goal => return goal
+  | .unfocus => state.mainGoal?
+
 @[export pantograph_goal_state_goals]
 protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
@@ -69,8 +121,10 @@ protected def GoalState.env (state: GoalState): Environment :=
 protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
   let mvarDecl ← state.mctx.findDecl? mvarId
   return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
+@[always_inline]
 protected def GoalState.metaState (state: GoalState): Meta.State :=
   state.savedState.term.meta.meta
+@[always_inline]
 protected def GoalState.coreState (state: GoalState): Core.SavedState :=
   state.savedState.term.meta.core
 
@@ -78,64 +132,32 @@ protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: Met
   mvarId.withContext m |>.run' (← read) state.metaState
 protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
   Meta.mapMetaM <| state.withContext' mvarId
+/-- Uses context of the first parent -/
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext' state.parentMVars[0]!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
   Meta.mapMetaM <| state.withContext' state.root
 
-private def GoalState.mvars (state: GoalState): SSet MVarId :=
-  state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
+private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
+  let { nextMacroScope, ngen, .. } := state
+  modifyThe Core.State ({ · with nextMacroScope, ngen })
 -- Restore the name generator and macro scopes of the core state
-protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit := do
-  let savedCore := state.coreState
-  modifyGetThe Core.State (fun st => ((),
-    { st with nextMacroScope := savedCore.nextMacroScope, ngen := savedCore.ngen }))
+protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
+  restoreCoreMExtra state.coreState
 protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := do
   state.restoreCoreMExtra
   state.savedState.term.meta.restore
 protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := do
   state.restoreCoreMExtra
   state.savedState.term.restore
-private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
-  state.restoreElabM
-  Elab.Tactic.setGoals [goal]
-
-@[export pantograph_goal_state_focus]
-protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
-  let goal ← state.savedState.tactic.goals[goalId]?
-  return {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := [goal] },
-    },
-    calcPrevRhs? := .none,
-  }
-
-/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[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 =>
-    let isDuplicate := state.goals.contains goal
-    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
-  {
-    state with
-    savedState := {
-      state.savedState with
-      tactic := { goals := state.goals ++ parentGoals },
-    },
-  }
 
 /--
-Brings into scope a list of goals. User must ensure `goals` is distinct.
+Brings into scope a list of goals. User must ensure `goals` are distinct.
 -/
 @[export pantograph_goal_state_resume]
-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)
+protected def GoalState.resume (state : GoalState) (goals : List MVarId) : Except String GoalState := do
+  if ¬ (goals.all (state.mctx.decls.contains ·)) then
+    let invalid_goals := goals.filter (λ goal => ¬ state.mctx.decls.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
   -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
   let unassigned := goals.filter λ goal =>
@@ -152,7 +174,7 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
 Brings into scope all goals from `branch`
 -/
 @[export pantograph_goal_state_continue]
-protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
+protected def GoalState.continue (target : GoalState) (branch : GoalState) : Except String GoalState :=
   if !target.goals.isEmpty then
     .error s!"Target state has unresolved goals"
   else if target.root != branch.root then
@@ -161,7 +183,7 @@ 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
@@ -173,27 +195,227 @@ protected def GoalState.isSolved (goalState : GoalState) : Bool :=
     | .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?
-  let expr := goalState.mctx.eAssignment.find! parent
-  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
-  return expr
 @[export pantograph_goal_state_get_mvar_e_assignment]
 protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
   let expr ← goalState.mctx.eAssignment.find? mvarId
   let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
   return expr
+@[export pantograph_goal_state_parent_exprs]
+protected def GoalState.parentExprs (state : GoalState) : List (Except Fragment Expr) :=
+  state.parentMVars.map λ goal => match state.getMVarEAssignment goal with
+    | .some e => .ok e
+    -- A parent goal which is not assigned must have a fragment
+    | .none => .error state.fragments[goal]!
+@[always_inline]
+protected def GoalState.hasUniqueParent (state : GoalState) : Bool :=
+  state.parentMVars.length == 1
+@[always_inline]
+protected def GoalState.parentExpr! (state : GoalState) : Expr :=
+  assert! state.parentMVars.length == 1
+  (state.getMVarEAssignment state.parentMVars[0]!).get!
+
+deriving instance BEq for DelayedMetavarAssignment
+
+/-- Given states `dst`, `src`, and `src'`, where `dst` and `src'` are
+descendants of `src`, replay the differential `src' - src` in `dst`. Colliding
+metavariable and lemma names will be automatically renamed to ensure there is no
+collision. This implements branch unification. Unification might be impossible
+if conflicting assignments exist. We also assume the monotonicity property: In a
+chain of descending goal states, a mvar cannot be unassigned, and once assigned
+its assignment cannot change. -/
+@[export pantograph_goal_state_replay_m]
+protected def GoalState.replay (dst : GoalState) (src src' : GoalState) : CoreM GoalState :=
+  withTraceNode `Pantograph.GoalState.replay (fun _ => return m!"replay") do
+  let srcNGen := src.coreState.ngen
+  let srcNGen' := src'.coreState.ngen
+  let dstNGen := dst.coreState.ngen
+  assert! srcNGen.namePrefix == srcNGen'.namePrefix
+  assert! srcNGen.namePrefix == dstNGen.namePrefix
+  assert! src.mctx.depth == src'.mctx.depth
+  assert! src.mctx.depth == dst.mctx.depth
+
+  let diffNGenIdx := dst.coreState.ngen.idx - srcNGen.idx
+
+  let env ← dst.coreState.env.replayConsts src.env src'.env (skipExisting := true)
+
+  trace[Pantograph.GoalState.replay] "Merging ngen {srcNGen.idx} -> ({srcNGen'.idx}, {dstNGen.idx})"
+  -- True if the name is generated after `src`
+  let isNewName : Name → Bool
+    | .num pref n =>
+      pref == srcNGen.namePrefix ∧ n ≥ srcNGen.idx
+    | _ => false
+  let mapId : Name → Name
+    | id@(.num pref n) =>
+      if isNewName id then
+        .num pref (n + diffNGenIdx)
+      else
+        id
+    | id => id
+  let mapMVar : MVarId → MVarId
+    | { name } => ⟨mapId name⟩
+  let rec mapLevel : Level → Level
+    | .succ x => .succ (mapLevel x)
+    | .max l1 l2 => .max (mapLevel l1) (mapLevel l2)
+    | .imax l1 l2 => .imax (mapLevel l1) (mapLevel l2)
+    | .mvar { name } => .mvar ⟨mapId name⟩
+    | l => l
+  let mapExpr (e : Expr) : CoreM Expr := Core.transform e λ
+    | .sort level => pure $ .done $ .sort (mapLevel level)
+    | .mvar { name } => pure $ .done $ .mvar ⟨mapId name⟩
+    | _ => pure .continue
+  let mapDelayedAssignment (d : DelayedMetavarAssignment) : CoreM DelayedMetavarAssignment := do
+    let { mvarIdPending, fvars } := d
+    return {
+      mvarIdPending := mapMVar mvarIdPending,
+      fvars := ← fvars.mapM mapExpr,
+    }
+  let mapLocalDecl (ldecl : LocalDecl) : CoreM LocalDecl := do
+    let ldecl := ldecl.setType (← mapExpr ldecl.type)
+    if let .some value := ldecl.value? then
+      return ldecl.setValue (← mapExpr value)
+    else
+      return ldecl
+
+  let { term := savedTerm@{ meta := savedMeta@{ core, meta := meta@{ mctx, .. } }, .. }, .. } := dst.savedState
+  trace[Pantograph.GoalState.replay] "Merging mvars {src.mctx.mvarCounter} -> ({src'.mctx.mvarCounter}, {dst.mctx.mvarCounter})"
+  let mctx := {
+    mctx with
+    mvarCounter := mctx.mvarCounter + (src'.mctx.mvarCounter - src.mctx.mvarCounter),
+    lDepth := src'.mctx.lDepth.foldl (init := mctx.lDepth) λ acc lmvarId@{ name } depth =>
+      if src.mctx.lDepth.contains lmvarId then
+        acc
+      else
+        acc.insert ⟨mapId name⟩ depth
+    decls := ← src'.mctx.decls.foldlM (init := mctx.decls) λ acc _mvarId@{ name } decl => do
+      if decl.index < src.mctx.mvarCounter then
+        return acc
+      let mvarId := ⟨mapId name⟩
+      let decl := {
+        decl with
+        lctx := ← decl.lctx.foldlM (init := .empty) λ acc decl => do
+          let decl ← mapLocalDecl decl
+          return acc.addDecl decl,
+        type := ← mapExpr decl.type,
+      }
+      return acc.insert mvarId decl
+
+    -- Merge mvar assignments
+    userNames := src'.mctx.userNames.foldl (init := mctx.userNames) λ acc userName mvarId =>
+      if acc.contains userName then
+        acc
+      else
+        acc.insert userName mvarId,
+    lAssignment := src'.mctx.lAssignment.foldl (init := mctx.lAssignment) λ acc lmvarId' l =>
+      let lmvarId := ⟨mapId lmvarId'.name⟩
+      if mctx.lAssignment.contains lmvarId then
+        -- Skip the intersecting assignments for now
+        acc
+      else
+        let l := mapLevel l
+        acc.insert lmvarId l,
+    eAssignment := ← src'.mctx.eAssignment.foldlM (init := mctx.eAssignment) λ acc mvarId' e => do
+      let mvarId := ⟨mapId mvarId'.name⟩
+      if mctx.eAssignment.contains mvarId then
+        -- Skip the intersecting assignments for now
+        return acc
+      else
+        let e ← mapExpr e
+        return acc.insert mvarId e,
+    dAssignment := ← src'.mctx.dAssignment.foldlM (init := mctx.dAssignment) λ acc mvarId' d => do
+      let mvarId := ⟨mapId mvarId'.name⟩
+      if mctx.dAssignment.contains mvarId then
+        return acc
+      else
+        let d ← mapDelayedAssignment d
+        return acc.insert mvarId d
+  }
+  let ngen := {
+    core.ngen with
+    idx := core.ngen.idx + (srcNGen'.idx - srcNGen.idx)
+  }
+  -- Merge conflicting lmvar and mvar assignments using `isDefEq`
+
+  let savedMeta := {
+    savedMeta with
+    core := {
+      core with
+      ngen,
+      env,
+      -- Reset the message log when declaration uses `sorry`
+      messages := {}
+    }
+    meta := {
+      meta with
+      mctx,
+    }
+  }
+  let m : MetaM Meta.SavedState := Meta.withMCtx mctx do
+    restoreCoreMExtra savedMeta.core
+    savedMeta.restore
+
+    for (lmvarId, l') in src'.mctx.lAssignment do
+      if isNewName lmvarId.name then
+        continue
+      let .some l ← getLevelMVarAssignment? lmvarId | continue
+      let l' := mapLevel l'
+      trace[Pantograph.GoalState.replay] "Merging level assignments on {lmvarId.name}"
+      unless ← Meta.isLevelDefEq l l' do
+        throwError "Conflicting assignment of level metavariable {lmvarId.name}"
+    for (mvarId, e') in src'.mctx.eAssignment do
+      if isNewName mvarId.name then
+        continue
+      if ← mvarId.isDelayedAssigned then
+        throwError "Conflicting assignment of expr metavariable (e != d) {mvarId.name}"
+      let .some e ← getExprMVarAssignment? mvarId | continue
+      let e' ← mapExpr e'
+      trace[Pantograph.GoalState.replay] "Merging expr assignments on {mvarId.name}"
+      unless ← Meta.isDefEq e e' do
+        throwError "Conflicting assignment of expr metavariable (e != e) {mvarId.name}"
+    for (mvarId, d') in src'.mctx.dAssignment do
+      if isNewName mvarId.name then
+        continue
+      if ← mvarId.isAssigned then
+        throwError "Conflicting assignment of expr metavariable (d != e) {mvarId.name}"
+      let .some d ← getDelayedMVarAssignment? mvarId | continue
+      trace[Pantograph.GoalState.replay] "Merging expr (delayed) assignments on {mvarId.name}"
+      unless d == d' do
+        throwError "Conflicting assignment of expr metavariable (d != d) {mvarId.name}"
+
+    Meta.saveState
+  let goals := dst.savedState.tactic.goals ++
+    src'.savedState.tactic.goals.map (⟨mapId ·.name⟩)
+  let fragments ← src'.fragments.foldM (init := dst.fragments) λ acc mvarId' fragment' => do
+    let mvarId := ⟨mapId mvarId'.name⟩
+    let fragment ← fragment'.map mapExpr
+    if let .some _fragment0 := acc[mvarId]? then
+      throwError "Conflicting fragments on {mvarId.name}"
+    return acc.insert mvarId fragment
+  return {
+    dst with
+    savedState := {
+      tactic := {
+        goals
+      },
+      term := {
+        savedTerm with
+        meta := ← m.run',
+      },
+    },
+    parentMVars := dst.parentMVars ++ src.parentMVars.map mapMVar,
+    fragments,
+  }
 
 --- Tactic execution functions ---
 
--- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
+/--
+These descendants serve as "seed" mvars. If a MVarError's mvar is related to one
+of these seed mvars, it means an error has occurred when a tactic was executing
+on `src`. `evalTactic`, will not capture these mvars, so we need to manually
+find them and save them into the goal list. See the rationales document for the
+inspiration of this function.
+-/
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
-  -- These descendants serve as "seed" mvars. If a MVarError's mvar is related
-  -- to one of these seed mvars, it means an error has occurred when a tactic
-  -- was executing on `src`. `evalTactic`, will not capture these mvars, so we
-  -- need to manually find them and save them into the goal list.
-
+  -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
   let descendants ←  Meta.getMVars (.mvar src)
   --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
@@ -208,6 +430,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
         result := mvarDeps.foldl (·.insert ·) result
   return result.toList
 
+/-- Merger of two unique lists -/
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
   let li2' := li2.filter (¬ li1.contains ·)
   li1 ++ li2'
@@ -217,97 +440,120 @@ Set `guardMVarErrors` to true to capture mvar errors. Lean will not
 automatically collect mvars from text tactics (vide
 `test_tactic_failure_synthesize_placeholder`)
 -/
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
-  : Elab.TermElabM GoalState := do
-  unless (← getMCtx).decls.contains goal do
-    throwError s!"Goal is not in context: {goal.name}"
-  goal.checkNotAssigned `GoalState.step
-  let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+protected def GoalState.step' { α } (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM α) (guardMVarErrors : Bool := false)
+  : Elab.TermElabM (α × GoalState) := do
+  let ((a, parentMVars), { goals }) ← site.runTacticM tacticM
+    |>.run { elaborator := .anonymous }
+    |>.run state.savedState.tactic
   let nextElabState ← MonadBacktrack.saveState
   --Elab.Term.synthesizeSyntheticMVarsNoPostponing
 
   let goals ← if guardMVarErrors then
-      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
+      parentMVars.foldlM (init := goals) λ goals parent => do
+        let errors ← collectAllErroredMVars parent
+        return mergeMVarLists goals errors
     else
       pure goals
-  return {
+  let state' := {
     state with
     savedState := { term := nextElabState, tactic := { goals }, },
-    parentMVar? := .some goal,
-    calcPrevRhs? := .none,
+    parentMVars,
   }
+  return (a, state')
+protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false)
+  : Elab.TermElabM GoalState :=
+  Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors
 
-/-- Response for executing a tactic -/
+/-- Result for executing a tactic, capturing errors in the process -/
 inductive TacticResult where
   -- Goes to next state
-  | success (state : GoalState) (messages : Array String)
+  | success (state : GoalState) (messages : Array Message)
   -- Tactic failed with messages
-  | failure (messages : Array String)
+  | failure (messages : Array Message)
   -- Could not parse tactic
   | parseError (message : String)
   -- The given action cannot be executed in the state
   | invalidAction (message : String)
 
-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Bool × Array String) := do
+private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (List Message) := do
   let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
-  let hasErrors := newMessages.any (·.severity == .error)
-  let newMessages ← newMessages.mapM λ m => m.toString
   Core.resetMessageLog
-  return (hasErrors, newMessages.toArray)
+  return newMessages
+
+/-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
+def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
+  let messageLog ← Core.getMessageLog
+  unless messageLog.toList.isEmpty do
+    IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}"
+    throwError "Message log must be empty at the beginning."
+  try
+    let state ← elabM
+
+    -- Check if error messages have been generated in the core.
+    let newMessages ← dumpMessageLog
+    let hasErrors := newMessages.any (·.severity == .error)
+    if hasErrors then
+      return .failure newMessages.toArray
+    else
+      return .success state newMessages.toArray
+  catch exception =>
+    let messages ← dumpMessageLog
+    let message := {
+      fileName := ← getFileName,
+      pos := ← getRefPosition,
+      data := exception.toMessageData,
+    }
+    return .failure (message :: messages).toArray
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM
-    (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+    (state: GoalState) (site : Site)
+    (tacticM: Elab.Tactic.TacticM Unit)
     (guardMVarErrors : Bool := false)
     : Elab.TermElabM TacticResult := do
-  let prevMessageLength := state.coreState.messages.toList.length
-  try
-    let nextState ← state.step goal tacticM guardMVarErrors
-
-    -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog prevMessageLength
-    if hasError then
-      return .failure newMessages
-    else
-      return .success nextState newMessages
-  catch exception =>
-    match exception with
-    | .internal _ =>
-      let (_, messages) ← dumpMessageLog prevMessageLength
-      return .failure messages
-    | _ => return .failure #[← exception.toMessageData.toString]
+  state.restoreElabM
+  withCapturingError do
+    state.step site tacticM guardMVarErrors
 
 /-- Execute a string tactic on given state. Restores TermElabM -/
 @[export pantograph_goal_state_try_tactic_m]
-protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
+protected def GoalState.tryTactic (state: GoalState) (site : Site) (tactic: String):
     Elab.TermElabM TacticResult := do
   state.restoreElabM
+  let .some goal := state.actingGoal? site | throwNoGoals
+  if let .some fragment := state.fragments[goal]? then
+    return ← withCapturingError do
+      let (fragments, state') ← state.step' site do
+        fragment.step goal tactic $ state.fragments.erase goal
+      return { state' with fragments }
+  -- Normal tactic without fragment
   let tactic ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
-    (catName := if state.isConv then `conv else `tactic)
+    (env := ← getEnv)
+    (catName := `tactic)
     (input := tactic)
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  assert! ¬ (← goal.isAssigned)
-  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
+  let tacticM := Elab.Tactic.evalTactic tactic
+  withCapturingError do
+    state.step site tacticM (guardMVarErrors := true)
 
-protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
-      Elab.TermElabM TacticResult := do
+-- Specialized Tactics
+
+protected def GoalState.tryAssign (state : GoalState) (site : Site) (expr : String)
+    : Elab.TermElabM TacticResult := do
   state.restoreElabM
   let expr ← match Parser.runParserCategory
-    (env := ← MonadEnv.getEnv)
+    (env := ← getEnv)
     (catName := `term)
     (input := expr)
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalAssign expr
+  state.tryTacticM site $ Tactic.evalAssign expr
 
--- Specialized Tactics
-
-protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
-      Elab.TermElabM TacticResult := do
+protected def GoalState.tryLet (state : GoalState) (site : Site) (binderName : String) (type : String)
+    : Elab.TermElabM TacticResult := do
   state.restoreElabM
   let type ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
@@ -316,150 +562,59 @@ protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: St
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.tryTacticM goal $ Tactic.evalLet binderName.toName type
+  state.tryTacticM site $ Tactic.evalLet binderName.toName type
 
 /-- Enter conv tactic mode -/
-protected def GoalState.conv (state: GoalState) (goal: MVarId):
+@[export pantograph_goal_state_conv_enter_m]
+protected def GoalState.convEnter (state : GoalState) (site : Site) :
       Elab.TermElabM TacticResult := do
-  if state.convMVar?.isSome then
+  let .some goal := state.actingGoal? site | throwNoGoals
+  if let .some (.conv ..) := state.fragments[goal]? then
     return .invalidAction "Already in conv state"
-  goal.checkNotAssigned `GoalState.conv
-  let tacticM :  Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
-    state.restoreTacticM goal
-
-    -- See Lean.Elab.Tactic.Conv.convTarget
-    let convMVar ← Elab.Tactic.withMainContext do
-      let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
-      Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
-      pure rhs.mvarId!
-    return (← MonadBacktrack.saveState, convMVar)
-  try
-    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    -- Other goals are now dormant
-    let otherGoals := state.goals.filter $ λ g => g != goal
-    return .success {
-      root := state.root,
-      savedState := nextSavedState
-      parentMVar? := .some goal,
-      convMVar? := .some (convRhs, goal, otherGoals),
-      calcPrevRhs? := .none
-    } #[]
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
-@[export pantograph_goal_state_conv_exit_m]
-protected def GoalState.convExit (state: GoalState):
-      Elab.TermElabM TacticResult := do
-  let (convRhs, convGoal, _) ← match state.convMVar? with
-    | .some mvar => pure mvar
-    | .none => return .invalidAction "Not in conv state"
-  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-    -- Vide `Lean.Elab.Tactic.Conv.convert`
-    state.savedState.restore
-
-    -- Close all existing goals with `refl`
-    for mvarId in (← Elab.Tactic.getGoals) do
-      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
-    Elab.Tactic.pruneSolvedGoals
-    unless (← Elab.Tactic.getGoals).isEmpty do
-      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
-
-    Elab.Tactic.setGoals [convGoal]
-
-    let targetNew ← instantiateMVars (.mvar convRhs)
-    let proof ← instantiateMVars (.mvar convGoal)
-
-    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-    MonadBacktrack.saveState
-  try
-    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    return .success {
-      root := state.root,
-      savedState := nextSavedState
-      parentMVar? := .some convGoal,
-      convMVar? := .none
-      calcPrevRhs? := .none
-    } #[]
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
-  let (mvarId, rhs) ← state.calcPrevRhs?
-  if mvarId == goal then
-    .some rhs
-  else
-    .none
-@[export pantograph_goal_state_try_calc_m]
-protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
-      Elab.TermElabM TacticResult := do
   state.restoreElabM
-  if state.convMVar?.isSome then
-    return .invalidAction "Cannot initiate `calc` while in `conv` state"
-  let `(term|$pred) ← match Parser.runParserCategory
-    (env := state.env)
-    (catName := `term)
-    (input := pred)
-    (fileName := ← getFileName) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  goal.checkNotAssigned `GoalState.tryCalc
-  let calcPrevRhs? := state.calcPrevRhsOf? goal
-  let decl ← goal.getDecl
-  let target ← instantiateMVars decl.type
-  let tag := decl.userName
-  try
-    goal.withContext do
+  withCapturingError do
+    let (fragments, state') ← state.step' site Fragment.enterConv
+    return {
+      state' with
+      fragments := fragments.fold (init := state'.fragments) λ acc goal fragment =>
+        acc.insert goal fragment
+    }
 
-    let mut step ← Elab.Term.elabType <| ← do
-      if let some prevRhs := calcPrevRhs? then
-        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
-      else
-        pure pred
+/-- Exit from a tactic fragment. -/
+@[export pantograph_goal_state_fragment_exit_m]
+protected def GoalState.fragmentExit (state : GoalState) (site : Site):
+      Elab.TermElabM TacticResult := do
+  let .some goal := state.actingGoal? site | throwNoGoals
+  let .some fragment := state.fragments[goal]? |
+    return .invalidAction "Goal does not have a fragment"
+  state.restoreElabM
+  withCapturingError do
+    let (fragments, state') ← state.step' goal (fragment.exit goal state.fragments)
+    return {
+      state' with
+      fragments,
+    }
 
-    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
-      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
-    if let some prevRhs := calcPrevRhs? then
-      unless ← Meta.isDefEqGuarded lhs prevRhs do
-        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
+protected def GoalState.calcPrevRhsOf? (state : GoalState) (goal : MVarId) : Option Expr := do
+  let .some (.calc prevRhs?) := state.fragments[goal]? | .none
+  prevRhs?
 
-    -- Creates a mvar to represent the proof that the calc tactic solves the
-    -- current branch
-    -- In the Lean `calc` tactic this is gobbled up by
-    -- `withCollectingNewGoalsFrom`
-    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
-      (userName := tag ++ `calc)
-    let mvarBranch := proof.mvarId!
+@[export pantograph_goal_state_calc_enter_m]
+protected def GoalState.calcEnter (state : GoalState) (site : Site)
+  : Elab.TermElabM TacticResult := do
+  let .some goal := state.actingGoal? site | throwNoGoals
+  if let .some _ := state.fragments[goal]? then
+    return .invalidAction "Goal already has a fragment"
+  state.restoreElabM
+  withCapturingError do
+    let fragment := Fragment.enterCalc
+    let fragments := state.fragments.insert goal fragment
+    return {
+      state with
+      fragments,
+    }
 
-    let mut proofType ← Meta.inferType proof
-    let mut remainder? := Option.none
-
-    -- The calc tactic either solves the main goal or leaves another relation.
-    -- Replace the main goal, and save the new goal if necessary
-    unless ← Meta.isDefEq proofType target do
-      let rec throwFailed :=
-        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
-      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
-      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
-      let lastStep := mkApp2 r rhs rhs'
-      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
-      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
-      unless ← Meta.isDefEq proofType target do throwFailed
-      remainder? := .some lastStepGoal.mvarId!
-    goal.assign proof
-
-    let goals := [ mvarBranch ] ++ remainder?.toList
-    let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals },
-      },
-      parentMVar? := .some goal,
-      calcPrevRhs?
-    } #[]
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+initialize
+  registerTraceClass `Pantograph.GoalState.replay
 
 end Pantograph

Pantograph/Library.lean

@@ -2,7 +2,6 @@ import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
 import Pantograph.Delate
-import Pantograph.Version
 
 import Lean
 
@@ -69,7 +68,7 @@ def createCoreContext (options: Array String): IO Core.Context := do
 @[export pantograph_create_core_state]
 def createCoreState (imports: Array String): IO Core.State := do
   let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
+    (imports := imports.map (λ str => { module := str.toName }))
     (opts := {})
     (trustLevel := 1)
     (loadExts := true)
@@ -117,10 +116,10 @@ def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState :
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
-  runMetaM <| state.serializeGoals (parent := .none) options
+  runMetaM <| state.serializeGoals options
 
 @[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
+def goalPrint (state: GoalState) (rootExpr: Bool) (parentExprs: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
   : CoreM Protocol.GoalPrintResult := runMetaM do
   state.restoreMetaM
 
@@ -130,9 +129,11 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
         serializeExpression options (← instantiateAll expr)
     else
       pure .none
-  let parent? ← if parentExpr then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
-        serializeExpression options (← instantiateAll expr)
+  let parentExprs? ← if parentExprs then
+      .some <$> state.parentMVars.mapM λ parent => parent.withContext do
+        let val? := state.getMVarEAssignment parent
+        val?.mapM λ val => do
+          serializeExpression options (← instantiateAll val)
     else
       pure .none
   let goals ← if goals then
@@ -148,7 +149,7 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   let env ← getEnv
   return {
     root?,
-    parent?,
+    parentExprs?,
     goals,
     extraMVars,
     rootHasSorry := rootExpr?.map (·.hasSorry) |>.getD false,
@@ -157,26 +158,26 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
   }
 
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (site : Site) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal $ Tactic.evalHave binderName.toName type
+  state.tryTacticM site $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (site : Site) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
+  state.tryTacticM site $ Tactic.evalDefine binderName.toName expr
 @[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (site : Site) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
   state.restoreElabM
-  state.tryTacticM goal (Tactic.evalDraft expr)
+  state.tryTacticM site $ Tactic.evalDraft expr
 
 -- Cancel the token after a timeout.
 @[export pantograph_run_cancel_token_with_timeout_m]
@@ -186,4 +187,9 @@ def runCancelTokenWithTimeout (cancelToken : IO.CancelToken) (timeout : UInt32)
     cancelToken.set
   return ()
 
+def spawnCancelToken (timeout : UInt32) : IO IO.CancelToken := do
+  let token ← IO.CancelToken.new
+  runCancelTokenWithTimeout token timeout
+  return token
+
 end Pantograph

Pantograph/Protocol.lean

@@ -6,6 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
 import Lean.Data.Position
+import Lean.Message
 
 namespace Pantograph.Protocol
 
@@ -60,20 +61,23 @@ structure Variable where
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
+inductive Fragment where
+  | tactic
+  | conv
+  | calc
+  deriving BEq, DecidableEq, Repr, Lean.ToJson
 structure Goal where
-  name: String := ""
   /-- Name of the metavariable -/
-  userName?: Option String  := .none
-  /-- Is the goal in conversion mode -/
-  isConversion: Bool        := false
+  name : String := ""
+  /-- User-facing name -/
+  userName? : Option String  := .none
+  fragment : Fragment := .tactic
   /-- target expression type -/
-  target: Expression
+  target : Expression
   /-- Variables -/
-  vars: Array Variable      := #[]
+  vars : Array Variable      := #[]
   deriving Lean.ToJson
 
-
-
 --- Individual Commands and return types ---
 
 structure Command where
@@ -87,12 +91,10 @@ structure InteractionError where
   deriving Lean.ToJson
 
 def errorIndex (desc: String): InteractionError := { error := "index", desc }
+def errorOperation (desc: String): InteractionError := { error := "operation", desc }
 def errorExpr (desc: String): InteractionError := { error := "expr", desc }
 
 
---- Individual command and return types ---
-
-
 structure Reset where
   deriving Lean.FromJson
 structure Stat where
@@ -248,20 +250,23 @@ structure GoalStartResult where
   root: String
   deriving Lean.ToJson
 structure GoalTactic where
-  -- Identifiers for tree, state, and goal
   stateId: Nat
-  goalId: Nat := 0
+  -- If omitted, act on the first goal
+  goalId?: Option Nat := .none
+  -- If set to true, goal will not go dormant. Defaults to `automaticMode`
+  autoResume?: Option Bool := .none
   -- One of the fields here must be filled
   tactic?: Option String := .none
+  -- Changes the current category to {"tactic", "calc", "conv"}
+  mode?: Option String := .none
+  -- Assigns an expression to the current goal
   expr?: Option String := .none
   have?: Option String := .none
   let?: Option String := .none
-  calc?: Option String := .none
-  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
-  conv?: Option Bool := .none
   draft?: Option String := .none
 
-  -- In case of the `have` tactic, the new free variable name is provided here
+  -- In case of the `have` and `let` tactics, the new free variable name is
+  -- provided here
   binderName?: Option String := .none
 
   deriving Lean.FromJson
@@ -272,7 +277,7 @@ structure GoalTacticResult where
   -- is .none, there has been a tactic error.
   goals?: Option (Array Goal)       := .none
 
-  messages? : Option (Array String) := .some #[]
+  messages? : Option (Array Lean.SerialMessage) := .some #[]
 
   -- Existence of this field shows the tactic parsing has failed
   parseError? : Option String       := .none
@@ -308,8 +313,8 @@ structure GoalPrint where
 
   -- Print root?
   rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
+  -- Print the parent expressions
+  parentExprs?: Option Bool := .some False
   -- Print goals?
   goals?: Option Bool := .some False
   -- Print values of extra mvars?
@@ -319,7 +324,7 @@ structure GoalPrintResult where
   -- The root expression
   root?: Option Expression := .none
   -- The filling expression of the parent goal
-  parent?: Option Expression := .none
+  parentExprs?: Option (List (Option Expression)) := .none
   goals: Array Goal := #[]
   extraMVars: Array Expression := #[]
 
@@ -382,7 +387,7 @@ structure InvokedTactic where
 structure CompilationUnit where
   -- String boundaries of compilation units
   boundary: (Nat × Nat)
-  messages: Array String := #[]
+  messages: Array Lean.SerialMessage := #[]
   -- Number of tactic invocations
   nInvocations?: Option Nat := .none
   goalStateId?: Option Nat := .none

Pantograph/Serial.lean

@@ -1,19 +1,19 @@
-import Lean.Environment
-import Lean.Replay
-import Init.System.IOError
-import Std.Data.HashMap
 import Pantograph.Goal
 
+import Lean.Environment
+import Lean.Replay
+import Std.Data.HashMap
+
+open Lean
+
 /-!
-Input/Output functions
+Input/Output functions borrowed from REPL
 
 # Pickling and unpickling objects
 
 By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
 -/
 
-open Lean
-
 namespace Pantograph
 
 /--
@@ -46,6 +46,21 @@ unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
   region.free
   pure r
 
+abbrev ConstArray := Array (Name × ConstantInfo)
+abbrev DistilledEnvironment := Array Import × ConstArray
+
+/-- Boil an environment down to minimal components -/
+def distillEnvironment (env : Environment) (background? : Option Environment := .none)
+  : DistilledEnvironment :=
+  let filter : Name → Bool := match background? with
+    | .some env => (¬ env.contains ·)
+    | .none => λ _ => true
+  let constants : ConstArray := env.constants.map₂.foldl (init := #[]) λ acc name info =>
+    if filter name then
+      acc.push (name, info)
+    else
+      acc
+  (env.header.imports, constants)
 /--
 Pickle an `Environment` to disk.
 
@@ -56,15 +71,23 @@ and when unpickling, we build a fresh `Environment` from the imports,
 and then add the new constants.
 -/
 @[export pantograph_env_pickle_m]
-def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit :=
-  Pantograph.pickle path (env.header.imports, env.constants.map₂)
+def environmentPickle (env : Environment) (path : System.FilePath) (background? : Option Environment := .none)
+  : IO Unit :=
+  pickle path $ distillEnvironment env background?
+
+deriving instance BEq for Import
 
 def resurrectEnvironment
-  (imports : Array Import)
-  (map₂ : PHashMap Name ConstantInfo)
+  (distilled : DistilledEnvironment)
+  (background? : Option Environment := .none)
   : IO Environment := do
-  let env ← importModules imports {} 0 (loadExts := true)
-  env.replay (Std.HashMap.ofList map₂.toList)
+  let (imports, constArray) := distilled
+  let env ← match background? with
+    | .none => importModules imports {} 0 (loadExts := true)
+    | .some env =>
+      assert! env.imports == imports
+      pure env
+  env.replay (Std.HashMap.ofList constArray.toList)
 /--
 Unpickle an `Environment` from disk.
 
@@ -72,90 +95,103 @@ We construct a fresh `Environment` with the relevant imports,
 and then replace the new constants.
 -/
 @[export pantograph_env_unpickle_m]
-def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
-  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
-  return (← resurrectEnvironment imports map₂, region)
+def environmentUnpickle (path : System.FilePath) (background? : Option Environment := .none)
+  : IO (Environment × CompactedRegion) := unsafe do
+  let (distilled, region) ← unpickle (Array Import × ConstArray) path
+  return (← resurrectEnvironment distilled background?, region)
 
 
-open Lean.Core in
+/-- `CoreM`'s state, with information irrelevant to pickling masked out -/
 structure CompactCoreState where
   -- env             : Environment
   nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1
   ngen            : NameGenerator  := {}
+  auxDeclNGen     : DeclNameGenerator := {}
   -- traceState      : TraceState     := {}
   -- cache           : Cache     := {}
   -- messages        : MessageLog     := {}
   -- infoState       : Elab.InfoState := {}
 
+structure CompactGoalState where
+  env : DistilledEnvironment
+
+  core : CompactCoreState
+  meta : Meta.State
+  «elab»: Elab.Term.State
+  tactic: Elab.Tactic.State
+  root: MVarId
+  parentMVars: List MVarId
+  fragments: FragmentMap
+
+/-- Pickles a goal state by taking its diff relative to a background
+environment. This function eliminates all `MessageData` from synthetic
+metavariables, because these `MessageData` objects frequently carry closures,
+which cannot be pickled. If there is no synthetic metavariable, this would not
+cause a difference. -/
 @[export pantograph_goal_state_pickle_m]
-def goalStatePickle (goalState : GoalState) (path : System.FilePath) : IO Unit :=
+def goalStatePickle (goalState : GoalState) (path : System.FilePath) (background? : Option Environment := .none)
+  : IO Unit :=
   let {
     savedState := {
       term := {
         meta := {
           core := {
-            env, nextMacroScope, ngen, ..
+            env, nextMacroScope, ngen, auxDeclNGen, ..
           },
           meta,
         }
-        «elab»,
+        «elab» := «elab»@{
+          syntheticMVars, ..
+        },
       },
       tactic
     }
     root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
+    parentMVars,
+    fragments,
   } := goalState
-  Pantograph.pickle path (
-    env.constants.map₂,
+  -- Delete `MessageData`s
+  let syntheticMVars : MVarIdMap _ := syntheticMVars.fold (init := .empty) λ acc key val =>
+    let kind := match val.kind with
+      | .typeClass _ => .typeClass .none
+      | .coe header? expectedType e f? _ => .coe header? expectedType e f? .none
+      | k => k
+    acc.insert key { val with kind }
+  pickle path ({
+    env := distillEnvironment env background?,
 
-    ({ nextMacroScope, ngen } : CompactCoreState),
+    core := ({ nextMacroScope, ngen, auxDeclNGen } : CompactCoreState),
     meta,
-    «elab»,
+    «elab» := { «elab» with syntheticMVars },
     tactic,
 
     root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  )
+    parentMVars,
+    fragments,
+  } : CompactGoalState)
 
 @[export pantograph_goal_state_unpickle_m]
-def goalStateUnpickle (path : System.FilePath) (env : Environment)
+def goalStateUnpickle (path : System.FilePath) (background? : Option Environment := .none)
     : IO (GoalState × CompactedRegion) := unsafe do
-  let ((
-    map₂,
+  let ({
+    env,
 
-    compactCore,
+    core,
     meta,
     «elab»,
     tactic,
 
     root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
-  ), region) ← Pantograph.unpickle (
-    PHashMap Name ConstantInfo ×
-
-    CompactCoreState ×
-    Meta.State ×
-    Elab.Term.State ×
-    Elab.Tactic.State ×
-
-    MVarId ×
-    Option MVarId ×
-    Option (MVarId × MVarId × List MVarId) ×
-    Option (MVarId × Expr)
-  ) path
-  let env ← env.replay (Std.HashMap.ofList map₂.toList)
+    parentMVars,
+    fragments,
+  }, region) ← Pantograph.unpickle CompactGoalState path
+  let env ← resurrectEnvironment env background?
   let goalState := {
     savedState := {
       term := {
         meta := {
           core := {
-            compactCore with
+            core with
             passedHeartbeats := 0,
             env,
           },
@@ -166,9 +202,8 @@ def goalStateUnpickle (path : System.FilePath) (env : Environment)
       tactic,
     },
     root,
-    parentMVar?,
-    convMVar?,
-    calcPrevRhs?,
+    parentMVars,
+    fragments,
   }
   return (goalState, region)
 

Pantograph/Tactic.lean

@@ -1,2 +1,3 @@
 import Pantograph.Tactic.Assign
+import Pantograph.Tactic.Fragment
 import Pantograph.Tactic.Prograde

Pantograph/Tactic/Fragment.lean

@@ -0,0 +1,189 @@
+/- Fragmented tactics are the tactics which can give incremental feedback and
+whose integrity as a block is crucial to its operation. e.g. `calc` or `conv`.
+Here, a unified system handles all fragments.
+
+Inside a tactic fragment, the parser category may be different. An incomplete
+fragmented tactic may not be elaboratable..
+
+In line with continuation/resumption paradigms, the exit function of a fragment
+tactic is responsible for resuming incomplete goals with fragments. For example,
+when a conversion tactic finishes, the sentinels should resume the root of the
+conversion tactic goal. The user cannot be expected to execute this resumption,
+since the root is automatically dormanted at the entry of the conversion tactic
+mode.
+-/
+import Lean.Meta
+import Lean.Elab
+
+open Lean
+
+namespace Pantograph
+
+inductive Fragment where
+  | calc (prevRhs? : Option Expr)
+  | conv (rhs : MVarId)
+  -- This goal is spawned from a `conv`
+  | convSentinel (parent : MVarId)
+  deriving BEq, Inhabited
+
+abbrev FragmentMap := Std.HashMap MVarId Fragment
+def FragmentMap.empty : FragmentMap := Std.HashMap.emptyWithCapacity 2
+protected def FragmentMap.filter (map : FragmentMap) (pred : MVarId → Fragment → Bool) : FragmentMap :=
+  map.fold (init := FragmentMap.empty) λ acc mvarId fragment =>
+    if pred mvarId fragment then
+      acc.insert mvarId fragment
+    else
+      acc
+
+protected def Fragment.map (fragment : Fragment) (mapExpr : Expr → CoreM Expr) : CoreM Fragment :=
+  let mapMVar (mvarId : MVarId) : CoreM MVarId :=
+    return (← mapExpr (.mvar mvarId)) |>.mvarId!
+  match fragment with
+  | .calc prevRhs? => return .calc (← prevRhs?.mapM mapExpr)
+  | .conv rhs => do
+    let rhs' ← mapMVar rhs
+    return .conv rhs'
+  | .convSentinel parent => do
+    return .convSentinel (← mapMVar parent)
+
+protected def Fragment.enterCalc : Fragment := .calc .none
+protected def Fragment.enterConv : Elab.Tactic.TacticM FragmentMap := do
+  let goal ← Elab.Tactic.getMainGoal
+  goal.checkNotAssigned `GoalState.conv
+  let (rhs, newGoal) ← goal.withContext do
+    let target ← instantiateMVars (← goal.getType)
+    let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor target
+    pure (rhs.mvarId!, newGoal.mvarId!)
+  Elab.Tactic.replaceMainGoal [newGoal]
+  return FragmentMap.empty
+    |>.insert goal (.conv rhs)
+    |>.insert newGoal (.convSentinel goal)
+
+protected partial def Fragment.exit (fragment : Fragment) (goal : MVarId) (fragments : FragmentMap)
+  : Elab.Tactic.TacticM FragmentMap :=
+  match fragment with
+  | .calc .. => do
+    Elab.Tactic.setGoals [goal]
+    return fragments.erase goal
+  | .conv rhs => do
+    let goals := (← Elab.Tactic.getGoals).filter λ descendant =>
+      match fragments[descendant]? with
+      | .some s => (.convSentinel goal) == s
+      | _ => false -- Not a conv goal from this
+    -- Close all existing goals with `refl`
+    for mvarId in goals do
+      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    unless (← goals.filterM (·.isAssignedOrDelayedAssigned)).isEmpty do
+      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (goals)}"
+
+    -- Ensure the meta tactic runs on `goal` even if its dormant by forcing resumption
+    Elab.Tactic.setGoals $ goal :: (← Elab.Tactic.getGoals)
+    let targetNew ← instantiateMVars (.mvar rhs)
+    let proof ← instantiateMVars (.mvar goal)
+
+    Elab.Tactic.liftMetaTactic1 (·.replaceTargetEq targetNew proof)
+
+    -- Try to solve maiinline by rfl
+    let mvarId ← Elab.Tactic.getMainGoal
+    liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+    Elab.Tactic.pruneSolvedGoals
+    return fragments.filter λ mvarId fragment =>
+      !(mvarId == goal || fragment == .convSentinel goal)
+  | .convSentinel parent =>
+    let parentFragment := fragments[parent]!
+    parentFragment.exit parent (fragments.erase goal)
+
+protected def Fragment.step (fragment : Fragment) (goal : MVarId) (s : String) (map : FragmentMap)
+  : Elab.Tactic.TacticM FragmentMap := goal.withContext do
+  assert! ¬ (← goal.isAssigned)
+  match fragment with
+  | .calc prevRhs? => do
+    let .ok stx := Parser.runParserCategory
+      (env := ← getEnv)
+      (catName := `term)
+      (input := s)
+      (fileName := ← getFileName) | throwError s!"Failed to parse calc element {s}"
+    let `(term|$pred) := stx
+    let decl ← goal.getDecl
+    let target ← instantiateMVars decl.type
+    let tag := decl.userName
+
+    let mut step ← Elab.Term.elabType <| ← do
+      if let some prevRhs := prevRhs? then
+        Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
+      else
+        pure pred
+
+    let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
+      throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
+    if let some prevRhs := prevRhs? then
+      unless ← Meta.isDefEqGuarded lhs prevRhs do
+        throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}"
+
+    -- Creates a mvar to represent the proof that the calc tactic solves the
+    -- current branch
+    -- In the Lean `calc` tactic this is gobbled up by
+    -- `withCollectingNewGoalsFrom`
+    let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
+      (userName := tag ++ `calc)
+    let mvarBranch := proof.mvarId!
+
+    let mut proofType ← Meta.inferType proof
+    let mut remainder? := Option.none
+
+    -- The calc tactic either solves the main goal or leaves another relation.
+    -- Replace the main goal, and save the new goal if necessary
+    unless ← Meta.isDefEq proofType target do
+      let rec throwFailed :=
+        throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
+      let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
+      let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
+      let lastStep := mkApp2 r rhs rhs'
+      let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
+      (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
+      unless ← Meta.isDefEq proofType target do throwFailed
+      remainder? := .some lastStepGoal.mvarId!
+    goal.assign proof
+    let map := map.erase goal
+
+    let goals := [ mvarBranch ] ++ remainder?.toList
+    Elab.Tactic.setGoals goals
+    match remainder? with
+    | .some goal => return map.insert goal $ .calc (.some rhs)
+    | .none => return map
+  | .conv .. => do
+    throwError "Direct operation on conversion tactic parent goal is not allowed"
+  | fragment@(.convSentinel parent) => do
+    assert! isLHSGoal? (← goal.getType) |>.isSome
+    let tactic ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `conv)
+      (input := s)
+      (fileName := ← getFileName) with
+      | .ok stx => pure $ stx
+      | .error error => throwError error
+    let oldGoals ← Elab.Tactic.getGoals
+    -- Label newly generated goals as conv sentinels
+    Elab.Tactic.evalTactic tactic
+    let newConvGoals ← (← Elab.Tactic.getUnsolvedGoals).filterM λ g => do
+      -- conv tactic might generate non-conv goals
+      if oldGoals.contains g then
+        return false
+      return isLHSGoal? (← g.getType) |>.isSome
+    -- Conclude the conv by exiting the parent fragment if new goals is empty
+    if newConvGoals.isEmpty then
+      let hasSiblingFragment := map.fold (init := false) λ flag _ fragment =>
+        if flag then
+          true
+        else match fragment with
+          | .convSentinel parent' => parent == parent'
+          | _ => false
+      if ¬ hasSiblingFragment then
+        -- This fragment must exist since we have conv goals
+        let parentFragment := map[parent]!
+        -- All descendants exhausted. Exit from the parent conv.
+        return ← parentFragment.exit parent map
+    return newConvGoals.foldl (init := map) λ acc g =>
+      acc.insert g fragment
+
+end Pantograph

Pantograph/Version.lean

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

README.md

@@ -17,101 +17,33 @@ nix build .#{sharedLib,executable}
 ```
 to build either the shared library or executable.
 
-Install `lake` and `lean` fixed to the version of the `lean-toolchain` file, and
-run
+For non-Nix users, install `lake` and `lean` fixed to the version of the
+`lean-toolchain` file, and run
 
 ``` sh
 lake build
 ```
-This builds the executable in `.lake/build/bin/pantograph-repl`.
+This builds the executable in `.lake/build/bin/repl`.
 
-## Executable Usage
+### Executable Usage
 
-``` sh
-pantograph-repl MODULES|LEAN_OPTIONS
-```
+The default build target is a Read-Eval-Print-Loop (REPL). See [REPL
+Documentation](./doc/repl.md)
 
-The `pantograph-repl` executable must be run with a list of modules to import.
-It can also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
+Another executable is the `tomograph`, which processes a Lean file and displays
+syntax or elaboration level data.
 
-The REPL loop accepts commands as single-line JSON inputs and outputs either an
-`Error:` (indicating malformed command) or a JSON return value indicating the
-result of a command execution.  The command can be passed in one of two formats
-```
-command { ... }
-{ "cmd": command, "payload": ... }
-```
-The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
-empty command aborts the REPL.
-
-
-Example: (~5k symbols)
-```
-$ pantograph Init
-env.catalog
-env.inspect {"name": "Nat.le_add_left"}
-```
-Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
-```
-$ pantograph Mathlib.Analysis.Seminorm
-env.catalog
-```
-Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
-```
-$ pantograph Init
-goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
-goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
-goal.delete {"stateIds": [0]}
-stat {}
-goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
-stat
-```
-where the application of `assumption` should lead to a failure.
-
-For a list of commands, see [REPL Documentation](doc/repl.md).
-
-### Project Environment
-
-To use Pantograph in a project environment, setup the `LEAN_PATH` environment
-variable so it contains the library path of lean libraries. The libraries must
-be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
-the environment might be setup like this:
-
-``` sh
-LIB="../lib"
-LIB_MATHLIB="$LIB/mathlib4/.lake"
-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 $@
-```
-The `$LEAN_PATH` executable of any project can be extracted by
-``` sh
-lake env printenv LEAN_PATH
-```
-
-### Troubleshooting
-
-If lean encounters stack overflow problems when printing catalog, execute this before running lean:
-```sh
-ulimit -s unlimited
-```
-
-## Library Usage
+### Library Usage
 
 `Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
-with `Pantograph` which mirrors the REPL commands above. It is recommended to
-call Pantograph via this FFI since it provides a tremendous speed up.
-
-The executable can be used as-is, but linking against the shared library
-requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
-between executable (REPL) commands and library functions.
+with `Pantograph` which mirrors the REPL commands above. Note that there isn't a
+1-1 correspondence between executable (REPL) commands and library functions.
 
 Inject any project path via the `pantograph_init_search` function.
 
-## Developing
+## Development
 
-A Lean development shell is provided in the Nix flake.
+A Lean development shell is provided in the Nix flake. Nix usage is optional.
 
 ### Testing
 

Repl.lean

@@ -97,6 +97,84 @@ def liftTermElabM { α } (termElabM : Elab.TermElabM α) (levelNames : List Name
   }
   runCoreM $ termElabM.run' context state |>.run'
 
+section Goal
+
+def goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
+  let state ← getMainState
+  let .some goalState := state.goalStates[args.stateId]? |
+    Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
+  let unshielded := args.autoResume?.getD state.options.automaticMode
+  let site ← match args.goalId?, unshielded with
+    | .some goalId, true => do
+      let .some goal := goalState.goals[goalId]? |
+        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
+      pure (.prefer goal)
+    | .some goalId, false => do
+      let .some goal := goalState.goals[goalId]? |
+        Protocol.throw $ Protocol.errorIndex s!"Invalid goal index {goalId}"
+      pure (.focus goal)
+    | .none, true => pure .unfocus
+    | .none, false => do
+      let .some goal := goalState.mainGoal? |
+        Protocol.throw $ Protocol.errorIndex s!"No goals to be solved"
+      pure (.focus goal)
+  let nextGoalState?: Except _ TacticResult ← liftTermElabM do
+    -- NOTE: Should probably use a macro to handle this...
+    match args.tactic?, args.mode?, args.expr?, args.have?, args.let?, args.draft?  with
+    | .some tactic, .none, .none, .none, .none, .none => do
+      pure $ Except.ok $ ← goalState.tryTactic site tactic
+    | .none, .some mode, .none, .none, .none, .none => match mode with
+      | "tactic" => do -- Exit from the current fragment
+        pure $ Except.ok $ ← goalState.fragmentExit site
+      | "conv" => do
+        pure $ Except.ok $ ← goalState.convEnter site
+      | "calc" => do
+        pure $ Except.ok $ ← goalState.calcEnter site
+      | _ => pure $ .error $ Protocol.errorOperation s!"Invalid mode {mode}"
+    | .none, .none, .some expr, .none, .none, .none => do
+      pure $ Except.ok $ ← goalState.tryAssign site expr
+    | .none, .none, .none, .some type, .none, .none => do
+      let binderName := args.binderName?.getD ""
+      pure $ Except.ok $ ← goalState.tryHave site binderName type
+    | .none, .none, .none, .none, .some type, .none => do
+      let binderName := args.binderName?.getD ""
+      pure $ Except.ok $ ← goalState.tryLet site binderName type
+    | .none, .none, .none, .none, .none, .some draft => do
+      pure $ Except.ok $ ← goalState.tryDraft site draft
+    | _, _, _, _, _, _ =>
+      pure $ .error $ Protocol.errorOperation
+        "Exactly one of {tactic, mode, expr, have, let, draft} must be supplied"
+  match nextGoalState? with
+  | .error error => Protocol.throw error
+  | .ok (.success nextGoalState messages) => do
+    let env ← getEnv
+    let nextStateId ← newGoalState nextGoalState
+    let parentExprs := nextGoalState.parentExprs
+    let hasSorry := parentExprs.any λ
+      | .ok e => e.hasSorry
+      | .error _ => false
+    let hasUnsafe := parentExprs.any λ
+      | .ok e => env.hasUnsafe e
+      | .error _ => false
+    let goals ← runCoreM $ nextGoalState.serializeGoals (options := state.options) |>.run'
+    let messages ← messages.mapM (·.serialize)
+    return {
+      nextStateId? := .some nextStateId,
+      goals? := .some goals,
+      messages? := .some messages,
+      hasSorry,
+      hasUnsafe,
+    }
+  | .ok (.parseError message) =>
+    return { messages? := .none, parseError? := .some message }
+  | .ok (.invalidAction message) =>
+    Protocol.throw $ errorI "invalid" message
+  | .ok (.failure messages) =>
+    let messages ← messages.mapM (·.serialize)
+    return { messages? := .some messages }
+
+end Goal
+
 section Frontend
 
 structure CompilationUnit where
@@ -105,7 +183,7 @@ structure CompilationUnit where
   boundary : Nat × Nat
   invocations : List Protocol.InvokedTactic
   sorrys : List Frontend.InfoWithContext
-  messages : Array String
+  messages : Array SerialMessage
   newConstants : List Name
 
 def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendProcessResult := do
@@ -122,7 +200,7 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
     else do
       .some <$> getEnv
   let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
-  let frontendM: Elab.Frontend.FrontendM (List CompilationUnit) :=
+  let frontendM: Frontend.FrontendM (List CompilationUnit) :=
     Frontend.mapCompilationSteps λ step => do
     let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
     let invocations: Option (List Protocol.InvokedTactic) ← if args.invocations?.isSome then
@@ -133,7 +211,7 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
         Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
       else
         pure []
-    let messages ← step.messageStrings
+    let messages ← step.msgs.toArray.mapM (·.serialize)
     let newConstants ← if args.newConstants then
         Frontend.collectNewDefinedConstants step
       else
@@ -146,7 +224,10 @@ def frontend_process (args: Protocol.FrontendProcess): EMainM Protocol.FrontendP
       messages,
       newConstants
     }
-  let (li, state') ← frontendM.run context |>.run state
+  let cancelTk? ← match (← get).options.timeout with
+    | 0 => pure .none
+    | timeout => .some <$> spawnCancelToken (timeout := .ofBitVec timeout)
+  let (li, state') ← frontendM.run { cancelTk? } |>.run context |>.run state
   if args.inheritEnv then
     setEnv state'.commandState.env
     if let .some scope := state'.commandState.scopes.head? then
@@ -191,7 +272,10 @@ def execute (command: Protocol.Command): MainM Json := do
     try
       match fromJson? command.payload with
       | .ok args => do
-        match (← comm args |>.run) with
+        let (msg, result) ← IO.FS.withIsolatedStreams (isolateStderr := false) $ comm args
+        if !msg.isEmpty then
+          IO.eprint s!"stdout: {msg}"
+        match result with
         | .ok result =>  return toJson result
         | .error ierror => return toJson ierror
       | .error error => return toJson $ errorCommand s!"Unable to parse json: {error}"
@@ -225,7 +309,6 @@ def execute (command: Protocol.Command): MainM Json := do
     return toJson error
   where
   errorCommand := errorI "command"
-  errorIndex := errorI "index"
   errorIO := errorI "io"
   -- Command Functions
   reset (_: Protocol.Reset): EMainM Protocol.StatResult := do
@@ -290,7 +373,7 @@ def execute (command: Protocol.Command): MainM Json := do
       | .some expr, .none => goalStartExpr expr |>.run
       | .none, .some copyFrom => do
         (match (← getEnv).find? <| copyFrom.toName with
-        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
+        | .none => return .error <| Protocol.errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
         return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
@@ -299,74 +382,14 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok goalState =>
       let stateId ← newGoalState goalState
       return { stateId, root := goalState.root.name.toString }
-  goal_tactic (args: Protocol.GoalTactic): EMainM Protocol.GoalTacticResult := do
-    let state ← getMainState
-    let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
-    let .some goal := goalState.goals[args.goalId]? |
-      Protocol.throw $ errorIndex s!"Invalid goal index {args.goalId}"
-    let nextGoalState?: Except _ TacticResult ← liftTermElabM do
-      -- NOTE: Should probably use a macro to handle this...
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?, args.draft?  with
-      | .some tactic, .none, .none, .none, .none, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
-        let binderName := args.binderName?.getD ""
-        pure <| Except.ok <| ← goalState.tryHave goal binderName type
-      | .none, .none, .none, .some type, .none, .none, .none => do
-        let binderName := args.binderName?.getD ""
-        pure <| Except.ok <| ← goalState.tryLet goal binderName type
-      | .none, .none, .none, .none, .some pred, .none, .none => do
-        pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
-        pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
-        pure <| Except.ok <| ← goalState.convExit
-      | .none, .none, .none, .none, .none, .none, .some draft => do
-        pure <| Except.ok <| ← goalState.tryDraft goal draft
-      | _, _, _, _, _, _, _ =>
-        let error := errorI "arguments" "Exactly one of {tactic, expr, have, let, calc, conv, draft} must be supplied"
-        pure $ .error error
-    match nextGoalState? with
-    | .error error => Protocol.throw error
-    | .ok (.success nextGoalState messages) => do
-      let nextGoalState ← match state.options.automaticMode, args.conv? with
-        | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
-        | true, .some true => pure nextGoalState
-        | true, .some false => do
-          let .some (_, _, dormantGoals) := goalState.convMVar? |
-            Protocol.throw $ errorIO "If conv exit succeeded this should not fail"
-          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
-            Protocol.throw $ errorIO "Resuming known goals"
-          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 { messages? := .none, parseError? := .some message }
-    | .ok (.invalidAction message) =>
-      Protocol.throw $ errorI "invalid" message
-    | .ok (.failure messages) =>
-      return { messages? := .some messages }
   goal_continue (args: Protocol.GoalContinue): EMainM Protocol.GoalContinueResult := do
     let state ← getMainState
     let .some target := state.goalStates[args.target]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.target}"
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.target}"
     let nextGoalState? : GoalState  ← match args.branch?, args.goals? with
       | .some branchId, .none => do
         match state.goalStates[branchId]? with
-        | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
+        | .none => Protocol.throw $ Protocol.errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
         let goals := goals.toList.map (λ n => { name := n.toName })
@@ -389,11 +412,11 @@ def execute (command: Protocol.Command): MainM Json := do
   goal_print (args: Protocol.GoalPrint): EMainM Protocol.GoalPrintResult := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.stateId]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.stateId}"
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.stateId}"
     let result ← liftMetaM <| goalPrint
         goalState
         (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
+        (parentExprs := args.parentExprs?.getD False)
         (goals := args.goals?.getD False)
         (extraMVars := args.extraMVars?.getD #[])
         (options := state.options)
@@ -401,11 +424,11 @@ def execute (command: Protocol.Command): MainM Json := do
   goal_save (args: Protocol.GoalSave): EMainM Protocol.GoalSaveResult := do
     let state ← getMainState
     let .some goalState := state.goalStates[args.id]? |
-      Protocol.throw $ errorIndex s!"Invalid state index {args.id}"
-    goalStatePickle goalState args.path
+      Protocol.throw $ Protocol.errorIndex s!"Invalid state index {args.id}"
+    goalStatePickle goalState args.path (background? := .some $ ← getEnv)
     return {}
   goal_load (args: Protocol.GoalLoad): EMainM Protocol.GoalLoadResult := do
-    let (goalState, _) ← goalStateUnpickle args.path (← MonadEnv.getEnv)
+    let (goalState, _) ← goalStateUnpickle args.path (background? := .some $ ← getEnv)
     let id ← newGoalState goalState
     return { id }
 

Test/Common.lean

@@ -69,12 +69,13 @@ end Condensed
 
 def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals[i]!
 def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.get! goalId) tactic
+def GoalState.tacticOn' (state: GoalState) (goalId: Nat) (tactic: TSyntax `tactic) :=
+  state.tryTacticM (state.get! goalId) (Elab.Tactic.evalTactic tactic) true
 
 def TacticResult.toString : TacticResult → String
   | .success state _messages => s!".success ({state.goals.length} goals)"
   | .failure messages =>
-    let messages := "\n".intercalate messages.toList
-    s!".failure {messages}"
+    s!".failure ({messages.size} messages)"
   | .parseError error => s!".parseError {error}"
   | .invalidAction error => s!".invalidAction {error}"
 
@@ -94,12 +95,14 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
   | .ok a            => return a
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
   runCoreMSeq env metaM.run'
-def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
+def runTermElabMInMeta { α } (termElabM: Elab.TermElabM α): MetaM α :=
   termElabM.run' (ctx := defaultElabContext)
+def runTermElabMInCore { α } (termElabM: Elab.TermElabM α): CoreM α :=
+  (runTermElabMInMeta termElabM).run'
 def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
   runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
 
-def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
+def exprToStr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
 
 def strToTermSyntax (s: String): CoreM Syntax := do
   let .ok stx := Parser.runParserCategory
@@ -157,6 +160,13 @@ end Monadic
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
   IO LSpec.TestSeq :=
   runTermElabMSeq env $ runTest t
+def transformTestT { α } { μ μ' : Type → Type }
+    [Monad μ] [Monad μ'] [MonadLiftT (ST IO.RealWorld) μ] [MonadLiftT (ST IO.RealWorld) μ']
+    (tr : {β : Type} → μ β  → μ' β) (m : TestT μ α) : TestT μ' α := do
+  let tests ← get
+  let (a, tests) ← tr (β := α × LSpec.TestSeq) (m.run tests)
+  set tests
+  return a
 
 def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
   { userName, type }
@@ -172,6 +182,29 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
     })).toArray
   }
 
+namespace Tactic
+
+/-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
+exercises the aux lemma generator. -/
+def assignWithAuxLemma (type : Expr) (value? : Option Expr := .none) : Elab.Tactic.TacticM Unit := do
+  let type ← instantiateMVars type
+  let value ← match value? with
+    | .some value => instantiateMVars value
+    | .none => Meta.mkSorry type (synthetic := false)
+  if type.hasExprMVar then
+    throwError "Type has expression mvar"
+  if value.hasExprMVar then
+    throwError "value has expression mvar"
+  let goal ← Elab.Tactic.getMainGoal
+  goal.withContext do
+  let name ← Meta.mkAuxLemma [] type value
+  unless ← Meta.isDefEq type (← goal.getType) do
+    throwError "Type provided is incorrect"
+  goal.assign (.const name [])
+  Elab.Tactic.pruneSolvedGoals
+
+end Tactic
+
 end Test
 
 end Pantograph

Test/Delate.lean

@@ -48,10 +48,9 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
 def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
   let entries: List (String × (List Name) × String) := [
     ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
-    ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
     ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
     ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
-    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
+    ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"),
   ]
   entries.foldlM (λ suites (source, levels, target) =>
     let termElabM := do

Test/Environment.lean

@@ -30,7 +30,6 @@ def test_symbol_visibility: IO LSpec.TestSeq := do
   let entries: List (Name × Bool) := [
     ("Nat.add_comm".toName, false),
     ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
-    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
   ]
   let suite := entries.foldl (λ suites (symbol, target) =>
     let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
@@ -96,10 +95,10 @@ def test_symbol_location (env : Environment) : TestT IO Unit := do
 
     -- Extraction of source doesn't work for symbols in `Init` for some reason
     checkTrue "file" result.sourceUri?.isNone
-    checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0
-    checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88
+    checkEq "sourceStart" (result.sourceStart?.map (·.column)) <| .some 0
+    checkEq "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88
     let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩
-    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
+    checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero", "Init.Grind.Tactics"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 
 def test_matcher (env : Environment) : TestT IO Unit := do

Test/Frontend.lean

@@ -7,11 +7,16 @@ import LSpec
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def runFrontend { α } (source: String) (f : Frontend.CompilationStep → IO α) : MetaM (List α) := do
+open Frontend
+
+def runFrontend { α } (source: String) (f : CompilationStep → FrontendM α) (timeout : UInt32 := 0): MetaM (List α) := do
   let filename := "<anonymous>"
-  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
-  let m := Frontend.mapCompilationSteps f
-  m.run context |>.run' state
+  let (context, state) ← do createContextStateFromFile source filename (← getEnv) {}
+  let m := mapCompilationSteps f
+  let cancelTk? ← match timeout with
+    | 0 => pure .none
+    | timeout => .some <$> spawnCancelToken timeout
+  m.run { cancelTk? } |>.run context |>.run' state
 
 def test_open : TestT MetaM Unit := do
   let sketch := "
@@ -29,7 +34,7 @@ def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionO
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
     return (step.before, ← Frontend.collectSorrys step options)
-  let li ← m.run context |>.run' state
+  let li ← m.run {} |>.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
       return .none
@@ -177,6 +182,43 @@ example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
     }
   ])
 
+def test_sorry_with_local_instance : TestT MetaM Unit := do
+  let sketch := "
+def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s
+example (α : Type) [Inhabited α] : α := sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  let result ← runTermElabMInMeta $ goalState.tryTactic .unfocus "exact test α"
+  checkTrue "success" $ result matches .success ..
+  match result with
+  | .success .. => return ()
+  | .failure messages =>
+    let messages ← messages.mapM (·.toString)
+    fail s!"Could not execute tactic {messages}"
+  | .parseError e =>
+    fail s!"Parse error: {e}"
+  | .invalidAction e =>
+    fail s!"Invalid action: {e}"
+
+def test_sorry_circular : TestT MetaM Unit := do
+  let sketch := "
+theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by sorry
+  "
+  let goalStates ← (collectSorrysFromSource sketch).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  let result ← runTermElabMInMeta $ goalState.tryTactic .unfocus "exact test α"
+  checkTrue "failure" $ result matches .failure ..
+  match result with
+  | .success .. =>
+    fail s!"This should not succeed"
+  | .failure .. =>
+    return ()
+  | .parseError e =>
+    fail s!"Parse error: {e}"
+  | .invalidAction e =>
+    fail s!"Invalid action: {e}"
+
 def test_environment_capture: TestT MetaM Unit := do
   let sketch := "
 def mystery (n: Nat) := n + 1
@@ -227,7 +269,7 @@ def collectNewConstants (source: String) : MetaM (List (List Name)) := do
   let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
   let m := Frontend.mapCompilationSteps λ step => do
     Frontend.collectNewDefinedConstants step
-  m.run context |>.run' state
+  m.run {} |>.run context |>.run' state
 
 def test_collect_one_constant : TestT MetaM Unit := do
   let input := "
@@ -252,9 +294,11 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("open", test_open),
     ("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
-    ("sorry_in_middle", test_sorry_in_middle),
-    ("sorry_in_induction", test_sorry_in_induction),
-    ("sorry_in_coupled", test_sorry_in_coupled),
+    ("sorry in middle", test_sorry_in_middle),
+    ("sorry in induction", test_sorry_in_induction),
+    ("sorry in coupled", test_sorry_in_coupled),
+    ("sorry with local instances", test_sorry_with_local_instance),
+    ("sorry circular", test_sorry_circular),
     ("environment_capture", test_environment_capture),
     ("capture_type_mismatch", test_capture_type_mismatch),
     --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),

Test/Integration.lean

@@ -23,6 +23,9 @@ deriving instance Lean.ToJson for Protocol.FrontendData
 abbrev TestM α := TestT MainM α
 abbrev Test := TestM Unit
 
+def getFileName : TestM String := do
+  return (← read).coreContext.fileName
+
 def step { α β } [Lean.ToJson α] [Lean.ToJson β] (cmd: String) (payload: α)
     (expected: β) (name? : Option String := .none) : TestM Unit := do
   let payload := Lean.toJson payload
@@ -88,23 +91,29 @@ def test_tactic : Test := do
    ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult)
   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)
+  step "goal.print" ({ stateId := 1, parentExprs? := .some true, rootExpr? := .some true }: Protocol.GoalPrint)
    ({
      root? := .some { pp? := "fun x => ?m.11"},
-     parent? := .some { pp? := .some "fun x => ?m.11" },
+     parentExprs? := .some [.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)
-   ({ 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)
+    ({
+      messages? := .some #[{
+        fileName := ← getFileName,
+        kind := .anonymous,
+        pos := ⟨0, 0⟩,
+        data := "tactic 'apply' failed, could not unify the conclusion of `@Nat.le_of_succ_le`\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith the goal\n  ∀ (q : Prop), x ∨ q → q ∨ x\n\nNote: The full type of `@Nat.le_of_succ_le` is\n  ∀ {n m : Nat}, n.succ ≤ m → n ≤ m\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
 def test_tactic_timeout : Test := do
   step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.370" }: Protocol.GoalStartResult)
   -- timeout of 10 milliseconds
   step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet)
    ({ }: Protocol.OptionsSetResult)
@@ -164,6 +173,48 @@ def test_automatic_mode (automatic: Bool): Test := do
   step "goal.tactic" ({ stateId := 2, tactic? := .some "apply Or.inr" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult)
 
+def test_conv_calc : Test := do
+  step "options.set" ({automaticMode? := .some false}: Protocol.OptionsSet)
+   ({}: Protocol.OptionsSetResult)
+  step "goal.start" ({ expr := "∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b"} : Protocol.GoalStart)
+   ({ stateId := 0, root := "_uniq.171" }: Protocol.GoalStartResult)
+  let vars := #[
+    { name := "_uniq.172", userName := "a", type? := .some { pp? := .some "Nat" }},
+    { name := "_uniq.175", userName := "b", type? := .some { pp? := .some "Nat" }},
+    { name := "_uniq.178", userName := "h", type? := .some { pp? := .some "b = 2" }},
+  ]
+  let goal : Protocol.Goal := {
+    vars,
+    name := "_uniq.179",
+    target := { pp? := "1 + a + 1 = a + b" },
+  }
+  step "goal.tactic" ({ stateId := 0, tactic? := .some "intro a b h" }: Protocol.GoalTactic)
+   ({ nextStateId? := .some 1, goals? := #[goal], }: Protocol.GoalTacticResult)
+  step "goal.tactic" ({ stateId := 1, mode? := .some "calc" }: Protocol.GoalTactic)
+   ({ nextStateId? := .some 2, goals? := #[{ goal with fragment := .calc }], }: Protocol.GoalTacticResult)
+  let goalCalc : Protocol.Goal := {
+    vars,
+    name := "_uniq.381",
+    userName? := .some "calc",
+    target := { pp? := "1 + a + 1 = a + 1 + 1" },
+  }
+  let goalMain : Protocol.Goal := {
+    vars,
+    name := "_uniq.400",
+    fragment := .calc,
+    target := { pp? := "a + 1 + 1 = a + b" },
+  }
+  step "goal.tactic" ({ stateId := 2, tactic? := .some "1 + a + 1 = a + 1 + 1" }: Protocol.GoalTactic)
+   ({ nextStateId? := .some 3, goals? := #[goalCalc, goalMain], }: Protocol.GoalTacticResult)
+  let goalConv : Protocol.Goal := {
+    goalCalc with
+    fragment := .conv,
+    userName? := .none,
+    name := "_uniq.468",
+  }
+  step "goal.tactic" ({ stateId := 3, mode? := .some "conv" }: Protocol.GoalTactic)
+   ({ nextStateId? := .some 4, goals? := #[goalConv], }: Protocol.GoalTacticResult)
+
 def test_env_add_inspect : Test := do
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
@@ -270,16 +321,23 @@ def test_frontend_process_sorry : Test := do
        goalStateId? := .some 0,
        goals? := .some #[goal1],
        goalSrcBoundaries? := .some #[(57, 62)],
-       messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
+       messages := #[{
+         fileName := "<anonymous>",
+         kind := `hasSorry,
+         pos := ⟨2, 0⟩,
+         endPos := .some ⟨2, 7⟩,
+         severity := .warning,
+         data := "declaration uses 'sorry'",
+       }],
      }],
    }: Protocol.FrontendProcessResult)
 
 def test_import_open : Test := do
   let header := "import Init\nopen Nat\nuniverse u"
   let goal1: Protocol.Goal := {
-    name := "_uniq.67",
+    name := "_uniq.81",
     target := { pp? := .some "n + 1 = n.succ" },
-    vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}],
+    vars := #[{ name := "_uniq.80", userName := "n", type? := .some { pp? := .some "Nat" }}],
   }
   step "frontend.process"
     ({
@@ -294,7 +352,7 @@ def test_import_open : Test := do
      ],
    }: Protocol.FrontendProcessResult)
   step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
-   ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult)
+   ({ stateId := 0, root := "_uniq.79" }: Protocol.GoalStartResult)
   step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic)
    ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult)
   step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
@@ -321,12 +379,25 @@ def test_frontend_process_circular : Test := do
        goalStateId? := .some 0,
        goals? := .some #[goal1],
        goalSrcBoundaries? := .some #[(35, 40)],
-       messages := #["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],
+       messages := #[{
+         fileName := "<anonymous>",
+         kind := `hasSorry,
+         pos := ⟨1, 8⟩,
+         endPos := .some ⟨1, 15⟩,
+         severity := .warning,
+         data := "declaration uses 'sorry'"
        }],
-   }: Protocol.FrontendProcessResult)
+     }],
+   } : 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)
+   ({
+      messages? := .some #[{
+        fileName := ← getFileName,
+        kind := .anonymous,
+        pos := ⟨0, 0⟩,
+        data := "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
+      }]
+    } : Protocol.GoalTacticResult)
 
 def runTestSuite (env : Lean.Environment) (steps : Test): IO LSpec.TestSeq := do
   -- Setup the environment for execution
@@ -343,6 +414,7 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
     ("Tactic Timeout", test_tactic_timeout),
     ("Manual Mode", test_automatic_mode false),
     ("Automatic Mode", test_automatic_mode true),
+    ("Conv-Calc", test_conv_calc),
     ("env.add env.inspect", test_env_add_inspect),
     ("frontend.process invocation", test_frontend_process),
     ("frontend.process sorry", test_frontend_process_sorry),

Test/Main.lean

@@ -1,4 +1,3 @@
-import LSpec
 import Test.Delate
 import Test.Environment
 import Test.Frontend
@@ -9,6 +8,8 @@ import Test.Proofs
 import Test.Serial
 import Test.Tactic
 
+import LSpec
+
 -- Test running infrastructure
 
 namespace Pantograph.Test
@@ -55,6 +56,7 @@ def main (args: List String) := do
     ("Delate", Delate.suite),
     ("Serial", Serial.suite),
     ("Tactic/Assign", Tactic.Assign.suite),
+    ("Tactic/Fragment", Tactic.Fragment.suite),
     ("Tactic/Prograde", Tactic.Prograde.suite),
     ("Tactic/Special", Tactic.Special.suite),
   ]

Test/Metavar.lean

@@ -25,8 +25,8 @@ def test_instantiate_mvar: TestM Unit := do
       addTest $ assertUnreachable e
       return ()
   let t ← Lean.Meta.inferType expr
-  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
-    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
+  checkEq "typing" (toString (← serializeExpressionSexp t))
+    "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"
   return ()
 
 def startProof (expr: String): TestM (Option GoalState) := do
@@ -118,8 +118,9 @@ def test_m_couple_simp: TestM Unit := do
   let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
   addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  let n := state1.goals[2]!
   addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
-    #[#["_uniq.38"], #["_uniq.38"], #[]])
+    #[#[toString n.name], #[toString n.name], #[]])
 
   let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
     | .success state _ => pure state
@@ -158,10 +159,10 @@ def test_m_couple_simp: TestM Unit := do
       addTest $ assertUnreachable "(5 root)"
       return ()
   let rootStr: String := toString (← Lean.Meta.ppExpr root)
-  addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  --checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   let unfoldedRoot ←  unfoldAuxLemmas root
-  addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
-    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
+  checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot))
+    "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))"
   return ()
 
 def test_proposition_generation: TestM Unit := do
@@ -252,20 +253,60 @@ def test_partial_continuation: TestM Unit := do
       addTest $ assertUnreachable $ msg
       return ()
     | .ok state => pure state
-  addTest $ LSpec.check "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+  checkEq "(continue 2)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?))
+    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"]
   checkTrue "(2 root)" state1b.rootExpr?.get!.hasExprMVar
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
-  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
+  | .error error => checkEq "(continuation failure message)" error "Goals [_uniq.45, _uniq.46, _uniq.43, _uniq.52] are not in scope"
+  | .ok _ => fail "(continuation should fail)"
   -- Continuation should fail if some goals have not been solved
   match state2.continue state1 with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
-  | .ok _ => addTest $ assertUnreachable "(continuation failure)"
+  | .error error => checkEq "(continuation failure message)" error "Target state has unresolved goals"
+  | .ok _ => fail "(continuation should fail)"
   return ()
 
+def test_branch_unification : TestM Unit := do
+  let .ok rootTarget ← elabTerm (← `(term|∀ (p q : Prop), p → p ∧ (p ∨ q))) .none | unreachable!
+  let state ← GoalState.create rootTarget
+  let .success state _  ← state.tacticOn' 0 (← `(tactic|intro p q h)) | fail "intro failed to run"
+  let .success state _  ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | fail "apply And.intro failed to run"
+  let .success state1 _  ← state.tacticOn' 0 (← `(tactic|exact h)) | fail "exact h failed to run"
+  let .success state2 _  ← state.tacticOn' 1 (← `(tactic|apply Or.inl)) | fail "apply Or.inl failed to run"
+  checkEq "(state2 goals)" state2.goals.length 1
+  let state' ← state2.replay state state1
+  checkEq "(state' goals)" state'.goals.length 1
+  let .success stateT _ ← state'.tacticOn' 0 (← `(tactic|exact h)) | fail "exact h failed to run"
+  let .some root := stateT.rootExpr? | fail "Root expression must exist"
+  checkEq "(root)" (toString $ ← Meta.ppExpr root) "fun p q h => ⟨h, Or.inl h⟩"
+
+/-- Test merger when both branches have new aux lemmas -/
+def test_replay_environment : TestM Unit := do
+  let .ok rootTarget ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
+  let state ← GoalState.create rootTarget
+  let .success state _  ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | fail "apply And.intro failed to run"
+  let goal := state.goals[0]!
+  let type ← goal.withContext do
+    let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
+    pure type
+  let .success state1 _  ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "left"
+
+  state.restoreMetaM
+  let goal := state.goals[1]!
+  let type ← goal.withContext do
+    let .ok type ← elabTerm (← `(term|(3: Nat) ≤ 5)) (.some $ .sort 0) | unreachable!
+    pure type
+  let .success state2 _  ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | fail "right"
+  checkEq "(state1 goals)" state1.goals.length 0
+  checkEq "(state2 goals)" state2.goals.length 0
+  let stateT ← state2.replay state state1
+  checkEq "(stateT goals)" stateT.goals.length 0
+  let .some root := stateT.rootExpr? | fail "Root expression must exist"
+  checkTrue "root has aux lemma" $ root.getUsedConstants.any isAuxLemma
+  checkEq "(root)" (toString $ ← Meta.ppExpr root) "⟨_proof_1, _proof_2⟩"
+  let root ← unfoldAuxLemmas root
+  checkEq "(root unfold)" (toString $ ← Meta.ppExpr root) "⟨sorry, sorry⟩"
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -273,7 +314,9 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("2 < 5", test_m_couple),
     ("2 < 5", test_m_couple_simp),
     ("Proposition Generation", test_proposition_generation),
-    ("Partial Continuation", test_partial_continuation)
+    ("Partial Continuation", test_partial_continuation),
+    ("Branch Unification", test_branch_unification),
+    --("Replay Environment", test_replay_environment),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

Test/Proofs.lean

@@ -32,7 +32,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
     let expr ← parseSentence expr
     return .some $ ← GoalState.create (expr := expr)
 
-def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+private def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
     (userName?: Option String := .none): Protocol.Goal :=
   {
     name,
@@ -43,7 +43,7 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
       type? := .some { pp? := .some x.snd },
     })).toArray
   }
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+private def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
     Protocol.Goal :=
   {
     userName?,
@@ -53,7 +53,7 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
       type? := .some { pp? := .some x.snd },
     })).toArray
   }
-def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
+private def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
   let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
 
   let coreContext: Lean.Core.Context ← createCoreContext #[]
@@ -66,18 +66,18 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
     return a
 
 def test_identity: TestM Unit := do
-  let state0 ← GoalState.create (expr := ← parseSentence "∀ (p: Prop), p → p")
-  let tactic := "intro p h"
-  let state1 ← match ← state0.tacticOn 0 tactic with
+  let rootTarget ← Elab.Term.elabTerm (← `(term|∀ (p: Prop), p → p)) .none
+  let state0 ← GoalState.create (expr := rootTarget)
+  let state1 ← match ← state0.tacticOn' 0 (← `(tactic|intro p h)) with
     | .success state _ => pure state
     | other => do
       fail other.toString
       return ()
   let inner := "_uniq.11"
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
+  addTest $ LSpec.check "intro" ((← state1.serializeGoals (options := ← read)).map (·.name) =
     #[inner])
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -105,9 +105,11 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
 
   match ← state1.tacticOn 0 "assumption" with
   | .failure #[message] =>
-    addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
+    checkEq "assumption"
+      (← message.toString)
+      s!"{← getFileName}:0:0: error: tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n\n"
   | other => do
-    addTest $ assertUnreachable $ other.toString
+    addTest $ assertUnreachable other.toString
 
   let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
     | .success state _ => pure state
@@ -117,41 +119,6 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
   addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
 
   return ()
-def test_delta_variable: TestM Unit := do
-  let options: Protocol.Options := { noRepeat := true }
-  let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
-  addTest $ LSpec.check "Start goal" state?.isSome
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
-    | .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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
-    #[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
-  return ()
-  where
--- Like `buildGoal` but allow certain variables to be elided.
-  buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
-    {
-      target := { pp? := .some target},
-      vars := (nameType.map fun x => ({
-        userName := x.fst,
-        type? := x.snd.map (λ type => { pp? := type }),
-      })).toArray
-    }
 
 example (w x y z : Nat) (p : Nat → Prop)
         (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
@@ -212,8 +179,8 @@ def test_or_comm: TestM Unit := do
     | .none => do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
-  addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
-  addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
+  checkTrue "(0 parent)" state0.parentMVars.isEmpty
+  checkTrue "(0 root)" state0.rootExpr?.isNone
 
   let tactic := "intro p q h"
   let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
@@ -237,11 +204,11 @@ def test_or_comm: TestM Unit := do
         { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
       ]
     }])
-  checkTrue "(1 parent)" state1.parentExpr?.isSome
+  checkTrue "(1 parent)" state1.hasUniqueParent
   checkTrue "(1 root)" $ ¬ state1.isSolved
 
   let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr!)
   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
@@ -256,11 +223,11 @@ 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])
-  checkTrue "(2 parent exists)" state2.parentExpr?.isSome
+  checkTrue "(2 parent exists)" state2.hasUniqueParent
   checkTrue "(2 root)" $ ¬ state2.isSolved
 
   let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr!)
   let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
   let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
   let motive := s!"(:lambda t {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
@@ -276,7 +243,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr!)
   let [state3_1goal0] := state3_1.goals | fail "Should have 1 goal"
   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)
@@ -286,7 +253,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  let state4_1parent ← instantiateAll state4_1.parentExpr!
   addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   checkTrue "(4_1 root)" $ ¬ state4_1.isSolved
   let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
@@ -336,193 +303,6 @@ def test_or_comm: TestM Unit := do
       ]
     }
 
-example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
-  intro a b c1 c2 h
-  conv =>
-    lhs
-    congr
-    . rw [Nat.add_comm]
-    . rfl
-  exact h
-
-def test_conv: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-
-  let tactic := "intro a b c1 c2 h"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "a + b + c1 = b + a + c2"])
-
-  let state2 ← match ← state1.conv (state1.get! 0) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
-
-  let convTactic := "rhs"
-  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
-
-  let convTactic := "lhs"
-  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
-
-  let convTactic := "congr"
-  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
-      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
-    ])
-
-  let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
-
-  let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state4_1 ← match state6_1.continue state4 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-
-  let convTactic := "rfl"
-  let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state1_1 ← match ← state6.convExit with
-    | .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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  where
-    h := "b + a + c1 = b + a + c2"
-    interiorGoal (free: List (String × String)) (target: String) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
-      buildGoal free target
-
-example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
-  intro a b c d h1 h2
-  calc a + b = b + c := by apply h1
-    _ = c + d := by apply h2
-
-def test_calc: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro a b c d h1 h2"
-  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "a + b = b + c" (.some "calc"),
-      interiorGoal [] "b + c = c + d"
-    ])
-  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
-  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
-
-  let tactic := "apply h1"
-  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  let state3 ← match state2m.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-  let pred := "_ = c + d"
-  let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
-    | .success state _ => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      interiorGoal [] "b + c = c + d" (.some "calc")
-    ])
-  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
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
-  where
-    interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
-        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
-      buildGoal free target userName?
-
 def test_tactic_failure_unresolved_goals : TestM Unit := do
   let state? ← startProof (.expr "∀ (p : Nat → Prop), ∃ (x : Nat), p (0 + x + 0)")
   let state0 ← match state? with
@@ -539,8 +319,10 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
       return ()
 
   let tactic := "exact ⟨0, by simp⟩"
-  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  checkEq s!"{tactic} fails" messages #[s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"]
+  let .failure #[message] ← state1.tacticOn 0 tactic
+    | fail s!"{tactic} should fail with 1 message"
+  checkEq s!"{tactic} fails" (← message.toString)
+    s!"{← getFileName}:0:12: error: unsolved goals\np : Nat → Prop\n⊢ p 0\n"
 
 def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
@@ -570,9 +352,10 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   --  buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
   --]
 
-  let .failure messages ← state1.tacticOn 0 tactic | addTest $ assertUnreachable s!"{tactic} should fail"
-  let message := s!"<Pantograph>:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
-  checkEq s!"{tactic} fails" messages #[message]
+  let .failure #[_head, message] ← state1.tacticOn 0 tactic
+    | addTest $ assertUnreachable s!"{tactic} should fail with 2 messages"
+  checkEq s!"{tactic} fails" (← message.toString)
+    s!"{← getFileName}:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"
 
 def test_deconstruct : TestM Unit := do
   let state? ← startProof (.expr "∀ (p q : Prop) (h : And p q), And q p")
@@ -599,11 +382,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("identity", test_identity),
     ("Nat.add_comm", test_nat_add_comm false),
     ("Nat.add_comm manual", test_nat_add_comm true),
-    ("Nat.add_comm delta", test_delta_variable),
     ("arithmetic", test_arith),
     ("Or.comm", test_or_comm),
-    ("conv", test_conv),
-    ("calc", test_calc),
     ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
     ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
     ("deconstruct", test_deconstruct),

Test/Serial.lean

@@ -7,9 +7,6 @@ open Lean
 
 namespace Pantograph.Test.Serial
 
-def tempPath : IO System.FilePath := do
-  Prod.snd <$> IO.FS.createTempFile
-
 structure MultiState where
   coreContext : Core.Context
   env: Environment
@@ -30,22 +27,22 @@ def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (
     set $ (← getThe LSpec.TestSeq) ++ tests
     return (a, state')
 
-def test_environment_pickling : TestM Unit := do
+def test_pickling_environment : TestM Unit := do
   let coreSrc : Core.State := { env := ← getEnv }
   let coreDst : Core.State := { env := ← getEnv }
 
   let name := `mystery
-  let envPicklePath ← tempPath
+  IO.FS.withTempFile λ _ envPicklePath => do
   let ((), _) ← runCoreM coreSrc do
     let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
     let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default
-    let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
+    let c := Declaration.defnDecl <| mkDefinitionValEx
       (name := name)
       (levelParams := [])
       (type := type)
       (value := value)
-      (hints := Lean.mkReducibilityHintsRegularEx 1)
-      (safety := Lean.DefinitionSafety.safe)
+      (hints := mkReducibilityHintsRegularEx 1)
+      (safety := .safe)
       (all := [])
     addDecl c
     environmentPickle (← getEnv) envPicklePath
@@ -56,13 +53,10 @@ def test_environment_pickling : TestM Unit := do
     let anotherName := `mystery2
     checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone
 
-  IO.FS.removeFile envPicklePath
-
-def test_goal_state_pickling_simple : TestM Unit := do
+def test_goal_state_simple : TestM Unit := do
   let coreSrc : Core.State := { env := ← getEnv }
   let coreDst : Core.State := { env := ← getEnv }
-  let statePath ← tempPath
-
+  IO.FS.withTempFile λ _ statePath => do
   let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default
   let stateGenerate : MetaM GoalState := runTermElabMInMeta do
     GoalState.create type
@@ -78,13 +72,50 @@ def test_goal_state_pickling_simple : TestM Unit := do
     let types ← metaM.run'
     checkTrue "Goals" $ types[0]!.equal type
 
-  IO.FS.removeFile statePath
+def test_pickling_env_extensions : TestM Unit := do
+  let coreSrc : Core.State := { env := ← getEnv }
+  let coreDst : Core.State := { env := ← getEnv }
+  IO.FS.withTempFile λ _ statePath => do
+  let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do
+    let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
+    let state ← GoalState.create e
+    let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable!
+
+    let goal := state.goals[0]!
+    let type ← goal.withContext do
+      let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
+      instantiateMVars type
+    let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type) | unreachable!
+    let parentExpr := state1.parentExpr!
+    checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
+    goalStatePickle state1 statePath
+  let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do
+    let (state1, _) ← goalStateUnpickle statePath (← getEnv)
+    let parentExpr := state1.parentExpr!
+    checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any isAuxLemma
+
+  return ()
+
+/-- Synthetic mvars in this case creates closures. These cannot be pickled. -/
+def test_pickling_synthetic_mvars : TestM Unit := do
+  let coreSrc : Core.State := { env := ← getEnv }
+  IO.FS.withTempFile λ _ statePath => do
+  let stateGenerate : MetaM GoalState := runTermElabMInMeta do
+    let type ← Elab.Term.elabTerm (← `(term|(0 : Nat) < 1)) .none
+    let state ← GoalState.create type
+    let .success state _ ← state.tryHave .unfocus "h" "0 < 2" | unreachable!
+    assert! state.savedState.term.elab.syntheticMVars.size > 0
+    return state
+
+  let ((), _) ← runCoreM coreSrc do
+    let state ← stateGenerate.run'
+    goalStatePickle state statePath
 
 structure Test where
   name : String
   routine: TestM Unit
 
-protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do
+protected def Test.run (test: Test) (env: Environment) : IO LSpec.TestSeq := do
   -- Create the state
   let state : MultiState := {
     coreContext := ← createCoreContext #[],
@@ -95,10 +126,12 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq :
   | .error e =>
     return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "")
 
-def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
+def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests: List Test := [
-    { name := "environment_pickling", routine := test_environment_pickling, },
-    { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, },
+    { name := "environment", routine := test_pickling_environment, },
+    { name := "goal simple", routine := test_goal_state_simple, },
+    { name := "goal synthetic mvars", routine := test_pickling_synthetic_mvars, },
+    { name := "extensions", routine := test_pickling_env_extensions, },
   ]
   tests.map (fun test => (test.name, test.run env))
 

Test/Tactic.lean

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

Test/Tactic/Fragment.lean

@@ -0,0 +1,313 @@
+import Pantograph.Goal
+import Test.Common
+
+open Lean
+
+namespace Pantograph.Test.Tactic.Fragment
+
+private def buildGoal (nameType: List (String × String)) (target: String):
+    Protocol.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+    })).toArray
+  }
+
+abbrev TestM := TestT $ Elab.TermElabM
+
+example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
+  intro a b c1 c2 h
+  conv =>
+    lhs
+    congr
+    . rw [Nat.add_comm]
+    . rfl
+  exact h
+
+def test_conv_simple: TestM Unit := do
+  let rootTarget ← parseSentence "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2"
+  let state0 ← GoalState.create rootTarget
+
+  let tactic := "intro a b c1 c2 h"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "a + b + c1 = b + a + c2"])
+
+  let goalConv := state1.goals[0]!
+  let state2 ← match ← state1.convEnter (state1.get! 0) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }])
+
+  let convTactic := "rhs"
+  let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a + c2" with fragment := .conv }])
+
+  let convTactic := "lhs"
+  let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "a + b + c1" with fragment := .conv }])
+
+  let convTactic := "congr"
+  let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" },
+      { interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" }
+    ])
+
+  let convTactic := "rw [Nat.add_comm]"
+  let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) =
+    #[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }])
+
+  let convTactic := "rfl"
+  let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let state4_1 ← match state6_1.continue state4 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+
+  let convTactic := "rfl"
+  let state1_1 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"  · {convTactic}" ((← state1_1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "b + a + c1 = b + a + c2"])
+  checkEq "(fragments)" state1_1.fragments.size 0
+
+  /-
+  let state1_1 ← match ← state6.fragmentExit goalConv with
+    | .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
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  checkEq tactic ((← stateF.serializeGoals).map (·.devolatilize)) #[]
+  checkEq "fragments" stateF.fragments.size 0
+
+  where
+    h := "b + a + c1 = b + a + c2"
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
+      buildGoal free target
+
+example (p : Prop) (x y z : Nat) : p → (p → x = y) → x + z = y + z ∧ p := by
+  intro hp hi
+  apply And.intro
+  conv =>
+    rhs
+    arg 1
+    rw [←hi]
+    rfl
+    tactic => exact hp
+  exact hp
+
+def test_conv_unshielded : TestM Unit := do
+  let rootTarget ← parseSentence "∀ (p : Prop) (x y z : Nat), p → (p → x = y) → x + z = y + z ∧ p"
+  let state ← GoalState.create rootTarget
+  let tactic := "intro p x y z hp hi"
+  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
+  let tactic := "apply And.intro"
+  let .success state _ ← state.tacticOn 0 tactic | fail "apply failed"
+  let .success state _ ← state.convEnter (.prefer state.goals[0]!) | fail "Cannot enter conversion tactic mode"
+  let .success state _ ← state.tryTactic .unfocus "rhs" | fail "rhs failed"
+  let tactic := "arg 1"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "y" with fragment := .conv },
+      { interiorGoal [] "p" with userName? := "right", },
+    ]
+  let tactic := "rw [←hi]"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" state.goals.length 3
+  let tactic := "rfl"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      interiorGoal [] "p",
+      { interiorGoal [] "p" with userName? := "right", },
+    ]
+  checkEq "(n goals)" state.goals.length 2
+  checkEq "(fragments)" state.fragments.size 0
+  let tactic := "exact hp"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let tactic := "exact hp"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let root? := state.rootExpr?
+  checkTrue "root" root?.isSome
+  checkEq "fragments" state.fragments.size 0
+  where
+  interiorGoal (free: List (String × String)) (target: String) :=
+    let free := [("p", "Prop"), ("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("hp", "p"), ("hi", "p → x = y")] ++ free
+    buildGoal free target
+
+example : ∀ (x y z w : Nat), y = z → x + z = w → x + y = w := by
+  intro x y z w hyz hxzw
+  conv =>
+    lhs
+    arg 2
+    rw [hyz]
+    rfl
+  exact hxzw
+
+def test_conv_unfinished : TestM Unit := do
+  let rootTarget ← parseSentence "∀ (x y z w : Nat), y = z → x + z = w → x + y = w"
+  let state ← GoalState.create rootTarget
+  let tactic := "intro x y z w hyz hxzw"
+  let .success state _ ← state.tacticOn 0 tactic | fail "intro failed"
+  let convParent := state.goals[0]!
+  let .success state _ ← state.convEnter (.prefer convParent) | fail "Cannot enter conversion tactic mode"
+  let .success state _ ← state.tryTactic .unfocus "lhs" | fail "rhs failed"
+  let tactic := "arg 2"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "y" with fragment := .conv },
+    ]
+  let tactic := "rw [hyz]"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      { interiorGoal [] "z" with fragment := .conv },
+    ]
+  checkTrue "  (fragment)" $ state.fragments.contains state.mainGoal?.get!
+  checkTrue "  (fragment parent)" $ state.fragments.contains convParent
+  checkTrue "  (main goal)" state.mainGoal?.isSome
+  let tactic := "rfl"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
+    #[
+      interiorGoal [] "x + z = w",
+    ]
+  checkEq "(fragments)" state.fragments.size 0
+  checkEq s!"  {tactic}" state.goals.length 1
+  let tactic := "exact hxzw"
+  let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
+  let root? := state.rootExpr?
+  checkTrue "root" root?.isSome
+  where
+  interiorGoal (free: List (String × String)) (target: String) :=
+    let free := [("x", "Nat"), ("y", "Nat"), ("z", "Nat"), ("w", "Nat"), ("hyz", "y = z"), ("hxzw", "x + z = w")] ++ free
+    buildGoal free target
+
+example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
+  intro a b c d h1 h2
+  calc a + b = b + c := by apply h1
+    _ = c + d := by apply h2
+
+def test_calc: TestM Unit := do
+  let rootTarget ← parseSentence "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d"
+  let state0 ← GoalState.create rootTarget
+  let tactic := "intro a b c d h1 h2"
+  let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[interiorGoal [] "a + b = c + d"])
+  let pred := "a + b = b + c"
+  let .success state1 _ ← state1.calcEnter state1.mainGoal?.get! | fail "Could not enter calc"
+  let state2 ← match ← state1.tacticOn 0 pred with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "a + b = b + c" with userName? := .some "calc" },
+      { interiorGoal [] "b + c = c + d" with fragment := .calc },
+    ])
+  addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
+  addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
+
+  let tactic := "apply h1"
+  let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  let state3 ← match state2m.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ expectationFailure "continue" e
+      return ()
+  let pred := "_ = c + d"
+  let state4 ← match ← state3.tacticOn 0 pred with
+    | .success state _ => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[
+      { interiorGoal [] "b + c = c + d" with userName? := .some "calc" },
+    ])
+  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
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  checkEq "(fragments)" state4m.fragments.size 0
+  addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
+  where
+    interiorGoal (free: List (String × String)) (target: String) :=
+      let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
+        ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
+      buildGoal free target
+
+def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
+  [
+    ("conv simple", test_conv_simple),
+    ("conv unshielded", test_conv_unshielded),
+    ("conv unfinished", test_conv_unfinished),
+    ("calc", test_calc),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
+
+end Pantograph.Test.Tactic.Fragment

Test/Tactic/Prograde.lean

@@ -185,8 +185,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
-    #[])
+  checkEq s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize)) #[]
 
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
@@ -264,9 +263,11 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
   let tactic := "exact h"
   match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
   | .failure #[message] =>
-    addTest $ LSpec.check tactic  (message = s!"type mismatch\n  h\nhas type\n  a : Prop\nbut is expected to have type\n  {mainTarget} : Prop")
+    checkEq tactic
+      (← message.toString)
+      s!"{← getFileName}:0:0: error: type mismatch\n  h\nhas type\n  a : Prop\nbut is expected to have type\n  {mainTarget} : Prop\n"
   | other => do
-    addTest $ assertUnreachable $ other.toString
+    fail s!"Should be a failure: {other.toString}"
 
   let tactic := "exact Or.inl (Or.inl h)"
   let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with

Test/Tactic/Special.lean

@@ -13,7 +13,9 @@ def test_exact_q : TestT Elab.TermElabM Unit := do
   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."]
+  checkEq "messages"
+    (← messages.mapM (·.toString))
+    #[s!"{← getFileName}:0:0: error: `exact?` could not close the goal. Try `apply?` to see partial suggestions.\n"]
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [

Tomograph.lean

@@ -0,0 +1,41 @@
+/- A tool for analysing Lean source code. -/
+import Pantograph.Frontend
+import Pantograph.Library
+
+open Lean
+
+namespace Pantograph
+
+def fail (s : String) : IO UInt32 := do
+  IO.eprintln s
+  return 2
+
+def dissect (args : List String) : IO UInt32 := do
+  let fileName :: _args := args | fail s!"Must supply a file name"
+  let file ← IO.FS.readFile fileName
+  let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {}
+  let frontendM: Frontend.FrontendM _ :=
+    Frontend.mapCompilationSteps λ step => do
+      IO.println s!"🐈 {step.stx.getKind.toString}"
+      for (tree, i) in step.trees.zipIdx do
+        IO.println s!"🌲[{i}] {← tree.toString}"
+      for (msg, i) in step.msgs.zipIdx do
+        IO.println s!"🔈[{i}] {← msg.toString}"
+  let (_, _) ← frontendM.run {} |>.run context |>.run state
+  return 0
+
+end Pantograph
+
+open Pantograph
+
+def help : IO UInt32 := do
+  IO.println "Usage: tomograph dissect FILE_NAME"
+  return 1
+
+def main (args : List String) : IO UInt32 := do
+  let command :: args := args | help
+  unsafe do
+    Pantograph.initSearch ""
+  match command with
+  | "dissect" => dissect args
+  | _ => fail s!"Unknown command {command}"

doc/rationale.md

@@ -37,10 +37,6 @@ differently from Lean in some times, but never at the sacrifice of soundness.
 - When Lean LSP says "unresolved goals", that means a proof cannot finish where
   it is supposed to finish at the end of a `by` block. Pantograph will raise the
   error in this case, since it indicates the termination of a proof search branch.
-- `pick_goal` or `swap` will not work since they run contrary to tree search
-  paradigms. However, if there are tactics which perform non-trivial operations
-  to multiple goals at the same time, this constrain could potentially be
-  relaxed at a cost of great bookkeeping overhead to the user.
 
 Pantograph cannot perform things that are inherently constrained by Lean. These
 include:

doc/repl.md

@@ -1,5 +1,83 @@
 # REPL
 
+This documentation is about interacting with the REPL.
+
+## Examples
+
+After building the `repl`, it will be available in `.lake/build/bin/repl`.
+Execute it by either directly referring to its name, or `lake exe repl`.
+
+``` sh
+repl MODULES|LEAN_OPTIONS
+```
+
+The `repl` executable must be given with a list of modules to import. By default
+it will import nothing, not even `Init`. It can also accept lean options of the
+form `--key=value` e.g. `--pp.raw=true`.
+
+After it emits the `ready.` signal, `repl` accepts commands as single-line JSON
+inputs and outputs either an `Error:` (indicating malformed command) or a JSON
+return value indicating the result of a command execution. The command must be
+given in one of two formats
+
+```
+command { ... }
+{ "cmd": command, "payload": ... }
+```
+
+The list of available commands can be found below. An empty command aborts the
+REPL.
+
+Example: (~5k symbols)
+```
+$ repl Init
+env.catalog
+env.inspect {"name": "Nat.le_add_left"}
+```
+
+Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
+
+```
+$ repl Mathlib.Analysis.Seminorm
+env.catalog
+```
+
+Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`)
+to prime the proof
+
+```
+$ repl Init
+goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
+goal.tactic {"stateId": 0, "tactic": "intro n m"}
+goal.tactic {"stateId": 1, "tactic": "assumption"}
+goal.delete {"stateIds": [0]}
+stat {}
+goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"}
+stat
+```
+where the application of `assumption` should lead to a failure.
+
+For a list of commands, see [REPL Documentation](doc/repl.md).
+
+### Project Environment
+
+To use Pantograph in a project environment, setup the `LEAN_PATH` environment
+variable so it contains the library path of lean libraries. The libraries must
+be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
+the environment might be setup like this:
+
+``` sh
+LIB="../lib"
+LIB_MATHLIB="$LIB/mathlib4/.lake"
+export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+
+LEAN_PATH=$LEAN_PATH repl $@
+```
+The `$LEAN_PATH` executable of any project can be extracted by
+``` sh
+lake env printenv LEAN_PATH
+```
+
 ## Commands
 
 See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
@@ -13,32 +91,27 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
   current environment to/from a file
-* `env.module_read { "module": <name }`: Reads a list of symbols from a module
+* `env.module_read { "module": <name> }`: Reads a list of symbols from a module
 * `env.describe {}`: Describes the imports and modules in the current environment
-* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
-  have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
-
-  One particular option for interest for machine learning researchers is the
-  automatic mode (flag: `"automaticMode"`).  By default it is turned on, with
-  all goals automatically resuming. This makes Pantograph act like a gym,
-  with no resumption necessary to manage your goals.
-
-  Set `timeout` to a non-zero number to specify timeout (milliseconds) for all `CoreM`
-  operations.
+* `options.set { key: value, ... }`: Set one or more options. These are not Lean
+  `CoreM` options; those have to be set via command line arguments.), for
+  options see below.
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol
-* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
-  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
-  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
-  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
-  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
-  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+* `goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}`:
+  Execute a tactic string on a given goal site. The tactic is supplied as additional
+  key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Executes a tactic in the current mode
+  - `{ "mode": <mode> }`: Enter a different tactic mode. The permitted values
+    are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must
     be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
     to the previous `rhs`.
-  - `{ "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.
+  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
+  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "let": <expr>, "binderName": <name> }`: Execute `let` and creates a branch goal
+  - `{ "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>]}`:
@@ -52,15 +125,25 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   state. The user is responsible to ensure the sender/receiver instances share
   the same environment.
 * `frontend.process { ["fileName": <fileName>,] ["file": <str>], readHeader: <bool>, inheritEnv: <bool>, invocations:
-  <bool>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
+  <string>, sorrys: <bool>, typeErrorsAsGoals: <bool>, newConstants: <bool> }`:
   Executes the Lean frontend on a file, collecting the tactic invocations
-  (`"invocations": true`), the sorrys and type errors into goal states
+  (`"invocations": output-path`), the sorrys and type errors into goal states
   (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
   `sorrys`, this command additionally outputs the position of each captured
   `sorry`. Conditionally inherit the environment from executing the file.
   Warning: Behaviour is unstable in case of multiple `sorry`s. Use the draft
   tactic if possible.
 
+## Options
+
+The full list of options can be found in `Pantograph/Protocol.lean`. Particularly:
+- `automaticMode` (default on): Goals will not become dormant when this is
+  turned on. By default it is turned on, with all goals automatically resuming.
+  This makes Pantograph act like a gym, with no resumption necessary to manage
+  your goals.
+- `timeout` (default 0): Set `timeout` to a non-zero number to specify timeout
+  (milliseconds) for all `CoreM` and frontend operations.
+
 ## Errors
 
 When an error pertaining to the execution of a command happens, the returning JSON structure is
@@ -75,3 +158,10 @@ Common error forms:
 * `index`: Indicates an invariant maintained by the output of one command and
   input of another is broken. For example, attempting to query a symbol not
   existing in the library or indexing into a non-existent proof state.
+
+## Troubleshooting
+
+If lean encounters stack overflow problems when printing catalog, execute this before running lean:
+```sh
+ulimit -s unlimited
+```

flake.lock

@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1743550720,
-        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "lastModified": 1751413152,
+        "narHash": "sha256-Tyw1RjYEsp5scoigs1384gIg6e0GoBVjms4aXFfRssQ=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "rev": "77826244401ea9de6e3bac47c2db46005e1f30b5",
         "type": "github"
       },
       "original": {
@@ -39,16 +39,14 @@
     "lean4-nix": {
       "inputs": {
         "flake-parts": "flake-parts_2",
-        "nixpkgs": [
-          "nixpkgs"
-        ]
+        "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1743534244,
-        "narHash": "sha256-WnoYs2iyrfgh35eXErCOyos8E2YbW3LT1xm/EtT88/k=",
+        "lastModified": 1751390929,
+        "narHash": "sha256-Wl2miy8PhNF6ue3R1ssQbsVK3foJ37tYtznNq/i14YM=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "5eb7f03be257e327fdb3cca9465392e68dc28a4d",
+        "rev": "68a07e4af5e2e56276056b172e046a2276d21aee",
         "type": "github"
       },
       "original": {
@@ -59,27 +57,27 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1743975612,
-        "narHash": "sha256-o4FjFOUmjSRMK7dn0TFdAT0RRWUWD+WsspPHa+qEQT8=",
+        "lastModified": 1743095683,
+        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "a880f49904d68b5e53338d1e8c7bf80f59903928",
+        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
         "type": "github"
       },
       "original": {
         "owner": "nixos",
-        "ref": "nixos-24.11",
+        "ref": "nixos-unstable",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1743296961,
-        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
+        "lastModified": 1751159883,
+        "narHash": "sha256-urW/Ylk9FIfvXfliA1ywh75yszAbiTEVgpPeinFyVZo=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "rev": "14a40a1d7fb9afa4739275ac642ed7301a9ba1ab",
         "type": "github"
       },
       "original": {
@@ -100,11 +98,27 @@
         "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
       }
     },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1751943650,
+        "narHash": "sha256-7orTnNqkGGru8Je6Un6mq1T8YVVU/O5kyW4+f9C1mZQ=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "88983d4b665fb491861005137ce2b11a9f89f203",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-25.05",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
     "root": {
       "inputs": {
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },

flake.nix

@@ -2,12 +2,9 @@
   description = "Pantograph";
 
   inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.11";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-25.05";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix = {
-      url = "github:lenianiva/lean4-nix";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
+    lean4-nix.url = "github:lenianiva/lean4-nix";
   };
 
   outputs = inputs @ {
@@ -48,10 +45,6 @@
           ./Pantograph.lean
           (fileFilter (file: file.hasExt "lean") ./Pantograph)
         ];
-        set-repl = unions [
-          ./Main.lean
-          ./Repl.lean
-        ];
         set-test = unions [
           (fileFilter (file: file.hasExt "lean") ./Test)
         ];
@@ -65,14 +58,22 @@
           root = src;
           fileset = unions [
             set-project
-            set-repl
+            ./Main.lean
+            ./Repl.lean
+          ];
+        };
+        src-tomograph = toSource {
+          root = src;
+          fileset = unions [
+            set-project
+            ./Tomograph.lean
           ];
         };
         src-test = toSource {
           root = src;
           fileset = unions [
             set-project
-            set-repl
+            ./Repl.lean
             set-test
           ];
         };
@@ -87,6 +88,12 @@
           deps = [project];
           src = src-repl;
         };
+        tomograph = pkgs.lean.buildLeanPackage {
+          name = "tomograph";
+          roots = ["Tomograph"];
+          deps = [project];
+          src = src-tomograph;
+        };
         test = pkgs.lean.buildLeanPackage {
           name = "Test";
           # NOTE: The src directory must be ./. since that is where the import
@@ -101,6 +108,7 @@
           inherit (pkgs.lean) lean lean-all;
           inherit (project) sharedLib iTree;
           inherit (repl) executable;
+          tomograph = tomograph.executable;
           default = repl.executable;
         };
         legacyPackages = {

lakefile.lean

@@ -10,6 +10,7 @@ lean_lib Pantograph {
 
 lean_lib Repl {
 }
+
 @[default_target]
 lean_exe repl {
   root := `Main
@@ -17,6 +18,12 @@ lean_exe repl {
   supportInterpreter := true
 }
 
+lean_exe tomograph {
+  root := `Tomograph
+  -- Solves the native symbol not found problem
+  supportInterpreter := true
+}
+
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.19.0
+leanprover/lean4:v4.21.0