chore: preserve reported messages in MessageLog

src/Lean/CoreM.lean

@@ -612,14 +612,14 @@ instance : MonadRuntimeException CoreM where
 
 /--
 Returns `true` if the given message kind has not been reported in the message log,
-and then mark it as reported. Otherwise, returns `false`.
-We use this API to ensure we don't report the same kind of warning multiple times.
+and then mark it as logged. Otherwise, returns `false`.
+We use this API to ensure we don't log the same kind of warning multiple times.
 -/
-def reportMessageKind (kind : Name) : CoreM Bool := do
-  if (← get).messages.reportedKinds.contains kind then
+def logMessageKind (kind : Name) : CoreM Bool := do
+  if (← get).messages.loggedKinds.contains kind then
     return false
   else
-    modify fun s => { s with messages.reportedKinds := s.messages.reportedKinds.insert kind }
+    modify fun s => { s with messages.loggedKinds := s.messages.loggedKinds.insert kind }
     return true
 
 end Lean

src/Lean/Message.lean

@@ -391,23 +391,14 @@ end Message
 A persistent array of messages.
 
 In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at
-various points inside a command, which will empty `unreported` and updated `hadErrors` accordingly
-(see `CoreM.getAndEmptyMessageLog`).
+various points inside a command, which will empty `unreported` and move its messages to `reported`.
+Reported messages are preserved for some specific "lookback" operations such as `hasError` that
+should consider the entire message history of the current command; most other functions such as
+`add` and `toList` will only operate on unreported messages.
 -/
 structure MessageLog where
-  /--
-  If true, there was an error in the log previously that has already been reported to the user and
-  removed from the log. Thus we say that in the current context (usually the current command), we
-  "have errors" if either this flag is set or there is an error in `msgs`; see
-  `MessageLog.hasErrors`. If we have errors, we suppress some error messages that are often the
-  result of a previous error.
-  -/
-  /-
-  Design note: We considered introducing a `hasErrors` field instead that already includes the
-  presence of errors in `msgs` but this would not be compatible with e.g.
-  `MessageLog.errorsToWarnings`.
-  -/
-  hadErrors : Bool := false
+  /-- The list of messages already reported (i.e. saved in a `Snapshot`), in insertion order. -/
+  reported : PersistentArray Message := {}
   /-- The list of messages not already reported, in insertion order. -/
   unreported : PersistentArray Message := {}
   /--
@@ -416,7 +407,7 @@ structure MessageLog where
   the configuration option `exponentiation.threshold`.
   We don't produce a warning if the kind is already in the following set.
   -/
-  reportedKinds : NameSet := {}
+  loggedKinds : NameSet := {}
   deriving Inhabited
 
 namespace MessageLog
@@ -426,24 +417,33 @@ def empty : MessageLog := {}
 using `MessageLog.toList/toArray`" (since := "2024-05-22")]
 def msgs : MessageLog → PersistentArray Message := unreported
 
+def reportedPlusUnreported : MessageLog → PersistentArray Message
+  | { reported := r, unreported := u, .. } => r ++ u
+
 def hasUnreported (log : MessageLog) : Bool :=
   !log.unreported.isEmpty
 
 def add (msg : Message) (log : MessageLog) : MessageLog :=
   { log with unreported := log.unreported.push msg }
 
-protected def append (l₁ l₂ : MessageLog) : MessageLog :=
-  { hadErrors := l₁.hadErrors || l₂.hadErrors, unreported := l₁.unreported ++ l₂.unreported }
+protected def append (l₁ l₂ : MessageLog) : MessageLog where
+  reported := l₁.reported ++ l₂.reported
+  unreported := l₁.unreported ++ l₂.unreported
+  loggedKinds := l₁.loggedKinds.union l₂.loggedKinds
 
 instance : Append MessageLog :=
   ⟨MessageLog.append⟩
 
+/--
+Checks if either of `reported` or `unreported` contains an error, i.e. whether the current command
+has errored yet.
+-/
 def hasErrors (log : MessageLog) : Bool :=
-  log.hadErrors || log.unreported.any (·.severity matches .error)
+  log.reported.any (·.severity matches .error) || log.unreported.any (·.severity matches .error)
 
-/-- Clears unreported messages while preserving `hasErrors`. -/
+/-- Moves `unreported` messages to `reported`. -/
 def markAllReported (log : MessageLog) : MessageLog :=
-  { log with unreported := {}, hadErrors  := log.hasErrors }
+  { log with unreported := {}, reported := log.reported ++ log.unreported }
 
 def errorsToWarnings (log : MessageLog) : MessageLog :=
   { unreported := log.unreported.map (fun m => match m.severity with | MessageSeverity.error => { m with severity := MessageSeverity.warning } | _ => m) }

src/Lean/Util/SafeExponentiation.lean

@@ -25,7 +25,7 @@ This method ensures there is at most one warning message of this kind in the mes
 def checkExponent (n : Nat) : CoreM Bool := do
   let threshold := exponentiation.threshold.get (← getOptions)
   if n > threshold then
-    if (← reportMessageKind `unsafe.exponentiation) then
+    if (← logMessageKind `unsafe.exponentiation) then
       logWarning s!"exponent {n} exceeds the threshold {threshold}, exponentiation operation was not evaluated, use `set_option {exponentiation.threshold.name} <num>` to set a new threshold"
     return false
   else