From 81fe3b6d05360bd00dea3604a184076deae5e4ff Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Mon, 8 Sep 2025 05:14:42 -0700
Subject: [PATCH] feat: pretty print sorry in "declaration uses 'sorry'"
 (#10034)

This PR changes the "declaration uses 'sorry'" error to pretty print an
actual `sorry` expression in the message. The effect is that the `sorry`
is hoverable and, if it's labeled, you can "go to definition" to see
where it came from.

The implementation prefers reporting synthetic sorries. These can appear
even if there are no error messages if a declaration refers to a
declaration that has elaboration errors. Users should focus on
elaboration errors before worrying about user-written `sorry`s.

In the future we could have some more precise logic for sorry reporting.
All the sorries in a declaration should be considered to be reported,
and we should not re-report sorries in later declarations. Some
elaborators use `warn.sorry` to avoid re-reporting sorries in auxiliary
declarations.
---
 src/Lean/AddDecl.lean    | 27 ++++++++++++++++++++++++---
 src/Lean/Meta/Sorry.lean | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 64 insertions(+), 3 deletions(-)

diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index f36e65ea1d..79eaeb8f72 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.CoreM
+public import Lean.Meta.Sorry
 public import Lean.Namespace
 public import Lean.Util.CollectAxioms
 
@@ -75,6 +76,28 @@ register_builtin_option warn.sorry : Bool := {
   descr    := "warn about uses of `sorry` in declarations added to the environment"
 }
 
+/--
+If the `warn.sorry` option is set to true and there are no errors in the log already,
+logs a warning if the declaration uses `sorry`.
+-/
+def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
+  if warn.sorry.get (← getOptions) then
+    if !(← MonadLog.hasErrors) && decl.hasSorry then
+      -- Find an actual sorry expression to use for 'sorry'.
+      -- That way the user can hover over it to see its type and use "go to definition" if it is a labeled sorry.
+      let findSorry : StateRefT (Array (Bool × MessageData)) MetaM Unit := decl.forEachSorryM fun s => do
+        let s' ← addMessageContext s
+        modify fun arr => arr.push (s.isSyntheticSorry, s')
+      let (_, sorries) ← findSorry |>.run #[] |>.run'
+      -- Prefer reporting a synthetic sorry.
+      -- These can appear without logged errors if `decl` is referring to declarations with elaboration errors;
+      -- that's where a user should direct their focus.
+      if let some (_, s) := sorries.find? (·.1) <|> sorries[0]? then
+        logWarning <| .tagged `hasSorry m!"declaration uses '{s}'"
+      else
+        -- This case should not happen, but it ensures a warning will get logged no matter what.
+        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+
 def addDecl (decl : Declaration) : CoreM Unit := do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
@@ -143,9 +166,7 @@ where
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
       withTraceNode `Kernel (return m!"{exceptEmoji ·} typechecking declarations {decl.getTopLevelNames}") do
-        if warn.sorry.get (← getOptions) then
-          if !(← MonadLog.hasErrors) && decl.hasSorry then
-            logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        warnIfUsesSorry decl
         try
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
diff --git a/src/Lean/Meta/Sorry.lean b/src/Lean/Meta/Sorry.lean
index fb28d71971..b9485160f3 100644
--- a/src/Lean/Meta/Sorry.lean
+++ b/src/Lean/Meta/Sorry.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Data.Lsp.Utf16
+public import Lean.Meta.ForEachExpr
 public import Lean.Meta.InferType
 public import Lean.Util.Recognizers
 
@@ -123,3 +124,42 @@ def isLabeledSorry? (e : Expr) : Option SorryLabelView := do
     guard <| arg.appFn!.appArg!.isAppOfArity ``Unit.unit 0
     let tag ← arg.appArg!.name?
     SorryLabelView.decode? tag
+
+end Meta
+
+/--
+If `e` is a sorry application, returns the sorry itself,
+stripping off any arguments in case the `sorry` is standing in for a function.
+
+For labeled sorries, includes the label information.
+-/
+def Expr.getSorry? (e : Expr) : Option Expr :=
+  if e.isSorry then
+    if (Meta.isLabeledSorry? e).isSome then
+      e.getBoundedAppFn (e.getAppNumArgs - 3)
+    else
+      e.getBoundedAppFn (e.getAppNumArgs - 2)
+  else
+    none
+
+/--
+Evaluates `fn` on each `sorry` in the expression.
+Instantiates bound variables with free variables.
+-/
+def Meta.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr)
+    (fn : Expr → m Unit) : m Unit := do
+  Meta.forEachExpr' input fun e => do
+    if let some e' := e.getSorry? then
+      fn e'
+      return false
+    else
+      return true
+
+/--
+Evaluates `fn` on each `sorry` in the declaration.
+-/
+def Declaration.forEachSorryM {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (decl : Declaration)
+    (fn : Expr → m Unit) : m Unit := do
+  decl.forExprM (Meta.forEachSorryM · fn)
+
+end Lean