fix: use trimAscii instead of deprecated trim

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Elab/Deriving/Basic.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Elab.App
 public import Lean.Elab.DeclNameGen
+import Lean.Compiler.NoncomputableAttr
 
 public section
 
@@ -173,7 +174,8 @@ We prevent `classStx` from referring to these local variables; instead it's expe
 This function can handle being run from within a nontrivial local context,
 and it uses `mkValueTypeClosure` to construct the final instance.
 -/
-def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit := do
+def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable := false)
+    (cmdRef? : Option Syntax := none) : TermElabM Unit := do
   let { cls := classStx, hasExpose := _ /- todo? -/, .. } := view
   let decl ← whnfCore decl
   let .const declName _ := decl.getAppFn
@@ -220,7 +222,23 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit
     instName := mkPrivateName env instName
   let hints := ReducibilityHints.regular (getMaxHeight env result.value + 1)
   let decl ← mkDefinitionValInferringUnsafe instName result.levelParams.toList result.type result.value hints
-  addAndCompile (logCompileErrors := !(← read).isNoncomputableSection) <| Declaration.defnDecl decl
+  -- Pre-check: if the instance value depends on noncomputable definitions and the user didn't write
+  -- `noncomputable`, give an actionable error with a `Try this:` suggestion.
+  unless isNoncomputable || (← read).isNoncomputableSection do
+    let noncompRef? := result.value.foldConsts none fun n acc =>
+      acc <|> if Lean.isNoncomputable (asyncMode := .local) env n then some n else none
+    if let some noncompRef := noncompRef? then
+      if let some cmdRef := cmdRef? then
+        if let some origText := cmdRef.reprint then
+          let newText := (origText.replace "deriving instance " "deriving noncomputable instance ").trimAscii
+          logInfoAt cmdRef m!"Try this: {newText}"
+      throwError "failed to derive instance because it depends on \
+        `{.ofConstName noncompRef}`, which is noncomputable"
+  if isNoncomputable || (← read).isNoncomputableSection then
+    addDecl <| Declaration.defnDecl decl
+    modifyEnv (addNoncomputable · instName)
+  else
+    addAndCompile <| Declaration.defnDecl decl
   trace[Elab.Deriving] "Derived instance `{.ofConstName instName}`"
   registerInstance instName AttributeKind.global (eval_prio default)
   addDeclarationRangesFromSyntax instName (← getRef)
@@ -284,8 +302,8 @@ def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Arra
   withRef view.ref do
     applyDerivingHandlers (setExpose := view.hasExpose) (← liftCoreM <| view.getClassName) declNames
 
-private def elabDefDeriving (classes : Array DerivingClassView) (decls : Array Syntax) :
-    CommandElabM Unit := runTermElabM fun _ => do
+private def elabDefDeriving (classes : Array DerivingClassView) (decls : Array Syntax)
+    (isNoncomputable := false) (cmdRef? : Option Syntax := none) : CommandElabM Unit := runTermElabM fun _ => do
   for decl in decls do
     withRef decl <| withLogging do
       let declExpr ←
@@ -304,11 +322,12 @@ private def elabDefDeriving (classes : Array DerivingClassView) (decls : Array S
       for cls in classes do
         withLogging do
         withTraceNode `Elab.Deriving (fun _ => return m!"running delta deriving handler for `{cls.cls}` and definition `{declExpr}`") do
-          Term.processDefDeriving cls declExpr
+          Term.processDefDeriving cls declExpr (isNoncomputable := isNoncomputable) (cmdRef? := cmdRef?)
 
 
 @[builtin_command_elab «deriving»] def elabDeriving : CommandElab
-  | `(deriving instance $[$classes],* for $[$decls],*) => do
+  | stx@`(deriving $[noncomputable%$ncTk?]? instance $[$classes],* for $[$decls],*) => do
+    let isNoncomputable := ncTk?.isSome
     let classes ← liftCoreM <| classes.mapM DerivingClassView.ofSyntax
     let decls : Array Syntax := decls
     if decls.all Syntax.isIdent then
@@ -316,13 +335,18 @@ private def elabDefDeriving (classes : Array DerivingClassView) (decls : Array S
       -- If any of the declarations are definitions, then we commit to delta deriving.
       let infos ← declNames.mapM getConstInfo
       if infos.any (·.isDefinition) then
-        elabDefDeriving classes decls
+        elabDefDeriving classes decls (isNoncomputable := isNoncomputable) (cmdRef? := stx)
       else
         -- Otherwise, we commit to using deriving handlers.
-        for cls in classes do
-          cls.applyHandlers declNames
+        if isNoncomputable then
+          withScope (fun sc => { sc with isNoncomputable := true }) do
+            for cls in classes do
+              cls.applyHandlers declNames
+        else
+          for cls in classes do
+            cls.applyHandlers declNames
     else
-      elabDefDeriving classes decls
+      elabDefDeriving classes decls (isNoncomputable := isNoncomputable) (cmdRef? := stx)
   | _ => throwUnsupportedSyntax
 
 builtin_initialize

src/Lean/Parser/Command.lean

@@ -186,7 +186,7 @@ def derivingClass    := leading_parser
   optional ("@[" >> nonReservedSymbol "expose" >> "]") >> withForbidden "for" termParser
 def derivingClasses  := sepBy1 derivingClass ", "
 def optDefDeriving   :=
-  optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
+  optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance" >> notSymbol "noncomputable") >> derivingClasses)
 def definition     := leading_parser
   "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser
@@ -207,7 +207,7 @@ def ctor             := leading_parser
   atomic (optional docComment >> "\n| ") >>
   ppGroup (declModifiers true >> rawIdent >> optDeclSig)
 def optDeriving      := leading_parser
-  optional (ppLine >> atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
+  optional (ppLine >> atomic ("deriving " >> notSymbol "instance" >> notSymbol "noncomputable") >> derivingClasses)
 def computedField    := leading_parser
   declModifiers true >> ident >> " : " >> termParser >> Term.matchAlts
 def computedFields   := leading_parser
@@ -280,7 +280,7 @@ def «structure»          := leading_parser
   («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
    «inductive» <|> «coinductive» <|> classInductive <|> «structure»)
 @[builtin_command_parser] def «deriving»     := leading_parser
-  "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover termParser skip) ", "
+  "deriving " >> optional "noncomputable " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover termParser skip) ", "
 def sectionHeader := leading_parser
   optional ("@[" >> nonReservedSymbol "expose" >> "] ") >>
   optional ("public ") >>

tests/elab/derivingDelta.lean

@@ -319,3 +319,36 @@ can be inserted.
 #guard_msgs in
 def D3 := Bool
 deriving Decidable
+
+/-!
+Noncomputable delta deriving.
+-/
+
+class NC (α : Type) where
+  val : α
+
+noncomputable instance instNCNat : NC Nat where
+  val := Classical.choice ⟨0⟩
+
+def NCAlias := Nat
+
+deriving noncomputable instance NC for NCAlias
+
+/-- info: instNCNCAlias -/
+#guard_msgs in #synth NC NCAlias
+
+/-!
+Actionable error when `noncomputable` is omitted for a noncomputable instance.
+-/
+def NCAlias2 := Nat
+/--
+info: Try this: deriving noncomputable instance NC for NCAlias2
+---
+error: failed to derive instance because it depends on `instNCNat`, which is noncomputable
+-/
+#guard_msgs in deriving instance NC for NCAlias2
+
+/-!
+After the suggestion, `deriving noncomputable instance` works.
+-/
+deriving noncomputable instance NC for NCAlias2