From 9102f8cb13dce7e5be8dc556a296e92592a605bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jun 2022 06:19:56 -0700 Subject: [PATCH] fix: generate `sorry` warning only if there are no error messages see #1163 --- src/Lean/CoreM.lean | 4 +--- src/Lean/Elab/Command.lean | 1 + src/Lean/Elab/SyntheticMVars.lean | 2 +- src/Lean/Elab/Term.lean | 8 ++++---- src/Lean/Log.lean | 2 ++ src/Lean/MonadEnv.lean | 2 +- tests/lean/1163.lean | 20 ++++++++++++++++++-- tests/lean/1163.lean.expected.out | 3 ++- 8 files changed, 30 insertions(+), 12 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index e3cde2cf1d..ea9542a2a1 100644 --- a/src/Lean/CoreM.lean +++ b/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) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 04ac6d483c..f3bf808360 100644 --- a/src/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index ae6bf1092c..31dd341fd7 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/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! diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 1889165c4f..e3fb25a229 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean index 51aff999bf..73ae488e4c 100644 --- a/src/Lean/Log.lean +++ b/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] diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 5596f87252..5cc68818c7 100644 --- a/src/Lean/MonadEnv.lean +++ b/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 diff --git a/tests/lean/1163.lean b/tests/lean/1163.lean index 1bbd3c9eb1..6b0d134f99 100644 --- a/tests/lean/1163.lean +++ b/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 diff --git a/tests/lean/1163.lean.expected.out b/tests/lean/1163.lean.expected.out index 34c5f831f5..babe41d425 100644 --- a/tests/lean/1163.lean.expected.out +++ b/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'