From c734e8eda2e69880105b78fd4556c59bd367694d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 4 Dec 2024 15:49:48 +0100 Subject: [PATCH] chore: preserve reported messages in `MessageLog` --- src/Lean/CoreM.lean | 10 +++---- src/Lean/Message.lean | 42 +++++++++++++-------------- src/Lean/Util/SafeExponentiation.lean | 2 +- 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index ff774004492f..f6d34ca8042a 100644 --- a/src/Lean/CoreM.lean +++ b/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 diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 65fe62c274c3..0ee5785dc5d6 100644 --- a/src/Lean/Message.lean +++ b/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) } diff --git a/src/Lean/Util/SafeExponentiation.lean b/src/Lean/Util/SafeExponentiation.lean index 4a402e6e4fa9..7c6aa5cdd999 100644 --- a/src/Lean/Util/SafeExponentiation.lean +++ b/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} ` to set a new threshold" return false else