fix: generate sorry warning only if there are no error messages

see #1163

src/Lean/CoreM.lean

@@ -214,14 +214,12 @@ instance : MonadLog CoreM where
   getRef      := getRef
   getFileMap  := return (← read).fileMap
   getFileName := return (← read).fileName
+  hasErrors   := return (← get).messages.hasErrors
   logMessage msg := do
     let ctx ← read
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
     modify fun s => { s with messages := s.messages.add msg }
 
-def hasErrors : CoreM Bool :=
-  return (← get).messages.hasErrors
-
 end Core
 
 export Core (CoreM mkFreshUserName checkMaxHeartbeats withCurrHeartbeats)

src/Lean/Elab/Command.lean

@@ -183,6 +183,7 @@ instance : MonadLog CommandElabM where
   getRef      := getRef
   getFileMap  := return (← read).fileMap
   getFileName := return (← read).fileName
+  hasErrors   := return (← get).messages.hasErrors
   logMessage msg := do
     let currNamespace ← getCurrNamespace
     let openDecls ← getOpenDecls

src/Lean/Elab/SyntheticMVars.lean

@@ -233,7 +233,7 @@ def reportStuckSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (ignoreStuc
       unless ignoreStuckTC do
         withMVarContext mvarSyntheticDecl.mvarId do
           let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
-          unless (← Core.hasErrors) do
+          unless (← MonadLog.hasErrors) do
             throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}"
     | SyntheticMVarKind.coe header eNew expectedType eType e f? =>
       let mvarId := eNew.appArg!.mvarId!

src/Lean/Elab/Term.lean

@@ -374,7 +374,7 @@ def withoutErrToSorry (x : TermElabM α) : TermElabM α :=
 
 /-- For testing `TermElabM` methods. The #eval command will sign the error. -/
 def throwErrorIfErrors : TermElabM Unit := do
-  if (← Core.hasErrors) then
+  if (← MonadLog.hasErrors) then
     throwError "Error(s)"
 
 def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit :=
@@ -437,7 +437,7 @@ def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData)
   cannot continue if there are metavariables in patterns.
   We only want to log it if we haven't logged any error so far. -/
 def throwMVarError (m : MessageData) : TermElabM α := do
-  if (← Core.hasErrors) then
+  if (← MonadLog.hasErrors) then
     throwAbortTerm
   else
     throwError m
@@ -479,7 +479,7 @@ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Op
   if pendingMVarIds.isEmpty then
     return false
   else
-    let hasOtherErrors ← Core.hasErrors
+    let hasOtherErrors ← MonadLog.hasErrors
     let mut hasNewErrors := false
     let mut alreadyVisited : MVarIdSet := {}
     let mut errors : Array MVarErrorInfo := #[]
@@ -1279,7 +1279,7 @@ def commitIfNoErrors? (x : TermElabM α) : TermElabM (Option α) := do
   Core.resetMessageLog
   try
     let a ← x
-    if (← Core.hasErrors) then
+    if (← MonadLog.hasErrors) then
       restoreState saved
       return none
     else

src/Lean/Log.lean

@@ -10,6 +10,7 @@ namespace Lean
 class MonadLog (m : Type → Type) extends MonadFileMap m where
   getRef       : m Syntax
   getFileName  : m String
+  hasErrors    : m Bool
   logMessage   : Message → m Unit
 
 export MonadLog (getFileName logMessage)
@@ -18,6 +19,7 @@ instance (m n) [MonadLift m n] [MonadLog m] : MonadLog n where
   getRef      := liftM (MonadLog.getRef : m _)
   getFileMap  := liftM (getFileMap : m _)
   getFileName := liftM (getFileName : m _)
+  hasErrors   := liftM (MonadLog.hasErrors : m _)
   logMessage  := fun msg => liftM (logMessage msg : m _ )
 
 variable [Monad m] [MonadLog m] [AddMessageContext m]

src/Lean/MonadEnv.lean

@@ -123,7 +123,7 @@ def getConstInfoRec [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m
       | _ => failK ()
 
 def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadLog m] [AddMessageContext m] (decl : Declaration) : m Unit := do
-  if decl.hasNonSyntheticSorry then
+  if !(← MonadLog.hasErrors) && decl.hasSorry then
     logWarning "declaration uses 'sorry'"
   match (← getEnv).addDecl decl with
   | Except.ok    env => setEnv env

tests/lean/1163.lean

@@ -1,3 +1,19 @@
-macro "obviously" : tactic => `(exact sorryAx _)
+import Lean
+open Lean Elab Tactic
 
-theorem result : False := by obviously
+macro "obviously1" : tactic => `(exact sorryAx _)
+
+theorem result1 : False := by obviously1
+
+elab "obviously2" : tactic =>
+  liftMetaTactic1 (Meta.admit · *> pure none)
+
+theorem result2 : False := by obviously2
+
+def x : Bool := 0
+
+theorem result3 : False := by obviously2
+
+theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error
+  let x : Bool := 0
+  obviously2

tests/lean/1163.lean.expected.out

@@ -1 +1,2 @@
-1163.lean:3:8-3:14: warning: declaration uses 'sorry'
+1163.lean:6:8-6:15: warning: declaration uses 'sorry'
+1163.lean:11:8-11:15: warning: declaration uses 'sorry'