When debugging Lean core tests that use #guard_msgs it would be great if setting trace options would not affect #guard_msgs itself. By default, it should pass trace messages, but optionally capture them, e.g. #guard_msgs (trace) in ….

We don’t want a new message data severity for that (which would not map nicely to LSP severities), but instead use MessageData tags to annotate trace messages, and recognize them in #guard_msgs.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.