refactor: lake: introduce LogConfig (#10468)

This PR refactors the Lake log monads to take a `LogConfig` structure
when run (rather than multiple arguments). This breaking change should
help minimize future breakages due to changes in configurations options.

In addition, the CLI logging monad stack has been polished up and
`LogIO` now supports the `failLv` configuration option.

src/lake/Lake/Build/Context.lean

@@ -14,7 +14,7 @@ open System
 namespace Lake
 
 /-- Configuration options for a Lake build. -/
-public structure BuildConfig where
+public structure BuildConfig extends LogConfig where
   /-- Use modification times for trace checking. -/
   oldMode : Bool := false
   /-- Whether to trust `.hash` files. -/
@@ -23,23 +23,6 @@ public structure BuildConfig where
   noBuild : Bool := false
   /-- Verbosity level (`-q`, `-v`, or neither). -/
   verbosity : Verbosity := .normal
-  /--
-  Fail the top-level build if entries of at least this level have been logged.
-
-  Unlike some build systems, this does **NOT** convert such log entries to
-  errors, and it does not abort jobs when warnings are logged (i.e.,
-  dependent jobs will still continue unimpeded).
-  -/
-  failLv : LogLevel := .error
-  /-- The minimum log level for an log entry to be reported. -/
-  outLv : LogLevel := verbosity.minLogLv
-  /--
-  The stream to which Lake reports build progress.
-  By default, Lake uses `stderr`.
-  -/
-  out : OutStream := .stderr
-  /-- Whether to use ANSI escape codes in build output. -/
-  ansiMode : AnsiMode := .auto
   /-- Whether to print a message when the build finishes successfully (if not quiet). -/
   showSuccess : Bool := false
   /-- File to save input-to-output mappings from the build of the worksoace's root -/

src/lake/Lake/Build/Run.lean

@@ -275,7 +275,8 @@ public def Workspace.runFetchM
   let isNoBuild := cfg.noBuild
   if failures.isEmpty then
     let some a ← job.wait?
-      | error "uncaught top-level build failure (this is likely a bug in Lake)"
+      | print! out "Uncaught top-level build failure (this is likely a bug in Lake).\n"
+        error "build failed"
     if showProgress && showSuccess then
       let jobs := if numJobs == 1 then "1 job" else s!"{numJobs} jobs"
       if isNoBuild then

src/lake/Lake/CLI/Main.lean

@@ -73,6 +73,12 @@ public structure LakeOptions where
 def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
   opts.outLv?.getD opts.verbosity.minLogLv
 
+@[inline] def LakeOptions.toLogConfig (opts : LakeOptions) : LogConfig where
+  failLv := opts.failLv
+  outLv := opts.outLv
+  ansiMode := opts.ansiMode
+  out := .stderr
+
 /-- Get the Lean installation. Error if missing. -/
 def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
   match opts.leanInstall? with
@@ -139,15 +145,13 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
   let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
   main.run
 
-@[inline] def CliStateM.runLogIO (x : LogIO α) : CliStateM α := do
-  let opts ← get
-  MainM.runLogIO x opts.outLv opts.ansiMode
+def CliStateM.runLogIO (x : LogIO α) : CliStateM α := do
+  MainM.runLogIO x (← get).toLogConfig
 
 instance (priority := low) : MonadLift LogIO CliStateM := ⟨CliStateM.runLogIO⟩
 
-@[inline] def CliStateM.runLoggerIO (x : LoggerIO α) : CliStateM α := do
-  let opts ← get
-  MainM.runLoggerIO x opts.outLv opts.ansiMode
+def CliStateM.runLoggerIO (x : LoggerIO α) : CliStateM α := do
+  MainM.runLoggerIO x (← get).toLogConfig
 
 instance (priority := low) : MonadLift LoggerIO CliStateM := ⟨CliStateM.runLoggerIO⟩
 
@@ -651,7 +655,7 @@ protected def setupFile : CliM PUnit := do
     match Json.parse header >>= fromJson? with
     | .ok header => pure header
     | .error e => error s!"failed to parse header JSON: {e}"
-  setupFile loadConfig filePath header buildConfig
+  exit <| ← setupFile loadConfig filePath header buildConfig
 
 protected def test : CliM PUnit := do
   processOptions lakeOption

src/lake/Lake/CLI/Serve.lean

@@ -8,13 +8,12 @@ module
 prelude
 public import Lake.Load.Config
 public import Lake.Build.Context
-public import Lake.Util.MainM
+public import Lake.Util.Exit
 import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Load.Package
 import Lake.Load.Lean.Elab
 import Lake.Load.Workspace
-import Lake.Util.MainM
 import Lake.Util.IO
 
 open Lean
@@ -44,27 +43,45 @@ The `setup-file` command is used internally by the Lean server.
 public def setupFile
   (loadConfig : LoadConfig) (leanFile : FilePath)
   (header? : Option ModuleHeader := none) (buildConfig : BuildConfig := {})
-: MainM PUnit := do
+: BaseIO ExitCode := do
   let path ← resolvePath leanFile
   let configFile ← realConfigFile loadConfig.configFile
   if configFile.toString.isEmpty then
-    exit noConfigFileCode
+    return noConfigFileCode
   else if configFile == path then do
     let setup : ModuleSetup := {
       name := configModuleName
       plugins :=  #[loadConfig.lakeEnv.lake.sharedLib]
     }
-    IO.println (toJson setup).compress
+    print! (toJson setup).compress
   else if let some errLog := (← IO.getEnv invalidConfigEnvVar) then
-    IO.eprint errLog
-    IO.eprintln s!"Failed to configure the Lake workspace. Please restart the server after fixing the error above."
-    exit 1
+    eprint! errLog
+    eprint! "Failed to configure the Lake workspace. \
+      Please restart the server after fixing the error above.\n"
+    return 1
   else
-    let some ws ← loadWorkspace loadConfig |>.toBaseIO buildConfig.outLv buildConfig.ansiMode
-      | error "failed to load workspace"
-    let setup ← ws.runBuild (cfg := buildConfig) do
+    let some ws ← loadWorkspace loadConfig |>.toBaseIO buildConfig.toLogConfig
+      | eprint! "Failed to load the Lake workspace.\n"
+        return 1
+    let setup := ws.runBuild (cfg := buildConfig) do
       setupServerModule leanFile.toString path header?
-    IO.println (toJson setup).compress
+    match (← setup.toBaseIO) with
+    | .ok setup =>
+      print! (toJson setup).compress
+    | .error _ =>
+      eprint! "Failed to build module dependencies.\n"
+      return 1
+where
+  print! msg := do
+    match (← IO.println msg |>.toBaseIO) with
+    | .ok _ =>
+      return 0
+    | .error e =>
+      panic! s!"Failed to print `setup-file` result: {e}"
+      return 1
+  eprint! msg := do
+    IO.eprint msg |>.catchExceptions fun e =>
+      panic! s!"Failed to print `setup-file` error: {e}\nOriginal error:\n{msg}"
 
 /--
 Start the Lean LSP for the `Workspace` loaded from `config`

src/lake/Lake/Util/Log.lean

@@ -586,28 +586,49 @@ a `failure` in the new monad.
 
 end ELogT
 
+/-- Configuration options for Lake logging. -/
+public structure LogConfig where
+  /--
+  Fail if entries of at least this level have been logged.
+
+  Unlike some build systems, this does **NOT** convert such log entries to
+  errors, and it does not necessarily abort execution when warnings are logged.
+
+  **NOTE:** Some logging monads do not support this option (e.g., `LoggerIO`).
+  -/
+  failLv : LogLevel := .error
+  /-- The minimum log level for an log entry to be reported. -/
+  outLv : LogLevel := .info
+  /-- Whether to use ANSI escape codes in log output. -/
+  ansiMode : AnsiMode := .auto
+  /-- Where to write logs. -/
+  out : OutStream := .stderr
+
+@[inline] public def LogConfig.getLogger [MonadLiftT BaseIO m] (self : LogConfig) : BaseIO (MonadLog m) := do
+  self.out.getLogger self.outLv self.ansiMode
+
 /-- A monad equipped with a log, a log error position, and the ability to perform I/O. -/
 public abbrev LogIO := ELogT BaseIO
 
-public instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
-
 namespace LogIO
 
+public instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩
+
 /--
-Runs a `LogIO` action in `BaseIO`.
-Prints log entries of at least `minLv` to `out`.
+Runs a `LogIO` action in `BaseIO` using the specified log configuration.
+
+Returns `none` if the action fails or if an entry of at least `LogConfig.failLv` has been logged.
+On failure, all logs will be printed, ignoring the  `LogConfig.outLv` setting.
 -/
-@[inline] public def toBaseIO (self : LogIO α)
-  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
+@[inline] public def toBaseIO
+  (self : LogIO α) (cfg : LogConfig := {})
 : BaseIO (Option α) := do
-  let logger ← out.getLogger minLv ansiMode
   let (a?, log) ← self.run? {}
-  replay log logger
-  return a?
-where
-  -- avoid specialization of this call at each call site
-  replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit :=
-    log.replay (logger := logger)
+  let failed := a?.isNone ∨ cfg.failLv ≤ log.maxLv
+  let outLv := if failed then .trace else cfg.outLv
+  let logger ← cfg.out.getLogger outLv cfg.ansiMode
+  log.replay (logger := logger)
+  return if failed  then none else a?
 
 -- deprecated 2024-05-18, reversed 2024-10-18
 public abbrev captureLog := @ELogT.run?
@@ -619,31 +640,31 @@ A monad equipped with a log function and the ability to perform I/O.
 Unlike `LogIO`, log entries are not retained by the monad but instead eagerly
 passed to the log function.
 -/
-public abbrev LoggerIO := MonadLogT BaseIO (EIO PUnit)
+public abbrev LoggerIO := MonadLogT BaseIO (EIO Unit)
+
+namespace LoggerIO
 
 public instance : MonadError LoggerIO := ⟨MonadLog.error⟩
 public instance : MonadLift IO LoggerIO := ⟨MonadError.runIO⟩
 public instance : MonadLift LogIO LoggerIO := ⟨ELogT.replayLog⟩
 
-namespace LoggerIO
-
 /--
-Runs a `LoggerIO` action in `BaseIO`.
-Prints log entries of at least `minLv` to `out`.
+Runs a `LoggerIO` action in `BaseIO` using the specified log configuration.
+
+Does not support `LogConfig.failLv`.
 -/
 @[inline] public def toBaseIO
-  (self : LoggerIO α)
-  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
-: BaseIO (Option α) := do
-  (·.toOption) <$> (self.run (← out.getLogger minLv ansiMode)).toBaseIO
+  (self : LoggerIO α) (cfg : LogConfig := {})
+: BaseIO (Option α) := do (·.toOption) <$> (self.run (← cfg.getLogger)).toBaseIO
 
+/-- Runs a `LoggerIO` action in `BaseIO` and returns the produced log. -/
 public def captureLog (self : LoggerIO α) : BaseIO (Option α × Log) := do
   let ref ← IO.mkRef ({} : Log)
   let e ← self.run ⟨fun e => ref.modify (·.push e)⟩ |>.toBaseIO
   return (e.toOption, ← ref.get)
 
 -- For parity with `LogIO.run?`
-public abbrev run? := @captureLog
+@[inherit_doc captureLog] public abbrev run? := @captureLog
 
 -- For parity with `LogIO.run?'`
 @[inline] public def run?'

src/lake/Lake/Util/MainM.lean

@@ -78,24 +78,18 @@ public instance : MonadLog MainM := .stderr
 public instance : MonadError MainM := ⟨MainM.error⟩
 public instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
 
-@[inline] public def runLogIO (x : LogIO α)
-  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
-: MainM α := do
-  match (← x.run {}) with
-  | .ok a  log => replay log (← out.getLogger minLv ansiMode); return a
-  | .error _ log => replay log (← out.getLogger .trace ansiMode); exit 1
-where
-  -- avoid specialization of this call at each call site
-  replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit :=
-    log.replay (logger := logger)
+@[inline] public def runLogIO
+  (x : LogIO α) (cfg : LogConfig := {})
+: MainM α := do (← x.toBaseIO cfg).getDM do exit 1
 
-public instance (priority := low) : MonadLift LogIO MainM := ⟨runLogIO⟩
+public def liftLogIO (x : LogIO α) : MainM α := runLogIO x
 
-@[inline] public def runLoggerIO (x : LoggerIO α)
-  (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr)
-: MainM α := do
-  let some a ← x.run (← out.getLogger minLv ansiMode) |>.toBaseIO
-    | exit 1
-  return a
+public instance (priority := low) : MonadLift LogIO MainM := ⟨liftLogIO⟩
 
-public instance (priority := low) : MonadLift LoggerIO MainM := ⟨runLoggerIO⟩
+@[inline] public def runLoggerIO
+  (x : LoggerIO α) (cfg : LogConfig := {})
+: MainM α := do (← x.toBaseIO cfg).getDM do exit 1
+
+public def liftLoggerIO (x : LoggerIO α) : MainM α := runLoggerIO x
+
+public instance (priority := low) : MonadLift LoggerIO MainM := ⟨liftLoggerIO⟩