From c0090dec975cd30303060f172ec1da28782e53ad Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 15 Dec 2024 12:40:47 -0800
Subject: [PATCH 01/10] fix: Quote string literal in sexp

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

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 4b3bd51..582b783 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -369,7 +369,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       -- is wrapped in a :lit sexp.
       let v' := match v with
         | .natVal val => toString val
-        | .strVal val => s!"\"{val}\""
+        | .strVal val => IR.EmitC.quoteString val
       pure s!"(:lit {v'})"
     | .mdata _ inner =>
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter

From 7a3b89cc0edcb223ddaf23ff2f35c3fa14dfb3bd Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 15 Dec 2024 12:48:49 -0800
Subject: [PATCH 02/10] feat: Simplify sexp binder

---
 Pantograph/Delate.lean | 6 +++---
 Test/Delate.lean       | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index 582b783..c68d7cd 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -384,9 +384,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
   -- Elides all unhygenic names
   binderInfoSexp : Lean.BinderInfo → String
     | .default => ""
-    | .implicit => " :implicit"
-    | .strictImplicit => " :strictImplicit"
-    | .instImplicit => " :instImplicit"
+    | .implicit => " :i"
+    | .strictImplicit => " :si"
+    | .instImplicit => " :ii"
 
 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp?: Option String ← match options.printExprPretty with
diff --git a/Test/Delate.lean b/Test/Delate.lean
index d918dc8..013be73 100644
--- 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)) :implicit) :implicit)"),
+    ("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)"),
     -- 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) :implicit)"),
-    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
+    ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"),
+    ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"),
     ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
   ]
   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)) :implicit) :implicit)"
+      "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)"
     ),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do

From 53bad1c4c995ee44f145439add930177ac49f16f Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 15 Dec 2024 12:52:08 -0800
Subject: [PATCH 03/10] refactor: Remove obsolete sanitize option

---
 Pantograph/Delate.lean | 20 ++++++++++----------
 Test/Proofs.lean       |  8 ++++----
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean
index c68d7cd..38d8bda 100644
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@@ -264,25 +264,24 @@ 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) (sanitize: Bool): String :=
+partial def serializeSortLevel (level: Level) : 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 sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serializeSortLevel v sanitize
-      let w := serializeSortLevel w sanitize
+      let v := serializeSortLevel v
+      let w := serializeSortLevel w
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := serializeName name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := serializeName id.name sanitize
+      let name := id.name
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
@@ -295,7 +294,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
 
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
   self expr
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
@@ -334,9 +333,10 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
         let name := mvarId.name
         pure s!"(:{pref} {name})"
     | .sort level =>
-      let level := serializeSortLevel level sanitize
+      let level := serializeSortLevel level
       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})"
@@ -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 (sanitize := false)
+          let sexp ← serializeExpressionSexp type
           pure <| " " ++ sexp
         else
           pure ""
diff --git a/Test/Proofs.lean b/Test/Proofs.lean
index a6b5487..104a849 100644
--- 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!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
 
 -- Individual test cases
@@ -259,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!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!)
   addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
@@ -276,7 +276,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← state2.withParentContext do
-    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!)
   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}))"
@@ -292,7 +292,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   let state3_1parent ← state3_1.withParentContext do
-    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+    serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!)
   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

From b42d917aa70fa82ebf07d4480ecd14441e07eb23 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 17 Dec 2024 08:18:27 +0900
Subject: [PATCH 04/10] fix: Unnecessary instantiation call

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

diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index 6ff14d2..f573332 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -183,7 +183,8 @@ 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 $ ← instantiateMVars (.mvar src)
+
+  let descendants ←  Meta.getMVars (.mvar src)
   --let _ ← Elab.Term.logUnassignedUsingErrorInfos descendants
   let mut alreadyVisited : MVarIdSet := {}
   let mut result : MVarIdSet := {}

From 48b924fae26f0354625d65eb047c57d034945aa1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 20 Dec 2024 19:10:38 +0900
Subject: [PATCH 05/10] fix(frontend): Incorrect capture of binder term

---
 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 3da5fca..a07efb0 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -106,7 +106,7 @@ 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
+    | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
       let .some ctx := ctx? | return (false, true)
       if expr.isSorry ∧ stx.isOfKind `Lean.Parser.Term.sorry then
         if expectedType?.isNone then

From 5a05e9e8d4d3226e49747e1fa4a4b820ecd46dac Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 22 Dec 2024 08:47:38 +0900
Subject: [PATCH 06/10] test: Add binder capturing test

---
 Test/Frontend.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index a3b73ae..2c5809f 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -193,6 +193,15 @@ 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 goalStates ← (collectSorrysFromSource input).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) {}
@@ -227,6 +236,7 @@ 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),
   ]

From 524314721b3213c380d54d461786abbddedf6c55 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 7 Jan 2025 19:40:03 +0900
Subject: [PATCH 07/10] feat: Gate type error collection behind flag

---
 Pantograph/Frontend/Elab.lean | 13 ++++++++++---
 Pantograph/Protocol.lean      |  8 +++++---
 Repl.lean                     |  2 +-
 Test/Frontend.lean            | 15 +++++++++------
 Test/Integration.lean         | 10 ++++++----
 5 files changed, 31 insertions(+), 17 deletions(-)

diff --git a/Pantograph/Frontend/Elab.lean b/Pantograph/Frontend/Elab.lean
index a07efb0..b5a7274 100644
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/Elab.lean
@@ -104,7 +104,11 @@ structure InfoWithContext where
   info: Elab.Info
   context?: Option Elab.ContextInfo := .none
 
-private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext) := do
+structure GoalCollectionOptions where
+  collectTypeErrors : Bool := false
+
+private def collectSorrysInTree (t : Elab.InfoTree) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
   let infos ← t.findAllInfoM none fun i ctx? => match i with
     | .ofTermInfo { expectedType?, expr, stx, lctx, isBinder := false, .. } => do
       let .some ctx := ctx? | return (false, true)
@@ -112,6 +116,8 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
         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
@@ -130,8 +136,9 @@ private def collectSorrysInTree (t : Elab.InfoTree) : IO (List InfoWithContext)
 
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
-def collectSorrys (step: CompilationStep) : IO (List InfoWithContext) := do
-  return (← step.trees.mapM collectSorrysInTree).join
+def collectSorrys (step: CompilationStep) (options : GoalCollectionOptions := {})
+    : IO (List InfoWithContext) := do
+  return (← step.trees.mapM $ λ tree => collectSorrysInTree tree options).join
 
 structure AnnotatedGoalState where
   state : GoalState
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 90ac149..47ed879 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -319,11 +319,13 @@ 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
-  -- If set to true, collect tactic invocations
+  -- collect tactic invocations
   invocations: Bool := false
-  -- If set to true, collect `sorry`s
+  -- collect `sorry`s
   sorrys: Bool := false
-  -- If set to true, extract new constants
+  -- collect type errors
+  typeErrorsAsGoals: Bool := false
+  -- list new constants from each compilation step
   newConstants: Bool := false
   deriving Lean.FromJson
 structure InvokedTactic where
diff --git a/Repl.lean b/Repl.lean
index eb02f59..1fd8266 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -265,7 +265,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           else
             pure .none
         let sorrys ← if args.sorrys then
-            Frontend.collectSorrys step
+            Frontend.collectSorrys step (options := { collectTypeErrors := args.typeErrorsAsGoals })
           else
             pure []
         let messages ← step.messageStrings
diff --git a/Test/Frontend.lean b/Test/Frontend.lean
index 2c5809f..571aa9f 100644
--- a/Test/Frontend.lean
+++ b/Test/Frontend.lean
@@ -6,11 +6,12 @@ import Test.Common
 open Lean Pantograph
 namespace Pantograph.Test.Frontend
 
-def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
+def collectSorrysFromSource (source: String) (options : Frontend.GoalCollectionOptions := {})
+    : 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)
+    return (step.before, ← Frontend.collectSorrys step options)
   let li ← m.run context |>.run' state
   let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
     if sorrys.isEmpty then
@@ -181,9 +182,10 @@ def test_capture_type_mismatch : TestT MetaM Unit := do
   let input := "
 def mystery (k: Nat) : Nat := true
   "
-  let goalStates ← (collectSorrysFromSource input).run' {}
+  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)) #[
+  checkEq "goals" ((← goalState.serializeGoals).map (·.devolatilize)) #[
     {
       target := { pp? := "Nat" },
       vars := #[{
@@ -197,7 +199,8 @@ 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 goalStates ← (collectSorrysFromSource input).run' {}
+  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)) #[
   ]
@@ -236,7 +239,7 @@ 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),
+    --("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),
   ]
diff --git a/Test/Integration.lean b/Test/Integration.lean
index 77968f0..1a2e97c 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -171,10 +171,11 @@ 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),
-        ("newConstants", .bool false),
+        ("file",              .str file),
+        ("invocations",       .bool true),
+        ("sorrys",            .bool false),
+        ("typeErrorsAsGoals", .bool false),
+        ("newConstants",      .bool false),
       ]
      ({
        units := [{
@@ -215,6 +216,7 @@ def test_frontend_process_sorry : Test :=
         ("file", .str file),
         ("invocations", .bool false),
         ("sorrys", .bool true),
+        ("typeErrorsAsGoals", .bool false),
         ("newConstants", .bool false),
       ]
      ({

From 97eaadc93ce912875f841113d7f773d27bdc8089 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 10 Jan 2025 12:16:23 -0800
Subject: [PATCH 08/10] feat: Add source location extraction

---
 Pantograph/Environment.lean | 18 ++++++++++++++++--
 Pantograph/Protocol.lean    | 13 ++++++++++---
 2 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index ad21284..c9f9fec 100644
--- 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) |>.map toString
+    (λ idx => env.allImportedModuleNames.get? idx.toNat)
   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?
+    module? := module?.map (·.toString)
   }
   let result ← match info with
     | .inductInfo induct => pure { core with inductInfo? := .some {
@@ -113,6 +113,20 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           k := r.k,
       } }
     | _ => pure core
+  let result ← if args.source?.getD false then
+      let searchPath ← searchPathRef.get
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule searchPath ·)
+      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
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 90ac149..67a37df 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -5,6 +5,7 @@ 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
 
@@ -121,11 +122,13 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
-  -- If true/false, show/hide the value expressions; By default definitions
-  -- values are shown and theorem values are hidden.
+  -- Show the value expressions; By default definitions values are shown and
+  -- theorem values are hidden.
   value?: Option Bool := .some false
-  -- If true, show the type and value dependencies
+  -- 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
@@ -172,6 +175,10 @@ structure EnvInspectResult where
   inductInfo?:      Option InductInfo      := .none
   constructorInfo?: Option ConstructorInfo := .none
   recursorInfo?:    Option RecursorInfo    := .none
+
+  sourceUri?: Option String := .none
+  sourceStart?: Option Lean.Position := .none
+  sourceEnd?: Option Lean.Position := .none
   deriving Lean.ToJson
 
 structure EnvAdd where

From 4a4b02d7b05ff0a669ce59cc91f2b842d0ef361d Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 10 Jan 2025 12:47:13 -0800
Subject: [PATCH 09/10] test: Source location extraction

---
 Pantograph/Environment.lean |  4 ++--
 Pantograph/Protocol.lean    |  1 +
 Test/Common.lean            |  2 ++
 Test/Environment.lean       | 15 +++++++++++++++
 4 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean
index c9f9fec..c48414a 100644
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@@ -114,8 +114,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       } }
     | _ => pure core
   let result ← if args.source?.getD false then
-      let searchPath ← searchPathRef.get
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule searchPath ·)
+      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)
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index 67a37df..a8abb3d 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -176,6 +176,7 @@ structure EnvInspectResult where
   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
diff --git a/Test/Common.lean b/Test/Common.lean
index 53adaa0..3cad256 100644
--- a/Test/Common.lean
+++ b/Test/Common.lean
@@ -143,6 +143,8 @@ 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
 
diff --git a/Test/Environment.lean b/Test/Environment.lean
index 79d04ed..a9f6cdc 100644
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@@ -97,11 +97,26 @@ 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"
+
+    -- Doesn't work for symbols in `Init` for some reason
+    --checkEq "file" result.sourceUri? <| .some "??"
+    checkEq "pos" result.sourceStart? <| .some { line := 344, column := 0 }
+    checkEq "pos" result.sourceEnd? <| .some { line := 344, column := 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

From ef4e5ecbf8057c6baf542391d4c40ec068810aa4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 10 Jan 2025 12:55:26 -0800
Subject: [PATCH 10/10] chore: Update version

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

diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean
index 9d044d4..d20dec5 100644
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.23"
+def version := "0.2.24"
 
 end Pantograph