upgrade trace class to warning or error

Stream: lean4

[Matthew Ballard]

Is there a mechanism by which one can globally turn on a trace class in a library and have its output upgraded to a warning or error?

[Kyle Miller]

It looks like docs#Lean.addTrace (the implementation of trace[...] ...) uses docs#Lean.MonadTrace but docs#Lean.log uses docs#Lean.MonadLog, so at this low level the answer is "no" (but that doesn't mean particular instances of these monads can't have what you're asking for).

Here's where the command elaborator monad turns the collected trace messages into log messages, and on the penultimate line it sets the severity to .information.