fix tests

Author: Kha

src/Lean/Elab/Command.lean

@@ -303,7 +303,7 @@ def wrapAsyncAsSnapshot {α : Type} (act : α → CommandElabM Unit) (cancelTk?
         withTraceNode `Elab.async (fun _ => return desc) do
           act a
       catch e =>
-        logError e.toMessageData
+        logException e
       finally
         addTraceAsMessages
       get

src/Lean/Elab/Exception.lean

@@ -64,6 +64,11 @@ def isAbortTacticException (ex : Exception) : Bool :=
 def isAbortExceptionId (id : InternalExceptionId) : Bool :=
   id == abortCommandExceptionId || id == abortTermExceptionId || id == abortTacticExceptionId
 
+def isAbortException (ex : Exception) : Bool :=
+  match ex with
+  | Exception.internal id .. => isAbortExceptionId id
+  | _ => false
+
 def mkMessageCore (fileName : String) (fileMap : FileMap) (data : MessageData) (severity : MessageSeverity) (pos : String.Pos.Raw) (endPos : String.Pos.Raw) : Message :=
   let pos := fileMap.toPosition pos
   let endPos := fileMap.toPosition endPos

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -412,7 +412,14 @@ private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType
     hints := .abbrev
     safety := .safe
   }
-  addAndCompile decl
+  try
+    -- disable async codegen so we can catch its exceptions; we don't want to report `evalConst`
+    -- failures below when the actual reason was a codegen failure
+    withOptions (Elab.async.set · false) do
+      addAndCompile decl
+  catch ex =>
+    throwError m!"Tactic `{tacticName}` failed. Error: {ex.toMessageData}"
+
   -- get instance from `d`
   let s := d.appArg!
   let rflPrf ← mkEqRefl (toExpr true)

src/Lean/Linter/MissingDocs.lean

@@ -209,9 +209,9 @@ def checkSyntax : SimpleHandler := fun stx => do
     if stx[5].isNone then lint stx[3] "syntax"
     else lintNamed stx[5][0][3] "syntax"
 
-def mkSimpleHandler (name : String) : SimpleHandler := fun stx => do
+def mkSimpleHandler (name : String) (declNameStxIdx := 2) : SimpleHandler := fun stx => do
   if stx[0].isNone then
-    lintNamed stx[2] name
+    lintNamed stx[declNameStxIdx] name
 
 @[builtin_missing_docs_handler syntaxAbbrev]
 def checkSyntaxAbbrev : SimpleHandler := mkSimpleHandler "syntax"
@@ -240,10 +240,10 @@ def checkClassAbbrev : SimpleHandler := fun stx => do
 def checkSimpLike : SimpleHandler := mkSimpleHandler "simp-like tactic"
 
 @[builtin_missing_docs_handler Option.registerBuiltinOption]
-def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler "option"
+def checkRegisterBuiltinOption : SimpleHandler := mkSimpleHandler (declNameStxIdx := 3) "option"
 
 @[builtin_missing_docs_handler Option.registerOption]
-def checkRegisterOption : SimpleHandler := mkSimpleHandler "option"
+def checkRegisterOption : SimpleHandler := mkSimpleHandler (declNameStxIdx := 3) "option"
 
 @[builtin_missing_docs_handler registerSimpAttr]
 def checkRegisterSimpAttr : SimpleHandler := mkSimpleHandler "simp attr"

tests/lean/run/10213.lean

@@ -12,9 +12,7 @@ error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f =
 theorem bad_csimp : @funnyChoice.{0} = @id.{0} := rfl
 
 /--
-error: Tactic `native_decide` failed: Could not evaluate decidable instance. Error: (interpreter) unknown declaration '_example._nativeDecide_1'
----
-error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable'
+error: Tactic `native_decide` failed. Error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable'
 -/
 #guard_msgs in
 example : False := by

tests/lean/run/grind_bintree.lean

@@ -62,7 +62,7 @@ where
      : toListTR.go t acc = t.toList ++ acc := by
     induction t generalizing acc <;> grind [toListTR.go, toList]
 
-@[csimp] theorem Tree.toList_eq_toListTR_csimp
+@[local csimp] theorem Tree.toList_eq_toListTR_csimp
                  : @Tree.toList = @Tree.toListTR := by
   grind [toList_eq_toListTR]
 

tests/lean/run/noncomputable_decide.lean

@@ -1,9 +1,7 @@
 open scoped Classical
 
 /--
-error: Tactic `native_decide` failed: Could not evaluate decidable instance. Error: (interpreter) unknown declaration 'ohno._nativeDecide_1_1'
----
-error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', which is 'noncomputable'
+error: Tactic `native_decide` failed. Error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', which is 'noncomputable'
 -/
 #guard_msgs in
 theorem ohno : False := by