29 changed files with 223 additions and 456 deletions
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -264,24 +264,25 @@ def serializeName (name: Name) (sanitize: Bool := true): String :=
    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n

 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serializeSortLevel (level: Level) : String :=
+partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
  let k := level.getOffset
  let u := level.getLevelOffset
  let u_str := match u with
    | .zero => "0"
    | .succ _ => panic! "getLevelOffset should not return .succ"
    | .max v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
      s!"(:max {v} {w})"
    | .imax v w =>
-      let v := serializeSortLevel v
-      let w := serializeSortLevel w
+      let v := serializeSortLevel v sanitize
+      let w := serializeSortLevel w sanitize
      s!"(:imax {v} {w})"
    | .param name =>
+      let name := serializeName name sanitize
      s!"{name}"
    | .mvar id =>
-      let name := id.name
+      let name := serializeName id.name sanitize
      s!"(:mv {name})"
  match k, u with
  | 0, _ => u_str
@ -294,7 +295,7 @@ partial def serializeSortLevel (level: Level) : String :=

 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
  self expr
  where
  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@ -333,10 +334,9 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
        let name := mvarId.name
        pure s!"(:{pref} {name})"
    | .sort level =>
-      let level := serializeSortLevel level
+      let level := serializeSortLevel level sanitize
      pure s!"(:sort {level})"
    | .const declName _ =>
-      let declName := serializeName declName (sanitize := false)
      -- The universe level of the const expression is elided since it should be
      -- inferrable from surrounding expression
      pure s!"(:c {declName})"
@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
      -- is wrapped in a :lit sexp.
      let v' := match v with
        | .natVal val => toString val
-        | .strVal val => IR.EmitC.quoteString val
+        | .strVal val => s!"\"{val}\""
      pure s!"(:lit {v'})"
    | .mdata _ inner =>
      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
@ -384,9 +384,9 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
  -- Elides all unhygenic names
  binderInfoSexp : Lean.BinderInfo → String
    | .default => ""
-    | .implicit => " :i"
-    | .strictImplicit => " :si"
-    | .instImplicit => " :ii"
+    | .implicit => " :implicit"
+    | .strictImplicit => " :strictImplicit"
+    | .instImplicit => " :instImplicit"

 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
  let pp?: Option String ← match options.printExprPretty with
@ -532,7 +532,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
        then instantiateAll decl.type
        else pure $ decl.type
      let type_sexp ← if options.printSexp then
-          let sexp ← serializeExpressionSexp type
+          let sexp ← serializeExpressionSexp type (sanitize := false)
          pure <| " " ++ sexp
        else
          pure ""
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -58,7 +58,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
    | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
    | some info => pure info
  let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat)
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
  let value? := match args.value?, info with
    | .some true, _ => info.value?
    | .some false, _ => .none
@ -80,7 +80,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
      then value?.map (λ e =>
        e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
      else .none,
-    module? := module?.map (·.toString)
+    module? := module?
  }
  let result ← match info with
    | .inductInfo induct => pure { core with inductInfo? := .some {
@ -113,20 +113,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
          k := r.k,
      } }
    | _ => pure core
-  let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
-      let declRange? ← findDeclarationRanges? name
-      let sourceStart? := declRange?.map (·.range.pos)
-      let sourceEnd? := declRange?.map (·.range.endPos)
-      .pure {
-        result with
-        sourceUri?,
-        sourceStart?,
-        sourceEnd?,
-      }
-    else
-      .pure result
  return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
  let env ← Lean.MonadEnv.getEnv
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@ -67,7 +67,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
  let s := (← get).commandState
  let before := s.env
  let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back!
+  let stx := (← get).commands.back
  let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
  let s' := (← get).commandState
  let after := s'.env
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@ -80,10 +80,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=

@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
    | info@(.ofTacticInfo _) => info.isOriginal
    | _ => false
-  let tactics := tacticInfoTrees.flatMap collectTactics
+  let tactics := tacticInfoTrees.bind collectTactics
  tactics.mapM λ invocation => do
    let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
    let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@ -104,20 +104,14 @@ structure InfoWithContext where
  info: Elab.Info
  context?: Option Elab.ContextInfo := .none

-structure GoalCollectionOptions where
-  collectTypeErrors : Bool := false
-
-private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
+private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
  let infos ← t.findAllInfoM none fun i ctx? => match i with
-    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
+    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
      let .some ctx := ctx? | return (false, true)
      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
        if expectedType?.isNone then
          throw $ .userError "Sorry of indeterminant type is not allowed"
        return (true, false)
-      unless options.collectTypeErrors do
-        return (false, true)
      let .some expectedType := expectedType? | return (false, true)
      let typeMatch ← ctx.runMetaM lctx do
        let type ← Meta.inferType expr
@ -136,9 +130,8 @@ private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOpt

 -- NOTE: Plural deliberately not spelled "sorries"
@[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
-    : IO (List InfoWithContext) := do
-  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).flatten
+def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
+  return (← step.trees.mapM collectSorrysInTree).join

 structure AnnotatedGoalState where
  state : GoalState
@ -156,18 +149,13 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState
    match i.info with
    | .ofTermInfo termInfo  => do
      let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      if (← mvarId.getType).hasSorry then
-        throwError s!"Coupling is not allowed in drafting"
      return [(mvarId, stxByteRange termInfo.stx)]
    | .ofTacticInfo tacticInfo => do
      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
-      for mvarId in mvarIds do
-        if (← mvarId.getType).hasSorry then
-          throwError s!"Coupling is not allowed in drafting"
      let range := stxByteRange tacticInfo.stx
      return mvarIds.map (·, range)
    | _ => panic! "Invalid info"
-  let annotatedGoals := List.flatten (← goalsM.run {} |>.run' {})
+  let annotatedGoals := List.join (← goalsM.run {} |>.run' {})
  let goals := annotatedGoals.map Prod.fst
  let srcBoundaries := annotatedGoals.map Prod.snd
  let root := match goals with
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@ -26,8 +26,6 @@ protected def Info.stx? : Info → Option Syntax
  | .ofFVarAliasInfo      _    => none
  | .ofFieldRedeclInfo    info => info.stx
  | .ofOmissionInfo       info => info.stx
-  | .ofChoiceInfo         info => info.stx
-  | .ofPartialTermInfo    info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
 protected def Info.isOriginal (i : Info) : Bool :=
  match i.stx? with
@ -89,9 +87,9 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
  | .context ctx tree => tree.filter p m |>.map (.context ctx)
  | .node info children =>
    if p info then
-      [.node info (children.toList.map (filter p m)).flatten.toPArray']
+      [.node info (children.toList.map (filter p m)).join.toPArray']
    else
-      (children.toList.map (filter p m)).flatten
+      (children.toList.map (filter p m)).join
  | .hole mvar => if m mvar then [.hole mvar] else []

 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
@ -105,7 +103,7 @@ partial def InfoTree.findAllInfo
  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
  | .node i children  =>
    let head := if pred i then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.flatMap (fun t => findAllInfo t context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
    head ++ tail
  | _ => []

@ -121,7 +119,7 @@ partial def InfoTree.findAllInfoM [Monad m]
    let (flagCollect, flagRecurse) ← pred i context?
    let head := if flagCollect then [(i, context?, children)] else []
    let tail := if ¬ flagRecurse then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? pred)
-    return head ++ (← tail).flatten
+    return head ++ (← tail).join
  | _ => return []

@[export pantograph_infotree_to_string_m]
@ -143,8 +141,6 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
      | .ofFVarAliasInfo _ => pure "[fvar]"
      | .ofFieldRedeclInfo _ => pure "[field_redecl]"
      | .ofOmissionInfo _ => pure "[omission]"
-      | .ofChoiceInfo _ => pure "[choice]"
-      | .ofPartialTermInfo  _ => pure "[partial_term]"
      let children := "\n".intercalate (← children.toList.mapM λ t' => do pure $ indent $ ← t'.toString ctx)
      return s!"{node}\n{children}"
    else throw <| IO.userError "No `ContextInfo` available."
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/Pantograph/Frontend/MetaTranslate.lean
@ -68,8 +68,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
    match e with
    | .fvar fvarId =>
      let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
-      -- Delegating this to `Meta.check` later
-      --assert! (← getLCtx).contains fvarId'
+      assert! (← getLCtx).contains fvarId'
      return .done $ .fvar fvarId'
    | .mvar mvarId => do
      -- Must not be assigned
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -183,8 +183,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
  -- 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.
-
-  let descendants ←  Meta.getMVars (.mvar src)
+  let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
  let mut alreadyVisited : MVarIdSet := {}
  let mut result : MVarIdSet := {}
@ -238,34 +237,25 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message: String)

-private def dumpMessageLog (prevMessageLength : Nat) : CoreM (Array String) := do
-  let newMessages ← (← Core.getMessageLog).toList.drop prevMessageLength
-    |>.filterMapM λ m => do
-      if m.severity == .error then
-        return .some $ ← m.toString
-      else
-        return .none
-  Core.resetMessageLog
-  return newMessages.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)
-    (guardMVarErrors : Bool := false)
-    : Elab.TermElabM TacticResult := do
-  let prevMessageLength := state.coreState.messages.toList.length
+protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit) (guardMVarErrors : Bool := false):
+      Elab.TermElabM TacticResult := do
  try
    let nextState ← state.step goal tacticM guardMVarErrors

    -- Check if error messages have been generated in the core.
-    let newMessages ← dumpMessageLog prevMessageLength
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
+      |>.filterMapM λ m => do
+        if m.severity == .error then
+          return .some $ ← m.toString
+        else
+          return .none
+    Core.resetMessageLog
    if ¬ newMessages.isEmpty then
-      return .failure newMessages
+      return .failure newMessages.toArray
    return .success nextState
  catch exception =>
-    match exception with
-    | .internal _ => return .failure $ ← dumpMessageLog prevMessageLength
-    | _ => return .failure #[← exception.toMessageData.toString]
+    return .failure #[← exception.toMessageData.toString]

 /-- Execute a string tactic on given state. Restores TermElabM -/
@[export pantograph_goal_state_try_tactic_m]
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -138,36 +138,17 @@ def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array
  runMetaM <| state.serializeGoals (parent := .none) options

@[export pantograph_goal_print_m]
-def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Bool) (extraMVars : Array String) (options: @&Protocol.Options)
-  : CoreM Protocol.GoalPrintResult := runMetaM do
-  state.restoreMetaM
-
-  let root? ← if rootExpr then
-      state.rootExpr?.mapM λ expr => state.withRootContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let parent? ← if parentExpr then
-      state.parentExpr?.mapM λ expr => state.withParentContext do
-        serializeExpression options (← instantiateAll expr)
-    else
-      pure .none
-  let goals ← if goals then
-      goalSerialize state options
-    else
-      pure #[]
-  let extraMVars ← extraMVars.mapM λ mvarId => do
-    let mvarId: MVarId := { name := mvarId.toName }
-    let .some _ ← mvarId.findDecl? | return {}
-    state.withContext mvarId do
-      let .some expr ← getExprMVarAssignment? mvarId | return {}
-      serializeExpression options (← instantiateAll expr)
-  return {
-    root?,
-    parent?,
-    goals,
-    extraMVars,
-  }
+def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
+  runMetaM do
+    state.restoreMetaM
+    return {
+      root? := ← state.rootExpr?.mapM (λ expr =>
+        state.withRootContext do
+          serializeExpression options (← instantiateAll expr)),
+      parent? := ← state.parentExpr?.mapM (λ expr =>
+        state.withParentContext do
+          serializeExpression options (← instantiateAll expr)),
+    }

@[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
@ -207,14 +188,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: Stri
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
-@[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
-  let expr ← match (← parseTermM expr) with
-    | .ok syn => pure syn
-    | .error error => return .parseError error
-  runTermElabM do
-    state.restoreElabM
-    state.tryTacticM goal (Tactic.evalDraft expr)
@[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
  runTermElabM <| state.tryLet goal binderName type
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -5,7 +5,6 @@ Note that no command other than `InteractionError` may have `error` as one of
 its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
-import Lean.Data.Position

 namespace Pantograph.Protocol

@ -122,13 +121,11 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
  name: String
-  -- Show the value expressions; By default definitions values are shown and
-  -- theorem values are hidden.
+  -- If true/false, show/hide the value expressions; By default definitions
+  -- values are shown and theorem values are hidden.
  value?: Option Bool := .some false
-  -- Show the type and value dependencies
+  -- If true, show the type and value dependencies
  dependency?: Option Bool := .some false
-  -- Show source location
-  source?: Option Bool := .some false
  deriving Lean.FromJson
 -- See `InductiveVal`
 structure InductInfo where
@ -175,11 +172,6 @@ structure EnvInspectResult where
  inductInfo?:      Option InductInfo      := .none
  constructorInfo?: Option ConstructorInfo := .none
  recursorInfo?:    Option RecursorInfo    := .none
-
-  -- Location in source
-  sourceUri?: Option String := .none
-  sourceStart?: Option Lean.Position := .none
-  sourceEnd?: Option Lean.Position := .none
  deriving Lean.ToJson

 structure EnvAdd where
@ -237,7 +229,6 @@ structure GoalTactic where
  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
  binderName?: Option String := .none
@ -280,23 +271,12 @@ structure GoalDeleteResult where

 structure GoalPrint where
  stateId: Nat
-
-  -- Print root?
-  rootExpr?: Option Bool := .some False
-  -- Print the parent expr?
-  parentExpr?: Option Bool := .some False
-  -- Print goals?
-  goals?: Option Bool := .some False
-  -- Print values of extra mvars?
-  extraMVars?: Option (Array String) := .none
  deriving Lean.FromJson
 structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
  -- The filling expression of the parent goal
-  parent?: Option Expression := .none
-  goals: Array Goal := #[]
-  extraMVars: Array Expression := #[]
+  parent?: Option Expression
  deriving Lean.ToJson

 -- Diagnostic Options, not available in REPL
@ -328,13 +308,11 @@ structure FrontendProcess where
  -- One of these two must be supplied: Either supply the file name or the content.
  fileName?: Option String := .none
  file?: Option String := .none
-  -- collect tactic invocations
+  -- If set to true, collect tactic invocations
  invocations: Bool := false
-  -- collect `sorry`s
+  -- If set to true, collect `sorry`s
  sorrys: Bool := false
-  -- collect type errors
-  typeErrorsAsGoals: Bool := false
-  -- list new constants from each compilation step
+  -- If set to true, extract new constants
  newConstants: Bool := false
  deriving Lean.FromJson
 structure InvokedTactic where
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@ -27,38 +27,5 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
  goal.assign expr
  Elab.Tactic.replaceMainGoal nextGoals

-def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr := do
-  Meta.transform src λ
-    | .app (.app (.const ``sorryAx ..) type) .. => do
-      let type ← instantiateMVars type
-      if type.hasSorry then
-        throwError s!"Coupling is not allowed in draft tactic: {← Meta.ppExpr type}"
-      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
-      modify (mvar.mvarId! :: .)
-      pure $ .done mvar
-    | _ => pure .continue
-
-- Given a complete (no holes) expression, extract the sorry's from it and convert them into goals.
-def draft (goal : MVarId) (expr : Expr) : MetaM (List MVarId) := do
-  goal.checkNotAssigned `Pantograph.Tactic.draft
-  let exprType ← Meta.inferType expr
-  let goalType ← goal.getType
-  unless ← Meta.isDefEq goalType exprType do
-    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
-
-  let (expr', holes) ← sorryToHole expr |>.run []
-  goal.assign expr'
-  return holes.reverse
-
-def evalDraft : Elab.Tactic.Tactic := fun stx ↦ Elab.Tactic.withMainContext do
-  let target ← Elab.Tactic.getMainTarget
-  let goal ← Elab.Tactic.getMainGoal
-  let (expr, holeGoals) ← Elab.Tactic.elabTermWithHoles stx
-    (expectedType? := .some target)
-    (tagSuffix := .anonymous)
-    (allowNaturalHoles := true)
-  let draftGoals ← draft goal expr
-  Elab.Tactic.replaceMainGoal $ holeGoals ++ draftGoals
-

 end Pantograph.Tactic
--- a/Pantograph/Tactic/Prograde.lean
+++ b/Pantograph/Tactic/Prograde.lean
@ -40,7 +40,7 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
  let fvarId ← mkFreshFVarId
  let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
  let mvarUpstream ←
-    Meta.withLCtx lctxUpstream #[] do
+    withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
      Meta.withNewLocalInstances #[.fvar fvarId] 0 do
        let mvarUpstream ← mkUpstreamMVar mvarId
        --let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,6 +1,6 @@
 namespace Pantograph

@[export pantograph_version]
-def version := "0.2.25"
+def version := "0.2.22"

 end Pantograph
--- a/Repl.lean
+++ b/Repl.lean
@ -145,27 +145,24 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    let .some goal := goalState.goals.get? args.goalId |
      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM 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
+      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
+      | .some tactic, .none, .none, .none, .none, .none => do
        pure <| Except.ok <| ← goalState.tryTactic goal tactic
-      | .none, .some expr, .none, .none, .none, .none, .none => do
+      | .none, .some expr, .none, .none, .none, .none => do
        pure <| Except.ok <| ← goalState.tryAssign goal expr
-      | .none, .none, .some type, .none, .none, .none, .none => do
+      | .none, .none, .some type, .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
+      | .none, .none, .none, .some type, .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
+      | .none, .none, .none, .none, .some pred, .none => do
        pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true, .none => do
+      | .none, .none, .none, .none, .none, .some true => do
        pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false, .none => do
+      | .none, .none, .none, .none, .none, .some false => 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, calc, conv} must be supplied"
        pure $ Except.error $ error
    match nextGoalState? with
@ -226,13 +223,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    let state ← get
    let .some goalState := state.goalStates[args.stateId]? |
      return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    let result ← runMetaInMainM <| goalPrint
-        goalState
-        (rootExpr := args.rootExpr?.getD False)
-        (parentExpr := args.parentExpr?.getD False)
-        (goals := args.goals?.getD False)
-        (extraMVars := args.extraMVars?.getD #[])
-        (options := state.options)
+    let result ← runMetaInMainM <| goalPrint goalState state.options
    return .ok result
  goal_save (args: Protocol.GoalSave): MainM (CR Protocol.GoalSaveResult) := do
    let state ← get
@ -268,7 +259,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
          else
            pure .none
        let sorrys ← if args.sorrys then
-            Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
+            Frontend.collectSorrys step
          else
            pure []
        let messages ← step.messageStrings
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -48,12 +48,6 @@ namespace Condensed
 deriving instance BEq, Repr for LocalDecl
 deriving instance BEq, Repr for Goal

-- Enable string interpolation
-instance : ToString FVarId where
-  toString id := id.name.toString
-instance : ToString MVarId where
-  toString id := id.name.toString
-
 protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
  {
    decl with fvarId := { name := .anonymous }
@ -149,8 +143,6 @@ def runTest (t: TestT m Unit): m LSpec.TestSeq :=
  Prod.snd <$> t.run LSpec.TestSeq.done
 def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
  t.run LSpec.TestSeq.done
-def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
-  runCoreMSeq env (runTest coreM) options

 end Monadic

--- a/Test/Delate.lean
+++ b/Test/Delate.lean
@ -35,7 +35,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
    ("Nat.add", "(:forall a (:c Nat) (:forall a (:c Nat) (:c Nat)))"),
    -- These ones are normal and easy
    ("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
-    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :i) :i)"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
    -- Handling of higher order types
    ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
    ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
@ -50,8 +50,8 @@ 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)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
    ("(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)))"),
  ]
  entries.foldlM (λ suites (source, levels, target) =>
@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
            .default)
        .implicit)
      .implicit,
-      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
    ),
  ]
  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -97,26 +97,11 @@ def test_inspect: IO LSpec.TestSeq := do
    ) LSpec.TestSeq.done
  runCoreMSeq env inner

-def test_symbol_location : TestT IO Unit := do
-  let env: Environment ← importModules
-    (imports := #[`Init])
-    (opts := {})
-    (trustLevel := 1)
-  addTest $ ← runTestCoreM env do
-    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
-    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
-
-    -- 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
-
 def suite: List (String × IO LSpec.TestSeq) :=
  [
    ("Catalog", test_catalog),
    ("Symbol Visibility", test_symbol_visibility),
    ("Inspect", test_inspect),
-    ("Symbol Location", runTest test_symbol_location),
  ]

 end Pantograph.Test.Environment
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@ -6,12 +6,11 @@ import Test.Common
 open Lean Pantograph
 namespace Pantograph.Test.Frontend

-def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
-    : MetaM (List GoalState) := do
+def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
  let filename := "<anonymous>"
  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
  let m := Frontend.mapCompilationSteps λ step => do
-    return (step.before, ← Frontend.collectSorrys step options)
+    return (step.before, ← Frontend.collectSorrys step)
  let li ← m.run context |>.run' state
  let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
    if sorrys.isEmpty then
@ -182,10 +181,9 @@ def test_capture_type_mismatch : TestT MetaM Unit := do
  let input := "
 def mystery (k: Nat) : Nat := true
  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
+  let goalStates ← (collectSorrysFromSource input).run' {}
  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
+  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
    {
      target := { pp? := "Nat" },
      vars := #[{
@ -195,16 +193,6 @@ def mystery (k: Nat) : Nat := true
    }
  ]

-def test_capture_type_mismatch_in_binder : TestT MetaM Unit := do
-  let input := "
-example (p: Prop) (h: (∀ (x: Prop), Nat) → p): p := h (λ (y: Nat) => 5)
-  "
-  let options := { collectTypeErrors := true }
-  let goalStates ← (collectSorrysFromSource input options).run' {}
-  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
-  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
-  ]
-
 def collectNewConstants (source: String) : MetaM (List (List Name)) := do
  let filename := "<anonymous>"
  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
@ -239,7 +227,6 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
    ("sorry_in_coupled", test_sorry_in_coupled),
    ("environment_capture", test_environment_capture),
    ("capture_type_mismatch", test_capture_type_mismatch),
-    --("capture_type_mismatch_in_binder", test_capture_type_mismatch_in_binder),
    ("collect_one_constant", test_collect_one_constant),
    ("collect_one_theorem", test_collect_one_theorem),
  ]
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@ -72,8 +72,8 @@ def test_tactic : Test :=
     ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
    step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
     ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
-    step "goal.print" [("stateId", .num 1), ("parentExpr", .bool true), ("rootExpr", .bool true)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
+    step "goal.print" [("stateId", .num 1)]
+     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
    step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
     ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
  ]
@ -90,27 +90,27 @@ def test_automatic_mode (automatic: Bool): Test :=
    ],
  }
  let goal2l: Protocol.Goal := {
-    name := "_uniq.61",
+    name := "_uniq.59",
    userName? := .some "inl",
    target := { pp? := .some "q ∨ p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
    ],
  }
  let goal2r: Protocol.Goal := {
-    name := "_uniq.74",
+    name := "_uniq.72",
    userName? := .some "inr",
    target := { pp? := .some "q ∨ p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.62", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
+      { name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
    ],
  }
  let goal3l: Protocol.Goal := {
-    name := "_uniq.80",
+    name := "_uniq.78",
    userName? := .some "inl.h",
    target := { pp? := .some "p" },
    vars := varsPQ ++ #[
-      { name := "_uniq.49", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
+      { name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
    ],
  }
  [
@ -171,11 +171,10 @@ def test_frontend_process : Test :=
    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
    step "frontend.process"
      [
-        ("file",              .str file),
-        ("invocations",       .bool true),
-        ("sorrys",            .bool false),
-        ("typeErrorsAsGoals", .bool false),
-        ("newConstants",      .bool false),
+        ("file", .str file),
+        ("invocations", .bool true),
+        ("sorrys", .bool false),
+        ("newConstants", .bool false),
      ]
     ({
       units := [{
@ -216,7 +215,6 @@ def test_frontend_process_sorry : Test :=
        ("file", .str file),
        ("invocations", .bool false),
        ("sorrys", .bool true),
-        ("typeErrorsAsGoals", .bool false),
        ("newConstants", .bool false),
      ]
     ({
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -53,7 +53,6 @@ def main (args: List String) := do
    ("Proofs", Proofs.suite env_default),
    ("Delate", Delate.suite env_default),
    ("Serial", Serial.suite env_default),
-    ("Tactic/Assign", Tactic.Assign.suite env_default),
    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
    ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -239,7 +239,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Roundtrip
@ -253,7 +253,7 @@ def test_partial_continuation: TestM Unit := do
      return ()
    | .ok state => pure state
  addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
+    #[.some "2 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
  addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone

  -- Continuation should fail if the state does not exist:
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -97,7 +97,7 @@ def test_identity: TestM Unit := do
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
    #[inner])
  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")

 -- Individual test cases
@ -241,15 +241,13 @@ def test_or_comm: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [state1g0] := state1.goals | fail "Should have 1 goal"
-  let (fvP, fvQ, fvH) ← state1.withContext state1g0 do
-    let lctx ← getLCtx
-    let #[fvP, fvQ, fvH] := lctx.getFVarIds.map (toString ·.name) |
-      panic! "Incorrect number of decls"
-    pure (fvP, fvQ, fvH)
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
    #[{
-      name := state1g0.name.toString,
+      name := state1g0,
      target := { pp? := .some "q ∨ p" },
      vars := #[
        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
@ -261,7 +259,7 @@ def test_or_comm: TestM Unit := do
  addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone

  let state1parent ← state1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
  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
@ -271,16 +269,14 @@ def test_or_comm: TestM Unit := do
      return ()
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[branchGoal "inl" "p", branchGoal "inr" "q"])
-  let [state2g0, state2g1] := state2.goals |
-    fail s!"Should have 2 goals, but it has {state2.goals.length}"
-  let (caseL, caseR) := (state2g0.name.toString, state2g1.name.toString)
+  let (caseL, caseR) := ("_uniq.64", "_uniq.77")
  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
    #[caseL, caseR])
  addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
  addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone

  let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
  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}))"
@ -296,9 +292,8 @@ 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!)
-  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}))")
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
  addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
  let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
    | .success state => pure state
@ -564,15 +559,12 @@ def test_nat_zero_add: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
    #[
-      buildNamedGoal mvarMotive.name.toString  [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString   [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString  [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
    ])

  let tactic := "exact n"
@ -655,15 +647,13 @@ def test_nat_zero_add_alt: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [mvarMotive, mvarMajor, mvarInduct, mvarConduit] := state2.goals |
-      fail "Incorrect number of goals"
-  let .num _ major := mvarMajor.name | fail "Incorrect form of mvar id"
+  let major := "_uniq.68"
  addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
    #[
-      buildNamedGoal mvarMotive.name.toString [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal mvarMajor.name.toString [("n", "Nat")] "Nat",
-      buildNamedGoal mvarInduct.name.toString [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal mvarConduit.name.toString [("n", "Nat")] s!"?motive ?m.{major} = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal major [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
    ])

  let tactic := "intro x"
@ -680,7 +670,8 @@ def test_nat_zero_add_alt: TestM Unit := do
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
-  let [eqL, eqR, eqT] := state3m2.goals | fail "Incorrect number of goals"
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
  let state2b ← match state3m2.resume [conduit] with
    | .ok state => pure state
@ -690,26 +681,20 @@ def test_nat_zero_add_alt: TestM Unit := do

  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
-  let fvN ← state2b.withContext conduit do
-    let lctx ← getLCtx
-    pure $ lctx.getFVarIds.get! 0 |>.name
+  let fvN := "_uniq.63"
  let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
-  let substOf (mvarId: MVarId) := s!"(:subst (:mv {mvarId.name}) (:fv {fvN}) (:mv {mvarMajor}))"
-  let .num _ nL := eqL.name | fail "Incorrect form of mvar id"
-  let .num _ nR := eqR.name | fail "Incorrect form of mvar id"
-  let nL' := nL + 4
-  let nR' := nR + 5
+  let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
    #[
      {
-        name := mvarConduit.name.toString,
+        name := "_uniq.70",
        userName? := .some "conduit",
        target := {
-          pp? := .some s!"(?m.{nL'} ?m.{major} = ?m.{nR'} ?m.{major}) = (n + 0 = n)",
+          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
        },
        vars := #[{
-          name := fvN.toString,
+          name := fvN,
          userName := "n",
          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
        }],
@ -735,6 +720,7 @@ def test_tactic_failure_unresolved_goals : TestM Unit := do
  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"]

+
 def test_tactic_failure_synthesize_placeholder : TestM Unit := do
  let state? ← startProof (.expr "∀ (p q r : Prop) (h : p → q), q ∧ r")
  let state0 ← match state? with
@ -750,25 +736,20 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()

-  let iex : InternalExceptionId := { idx := 4 }
-  IO.println s!"{← iex.getName}"
  let tactic := "simpa [h] using And.imp_left h _"
-  --let state2 ← match ← state1.tacticOn 0 tactic with
-  --  | .success state => pure state
-  --  | other => do
-  --    addTest $ assertUnreachable $ other.toString
-  --    return ()
+  let state2 ← match ← state1.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()

-  -- Volatile behaviour. This easily changes across Lean versions
-
-  --checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
-  --  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]
+  checkEq tactic ((← state2.serializeGoals).map (·.devolatilize))  #[
+    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]

 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  let tests := [
--- a/Test/Tactic.lean
+++ b/Test/Tactic.lean
@ -1,4 +1,3 @@
-import Test.Tactic.Assign
 import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse
--- a/Test/Tactic/Assign.lean
+++ b/Test/Tactic/Assign.lean
@ -1,33 +0,0 @@
-import Lean.Meta
-import Lean.Elab
-import LSpec
-import Test.Common
-
-open Lean
-
-namespace Pantograph.Test.Tactic.Assign
-
-def test_draft : TestT Elab.TermElabM Unit := do
-  let expr := "forall (p : Prop), (p ∨ p) ∨ p"
-  let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
-  let expr ← parseSentence expr
-  Meta.forallTelescope expr $ λ _ body => do
-    let skeleton' ← match Parser.runParserCategory
-      (env := ← MonadEnv.getEnv)
-      (catName := `term)
-      (input := skeleton)
-      (fileName := ← getFileName) with
-      | .ok syn => pure syn
-      | .error error => throwError "Failed to parse: {error}"
-    -- Apply the tactic
-    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-    let tactic := Tactic.evalDraft skeleton'
-    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
-
-def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
-  [
-    ("draft", test_draft),
-  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
-
-end Pantograph.Test.Tactic.Assign
--- a/Test/Tactic/Congruence.lean
+++ b/Test/Tactic/Congruence.lean
@ -28,7 +28,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
    let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
    addTest $ LSpec.check "apply" (results.length = 0)
    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(List.reverse ?a₁ = List.reverse ?a₂) = (l1.reverse = l2.reverse)")
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
 def test_congr_arg : TestT Elab.TermElabM Unit := do
  let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
  let expr ← parseSentence expr
@ -37,7 +37,7 @@ def test_congr_arg : TestT Elab.TermElabM Unit := do
    let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
      [
-        (`α, "Sort ?u.73"),
+        (`α, "Sort ?u.70"),
        (`a₁, "?α"),
        (`a₂, "?α"),
        (`f, "?α → Nat"),
@ -52,7 +52,7 @@ def test_congr_fun : TestT Elab.TermElabM Unit := do
    let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
      [
-        (`α, "Sort ?u.165"),
+        (`α, "Sort ?u.159"),
        (`f₁, "?α → Nat"),
        (`f₂, "?α → Nat"),
        (`h, "?f₁ = ?f₂"),
--- a/Test/Tactic/MotivatedApply.lean
+++ b/Test/Tactic/MotivatedApply.lean
@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
        "Nat → Prop",
        "Nat",
        "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.74 = (n + 0 = n)",
+        "?motive ?m.67 = (n + 0 = n)",
      ])
    addTest test

@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
    let tactic := Tactic.evalMotivatedApply recursor
    let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 74
+    let majorId := 67
    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
      [
        "Nat → Prop",
@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do

    addTest $ ← conduit.withContext do
      let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(Nat.add ?m.{majorId} + 0 = ?m.149 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")

 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
  [
--- a/doc/repl.md
+++ b/doc/repl.md
@ -33,7 +33,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
    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.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
  Execute continuation/resumption
  - `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
@ -45,12 +44,11 @@ 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>], invocations:
-  <bool>, 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
-  (`"sorrys": true`), and new constants (`"newConstants": true`). In the case of
-  `sorrys`, this command additionally outputs the position of each captured
-  `sorry`.
+  <bool>, sorrys: <bool>, newConstants: <bool> }`: Executes the Lean frontend on
+  a file, collecting the tactic invocations (`"invocations": true`), 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`.

 ## Errors

--- a/flake.lock
+++ b/flake.lock
@ -42,11 +42,11 @@
        "nixpkgs": "nixpkgs"
      },
      "locked": {
-        "lastModified": 1736388194,
-        "narHash": "sha256-ymSrd/A8Pw+9FzbxUbR7CkFHLJK1b4SnFFWg/1e0JeE=",
+        "lastModified": 1731711316,
+        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
        "owner": "lenianiva",
        "repo": "lean4-nix",
-        "rev": "90f496bc0694fb97bdfa6adedfc2dc2c841a4cf2",
+        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
        "type": "github"
      },
      "original": {
--- a/flake.nix
+++ b/flake.nix
@ -18,89 +18,82 @@
    lean4-nix,
    lspec,
    ...
-  }:
-    flake-parts.lib.mkFlake {inherit inputs;} {
-      flake = {
+  } : flake-parts.lib.mkFlake { inherit inputs; } {
+    flake = {
+    };
+    systems = [
+      "aarch64-linux"
+      "aarch64-darwin"
+      "x86_64-linux"
+      "x86_64-darwin"
+    ];
+    perSystem = { system, pkgs, ... }: let
+      pkgs = import nixpkgs {
+        inherit system;
+        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
      };
-      systems = [
-        "aarch64-linux"
-        "aarch64-darwin"
-        "x86_64-linux"
-        "x86_64-darwin"
-      ];
-      perSystem = {
-        system,
-        pkgs,
-        ...
-      }: let
-        pkgs = import nixpkgs {
-          inherit system;
-          overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
-        };
-        lspecLib = pkgs.lean.buildLeanPackage {
-          name = "LSpec";
-          roots = ["Main" "LSpec"];
-          src = "${lspec}";
-        };
-        project = pkgs.lean.buildLeanPackage {
-          name = "Pantograph";
-          roots = ["Pantograph"];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path)
-              && !(pkgs.lib.hasSuffix "Repl.lean" path);
-          });
-        };
-        repl = pkgs.lean.buildLeanPackage {
-          name = "Repl";
-          roots = ["Main" "Repl"];
-          deps = [project];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "/Test/" path)
-              && !(pkgs.lib.hasSuffix ".md" path);
-          });
-        };
-        test = pkgs.lean.buildLeanPackage {
-          name = "Test";
-          # NOTE: The src directory must be ./. since that is where the import
-          # root begins (e.g. `import Test.Environment` and not `import
-          # Environment`) and thats where `lakefile.lean` resides.
-          roots = ["Test.Main"];
-          deps = [lspecLib repl];
-          src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
-            src = ./.;
-            filter = path: type:
-              !(pkgs.lib.hasInfix "Pantograph" path);
-          });
-        };
-      in rec {
-        packages = {
-          inherit (pkgs.lean) lean lean-all;
-          inherit (project) sharedLib iTree;
-          inherit (repl) executable;
-          default = repl.executable;
-        };
-        legacyPackages = {
-          inherit project;
-          leanPkgs = pkgs.lean;
-        };
-        checks = {
-          test =
-            pkgs.runCommand "test" {
-              buildInputs = [test.executable pkgs.lean.lean-all];
-            } ''
-              #export LEAN_SRC_PATH="${./.}"
-              ${test.executable}/bin/test > $out
-            '';
-        };
-        formatter = pkgs.alejandra;
-        devShells.default = pkgs.mkShell {
-          buildInputs = [pkgs.lean.lean-all pkgs.lean.lean];
-        };
+      lspecLib = pkgs.lean.buildLeanPackage {
+        name = "LSpec";
+        roots = [ "Main" "LSpec" ];
+        src = "${lspec}";
+      };
+      project = pkgs.lean.buildLeanPackage {
+        name = "Pantograph";
+        roots = [ "Pantograph" ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path) &&
+            !(pkgs.lib.hasSuffix "Repl.lean" path);
+        });
+      };
+      repl = pkgs.lean.buildLeanPackage {
+        name = "Repl";
+        roots = [ "Main" "Repl" ];
+        deps = [ project ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "/Test/" path) &&
+            !(pkgs.lib.hasSuffix ".md" path);
+        });
+      };
+      test = pkgs.lean.buildLeanPackage {
+        name = "Test";
+        # NOTE: The src directory must be ./. since that is where the import
+        # root begins (e.g. `import Test.Environment` and not `import
+        # Environment`) and thats where `lakefile.lean` resides.
+        roots = [ "Test.Main" ];
+        deps = [ lspecLib repl ];
+        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
+          src = ./.;
+          filter = path: type:
+            !(pkgs.lib.hasInfix "Pantograph" path);
+        });
+      };
+    in rec {
+      packages = {
+        inherit (pkgs.lean) lean lean-all;
+        inherit (project) sharedLib iTree;
+        inherit (repl) executable;
+        default = repl.executable;
+      };
+      legacyPackages = {
+        inherit project;
+        leanPkgs = pkgs.lean;
+      };
+      checks = {
+        test = pkgs.runCommand "test" {
+          buildInputs = [ test.executable pkgs.lean.lean-all ];
+        } ''
+          #export LEAN_SRC_PATH="${./.}"
+          ${test.executable}/bin/test > $out
+        '';
+      };
+      devShells.default = pkgs.mkShell {
+        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
      };
    };
+  };
 }
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.12.0