fix: lake: log config messages like build ones (#7667)

This PR changes Lake to log messages from a Lean configuration the same
way it logs message from a Lean build. This, for instance, removes
redundant severity captions.

For example, Lake would previously log a configuration warning as
`warning: <source>: warning: <message>`. It now logs it as `warning:
<source>: <message>`.

src/lake/Lake/Build/Actions.lean

@@ -56,8 +56,7 @@ def compileLeanModule
       if let .ok (msg : SerialMessage) := Json.parse ln >>= fromJson? then
         unless txt.isEmpty do
           logInfo s!"stdout:\n{txt}"
-        unless msg.isSilent do
-          logSerialMessage msg
+        logSerialMessage msg
         return txt
       else if txt.isEmpty && ln.isEmpty then
         return txt

src/lake/Lake/Load/Lean/Elab.lean

@@ -68,13 +68,7 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
   let s ← Elab.IO.processCommands inputCtx parserState commandState
 
   -- Log messages
-  for msg in s.commandState.messages.toList do
-    if msg.isSilent then
-      continue
-    match msg.severity with
-    | MessageSeverity.information => logInfo (← msg.toString)
-    | MessageSeverity.warning     => logWarning (← msg.toString)
-    | MessageSeverity.error       => logError (← msg.toString)
+  s.commandState.messages.forM (logMessage ·)
 
   -- Check result
   if s.commandState.messages.hasErrors then

src/lake/Lake/Util/Log.lean

@@ -149,6 +149,18 @@ instance : ToString LogEntry := ⟨LogEntry.toString⟩
 @[inline] def LogEntry.error (message : String) : LogEntry :=
   {level := .error, message}
 
+def LogEntry.ofSerialMessage (msg : SerialMessage) : LogEntry :=
+  let str := if msg.caption.trim.isEmpty then
+     msg.data.trim else s!"{msg.caption.trim}:\n{msg.data.trim}"
+  {
+    level := .ofMessageSeverity msg.severity
+    message := mkErrorStringWithPos msg.fileName msg.pos str none
+  }
+
+def LogEntry.ofMessage (msg : Message) : BaseIO LogEntry := do
+  -- Remark: The inline here avoids a new message allocation when `msg` is shared
+  return inline <| .ofSerialMessage (← msg.serialize)
+
 class MonadLog (m : Type u → Type v) where
   logEntry (e : LogEntry) : m PUnit
 
@@ -166,13 +178,13 @@ export MonadLog (logEntry)
 @[inline] def logError [MonadLog m] (message : String) : m PUnit :=
   logEntry (.error message)
 
-@[specialize] def logSerialMessage (msg : SerialMessage) [MonadLog m] : m PUnit :=
-  let str := if msg.caption.trim.isEmpty then
-     msg.data.trim else s!"{msg.caption.trim}:\n{msg.data.trim}"
-  logEntry {
-    level := .ofMessageSeverity msg.severity
-    message := mkErrorStringWithPos msg.fileName msg.pos str none
-  }
+@[inline] def logSerialMessage (msg : SerialMessage) [Monad m] [MonadLog m] : m PUnit := do
+  unless msg.isSilent do
+    logEntry (.ofSerialMessage msg)
+
+@[inline] def logMessage (msg : Message) [Monad m] [MonadLog m] [MonadLiftT BaseIO m] : m PUnit := do
+  unless msg.isSilent do
+    logEntry (← LogEntry.ofMessage msg)
 
 def logToStream
   (e : LogEntry) (out : IO.FS.Stream) (minLv : LogLevel) (useAnsi : Bool)

src/lake/tests/logLevel/test.sh

@@ -46,9 +46,9 @@ log_empty Trace
 
 # Test configuration-time output log level
 
-$LAKE resolve-deps -R -Klog=info 2>&1 | grep --color "info: bar"
+$LAKE resolve-deps -R -Klog=info 2>&1 | grep --color "info:"
 $LAKE resolve-deps -R -Klog=info -q 2>&1 |
-  grep --color "info: bar"  && exit 1 || true
-$LAKE resolve-deps -R -Klog=warning 2>&1 | grep --color "warning: bar"
+  grep --color "info:"  && exit 1 || true
+$LAKE resolve-deps -R -Klog=warning 2>&1 | grep --color "warning:"
 $LAKE resolve-deps -R -Klog=warning --log-level=error 2>&1 |
-  grep --color "warning: bar" && exit 1 || true
+  grep --color "warning:" && exit 1 || true

src/lake/tests/meta/lakefile.lean

@@ -10,10 +10,10 @@ meta if get_config? baz |>.isSome then #print "baz"
 
 meta if get_config? env = some "foo" then do
   #print "foo"
-  #print "1"
+  #print "lorem"
 else meta if get_config? env = some "bar" then do
   #print "bar"
-  #print "2"
+  #print "ipsum"
 
 script print_env do
   IO.eprintln <| get_config? env |>.getD "none"

src/lake/tests/meta/test.sh

@@ -14,7 +14,7 @@ $LAKE resolve-deps -R 2>&1 | grep --color impure
 $LAKE resolve-deps 2>&1 | (grep --color impure && exit 1 || true)
 
 # Test `meta if` and command `do`
-$LAKE resolve-deps -R 2>&1 | (grep --color -E "foo|bar|baz|1|2" && exit 1 || true)
+$LAKE resolve-deps -R 2>&1 | (grep --color -E "foo|bar|baz|lorem|ipsum" && exit 1 || true)
 $LAKE resolve-deps -R -Kbaz 2>&1 | grep --color baz
 $LAKE resolve-deps -R -Kenv=foo 2>&1 | grep --color foo
 $LAKE run print_env 2>&1 | grep --color foo