From ad55ea1a271196c326a81ba719819fb57b895ac6 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 1 May 2025 13:37:35 -0400
Subject: [PATCH] feat(repl): Detection of sorrys

---
 Repl.lean             | 3 +++
 Test/Integration.lean | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/Repl.lean b/Repl.lean
index a9193d3..ce6a9df 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -338,11 +338,14 @@ def execute (command: Protocol.Command): MainM Json := do
           pure result
         | false, _ => pure nextGoalState
       let nextStateId ← newGoalState nextGoalState
+      let parentExpr := nextGoalState.parentExpr?.get!
       let goals ← runCoreM $ nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
       return {
         nextStateId? := .some nextStateId,
         goals? := .some goals,
         messages? := .some messages,
+        hasSorry := parentExpr.hasSorry,
+        hasUnsafe := (← getEnv).hasUnsafe parentExpr,
       }
     | .ok (.parseError message) =>
       return { messages? := .none, parseError? := .some message }
diff --git a/Test/Integration.lean b/Test/Integration.lean
index beec62a..9945185 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -92,7 +92,9 @@ def test_tactic : Test :=
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply Nat.le_of_succ_le" }: Protocol.GoalTactic)
      ({ messages? := .some #["tactic 'apply' failed, failed to unify\n  ∀ {m : Nat}, Nat.succ ?n ≤ m → ?n ≤ m\nwith\n  ∀ (q : Prop), x ∨ q → q ∨ x\nx : Prop\n⊢ ∀ (q : Prop), x ∨ q → q ∨ x"] }:
-      Protocol.GoalTacticResult)
+      Protocol.GoalTacticResult),
+    step "goal.tactic" ({ stateId := 0, tactic? := .some "sorry" }: Protocol.GoalTactic)
+     ({ nextStateId? := .some 3, goals? := .some #[], hasSorry := true }: Protocol.GoalTacticResult),
   ]
 example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by
   simp