.

REPL/Main.lean

@@ -240,7 +240,7 @@ def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do
       let proofState' ← proofState.runString s.tactic
       return .inl (← createProofStepReponse proofState' proofState)
     catch ex =>
-      return .inr ⟨ex.toString⟩
+      return .inr ⟨"Lean error:\n" ++ ex.toString⟩
 
 end REPL
 
@@ -272,7 +272,8 @@ inductive Input
 def parse (query : String) : IO Input := do
   let json := Json.parse query
   match json with
-  | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error)
+  | .error e => throw <| IO.userError <| toString <| toJson <|
+      (⟨"Could not parse JSON:\n" ++ e⟩ : Error)
   | .ok j => match fromJson? j with
     | .ok (r : REPL.ProofStep) => return .proofStep r
     | .error _ => match fromJson? j with
@@ -285,7 +286,8 @@ def parse (query : String) : IO Input := do
     | .ok (r : REPL.UnpickleProofState) => return .unpickleProofSnapshot r
     | .error _ => match fromJson? j with
     | .ok (r : REPL.Command) => return .command r
-    | .error e => throw <| IO.userError <| toString <| toJson (⟨e⟩ : Error)
+    | .error e => throw <| IO.userError <| toString <| toJson <|
+        (⟨"Could not parse as a valid JSON command:\n" ++ e⟩ : Error)
 
 /-- Read-eval-print loop for Lean. -/
 unsafe def repl : IO Unit :=
@@ -294,6 +296,7 @@ where loop : M IO Unit := do
   let query ← getLines
   if query = "" then
     return ()
+  if query.startsWith "#" || query.startsWith "--" then loop else
   IO.println <| toString <| ← match ← parse query with
   | .command r => return toJson (← runCommand r)
   | .proofStep r => return toJson (← runProofStep r)

REPL/Snapshots.lean

@@ -182,7 +182,6 @@ def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
   Prod.fst <$> p.runMetaM do p.tacticState.goals.mapM (Meta.ppGoal ·)
-
 /--
 Construct a `ProofSnapshot` from a `ContextInfo` and optional `LocalContext`, and a list of goals.
 
@@ -193,6 +192,7 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext)
     (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
+    goals.head!.withContext do
     pure <|
     { coreState := ← getThe Core.State
       coreContext := ← readThe Core.Context

test/Mathlib/test/20240202/min.in

@@ -1,6 +1,24 @@
-{"cmd": "example {x : Int} (h0 : x > 0) : False := by sorry"}
+{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry"}
 
 {"tactic": "have h : x > 0 := by sorry", "proofState": 0}
 
-{"tactic": "simp [h0]", "proofState": 1}
+-- Some things work:
+
+{"tactic": "exact h0", "proofState": 1}
+
+{"tactic": "assumption", "proofState": 1}
+
+{"tactic": "simp only [of_eq_true (eq_true h0)]", "proofState": 1}
+
+-- These all fail with nonsensical "application type mismatch":
+
+{"tactic": "{ simp [h0] }", "proofState": 1}
+
+{"tactic": "{ simp (config := {memoize := false}) [h0] }", "proofState": 1}
+
+{"tactic": "{ rw (config := {}) [(show x = x from rfl)] }", "proofState": 1}
+
+--- This fails with "motive is not type correct"
+
+{"tactic": "{ rw [(show x = x from rfl)] }", "proofState": 1}
 

test/Mathlib/test/H20240202.lean

@@ -13,7 +13,7 @@ sorry
 
   have h3 := calc
     2 * x = 2 * |x| := by sorry
-    _ > 2 := by try simp [h0]
+    _ > 2 := by (trace_state; rw [(show x = x from rfl)]; simp [h0])
 
   sorry
 }

test/unknown_tactic.expected.out

@@ -10,5 +10,5 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"message": "<input>:1:1: unknown tactic"}
+{"message": "Lean error:\n<input>:1:1: unknown tactic"}