feat: recover from errors in attributes

src/Lean/Elab/Attributes.lean

@@ -57,14 +57,17 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
      So, we expand them before here before we invoke the attributer handlers implemented using `AttrM`. -/
   pure { kind := attrKind, name := attrName, stx := attr }
 
-def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (attrInstances : Array Syntax) : m (Array Attribute) := do
+def elabAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (attrInstances : Array Syntax) : m (Array Attribute) := do
   let mut attrs := #[]
   for attr in attrInstances do
-    attrs := attrs.push (← elabAttr attr)
+    try
+      attrs := attrs.push (← withRef attr do elabAttr attr)
+    catch ex =>
+      logException ex
   return attrs
 
 -- leading_parser "@[" >> sepBy1 attrInstance ", " >> "]"
-def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (stx : Syntax) : m (Array Attribute) :=
+def elabDeclAttrs [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m] (stx : Syntax) : m (Array Attribute) :=
   elabAttrs stx[1].getSepArgs
 
 end Lean.Elab

src/Lean/Elab/Command.lean

@@ -259,18 +259,6 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
   descr    := "show elaboration errors from partial syntax trees (i.e. after parser recovery)"
 }
 
-def withLogging (x : CommandElabM Unit) : CommandElabM Unit := do
-  try
-    x
-  catch ex => match ex with
-    | Exception.error _ _     => logException ex
-    | Exception.internal id _ =>
-      if isAbortExceptionId id then
-        pure ()
-      else
-        let idName ← liftIO <| id.getName;
-        logError m!"internal exception {idName}"
-
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do

src/Lean/Elab/DeclModifiers.lean

@@ -96,7 +96,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m (
 
 section Methods
 
-variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m]
+variable [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLog m] [MonadLiftT IO m]
 
 def elabModifiers (stx : Syntax) : m Modifiers := do
   let docCommentStx := stx[0]

src/Lean/Elab/Declaration.lean

@@ -183,16 +183,19 @@ def elabDeclaration : CommandElab := fun stx => do
     let newStx ← `(namespace $ns:ident $newStx end $ns:ident)
     withMacroExpansion stx newStx <| elabCommand newStx
   | none => do
-    let modifiers ← elabModifiers stx[0]
     let decl     := stx[1]
     let declKind := decl.getKind
     if declKind == ``Lean.Parser.Command.«axiom» then
+      let modifiers ← elabModifiers stx[0]
       elabAxiom modifiers decl
     else if declKind == ``Lean.Parser.Command.«inductive» then
+      let modifiers ← elabModifiers stx[0]
       elabInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.classInductive then
+      let modifiers ← elabModifiers stx[0]
       elabClassInductive modifiers decl
     else if declKind == ``Lean.Parser.Command.«structure» then
+      let modifiers ← elabModifiers stx[0]
       elabStructure modifiers decl
     else if isDefLike decl then
       elabMutualDef #[stx] (getTerminationHints stx)
@@ -310,9 +313,10 @@ def elabMutual : CommandElab := fun stx => do
   for attrKindStx in stx[2].getSepArgs do
     if attrKindStx.getKind == ``Lean.Parser.Command.eraseAttr then
       let attrName := attrKindStx[1].getId.eraseMacroScopes
-      unless isAttribute (← getEnv) attrName do
-        throwError "unknown attribute [{attrName}]"
-      toErase := toErase.push attrName
+      if isAttribute (← getEnv) attrName then
+        toErase := toErase.push attrName
+      else
+        logErrorAt attrKindStx "unknown attribute [{attrName}]"
     else
       attrInsts := attrInsts.push attrKindStx
   let attrs ← elabAttrs attrInsts

src/Lean/Elab/Term.lean

@@ -617,6 +617,7 @@ private def applyAttributesCore
     (declName : Name) (attrs : Array Attribute)
     (applicationTime? : Option AttributeApplicationTime) : TermElabM Unit :=
   for attr in attrs do
+    withRef attr.stx do withLogging do
     let env ← getEnv
     match getAttributeImpl env attr.name with
     | Except.error errMsg => throwError errMsg

src/Lean/Elab/Util.lean

@@ -204,6 +204,10 @@ def logException [Monad m] [MonadLog m] [AddMessageContext m] [MonadLiftT IO m]
       let name ← id.getName
       logError m!"internal exception: {name}"
 
+def withLogging [Monad m] [MonadLog m] [MonadExcept Exception m] [AddMessageContext m] [MonadLiftT IO m]
+    (x : m Unit) : m Unit := do
+  try x catch ex => logException ex
+
 @[inline] def trace [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
   if checkTraceOption (← getOptions) cls then
     logTrace cls (msg ())

tests/lean/248.lean.expected.out

@@ -1 +1 @@
-248.lean:1:28-1:31: error: invalid 'implementedBy' argument 'foo', function cannot be implemented by itself
+248.lean:1:2-1:19: error: invalid 'implementedBy' argument 'foo', function cannot be implemented by itself

tests/lean/973.lean.expected.out

@@ -1,2 +1,2 @@
-973.lean:5:8-5:22: error: invalid `simp` theorem, equation is equivalent to
+973.lean:4:2-4:6: error: invalid `simp` theorem, equation is equivalent to
   x = x

tests/lean/class_def_must_fail.lean.expected.out

@@ -1,2 +1,2 @@
-class_def_must_fail.lean:2:13-2:16: error: invalid 'class', declaration 'Foo' must be inductive datatype, structure, or constant
-class_def_must_fail.lean:7:18-7:21: error: invalid 'class', declaration 'Bla' must be inductive datatype, structure, or constant
+class_def_must_fail.lean:2:2-2:7: error: invalid 'class', declaration 'Foo' must be inductive datatype, structure, or constant
+class_def_must_fail.lean:7:11-7:16: error: invalid 'class', declaration 'Bla' must be inductive datatype, structure, or constant

tests/lean/csimpAttr.lean.expected.out

@@ -3,4 +3,4 @@
 def f (x_1 : obj) : obj :=
   let x_2 : obj := Nat.add x_1 x_1;
   let x_3 : obj := Nat.add x_2 x_2;
-  ret x_3csimpAttr.lean:7:17-7:28: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.
+  ret x_3csimpAttr.lean:7:2-7:7: error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.

tests/lean/heapSort.lean.expected.out

@@ -11,4 +11,4 @@ heapSort.lean:102:4-102:13: warning: declaration uses 'sorry'
     | some x =>
       let_fun this := (_ : BinaryHeap.size (BinaryHeap.popMax a) < BinaryHeap.size a);
       Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)
-heapSort.lean:178:17-178:39: warning: declaration uses 'sorry'
+heapSort.lean:178:11-178:15: warning: declaration uses 'sorry'

tests/lean/implementedByIssue.lean.expected.out

@@ -1,5 +1,5 @@
-implementedByIssue.lean:15:32-15:42: error: invalid 'implementedBy' argument 'Hidden.get_2', 'Hidden.get_2' has 0 universe level parameter(s), but 'Hidden.Array.data' has 1
-implementedByIssue.lean:19:32-19:42: error: invalid 'implementedBy' argument 'Hidden.get_3', 'Hidden.get_3' has type
+implementedByIssue.lean:15:11-15:30: error: invalid 'implementedBy' argument 'Hidden.get_2', 'Hidden.get_2' has 0 universe level parameter(s), but 'Hidden.Array.data' has 1
+implementedByIssue.lean:19:11-19:30: error: invalid 'implementedBy' argument 'Hidden.get_3', 'Hidden.get_3' has type
   {α : Type u} → {n : Nat} → Fin n → Array α n → α
 but 'Hidden.Array.data' has type
   {α : Type u} → {n : Nat} → Array α n → Fin n → α

tests/lean/inductive1.lean.expected.out

@@ -18,7 +18,7 @@ inductive1.lean:69:2-69:5: error: 'Boo.T1.bla' has already been declared
 inductive1.lean:73:10-73:12: error: 'Boo.T1' has already been declared
 inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declaration
 inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration
-inductive1.lean:82:10-82:30: error: declaration is not a definition 'T1''
+inductive1.lean:82:2-82:8: error: declaration is not a definition 'T1''
 inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype
 inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
 inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration

tests/lean/nonfatalattrs.lean

@@ -0,0 +1,13 @@
+-- Even if there are errors in the attributes,
+-- the definition should still be declared.
+
+-- Attributes without implementation
+syntax "unimplementedattr" : attr
+@[unimplementedattr] def foo := 42
+#check foo
+
+-- Attributes that fail during application
+def bar :=
+  let rec @[class] bar : Nat := 42
+  bar
+#check bar

tests/lean/nonfatalattrs.lean.expected.out

@@ -0,0 +1,4 @@
+nonfatalattrs.lean:6:2-6:19: error: unknown attribute [attrUnimplementedattr]
+foo : Nat
+nonfatalattrs.lean:11:12-11:17: error: invalid 'class', declaration 'bar.bar' must be inductive datatype, structure, or constant
+bar : Nat

tests/lean/scopedInstanceOutsideNamespace.lean.expected.out

@@ -1,4 +1,4 @@
 scopedInstanceOutsideNamespace.lean:1:0-2:38: error: scoped attributes must be used inside namespaces
 "true"
 scopedInstanceOutsideNamespace.lean:6:0-6:30: error: scoped attributes must be used inside namespaces
-scopedInstanceOutsideNamespace.lean:8:0-10:38: error: scoped attributes must be used inside namespaces
+scopedInstanceOutsideNamespace.lean:8:2-8:17: error: scoped attributes must be used inside namespaces

tests/lean/scopedMacros.lean.expected.out

@@ -1,7 +1,7 @@
 10 + 1 : Nat
 scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!'
 10 + 1 : Nat
-scopedMacros.lean:19:0-19:50: error: scoped attributes must be used inside namespaces
+scopedMacros.lean:19:0-19:37: error: scoped attributes must be used inside namespaces
 scopedMacros.lean:19:7-19:50: error: invalid syntax node kind 'termBla!_'
 scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!'
 scopedMacros.lean:36:0-36:45: error: scoped attributes must be used inside namespaces