From 3ca0aef098360340befe033b29dba4a682e40850 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Jan 2021 06:32:39 -0800
Subject: [PATCH] feat: generate warning when `sorry` is used

---
 src/Lean/Elab/BuiltinNotation.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 0c01369f39..4a2cf0fd7e 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -189,8 +189,10 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
   else
     `(dbgTrace (toString $arg) fun _ => $body)
 
-@[builtinMacro Lean.Parser.Term.«sorry»]  def expandSorry : Macro := fun _ =>
-  `(sorryAx _ false)
+@[builtinTermElab «sorry»] def elabSorry : TermElab := fun stx expectedType? => do
+  logWarning "declaration uses 'sorry'"
+  let stxNew ← `(sorryAx _ false)
+  withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
 
 @[builtinTermElab emptyC] def expandEmptyC : TermElab := fun stx expectedType? => do
   let stxNew ← `(EmptyCollection.emptyCollection)