feat: message kinds

[tydeu]

This PR adds a new definition Message.kind which returns the top-level tag of a message. This is serialized as the new field kind in SerialMessaege so that i can be used by external consumers (e.g., Lake) to identify messages via lean --json.

The tag of trace messages has also been changed from _traceMsg to the more friendly trace.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5945 has successfully built against this PR. (2024-11-04 18:02:10) View Log
• ✅ Mathlib branch lean-pr-testing-5945 has successfully built against this PR. (2024-11-04 20:24:58) View Log
• ✅ Mathlib branch lean-pr-testing-5945 has successfully built against this PR. (2024-11-06 20:23:12) View Log
• ✅ Mathlib branch lean-pr-testing-5945 has successfully built against this PR. (2024-11-07 20:58:11) View Log
• ✅ Mathlib branch lean-pr-testing-5945 has successfully built against this PR. (2024-11-12 17:20:59) View Log

[tydeu]

This is the first step for a potential solution to #5194. An alternative solution would be to collect all tags within a message and serialize them. However, as the goal here is to be able to identify messages by name to customize reporting, it is not clear how this would work in a multiple tag case. Hence, the approach here is restricted to a single "message kind". A tags field can be added in the future should a more appropriate use case emerge.

[Kha]

If it's always inferred, why is it a field?

[tydeu]

@Kha It is a field so that it will be part of SerialMessage (where it is not inferred since data is a String), and also thus a part of the JSON output. This solution seemed less disruptive than the alternative of different structures for Message and SerialMessage.

[Kha]

Oh you mean it is there for deriving ToJson. I don't love that it can't be defaulted. What would be disruptive about putting it in SerialMessage, can't we make it a structure extending BaseMessage String?

[tydeu]

@Kha

What would be disruptive about putting it in SerialMessage, can't we make it a structure extending BaseMessage String?

Good idea! For some reason it did not occur to me that SerialMessage could be written that way. (I was too stuck on them both needing to be BaseMessage α for some α.)

Separately, the odd JSON encoding of a anonymous kind has led me to propose #5980.

[Kha]

LGTM!