feat: do not propagate pretty printer errors through messages

src/Lean/Elab/GuardMsgs.lean

@@ -26,7 +26,7 @@ namespace Lean.Elab.Tactic.GuardMsgs
 
 /-- Gives a string representation of a message without source position information.
 Ensures the message ends with a '\n'. -/
-private def messageToStringWithoutPos (msg : Message) : IO String := do
+private def messageToStringWithoutPos (msg : Message) : BaseIO String := do
   let mut str ← msg.data.toString
   unless msg.caption == "" do
     str := msg.caption ++ ":\n" ++ str

src/Lean/Message.lean

@@ -91,7 +91,7 @@ inductive MessageData where
   If the thunked message is produced for a term that contains a synthetic sorry,
   `hasSyntheticSorry` should return `true`.
   This is used to filter out certain messages. -/
-  | ofLazy (f : Option PPContext → IO Dynamic) (hasSyntheticSorry : MetavarContext → Bool)
+  | ofLazy (f : Option PPContext → BaseIO Dynamic) (hasSyntheticSorry : MetavarContext → Bool)
   deriving Inhabited, TypeName
 
 namespace MessageData
@@ -103,7 +103,7 @@ def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty
 Lazy message data production, with access to the context as given by
 a surrounding `MessageData.withContext` (which is expected to exist).
 -/
-def lazy (f : PPContext → IO MessageData)
+def lazy (f : PPContext → BaseIO MessageData)
     (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData :=
   .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
     let msg ← match ctx? with
@@ -220,9 +220,9 @@ where
   | trace _ msg msgs        => visit mctx? msg || msgs.any (visit mctx?)
   | _                       => false
 
-partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format
-  | _, _,            ofFormatWithInfos fmt    => return fmt.1
-  | _,    none,      ofGoal mvarId            => return "goal " ++ format (mkMVar mvarId)
+partial def formatAux : NamingContext → Option MessageDataContext → MessageData → BaseIO Format
+  | _,    _,         ofFormatWithInfos fmt    => return fmt.1
+  | _,    none,      ofGoal mvarId            => return formatRawGoal mvarId
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, ctx,       ofWidget _ d             => formatAux nCtx ctx d
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
@@ -244,10 +244,10 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
       | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
     formatAux nCtx ctx? msg
 
-protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : IO Format :=
+protected def format (msgData : MessageData) (ctx? : Option MessageDataContext := none) : BaseIO Format :=
   formatAux { currNamespace := Name.anonymous, openDecls := [] } ctx? msgData
 
-protected def toString (msgData : MessageData) : IO String := do
+protected def toString (msgData : MessageData) : BaseIO String := do
   return toString (← msgData.format)
 
 instance : Append MessageData := ⟨compose⟩
@@ -374,14 +374,14 @@ namespace Message
   msg.data.kind
 
 /-- Serializes the message, converting its data into a string and saving its kind. -/
-@[inline] def serialize (msg : Message) : IO SerialMessage := do
+@[inline] def serialize (msg : Message) : BaseIO SerialMessage := do
   return {msg with kind := msg.kind, data := ← msg.data.toString}
 
-protected def toString (msg : Message) (includeEndPos := false) : IO String := do
+protected def toString (msg : Message) (includeEndPos := false) : BaseIO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared
   return inline <| (← msg.serialize).toString includeEndPos
 
-protected def toJson (msg : Message) : IO Json := do
+protected def toJson (msg : Message) : BaseIO Json := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared
   return inline <| toJson (← msg.serialize)
 

src/Lean/PrettyPrinter.lean

@@ -142,8 +142,10 @@ open Lean PrettyPrinter Delaborator
 Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value.
 -/
 def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData :=
-  .lazy fun ctx => ctx.runMetaM <|
-    .ofFormatWithInfos <$> fmt
+  .lazy fun ctx => do
+    match (← ctx.runMetaM fmt |>.toBaseIO) with
+    | .ok fmt => return .ofFormatWithInfos fmt
+    | .error ex => return m!"[Error pretty printing: {ex}]"
 
 /--
 Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
@@ -152,7 +154,11 @@ comprise the expressions that are included in the message data.
 -/
 def ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
   .lazy
-    (f := fun ppctxt => ppctxt.runMetaM f)
+    (f := fun ppctxt => do
+      match (← ppctxt.runMetaM f |>.toBaseIO) with
+      | .ok fmt => return fmt
+      | .error ex => return m!"[Error pretty printing: {ex}]"
+      )
     (hasSyntheticSorry := fun mvarctxt => es.any (fun a =>
         instantiateMVarsCore mvarctxt a |>.1.hasSyntheticSorry
     ))
@@ -168,11 +174,16 @@ def ofConst (e : Expr) : MessageData :=
     let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst
     .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delab) e)
   else
+    have : Inhabited MessageData :=
+      ⟨m!"[Error pretty printing: expression not a constant]{Format.line}{e}"⟩
     panic! "not a constant"
 
 /-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
 def signature (c : Name) : MessageData :=
-  .ofFormatWithInfosM (PrettyPrinter.ppSignature c)
+  .lazy fun ctx => do
+    match (← ctx.runMetaM (PrettyPrinter.ppSignature c) |>.toBaseIO) with
+    | .ok fmt => return .ofFormatWithInfos fmt
+    | .error ex => return m!"[Error pretty printing signature: {ex}]{Format.line}{c}"
 
 end MessageData
 

src/Lean/Util/PPExt.lean

@@ -54,55 +54,73 @@ structure PPFns where
   ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
   ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos
   ppTerm : PPContext → Term → IO Format
-  ppLevel : PPContext → Level → IO Format
+  ppLevel : PPContext → Level → BaseIO Format
   ppGoal : PPContext → MVarId → IO Format
   deriving Inhabited
 
+def formatRawTerm (ctx : PPContext) (stx : Term) : Format :=
+  stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
+
+def formatRawGoal (mvarId : MVarId) : Format :=
+  "goal " ++ format (mkMVar mvarId)
+
 builtin_initialize ppFnsRef : IO.Ref PPFns ←
   IO.mkRef {
     ppExprWithInfos := fun _ e => return format (toString e)
     ppConstNameWithInfos := fun _ n => return format n
-    ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts)
+    ppTerm := fun ctx stx => return formatRawTerm ctx stx
     ppLevel := fun _ l => return format l
-    ppGoal := fun _ _ => return "goal"
+    ppGoal := fun _ mvarId => return formatRawGoal mvarId
   }
 
 builtin_initialize ppExt : EnvExtension PPFns ←
   registerEnvExtension ppFnsRef.get
 
-def ppExprWithInfos (ctx : PPContext) (e : Expr) : IO FormatWithInfos := do
+def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do
   if pp.raw.get ctx.opts then
     let e := instantiateMVarsCore ctx.mctx e |>.1
     return format (toString e)
   else
-    try
-      ppExt.getState ctx.env |>.ppExprWithInfos ctx e
-    catch ex =>
+    match (← ppExt.getState ctx.env |>.ppExprWithInfos ctx e |>.toBaseIO) with
+    | .ok fmt => return fmt
+    | .error ex =>
       if pp.rawOnError.get ctx.opts then
         pure f!"[Error pretty printing expression: {ex}. Falling back to raw printer.]{Format.line}{e}"
       else
         pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppConstNameWithInfos (ctx : PPContext) (n : Name) : IO FormatWithInfos :=
-  ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n
+def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos := do
+  match (← ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n |>.toBaseIO) with
+  | .ok fmt => return fmt
+  | .error ex =>
+    if pp.rawOnError.get ctx.opts then
+      pure f!"[Error pretty printing constant: {ex}. Falling back to raw printer.]{Format.line}{format n}"
+    else
+      pure f!"failed to pretty print constant (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppTerm (ctx : PPContext) (stx : Term) : IO Format :=
-  let fmtRaw := fun () => stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts)
+def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
   if pp.raw.get ctx.opts then
-    return fmtRaw ()
+    return formatRawTerm ctx stx
   else
-    try
-      ppExt.getState ctx.env |>.ppTerm ctx stx
-    catch ex =>
+    match (← ppExt.getState ctx.env |>.ppTerm ctx stx  |>.toBaseIO) with
+    | .ok fmt => return fmt
+    | .error ex =>
       if pp.rawOnError.get ctx.opts then
-        pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{fmtRaw ()}"
+        pure f!"[Error pretty printing syntax: {ex}. Falling back to raw printer.]{Format.line}{formatRawTerm ctx stx}"
       else
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
-def ppLevel (ctx : PPContext) (l : Level) : IO Format :=
+def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format :=
   ppExt.getState ctx.env |>.ppLevel ctx l
 
-def ppGoal (ctx : PPContext) (mvarId : MVarId) : IO Format :=
-  ppExt.getState ctx.env |>.ppGoal ctx mvarId
+def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do
+  match (← ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with
+  | .ok fmt => return fmt
+  | .error ex =>
+    if pp.rawOnError.get ctx.opts then
+      pure f!"[Error pretty printing goal: {ex}. Falling back to raw printer.]{Format.line}{formatRawGoal mvarId}"
+    else
+      pure f!"failed to pretty print goal (use 'set_option pp.rawOnError true' for raw representation)"
+
 
 end Lean

src/Lean/Util/Trace.lean

@@ -86,7 +86,7 @@ variable {α : Type} {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions
 
 def printTraces : m Unit := do
   for {msg, ..} in (← getTraceState).traces do
-    IO.println (← msg.format)
+    IO.println (← msg.format.toIO)
 
 def resetTraceState : m Unit :=
   modifyTraceState (fun _ => {})

src/lake/Lake/Util/Message.lean

@@ -55,11 +55,8 @@ def mkMessageStringCore
 
 def mkMessageString (msg : Message) (includeEndPos := false) (infoWithPos := false) : BaseIO String := do
   let endPos? := if includeEndPos then msg.endPos else none
-  match (← msg.data.toString.toBaseIO) with
-  | .ok s =>
-    return mkMessageStringCore msg.severity msg.fileName msg.caption s msg.pos endPos? infoWithPos
-  | .error e =>
-    return mkMessageStringCore .error msg.fileName msg.caption (toString e) msg.pos endPos? infoWithPos
+  let s ← msg.data.toString
+  return mkMessageStringCore msg.severity msg.fileName msg.caption s msg.pos endPos? infoWithPos
 
 def mkMessageLogString (log : MessageLog) : BaseIO String :=
   log.toList.foldlM (init := "") fun s m => do