From edfd059d8915aa838c46a40007403b4f47833082 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 4 Nov 2024 11:35:55 -0500
Subject: [PATCH 1/5] feat: message kinds

---
 src/Lean/Log.lean     |  6 +++++-
 src/Lean/Message.lean | 20 ++++++++++++++++++--
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index 6485e15a1ffc..fbfa3d2c955e 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -66,7 +66,11 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
+    logMessage {
+      fileName := (← getFileName)
+      pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos
+      kind := msgData.inferKind, data := msgData, severity := severity
+    }
 
 /-- Log a new error message using the given message data. The position is provided by `ref`. -/
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 7753311bc60e..bd6eafa1e91d 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtress (`.ofLazy`); message tags
+This does not descend into lazily generated subtrees (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,6 +130,20 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
+/--
+Returns the top-level tag or trace class of the message.
+If none, returns `Name.anonymous`.
+
+This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
+The message kind is expected to describe the whole message.
+-/
+def inferKind : MessageData → Name
+  | withContext _ msg       => inferKind msg
+  | withNamingContext _ msg => inferKind msg
+  | tagged n _              => n
+  | trace data _ _          => data.cls
+  | _                       => .anonymous
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -307,8 +321,10 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := MessageSeverity.error
+  severity      : MessageSeverity := .error
   caption       : String          := ""
+  /-- The message kind (e.g., top-level tag or trace class). -/
+  kind          : Name := .anonymous
   /-- The content of the message. -/
   data          : α
   deriving Inhabited, ToJson, FromJson

From 9a8b08b7db5eb59f73bed74e419810cd0d0dccdf Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 4 Nov 2024 14:29:07 -0500
Subject: [PATCH 2/5] fix: trace message kind

---
 src/Lean/Elab/Command.lean   | 2 +-
 src/Lean/Elab/Exception.lean | 2 +-
 src/Lean/Message.lean        | 5 ++---
 3 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 296a2bede02f..d10fb3da6a62 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
     log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 
diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 0a27f965e284..8c50485eafcd 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -63,6 +63,6 @@ def isAbortExceptionId (id : InternalExceptionId) : Bool :=
 def mkMessageCore (fileName : String) (fileMap : FileMap) (data : MessageData) (severity : MessageSeverity) (pos : String.Pos) (endPos : String.Pos) : Message :=
   let pos := fileMap.toPosition pos
   let endPos := fileMap.toPosition endPos
-  { fileName, pos, endPos, data, severity }
+  { fileName, pos, endPos, kind := data.inferKind, data, severity }
 
 end Lean.Elab
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index bd6eafa1e91d..428e03ff8fa9 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -131,7 +131,7 @@ partial def hasTag : MessageData → Bool
   | _                       => false
 
 /--
-Returns the top-level tag or trace class of the message.
+Returns the top-level tag of the message.
 If none, returns `Name.anonymous`.
 
 This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
@@ -141,7 +141,6 @@ def inferKind : MessageData → Name
   | withContext _ msg       => inferKind msg
   | withNamingContext _ msg => inferKind msg
   | tagged n _              => n
-  | trace data _ _          => data.cls
   | _                       => .anonymous
 
 /-- An empty message. -/
@@ -323,7 +322,7 @@ structure BaseMessage (α : Type u) where
   keepFullRange : Bool := false
   severity      : MessageSeverity := .error
   caption       : String          := ""
-  /-- The message kind (e.g., top-level tag or trace class). -/
+  /-- The message kind (e.g., the top-level tag). -/
   kind          : Name := .anonymous
   /-- The content of the message. -/
   data          : α

From 15b011b56455ed19654f7a7efee0f28a2f535856 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 4 Nov 2024 14:29:46 -0500
Subject: [PATCH 3/5] chore: kinds in Lake messages

---
 src/lake/Lake/Util/Message.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/lake/Lake/Util/Message.lean b/src/lake/Lake/Util/Message.lean
index 0d7847fa6c98..5dbea4167aee 100644
--- a/src/lake/Lake/Util/Message.lean
+++ b/src/lake/Lake/Util/Message.lean
@@ -22,6 +22,7 @@ def mkExceptionMessage (ictx : InputContext) (e : Exception) : Message where
   fileName := ictx.fileName
   pos := ictx.fileMap.toPosition <| e.getRef.getPos?.getD 0
   endPos := ictx.fileMap.toPosition <$> e.getRef.getTailPos?
+  kind := e.toMessageData.inferKind
   data := e.toMessageData
 
 def mkMessageNoPos (ictx : InputContext) (data : MessageData) (severity := MessageSeverity.error) : Message where
@@ -29,6 +30,7 @@ def mkMessageNoPos (ictx : InputContext) (data : MessageData) (severity := Messa
   pos := ictx.fileMap.toPosition 0
   endPos := none
   severity := severity
+  kind := data.inferKind
   data := data
 
 def mkMessageStringCore

From e60e19f8b8b159810e567ce73e5cffafdec246ea Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Mon, 4 Nov 2024 14:29:53 -0500
Subject: [PATCH 4/5] chore: add test

---
 tests/lean/run/messageKind.lean | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 tests/lean/run/messageKind.lean

diff --git a/tests/lean/run/messageKind.lean b/tests/lean/run/messageKind.lean
new file mode 100644
index 000000000000..fb8714e312db
--- /dev/null
+++ b/tests/lean/run/messageKind.lean
@@ -0,0 +1,26 @@
+import Lean.Elab.Command
+
+open Lean Elab Command
+
+elab tk:"#guard_msg_kind " kind:ident " in " cmd:command : command => do
+  let initMsgs ← modifyGet fun st => (st.messages, {st with messages := {}})
+  elabCommandTopLevel cmd
+  let msgs ← modifyGet fun st => (st.messages, {st with messages := initMsgs})
+  let kind := kind.getId
+  for msg in msgs.toList do
+    if msg.kind != kind then
+      logErrorAt tk s!"expected {kind}, got {msg.kind}"
+
+/- Test inferring kind from a tag. -/
+#guard_msg_kind custom in
+run_cmd do logInfo <| .tagged `custom ""
+
+/- Test trace message kind. -/
+#guard_msg_kind trace in
+set_option trace.Elab.step true in
+def trace := ()
+
+/- Test linter kind. -/
+#guard_msg_kind linter.unusedVariables in
+#guard_msgs (info) in -- hack to avoid re-triggering the linter
+def unused (x : Unit) := ()

From b47358086e757f5aa6ab78825a6254821176e514 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 6 Nov 2024 14:04:16 -0500
Subject: [PATCH 5/5] refactor: `SerialMessage` extend `BaseMessage`

---
 src/Lean/Elab/Exception.lean    |  2 +-
 src/Lean/Log.lean               |  6 +-----
 src/Lean/Message.lean           | 19 ++++++++++++-------
 src/lake/Lake/Util/Message.lean |  2 --
 4 files changed, 14 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean
index 8c50485eafcd..0a27f965e284 100644
--- a/src/Lean/Elab/Exception.lean
+++ b/src/Lean/Elab/Exception.lean
@@ -63,6 +63,6 @@ def isAbortExceptionId (id : InternalExceptionId) : Bool :=
 def mkMessageCore (fileName : String) (fileMap : FileMap) (data : MessageData) (severity : MessageSeverity) (pos : String.Pos) (endPos : String.Pos) : Message :=
   let pos := fileMap.toPosition pos
   let endPos := fileMap.toPosition endPos
-  { fileName, pos, endPos, kind := data.inferKind, data, severity }
+  { fileName, pos, endPos, data, severity }
 
 end Lean.Elab
diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean
index fbfa3d2c955e..6485e15a1ffc 100644
--- a/src/Lean/Log.lean
+++ b/src/Lean/Log.lean
@@ -66,11 +66,7 @@ def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity :=
     let endPos := ref.getTailPos?.getD pos
     let fileMap ← getFileMap
     let msgData ← addMessageContext msgData
-    logMessage {
-      fileName := (← getFileName)
-      pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos
-      kind := msgData.inferKind, data := msgData, severity := severity
-    }
+    logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos, data := msgData, severity := severity }
 
 /-- Log a new error message using the given message data. The position is provided by `ref`. -/
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 428e03ff8fa9..135b68cfca50 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -137,9 +137,9 @@ If none, returns `Name.anonymous`.
 This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
 The message kind is expected to describe the whole message.
 -/
-def inferKind : MessageData → Name
-  | withContext _ msg       => inferKind msg
-  | withNamingContext _ msg => inferKind msg
+def kind : MessageData → Name
+  | withContext _ msg       => kind msg
+  | withNamingContext _ msg => kind msg
   | tagged n _              => n
   | _                       => .anonymous
 
@@ -322,8 +322,7 @@ structure BaseMessage (α : Type u) where
   keepFullRange : Bool := false
   severity      : MessageSeverity := .error
   caption       : String          := ""
-  /-- The message kind (e.g., the top-level tag). -/
-  kind          : Name := .anonymous
+
   /-- The content of the message. -/
   data          : α
   deriving Inhabited, ToJson, FromJson
@@ -335,7 +334,10 @@ abbrev Message := BaseMessage MessageData
 /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
 serialized and is thus appropriate for use in pure contexts where the effectful
 `MessageData.toString` cannot be used. -/
-abbrev SerialMessage := BaseMessage String
+structure SerialMessage extends BaseMessage String where
+  /-- The message kind (i.e., the top-level tag). -/
+  kind          : Name := .anonymous
+  deriving ToJson, FromJson
 
 namespace SerialMessage
 
@@ -361,8 +363,11 @@ end SerialMessage
 
 namespace Message
 
+abbrev kind (msg : Message) :=
+  msg.data.kind
+
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
-  return {msg with data := ← msg.data.toString}
+  return {msg with kind := msg.kind, data := ← msg.data.toString}
 
 protected def toString (msg : Message) (includeEndPos := false) : IO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared
diff --git a/src/lake/Lake/Util/Message.lean b/src/lake/Lake/Util/Message.lean
index 5dbea4167aee..0d7847fa6c98 100644
--- a/src/lake/Lake/Util/Message.lean
+++ b/src/lake/Lake/Util/Message.lean
@@ -22,7 +22,6 @@ def mkExceptionMessage (ictx : InputContext) (e : Exception) : Message where
   fileName := ictx.fileName
   pos := ictx.fileMap.toPosition <| e.getRef.getPos?.getD 0
   endPos := ictx.fileMap.toPosition <$> e.getRef.getTailPos?
-  kind := e.toMessageData.inferKind
   data := e.toMessageData
 
 def mkMessageNoPos (ictx : InputContext) (data : MessageData) (severity := MessageSeverity.error) : Message where
@@ -30,7 +29,6 @@ def mkMessageNoPos (ictx : InputContext) (data : MessageData) (severity := Messa
   pos := ictx.fileMap.toPosition 0
   endPos := none
   severity := severity
-  kind := data.inferKind
   data := data
 
 def mkMessageStringCore