diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean index 990cf08deb..4b3c2fabf6 100644 --- a/src/lake/Lake/Build/Context.lean +++ b/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 -/ diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean index 98211978e6..98cf524a79 100644 --- a/src/lake/Lake/Build/Run.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 3223f04f61..bda58d8a47 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index a8758301e4..335345d1bf 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/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` diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index f7f28ebe0f..7f9ba499c6 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/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?' diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean index dc03f89d76..586807540f 100644 --- a/src/lake/Lake/Util/MainM.lean +++ b/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⟩