From 9894ad7c7e2a8e7fde305e1a542f708fd1481c5e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 26 Nov 2024 12:16:14 -0800
Subject: [PATCH 01/28] refactor: InfoTree functions

---
 Pantograph/Frontend.lean          |  2 +-
 Pantograph/Frontend/Elab.lean     | 82 ++-----------------------------
 Pantograph/Frontend/InfoTree.lean | 81 ++++++++++++++++++++++++++++++
 3 files changed, 85 insertions(+), 80 deletions(-)
 create mode 100644 Pantograph/Frontend/InfoTree.lean

diff --git a/Pantograph/Frontend.lean b/Pantograph/Frontend.lean
index fd91823..9a41567 100644
--- a/Pantograph/Frontend.lean
+++ b/Pantograph/Frontend.lean
@@ -1,4 +1,4 @@
-/- Adapted from lean-training-data by semorrison -/
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.Elab
+import Pantograph.Frontend.InfoTree
 import Pantograph.Frontend.MetaTranslate
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index ceecfae..b3173a7 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -7,77 +7,10 @@ import Pantograph.Frontend.Basic
 import Pantograph.Frontend.MetaTranslate
 import Pantograph.Goal
 import Pantograph.Protocol
+import Pantograph.Frontend.InfoTree
 
 open Lean
 
-namespace Lean.Elab.Info
-/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
-protected def stx? : Info → Option Syntax
-  | .ofTacticInfo         info => info.stx
-  | .ofTermInfo           info => info.stx
-  | .ofCommandInfo        info => info.stx
-  | .ofMacroExpansionInfo info => info.stx
-  | .ofOptionInfo         info => info.stx
-  | .ofFieldInfo          info => info.stx
-  | .ofCompletionInfo     info => info.stx
-  | .ofUserWidgetInfo     info => info.stx
-  | .ofCustomInfo         info => info.stx
-  | .ofFVarAliasInfo      _    => none
-  | .ofFieldRedeclInfo    info => info.stx
-  | .ofOmissionInfo       info => info.stx
-/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
-protected def isOriginal (i : Info) : Bool :=
-  match i.stx? with
-  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
-  | some stx => match stx.getHeadInfo with
-    | .original .. => true
-    | _ => false
-end Lean.Elab.Info
-
-namespace Lean.Elab.TacticInfo
-
-/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
-def name? (t : TacticInfo) : Option Name :=
-  match t.stx with
-  | Syntax.node _ n _ => some n
-  | _ => none
-/-- Decide whether a tactic is "substantive",
-or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
-def isSubstantive (t : TacticInfo) : Bool :=
-  match t.name? with
-  | none => false
-  | some `null => false
-  | some ``cdot => false
-  | some ``cdotTk => false
-  | some ``Lean.Parser.Term.byTactic => false
-  | some ``Lean.Parser.Tactic.tacticSeq => false
-  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
-  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
-  | some ``Lean.Parser.Tactic.paren => false
-  | _ => true
-
-end Lean.Elab.TacticInfo
-
-namespace Lean.Elab.InfoTree
-
-/--
-Keep `.node` nodes and `.hole` nodes satisfying predicates.
-
-Returns a `List InfoTree`, although in most situations this will be a singleton.
--/
-partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
-    InfoTree → List InfoTree
-  | .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)).join.toPArray']
-    else
-      (children.toList.map (filter p m)).join
-  | .hole mvar => if m mvar then [.hole mvar] else []
-
-end Lean.Elab.InfoTree
-
-
 namespace Pantograph.Frontend
 
 -- Info tree filtering functions
@@ -131,19 +64,10 @@ protected def usedConstants (t: TacticInvocation) : NameSet :=
 
 end TacticInvocation
 
-/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
-    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
-  match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
-  | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
-  | _ => []
-
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
 private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
-  let infos := findAllInfo t none fun i => match i with
+  let infos := t.findAllInfo none fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -178,7 +102,7 @@ structure InfoWithContext where
   context?: Option Elab.ContextInfo := .none
 
 private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
-  let infos := findAllInfo t none fun i => match i with
+  let infos := t.findAllInfo none fun i => match i with
     | .ofTermInfo { expectedType?, expr, stx, .. } =>
       expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
     | .ofTacticInfo { stx, goalsBefore, .. } =>
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
new file mode 100644
index 0000000..4e60710
--- /dev/null
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -0,0 +1,81 @@
+/- Adapted from lean-training-data by semorrison -/
+import Lean.Elab.InfoTree
+import Lean.Parser.Term
+
+open Lean
+
+namespace Lean.Elab.Info
+/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
+protected def stx? : Info → Option Syntax
+  | .ofTacticInfo         info => info.stx
+  | .ofTermInfo           info => info.stx
+  | .ofCommandInfo        info => info.stx
+  | .ofMacroExpansionInfo info => info.stx
+  | .ofOptionInfo         info => info.stx
+  | .ofFieldInfo          info => info.stx
+  | .ofCompletionInfo     info => info.stx
+  | .ofUserWidgetInfo     info => info.stx
+  | .ofCustomInfo         info => info.stx
+  | .ofFVarAliasInfo      _    => none
+  | .ofFieldRedeclInfo    info => info.stx
+  | .ofOmissionInfo       info => info.stx
+/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
+protected def isOriginal (i : Info) : Bool :=
+  match i.stx? with
+  | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
+  | some stx => match stx.getHeadInfo with
+    | .original .. => true
+    | _ => false
+end Lean.Elab.Info
+
+namespace Lean.Elab.TacticInfo
+
+/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
+def name? (t : TacticInfo) : Option Name :=
+  match t.stx with
+  | Syntax.node _ n _ => some n
+  | _ => none
+/-- Decide whether a tactic is "substantive",
+or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
+def isSubstantive (t : TacticInfo) : Bool :=
+  match t.name? with
+  | none => false
+  | some `null => false
+  | some ``cdot => false
+  | some ``cdotTk => false
+  | some ``Lean.Parser.Term.byTactic => false
+  | some ``Lean.Parser.Tactic.tacticSeq => false
+  | some ``Lean.Parser.Tactic.tacticSeq1Indented => false
+  | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
+  | some ``Lean.Parser.Tactic.paren => false
+  | _ => true
+
+end Lean.Elab.TacticInfo
+
+namespace Lean.Elab.InfoTree
+
+/--
+Keep `.node` nodes and `.hole` nodes satisfying predicates.
+
+Returns a `List InfoTree`, although in most situations this will be a singleton.
+-/
+partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+    InfoTree → List InfoTree
+  | .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)).join.toPArray']
+    else
+      (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. -/
+partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+  match t with
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .node i children  =>
+      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+  | _ => []
+
+end Lean.Elab.InfoTree

From 9ede3cf7175db43e1e660f64e58eaac4251eed8b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 15:38:03 -0800
Subject: [PATCH 02/28] feat: InfoTree printing

---
 Pantograph/Frontend/InfoTree.lean | 73 ++++++++++++++++++++++++-------
 1 file changed, 58 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 4e60710..aa99db2 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -1,12 +1,19 @@
-/- Adapted from lean-training-data by semorrison -/
+/- Adapted from lean-training-data -/
 import Lean.Elab.InfoTree
 import Lean.Parser.Term
+import Lean.PrettyPrinter
 
 open Lean
 
-namespace Lean.Elab.Info
+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" ++ .)
+
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
-protected def stx? : Info → Option Syntax
+protected def Info.stx? : Info → Option Syntax
   | .ofTacticInfo         info => info.stx
   | .ofTermInfo           info => info.stx
   | .ofCommandInfo        info => info.stx
@@ -20,24 +27,35 @@ protected def stx? : Info → Option Syntax
   | .ofFieldRedeclInfo    info => info.stx
   | .ofOmissionInfo       info => info.stx
 /-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
-protected def isOriginal (i : Info) : Bool :=
+protected def Info.isOriginal (i : Info) : Bool :=
   match i.stx? with
   | none => true   -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
   | some stx => match stx.getHeadInfo with
     | .original .. => true
     | _ => false
-end Lean.Elab.Info
 
-namespace Lean.Elab.TacticInfo
+def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO Format :=
+  ctx.runMetaM lctx (do Meta.ppExpr (← instantiateMVars e))
+
+def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do
+  let stx := (← ctx.ppSyntax {} info.stx).pretty
+  return s!"{stx}\n{elaboratorToString info.elaborator}"
+
+def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do
+  let stx := (← ctx.ppSyntax info.lctx info.stx).pretty
+  let expectedType ← info.expectedType?.mapM fun ty => do
+    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}"
+  let expr := (← ctx.ppExpr info.lctx info.expr).pretty
+  return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}"
 
 /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
-def name? (t : TacticInfo) : Option Name :=
+def TacticInfo.name? (t : TacticInfo) : Option Name :=
   match t.stx with
   | Syntax.node _ n _ => some n
   | _ => none
 /-- Decide whether a tactic is "substantive",
 or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
-def isSubstantive (t : TacticInfo) : Bool :=
+def TacticInfo.isSubstantive (t : TacticInfo) : Bool :=
   match t.name? with
   | none => false
   | some `null => false
@@ -49,17 +67,22 @@ def isSubstantive (t : TacticInfo) : Bool :=
   | some ``Lean.Parser.Tactic.«tactic_<;>_» => false
   | some ``Lean.Parser.Tactic.paren => false
   | _ => true
-
-end Lean.Elab.TacticInfo
-
-namespace Lean.Elab.InfoTree
+def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format :=
+  ctx.runMetaM {} try
+    Lean.PrettyPrinter.ppTactic ⟨info.stx⟩
+  catch _ =>
+    pure "<failed to pretty print>"
+def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do
+  let name := i.name?
+  let stx := Format.pretty (← i.pp ctx)
+  return s!"{stx}\n{name} {stx}"
 
 /--
 Keep `.node` nodes and `.hole` nodes satisfying predicates.
 
 Returns a `List InfoTree`, although in most situations this will be a singleton.
 -/
-partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
+partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
     InfoTree → List InfoTree
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
@@ -70,7 +93,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
     List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
   match t with
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
@@ -78,4 +101,24 @@ partial def findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred
       (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
   | _ => []
 
-end Lean.Elab.InfoTree
+@[export pantograph_infotree_to_string_m]
+partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do
+  match t with
+  | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
+  | .node info children =>
+    if let some ctx := ctx? then
+      let node : Option String ← match info with
+      | .ofTermInfo    info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}")
+      | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}")
+      | .ofTacticInfo  info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}")
+      | _                   => pure none
+      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."
+  | .hole mvarId =>
+    if let some ctx := ctx? then
+      let payload := (← ctx.runMetaM {} (do Meta.ppGoal mvarId)).pretty
+      return s!"[hole] {payload}"
+    else throw <| IO.userError "No `ContextInfo` available."
+
+end Lean.Elab

From b950dc9b1a278aabfb7fb2a19be60d7b1e636494 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 22:51:55 -0800
Subject: [PATCH 03/28] fix: Verbose printing of infotree

---
 Pantograph/Frontend/InfoTree.lean | 32 +++++++++++++++++++------------
 1 file changed, 20 insertions(+), 12 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index aa99db2..3b57a54 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -9,7 +9,7 @@ namespace Lean.Elab
 
 private def elaboratorToString : Name → String
   | .anonymous => ""
-  | n => s!"[{n}]"
+  | n => s!"⟨{n}⟩ "
 private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
@@ -39,14 +39,14 @@ def ContextInfo.ppExpr (ctx : ContextInfo) (lctx : LocalContext) (e : Expr) : IO
 
 def CommandInfo.toString (info : CommandInfo) (ctx : ContextInfo) : IO String := do
   let stx := (← ctx.ppSyntax {} info.stx).pretty
-  return s!"{stx}\n{elaboratorToString info.elaborator}"
+  return s!"{elaboratorToString info.elaborator}\n{stx}"
 
 def TermInfo.toString (info : TermInfo) (ctx : ContextInfo) : IO String := do
   let stx := (← ctx.ppSyntax info.lctx info.stx).pretty
-  let expectedType ← info.expectedType?.mapM fun ty => do
-    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}"
+  let expectedType := (← info.expectedType?.mapM fun ty => do
+    pure s!": {(← ctx.ppExpr info.lctx ty).pretty}").getD ""
   let expr := (← ctx.ppExpr info.lctx info.expr).pretty
-  return s!"{stx}\n{elaboratorToString info.elaborator}{expr}{expectedType}"
+  return s!"{elaboratorToString info.elaborator}{expr}{expectedType}\n{stx}"
 
 /-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
 def TacticInfo.name? (t : TacticInfo) : Option Name :=
@@ -75,7 +75,7 @@ def TacticInfo.pp (info : TacticInfo) (ctx : ContextInfo) : IO Format :=
 def TacticInfo.toString (i : TacticInfo) (ctx : ContextInfo) : IO String := do
   let name := i.name?
   let stx := Format.pretty (← i.pp ctx)
-  return s!"{stx}\n{name} {stx}"
+  return s!"{name}\n{stx}"
 
 /--
 Keep `.node` nodes and `.hole` nodes satisfying predicates.
@@ -102,16 +102,24 @@ partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextIn
   | _ => []
 
 @[export pantograph_infotree_to_string_m]
-partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo) : IO String := do
+partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do
   match t with
   | .context ctx t => t.toString (ctx.mergeIntoOuter? ctx?)
   | .node info children =>
     if let some ctx := ctx? then
-      let node : Option String ← match info with
-      | .ofTermInfo    info => some <$> (do pure <| s!"[term] {(← info.toString ctx)}")
-      | .ofCommandInfo info => some <$> (do pure <| s!"[command] {(← info.toString ctx)}")
-      | .ofTacticInfo  info => some <$> (do pure <| s!"[tactic] {(← info.toString ctx)}")
-      | _                   => pure none
+      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)}"
+      | .ofMacroExpansionInfo _ => pure "[macro_exp]"
+      | .ofOptionInfo _ => pure "[option]"
+      | .ofFieldInfo _ => pure "[field]"
+      | .ofCompletionInfo _ => pure "[completion]"
+      | .ofUserWidgetInfo _ => pure "[user_widget]"
+      | .ofCustomInfo _ => pure "[custom]"
+      | .ofFVarAliasInfo _ => pure "[fvar]"
+      | .ofFieldRedeclInfo _ => pure "[field_redecl]"
+      | .ofOmissionInfo _ => pure "[omission]"
       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."

From ea813e5bc5d0116d09d9e8f43c3213fa33b2ae4d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 8 Dec 2024 23:21:36 -0800
Subject: [PATCH 04/28] feat: Monadic info collection

---
 Pantograph/Frontend/Elab.lean     | 26 ++++++++++++++++----------
 Pantograph/Frontend/InfoTree.lean | 29 +++++++++++++++++++++++++----
 Repl.lean                         |  4 ++--
 Test/Frontend.lean                | 12 +++++++++++-
 4 files changed, 54 insertions(+), 17 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index b3173a7..6bc67f3 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -67,7 +67,7 @@ end TacticInvocation
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
 private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
-  let infos := t.findAllInfo none fun i => match i with
+  let infos := t.findAllInfo none false fun i => match i with
     | .ofTacticInfo _ => true
     | _ => false
   infos.filterMap fun p => match p with
@@ -101,21 +101,27 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
-  let infos := t.findAllInfo none fun i => match i with
-    | .ofTermInfo { expectedType?, expr, stx, .. } =>
-      expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
+private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
+  let infos ← t.findAllInfoM none true fun i ctx? => match i with
+    | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
+      let .some expectedType := expectedType? | return false
+      let .some ctx := ctx? | return false
+      if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
+        return true
+      ctx.runMetaM lctx do
+        let type ← Meta.inferType expr
+        Bool.not <$> Meta.isDefEq type expectedType
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      isSorry ∧ !goalsBefore.isEmpty
-    | _ => false
-  infos.map fun (info, context?, _) => { info, context? }
+      return isSorry ∧ !goalsBefore.isEmpty
+    | _ => return false
+  return infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : List InfoWithContext :=
-  step.trees.bind collectSorrysInTree
+def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
+  return (← step.trees.mapM collectSorrysInTree).join
 
 
 
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 3b57a54..c72dbe6 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -93,14 +93,35 @@ partial def InfoTree.filter (p : Info → Bool) (m : MVarId → Bool := fun _ =>
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def InfoTree.findAllInfo (t : InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
-    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
+partial def InfoTree.findAllInfo
+    (t : InfoTree)
+    (context?: Option Elab.ContextInfo)
+    (haltOnMatch : Bool := false)
+    (pred : Elab.Info → Bool)
+    : List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
   match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+    let head := if pred i then [(i, context?, children)] else []
+    let tail := if haltOnMatch then [] else children.toList.bind (fun t => findAllInfo t context? haltOnMatch pred)
+    head ++ tail
   | _ => []
 
+/-- Monadic analogue of `findAllInfo` -/
+partial def InfoTree.findAllInfoM [Monad m]
+    (t : InfoTree)
+    (context?: Option Elab.ContextInfo)
+    (haltOnMatch : Bool)
+    (pred : Elab.Info → Option Elab.ContextInfo → m Bool)
+    : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do
+  match t with
+  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
+  | .node i children  =>
+    let head := if ← pred i context? then [(i, context?, children)] else []
+    let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    return head ++ (← tail).join
+  | _ => return []
+
 @[export pantograph_infotree_to_string_m]
 partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .none) : IO String := do
   match t with
diff --git a/Repl.lean b/Repl.lean
index 3f8a3c6..f1c8f42 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -257,10 +257,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
             pure $ .some invocations
           else
             pure .none
-        let sorrys := if args.sorrys then
+        let sorrys ← if args.sorrys then
             Frontend.collectSorrys step
           else
-            []
+            pure []
         let messages ← step.messageStrings
         return (step.before, boundary, invocations?, sorrys, messages)
       let li ← frontendM.run context |>.run' state
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 015cfa8..a03b283 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -10,7 +10,9 @@ 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)
+    for tree in step.trees do
+      IO.println s!"{← tree.toString}"
+    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
@@ -177,6 +179,13 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry
     }
   ])
 
+def test_capture_type_mismatch : TestT MetaM Unit := do
+  let input := "
+def mystery : Nat := true
+  "
+  let goalStates ← (collectSorrysFromSource input).run' {}
+  let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -185,6 +194,7 @@ def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
     ("sorry_in_induction", test_sorry_in_induction),
     ("sorry_in_coupled", test_sorry_in_coupled),
     ("environment_capture", test_environment_capture),
+    ("capture_type_mismatch", test_capture_type_mismatch),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

From 17ab2eafd8868652d83072f074696413825ebab5 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 00:03:53 -0800
Subject: [PATCH 05/28] fix: Halt on match guard

---
 Pantograph/Frontend/Elab.lean     | 2 --
 Pantograph/Frontend/InfoTree.lean | 4 ++--
 Test/Frontend.lean                | 2 --
 3 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 6bc67f3..d5af8b5 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -123,8 +123,6 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
   return (← step.trees.mapM collectSorrysInTree).join
 
-
-
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index c72dbe6..50b0965 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -103,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 then [] else children.toList.bind (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
   | _ => []
 
@@ -118,7 +118,7 @@ partial def InfoTree.findAllInfoM [Monad m]
   | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
   | .node i children  =>
     let head := if ← pred i context? then [(i, context?, children)] else []
-    let tail := if haltOnMatch then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
     return head ++ (← tail).join
   | _ => return []
 
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index a03b283..3b765fd 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -10,8 +10,6 @@ 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
-    for tree in step.trees do
-      IO.println s!"{← tree.toString}"
     return (step.before, ← Frontend.collectSorrys step)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do

From 2d068ecd5072386fd4043931b96e64fd47760aab Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 00:06:20 -0800
Subject: [PATCH 06/28] fix: Use guarded `isDefEq`

---
 Pantograph/Frontend/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index d5af8b5..c4704fc 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -110,7 +110,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
         return true
       ctx.runMetaM lctx do
         let type ← Meta.inferType expr
-        Bool.not <$> Meta.isDefEq type expectedType
+        Bool.not <$> Meta.isExprDefEqGuarded type expectedType
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry

From 7fc2bd0d0fc4901b7423782b6092518ac887e38b Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 08:15:01 -0800
Subject: [PATCH 07/28] test: Tactic failure on synthesizing placeholder

---
 Test/Proofs.lean | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 65f099f..1903306 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -701,7 +701,7 @@ def test_nat_zero_add_alt: TestM Unit := do
       }
     ])
 
-def test_composite_tactic_failure: TestM Unit := do
+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
     | .some state => pure state
@@ -720,6 +720,25 @@ def test_composite_tactic_failure: 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
+    | .some state => pure state
+    | .none => do
+      addTest $ assertUnreachable "Goal could not parse"
+      return ()
+
+  let tactic := "intro p q r h"
+  let state1 ← match ← state0.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  let tactic := "simpa [h] using And.imp_left h _"
+  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 suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
     ("identity", test_identity),
@@ -732,7 +751,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("calc", test_calc),
     ("Nat.zero_add", test_nat_zero_add),
     ("Nat.zero_add alt", test_nat_zero_add_alt),
-    ("composite tactic failure", test_composite_tactic_failure),
+    ("tactic failure with unresolved goals", test_tactic_failure_unresolved_goals),
+    ("tactic failure with synthesize placeholder", test_tactic_failure_synthesize_placeholder),
   ]
   tests.map (fun (name, test) => (name, proofRunner env test))
 

From 47d26badc82e606972a1b8a5285b78197411e067 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 17:30:33 -0800
Subject: [PATCH 08/28] feat: Capture mvar errors

---
 Pantograph/Goal.lean | 6 +++++-
 Test/Proofs.lean     | 4 +++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index e190d5d..4bb1afd 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -208,8 +208,12 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
   try
     let nextState ← state.step goal tacticM
 
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar goal)
+    let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
+
     -- Check if error messages have been generated in the core.
-    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
+    let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length
       |>.filterMapM λ m => do
         if m.severity == .error then
           return .some $ ← m.toString
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index 1903306..b48e3b0 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -720,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
@@ -737,7 +738,8 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
 
   let tactic := "simpa [h] using And.imp_left h _"
   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 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 := [

From d040d2006c7332eee67b9a0b3d8558e18469386e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 17:58:08 -0800
Subject: [PATCH 09/28] fix: Do not guard mvar errors in other tactics

---
 Pantograph/Goal.lean | 37 +++++++++++++++++++++++++++----------
 Test/Proofs.lean     | 16 +++++++++++++---
 2 files changed, 40 insertions(+), 13 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 4bb1afd..51aed88 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -177,16 +177,37 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 --- Tactic execution functions ---
 
-protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
+private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
+  let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
+  (← getThe Elab.Term.State).mvarErrorInfos
+    |>.map (·.mvarId)
+    |>.filterM λ mvarId =>
+      return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
+
+private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
+  let li2' := li2.filter (¬ li1.contains ·)
+  li1 ++ li2'
+
+/--
+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 (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
+  let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
+
+  let goals ← if guardMVarErrors then
+      pure $ mergeMVarLists goals (← collectAllErroredMVars goal)
+    else
+      pure goals
   return {
     state with
-    savedState := { term := nextElabState, tactic := newGoals },
+    savedState := { term := nextElabState, tactic := { goals }, },
     parentMVar? := .some goal,
     calcPrevRhs? := .none,
   }
@@ -203,14 +224,10 @@ inductive TacticResult where
   | invalidAction (message: String)
 
 /-- 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):
+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
-
-    Elab.Term.synthesizeSyntheticMVarsNoPostponing
-    let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar goal)
-    let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
+    let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
     let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length
@@ -237,7 +254,7 @@ protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: Str
     (fileName := ← getFileName) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
+  state.tryTacticM goal (Elab.Tactic.evalTactic tactic) true
 
 protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
       Elab.TermElabM TacticResult := do
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index b48e3b0..a6b5487 100644
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@@ -737,9 +737,19 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
       return ()
 
   let tactic := "simpa [h] using And.imp_left h _"
-  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 state2 ← match ← state1.tacticOn 0 tactic with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+
+  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 := [

From 5ef2b5c11840890471db123ecce3f26642e38478 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 19:40:00 -0800
Subject: [PATCH 10/28] feat: Collect newly defined constants

---
 Pantograph/Frontend/Elab.lean | 15 ++++++++++++++-
 Test/Frontend.lean            | 27 +++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index c4704fc..4ace608 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -2,6 +2,7 @@
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
+import Lean.DeclarationRange
 
 import Pantograph.Frontend.Basic
 import Pantograph.Frontend.MetaTranslate
@@ -128,7 +129,7 @@ Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
-@[export pantograph_frontend_sorrys_to_goal_state]
+@[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   assert! !sorrys.isEmpty
   let goalsM := sorrys.mapM λ i => do
@@ -147,5 +148,17 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
   GoalState.createFromMVars goals root
 
 
+@[export pantograph_frontend_collect_new_defined_constants_m]
+def collectNewDefinedConstants (step : CompilationStep) : IO (List Name) := do
+  step.after.constants.map₂.foldlM (λ acc name _ => do
+    if step.before.contains name then
+      return acc
+    let coreM : CoreM Bool := Option.isSome <$> findDeclarationRanges? name
+    let hasRange ← coreM.run' { fileName := step.fileName, fileMap := step.fileMap } { env := step.after } |>.toBaseIO
+    match hasRange with
+    | .ok true => return name :: acc
+    | .ok false => return acc
+    | .error e => throw $ IO.userError (← e.toMessageData.toString)
+    ) []
 
 end Pantograph.Frontend
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 3b765fd..68aaf94 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -184,6 +184,31 @@ def mystery : Nat := true
   let goalStates ← (collectSorrysFromSource input).run' {}
   let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
 
+def collectNewConstants (source: String) : MetaM (List (List Name)) := do
+  let filename := "<anonymous>"
+  let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
+  let m := Frontend.mapCompilationSteps λ step => do
+    Frontend.collectNewDefinedConstants step
+  m.run context |>.run' state
+
+def test_collect_one_constant : TestT MetaM Unit := do
+  let input := "
+def mystery : Nat := 123
+  "
+  let names ← collectNewConstants input
+  checkEq "constants" names [[`mystery]]
+def test_collect_one_theorem : TestT MetaM Unit := do
+  let input := "
+theorem mystery [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+  match as, i with
+  | a::as, ⟨0, _⟩  => simp_arith [get]
+  | a::as, ⟨i+1, h⟩ =>
+    have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
+    apply Nat.lt_trans ih
+    simp_arith
+  "
+  let names ← collectNewConstants input
+  checkEq "constants" names [[`mystery]]
 
 def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [
@@ -193,6 +218,8 @@ 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),
+    ("collect_one_constant", test_collect_one_constant),
+    ("collect_one_theorem", test_collect_one_theorem),
   ]
   tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
 

From 0b4ded10493585aeba2e9b345ddc9ed81d4a02ad Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:15:53 -0800
Subject: [PATCH 11/28] fix: Collect sorrys and type mismatches

---
 Pantograph/Frontend/Elab.lean     | 21 +++++++++++++--------
 Pantograph/Frontend/InfoTree.lean | 12 ++++++------
 Test/Frontend.lean                | 11 ++++++++++-
 3 files changed, 29 insertions(+), 15 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 4ace608..2eff084 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -103,20 +103,25 @@ structure InfoWithContext where
   context?: Option Elab.ContextInfo := .none
 
 private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
-  let infos ← t.findAllInfoM none true fun i ctx? => match i with
+  let infos ← t.findAllInfoM none fun i ctx? => match i with
     | .ofTermInfo { expectedType?, expr, stx, lctx, .. } => do
-      let .some expectedType := expectedType? | return false
-      let .some ctx := ctx? | return false
+      let .some expectedType := expectedType? | return (false, true)
+      let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
-        return true
-      ctx.runMetaM lctx do
+        return (true, false)
+      let typeMatch ← ctx.runMetaM lctx do
         let type ← Meta.inferType expr
-        Bool.not <$> Meta.isExprDefEqGuarded type expectedType
+        Meta.isExprDefEqGuarded type expectedType
+      return match typeMatch, expr.hasSorry with
+      | false, true => (true, false) -- Types mismatch but has sorry -> collect, halt
+      | false, false => (true, false) -- Types mistmatch but no sorry -> collect, halt
+      | true, true => (false, true) -- Types match but has sorry -> continue
+      | true, false => (false, false) -- Types match but no sorries -> halt
     | .ofTacticInfo { stx, goalsBefore, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
       let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      return isSorry ∧ !goalsBefore.isEmpty
-    | _ => return false
+      return (isSorry ∧ !goalsBefore.isEmpty, ¬ isSorry)
+    | _ => return (false, true)
   return infos.map fun (info, context?, _) => { info, context? }
 
 -- NOTE: Plural deliberately not spelled "sorries"
diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 50b0965..cfef621 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/Pantograph/Frontend/InfoTree.lean
@@ -107,18 +107,18 @@ partial def InfoTree.findAllInfo
     head ++ tail
   | _ => []
 
-/-- Monadic analogue of `findAllInfo` -/
+/-- Monadic analogue of `findAllInfo`, but predicate controls whether to recurse. -/
 partial def InfoTree.findAllInfoM [Monad m]
     (t : InfoTree)
     (context?: Option Elab.ContextInfo)
-    (haltOnMatch : Bool)
-    (pred : Elab.Info → Option Elab.ContextInfo → m Bool)
+    (pred : Elab.Info → Option Elab.ContextInfo → m (Bool × Bool))
     : m (List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree)) := do
   match t with
-  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) haltOnMatch pred
+  | .context inner t => t.findAllInfoM (inner.mergeIntoOuter? context?) pred
   | .node i children  =>
-    let head := if ← pred i context? then [(i, context?, children)] else []
-    let tail := if haltOnMatch ∧ !head.isEmpty then pure [] else children.toList.mapM (fun t => t.findAllInfoM context? haltOnMatch pred)
+    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).join
   | _ => return []
 
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 68aaf94..2259029 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -179,10 +179,19 @@ example (n: Nat) : mystery n + 1 = n + 2 := sorry
 
 def test_capture_type_mismatch : TestT MetaM Unit := do
   let input := "
-def mystery : Nat := true
+def mystery (k: Nat) : Nat := true
   "
   let goalStates ← (collectSorrysFromSource input).run' {}
   let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
+  checkEq "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize)) #[
+    {
+      target := { pp? := "Nat" },
+      vars := #[{
+         userName := "k",
+         type? := .some { pp? := "Nat" },
+      }],
+    }
+  ]
 
 def collectNewConstants (source: String) : MetaM (List (List Name)) := do
   let filename := "<anonymous>"

From dd00d803d1fe500f46710bb32bfcc9eeeb2d8062 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:38:27 -0800
Subject: [PATCH 12/28] feat: Collect sorry/elab failure boundaries

---
 Pantograph/Frontend/Basic.lean |  7 +++++++
 Pantograph/Frontend/Elab.lean  | 19 ++++++++++++++-----
 Pantograph/Protocol.lean       |  2 ++
 Repl.lean                      | 13 +++++++------
 Test/Frontend.lean             |  4 ++--
 5 files changed, 32 insertions(+), 13 deletions(-)

diff --git a/Pantograph/Frontend/Basic.lean b/Pantograph/Frontend/Basic.lean
index 1074a94..87decd4 100644
--- a/Pantograph/Frontend/Basic.lean
+++ b/Pantograph/Frontend/Basic.lean
@@ -30,6 +30,13 @@ end Lean.PersistentArray
 
 namespace Pantograph.Frontend
 
+@[export pantograph_frontend_stx_byte_range]
+def stxByteRange (stx : Syntax) : String.Pos × String.Pos :=
+  let pos := stx.getPos?.getD 0
+  let endPos := stx.getTailPos?.getD 0
+  (pos, endPos)
+
+
 abbrev FrontendM := Elab.Frontend.FrontendM
 
 structure CompilationStep where
diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index 2eff084..a33fbef 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -129,28 +129,37 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
   return (← step.trees.mapM collectSorrysInTree).join
 
+structure AnnotatedGoalState where
+  state : GoalState
+  srcBoundaries : List (String.Pos × String.Pos)
+
 /--
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
-def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
+def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
   assert! !sorrys.isEmpty
   let goalsM := sorrys.mapM λ i => do
     match i.info with
     | .ofTermInfo termInfo  => do
       let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
-      return [mvarId]
+      return [(mvarId, stxByteRange termInfo.stx)]
     | .ofTacticInfo tacticInfo => do
-      MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      let mvarIds ← MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
+      let range := stxByteRange tacticInfo.stx
+      return mvarIds.map (·, range)
     | _ => panic! "Invalid info"
-  let goals := List.join (← 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
     | [] => panic! "No MVars generated"
     | [g] => g
     | _ => { name := .anonymous }
-  GoalState.createFromMVars goals root
+  let state ← GoalState.createFromMVars goals root
+  return { state, srcBoundaries }
 
 
 @[export pantograph_frontend_collect_new_defined_constants_m]
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 0cb6cac..5cb24e8 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -329,6 +329,8 @@ structure CompilationUnit where
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
   goals: Array Goal := #[]
+  -- Code segments which generated the goals
+  goalSrcBoundaries: Array (Nat × Nat) := #[]
   messages: Array String := #[]
   deriving Lean.ToJson
 structure FrontendProcessResult where
diff --git a/Repl.lean b/Repl.lean
index f1c8f42..201a841 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -265,18 +265,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return (step.before, boundary, invocations?, sorrys, messages)
       let li ← frontendM.run context |>.run' state
       let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
-        let (goalStateId?, goals) ← if sorrys.isEmpty then do
-            pure (.none, #[])
+        let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
+            pure (.none, #[], #[])
           else do
-            let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
-            let stateId ← newGoalState goalState
-            let goals ← goalSerialize goalState options
-            pure (.some stateId, goals)
+            let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
+            let stateId ← newGoalState state
+            let goals ← goalSerialize state options
+            pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)))
         return {
           boundary,
           invocations?,
           goalStateId?,
           goals,
+          goalSrcBoundaries,
           messages,
         }
       return .ok { units }
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 2259029..a3b73ae 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -15,8 +15,8 @@ def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
       return .none
-    let goalState ← Frontend.sorrysToGoalState sorrys
-    return .some goalState
+    let { state, .. } ← Frontend.sorrysToGoalState sorrys
+    return .some state
   return goalStates
 
 def test_multiple_sorrys_in_proof : TestT MetaM Unit := do

From 9a69c48cb23f313e5986e87a8867eaf3d9b6528e Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:42:05 -0800
Subject: [PATCH 13/28] fix: Integration test failure

---
 Test/Integration.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Test/Integration.lean b/Test/Integration.lean
index 9fb86b7..171bc91 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -222,6 +222,7 @@ def test_frontend_process_sorry : Test :=
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
          goals := #[goal1],
+         goalSrcBoundaries := #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),

From eb0374dfb3cd73df86bfcfe5a0ed1f5d03d37cce Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 20:57:25 -0800
Subject: [PATCH 14/28] feat: Collect new constants in repl

---
 Pantograph/Protocol.lean |  3 +++
 Repl.lean                | 13 +++++++++++--
 Test/Integration.lean    |  2 ++
 3 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 5cb24e8..d80c761 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -312,6 +312,8 @@ structure FrontendProcess where
   invocations: Bool := false
   -- If set to true, collect `sorry`s
   sorrys: Bool := false
+  -- If set to true, extract new constants
+  newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
   goalBefore: String
@@ -332,6 +334,7 @@ structure CompilationUnit where
   -- Code segments which generated the goals
   goalSrcBoundaries: Array (Nat × Nat) := #[]
   messages: Array String := #[]
+  newConstants: Option (Array String) := .none
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit
diff --git a/Repl.lean b/Repl.lean
index 201a841..710b132 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -262,9 +262,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           else
             pure []
         let messages ← step.messageStrings
-        return (step.before, boundary, invocations?, sorrys, messages)
+        let newConstants ← if args.newConstants then
+            Frontend.collectNewDefinedConstants step
+          else
+            pure []
+        return (step.before, boundary, invocations?, sorrys, messages, newConstants)
       let li ← frontendM.run context |>.run' state
-      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
+      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
+        let newConstants := if args.newConstants then
+            .some $ newConstants.toArray.map λ name => name.toString
+          else
+            .none
         let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
             pure (.none, #[], #[])
           else do
@@ -279,6 +287,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goals,
           goalSrcBoundaries,
           messages,
+          newConstants,
         }
       return .ok { units }
     catch e =>
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 171bc91..8d53168 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -174,6 +174,7 @@ def test_frontend_process : Test :=
         ("file", .str file),
         ("invocations", .bool true),
         ("sorrys", .bool false),
+        ("newConstants", .bool false),
       ]
      ({
        units := [{
@@ -214,6 +215,7 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
+        ("newConstants", .bool false),
       ]
      ({
        units := [{

From 1527743900b2af65514be9cf6a3d9f18b818874a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 21:00:33 -0800
Subject: [PATCH 15/28] refactor: Optionalize CompilationUnit

---
 Pantograph/Protocol.lean | 10 ++++++----
 Repl.lean                | 17 +++++++++--------
 Test/Integration.lean    |  4 ++--
 3 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index d80c761..f232d9e 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -327,14 +327,16 @@ structure InvokedTactic where
 structure CompilationUnit where
   -- String boundaries of compilation units
   boundary: (Nat × Nat)
+  messages: Array String := #[]
   -- Tactic invocations
   invocations?: Option (List InvokedTactic) := .none
   goalStateId?: Option Nat := .none
-  goals: Array Goal := #[]
+  goals?: Option (Array Goal) := .none
   -- Code segments which generated the goals
-  goalSrcBoundaries: Array (Nat × Nat) := #[]
-  messages: Array String := #[]
-  newConstants: Option (Array String) := .none
+  goalSrcBoundaries?: Option (Array (Nat × Nat)) := .none
+
+  -- New constants defined in compilation unit
+  newConstants?: Option (Array String) := .none
   deriving Lean.ToJson
 structure FrontendProcessResult where
   units: List CompilationUnit
diff --git a/Repl.lean b/Repl.lean
index 710b132..283bcf3 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -269,25 +269,26 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return (step.before, boundary, invocations?, sorrys, messages, newConstants)
       let li ← frontendM.run context |>.run' state
       let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages, newConstants) => Lean.withEnv env do
-        let newConstants := if args.newConstants then
+        let newConstants? := if args.newConstants then
             .some $ newConstants.toArray.map λ name => name.toString
           else
             .none
-        let (goalStateId?, goals, goalSrcBoundaries) ← if sorrys.isEmpty then do
-            pure (.none, #[], #[])
+        let (goalStateId?, goals?, goalSrcBoundaries?) ← if sorrys.isEmpty then do
+            pure (.none, .none, .none)
           else do
             let { state, srcBoundaries } ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
             let stateId ← newGoalState state
             let goals ← goalSerialize state options
-            pure (.some stateId, goals, srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx)))
+            let srcBoundaries := srcBoundaries.toArray.map (λ (b, e) => (b.byteIdx, e.byteIdx))
+            pure (.some stateId, .some goals, .some srcBoundaries)
         return {
           boundary,
+          messages,
           invocations?,
           goalStateId?,
-          goals,
-          goalSrcBoundaries,
-          messages,
-          newConstants,
+          goals?,
+          goalSrcBoundaries?,
+          newConstants?,
         }
       return .ok { units }
     catch e =>
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 8d53168..3e9bed2 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -223,8 +223,8 @@ def test_frontend_process_sorry : Test :=
        }, {
          boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
          goalStateId? := .some 0,
-         goals := #[goal1],
-         goalSrcBoundaries := #[(57, 62)],
+         goals? := .some #[goal1],
+         goalSrcBoundaries? := .some #[(57, 62)],
          messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
        }],
     }: Protocol.FrontendProcessResult),

From 37a5884be40790a946e0b8e26879ed3bbf509077 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 9 Dec 2024 21:39:33 -0800
Subject: [PATCH 16/28] fix: Use `ppSyntax` instead of `ppTactic`

---
 Pantograph/Frontend/Elab.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index a33fbef..d9480f0 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -87,9 +87,11 @@ def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protoc
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
-    let tactic ← invocation.ctx.runMetaM {} do
-      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
-      return t.pretty
+    let tactic ← invocation.ctx.runMetaM {} <| Meta.withMCtx invocation.info.mctxBefore do
+      return (← invocation.ctx.ppSyntax {} invocation.info.stx).pretty
+      -- FIXME: Why does this not work? There are problems with `term.pseudo.antiquot`
+      --PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
+      --return t.pretty
     let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
     return {
       goalBefore,

From 681c3fb78d2055e4d8dbe1fcd2ef5c66d28b6469 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 12:21:56 -0800
Subject: [PATCH 17/28] fix: Disallow indeterminant type `sorry`

---
 Pantograph/Frontend/Elab.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index d9480f0..3da5fca 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -1,4 +1,3 @@
-/- Adapted from https://github.com/semorrison/lean-training-data -/
 import Lean.Elab.Import
 import Lean.Elab.Command
 import Lean.Elab.InfoTree
@@ -16,6 +15,7 @@ namespace Pantograph.Frontend
 
 -- Info tree filtering functions
 
+/- Adapted from lean-training-data -/
 structure TacticInvocation where
   info : Elab.TacticInfo
   ctx : Elab.ContextInfo
@@ -107,10 +107,12 @@ structure InfoWithContext where
 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, .. } => do
-      let .some expectedType := expectedType? | return (false, true)
       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)
+      let .some expectedType := expectedType? | return (false, true)
       let typeMatch ← ctx.runMetaM lctx do
         let type ← Meta.inferType expr
         Meta.isExprDefEqGuarded type expectedType

From 95503c45e4ac6217889cd21d63672d58768835f1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 21:45:57 -0800
Subject: [PATCH 18/28] doc: frontend.process newConstants

---
 doc/repl.md | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/repl.md b/doc/repl.md
index 464c7cc..d332986 100644
--- a/doc/repl.md
+++ b/doc/repl.md
@@ -44,9 +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> }`: Executes the Lean frontend on a file, collecting
-  either the tactic invocations (`"invocations": true`) or the sorrys into goal
-  states (`"sorrys": true`)
+  <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
 

From 1d10cd2b205f8baf172384733793cd2a55a1f5d8 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 23:16:33 -0800
Subject: [PATCH 19/28] fix: Collect errored mvars by iterating errorInfo

---
 Pantograph/Goal.lean | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 51aed88..f2eb25a 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -177,12 +177,25 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 --- Tactic execution functions ---
 
+-- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
 private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId) := do
   let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
-  (← getThe Elab.Term.State).mvarErrorInfos
-    |>.map (·.mvarId)
-    |>.filterM λ mvarId =>
-      return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
+  let mut alreadyVisited : MVarIdSet := {}
+  let mut result : MVarIdSet := {}
+  for mvarErrorInfo in (← get).mvarErrorInfos do
+    let mvarId := mvarErrorInfo.mvarId
+    unless alreadyVisited.contains mvarId do
+      alreadyVisited := alreadyVisited.insert mvarId
+      /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
+         delayed assigned to another metavariable that is unassigned. -/
+      let mvarDeps ← Meta.getMVars (mkMVar mvarId)
+      if mvarDeps.any descendants.contains then do
+        result := result.insert mvarId
+  return result.toList
+  --(← getThe Elab.Term.State).mvarErrorInfos
+  --  |>.map (·.mvarId)
+  --  |>.filterM λ mvarId =>
+  --    return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
 
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
   let li2' := li2.filter (¬ li1.contains ·)

From 755ba13c1b8f92d91dea492d4b8106a90f68e295 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 23:48:46 -0800
Subject: [PATCH 20/28] fix: Set `synthesizeSyntheticMVarsNoPostponing`

---
 Pantograph/Goal.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index f2eb25a..3a6e97a 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -179,6 +179,10 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarI
 
 -- Mimics `Elab.Term.logUnassignedUsingErrorInfos`
 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.
   let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}
@@ -213,6 +217,7 @@ protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Ta
   goal.checkNotAssigned `GoalState.step
   let (_, { goals }) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
   let nextElabState ← MonadBacktrack.saveState
+  Elab.Term.synthesizeSyntheticMVarsNoPostponing
 
   let goals ← if guardMVarErrors then
       pure $ mergeMVarLists goals (← collectAllErroredMVars goal)

From e0e5c9ec681d0423a12a0c0278fef38cd8c5af80 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 10 Dec 2024 23:51:47 -0800
Subject: [PATCH 21/28] chore: Code cleanup

---
 Pantograph/Goal.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 3a6e97a..7a09435 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -186,8 +186,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
   let descendants ←  Meta.getMVars $ ← instantiateMVars (.mvar src)
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}
-  for mvarErrorInfo in (← get).mvarErrorInfos do
-    let mvarId := mvarErrorInfo.mvarId
+  for { mvarId, .. } in (← get).mvarErrorInfos do
     unless alreadyVisited.contains mvarId do
       alreadyVisited := alreadyVisited.insert mvarId
       /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
@@ -196,10 +195,6 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
       if mvarDeps.any descendants.contains then do
         result := result.insert mvarId
   return result.toList
-  --(← getThe Elab.Term.State).mvarErrorInfos
-  --  |>.map (·.mvarId)
-  --  |>.filterM λ mvarId =>
-  --    return descendants.contains mvarId ∧ !(← mvarId.isAssignedOrDelayedAssigned)
 
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=
   let li2' := li2.filter (¬ li1.contains ·)

From cb87fcd9dd89fdeaaaad49f0dd0111b4e7416c49 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 00:16:52 -0800
Subject: [PATCH 22/28] fix: Insert `mvarDeps`

---
 Pantograph/Goal.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 7a09435..52562e7 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -184,6 +184,7 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
   -- 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 $ ← instantiateMVars (.mvar src)
+  --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}
   for { mvarId, .. } in (← get).mvarErrorInfos do
@@ -191,9 +192,9 @@ private def collectAllErroredMVars (src : MVarId) : Elab.TermElabM (List MVarId)
       alreadyVisited := alreadyVisited.insert mvarId
       /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
          delayed assigned to another metavariable that is unassigned. -/
-      let mvarDeps ← Meta.getMVars (mkMVar mvarId)
+      let mvarDeps ← Meta.getMVars (.mvar mvarId)
       if mvarDeps.any descendants.contains then do
-        result := result.insert mvarId
+        result := mvarDeps.foldl (·.insert ·) result
   return result.toList
 
 private def mergeMVarLists (li1 li2 : List MVarId) : List MVarId :=

From 58956d33fe25069c708213ccb625ac88c8f04a47 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 00:21:26 -0800
Subject: [PATCH 23/28] doc: Update behaviour rationale

---
 doc/rationale.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/doc/rationale.md b/doc/rationale.md
index 87c1606..4209474 100644
--- a/doc/rationale.md
+++ b/doc/rationale.md
@@ -24,6 +24,22 @@ The name Pantograph is a pun. It means two things
   a locomotive. In comparison the (relatively) simple Pantograph software powers
   theorem proving projects.
 
+## Caveats
+
+Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the
+flexibility it offers.  To support tree search means Pantograph has to act
+differently from Lean in some times, but never at the sacrifice of soundness.
+
+- When Lean LSP says "don't know how to synthesize placeholder", this indicates
+  the human operator needs to manually move the cursor to the placeholder and
+  type in the correct expression. This error therefore should not halt the proof
+  process, and the placeholder should be turned into a goal.
+- 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.
+
 ## References
 
 * [Pantograph Paper](https://arxiv.org/abs/2410.16429)

From aa122b2bb904e6cd757c1b5e0b75113510c1efaa Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 00:24:56 -0800
Subject: [PATCH 24/28] doc: Update rationale link

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e070fff..02de68c 100644
--- a/README.md
+++ b/README.md
@@ -7,7 +7,7 @@ A Machine-to-Machine interaction system for Lean 4.
 Pantograph provides interfaces to execute proofs, construct expressions, and
 examine the symbol list of a Lean project for machine learning.
 
-See [documentations](doc/) for design rationale and references.
+See [documentations](doc/rationale.md) for design rationale and references.
 
 ## Installation
 

From c96df2ed1cd834f3a04374f60c852ed8a2253e8f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 00:29:29 -0800
Subject: [PATCH 25/28] chore: Add `aarch64` build targets to flake

---
 flake.nix | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/flake.nix b/flake.nix
index 91901d8..f49a331 100644
--- a/flake.nix
+++ b/flake.nix
@@ -22,6 +22,8 @@
     flake = {
     };
     systems = [
+      "aarch64-linux"
+      "aarch64-darwin"
       "x86_64-linux"
       "x86_64-darwin"
     ];

From f2f71a60281f66d78687128b8fb879e0f7a11fe0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:01:57 -0800
Subject: [PATCH 26/28] fix: Reset core message log

---
 Pantograph/Goal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 52562e7..b140ee7 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -250,6 +250,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
           return .some $ ← m.toString
         else
           return .none
+    Core.resetMessageLog
     if ¬ newMessages.isEmpty then
       return .failure newMessages.toArray
     return .success nextState

From ab77418e242d81e502f4ae7a88ab7decf8d6b1a6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:05:47 -0800
Subject: [PATCH 27/28] fix: Drop previous message lists

---
 Pantograph/Goal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index b140ee7..6ff14d2 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -244,7 +244,7 @@ protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: E
     let nextState ← state.step goal tacticM guardMVarErrors
 
     -- Check if error messages have been generated in the core.
-    let newMessages ← (← Core.getMessageLog).toList --.drop state.coreState.messages.toList.length
+    let newMessages ← (← Core.getMessageLog).toList.drop state.coreState.messages.toList.length
       |>.filterMapM λ m => do
         if m.severity == .error then
           return .some $ ← m.toString

From 396a787771909d722e531acf2c11ffec2dd11900 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Wed, 11 Dec 2024 09:06:42 -0800
Subject: [PATCH 28/28] feat: Reset message log in MainM

---
 Repl.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Repl.lean b/Repl.lean
index 283bcf3..2060061 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -79,6 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let nGoals := state.goalStates.size
     set { state with nextId := 0, goalStates := .empty }
+    Lean.Core.resetMessageLog
     return .ok { nGoals }
   stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
     let state ← get