feat: lake: CLI options to control output & failure log levels

src/lake/Lake/Build/Basic.lean

@@ -30,6 +30,8 @@ structure BuildConfig where
   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`.
@@ -38,10 +40,6 @@ structure BuildConfig where
   /-- Whether to use ANSI escape codes in build output. -/
   ansiMode : AnsiMode := .auto
 
-/-- The minimum log level for an log entry to be reported. -/
-@[inline] def BuildConfig.outLv (cfg : BuildConfig) : LogLevel :=
-  cfg.verbosity.minLogLv
-
 /--
 Whether the build should show progress information.
 

src/lake/Lake/CLI/Error.lean

@@ -13,6 +13,7 @@ inductive CliError
 | unknownCommand (cmd : String)
 | missingArg (arg : String)
 | missingOptArg (opt arg : String)
+| invalidOptArg (opt arg : String)
 | unknownShortOption (opt : Char)
 | unknownLongOption (opt : String)
 | unexpectedArguments (args : List String)
@@ -51,7 +52,8 @@ def toString : CliError → String
 | missingCommand          => "missing command"
 | unknownCommand cmd      => s!"unknown command '{cmd}'"
 | missingArg arg          => s!"missing {arg}"
-| missingOptArg opt arg   => s!"missing {arg} after {opt}"
+| missingOptArg opt arg   => s!"missing {arg} for {opt}"
+| invalidOptArg opt arg   => s!"invalid argument for {opt}; expected {arg}"
 | unknownShortOption opt  => s!"unknown short option '-{opt}'"
 | unknownLongOption opt   => s!"unknown long option '{opt}'"
 | unexpectedArguments as  => s!"unexpected arguments: {" ".intercalate as}"

src/lake/Lake/CLI/Help.lean

@@ -35,24 +35,32 @@ COMMANDS:
   translate-config      change language of the package configuration
   serve                 start the Lean language server
 
-OPTIONS:
+BASIC OPTIONS:
   --version             print version and exit
   --help, -h            print help of the program or a command and exit
   --dir, -d=file        use the package configuration in a specific directory
   --file, -f=file       use a specific file for the package configuration
-  --quiet, -q           hide progress messages
-  --verbose, -v         show verbose information (command invocations)
   --lean=cmd            specify the `lean` command used by Lake
   -K key[=value]        set the configuration file option named key
   --old                 only rebuild modified modules (ignore transitive deps)
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update, -U          update manifest before building
   --reconfigure, -R     elaborate configuration files instead of using OLeans
-  --wfail               fail build if warnings are logged
-  --iofail              fail build if any I/O or other info is logged
-  --ansi, --no-ansi     toggle the use of ANSI escape codes to prettify output
   --no-build            exit immediately if a build target is not up-to-date
 
+OUTPUT OPTIONS:
+  --quiet, -q           hide informational logs and the progress indicator
+  --verbose, -v         show trace logs (command invocations) and built targets
+  --ansi, --no-ansi     toggle the use of ANSI escape codes to prettify output
+  --log-level=lv        minimum log level to output on success
+                        (levels: trace, info, warning, error)
+  --fail-level=lv       minimum log level to fail a build (default: error)
+  --iofail              fail build if any I/O or other info is logged
+                        (same as --fail-level=info)
+  --wfail               fail build if warnings are logged
+                        (same as --fail-level=warning)
+
+
 See `lake help <command>` for more information on a specific command."
 
 def templateHelp :=

src/lake/Lake/CLI/Main.lean

@@ -41,8 +41,12 @@ structure LakeOptions where
   trustHash : Bool := true
   noBuild : Bool := false
   failLv : LogLevel := .error
+  outLv? : Option LogLevel := .none
   ansiMode : AnsiMode := .auto
 
+def LakeOptions.outLv (opts : LakeOptions) : LogLevel :=
+  opts.outLv?.getD opts.verbosity.minLogLv
+
 /-- Get the Lean installation. Error if missing. -/
 def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
   match opts.leanInstall? with
@@ -82,6 +86,7 @@ def LakeOptions.mkBuildConfig (opts : LakeOptions) (out := OutStream.stderr) : B
   noBuild := opts.noBuild
   verbosity := opts.verbosity
   failLv := opts.failLv
+  outLv := opts.outLv
   ansiMode := opts.ansiMode
   out := out
 
@@ -101,7 +106,7 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
 
 @[inline] def CliStateM.runLogIO (x : LogIO α) : CliStateM α := do
   let opts ← get
-  MainM.runLogIO x opts.verbosity.minLogLv opts.ansiMode
+  MainM.runLogIO x opts.outLv opts.ansiMode
 
 instance (priority := low) : MonadLift LogIO CliStateM := ⟨CliStateM.runLogIO⟩
 
@@ -117,6 +122,10 @@ def takeOptArg (opt arg : String) : CliM String := do
   | none => throw <| CliError.missingOptArg opt arg
   | some arg => pure arg
 
+@[inline] def takeOptArg' (opt arg : String) (f : String → Option α)  : CliM α := do
+  if let some a :=  f (← takeOptArg opt arg) then return a
+  throw <| CliError.invalidOptArg opt arg
+
 /--
 Verify that there are no CLI arguments remaining
 before running the given action.
@@ -167,13 +176,25 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
 | "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
 | "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
+| "--log-level"   => do
+  let outLv ← takeOptArg' "--log-level" "log level" LogLevel.ofString?
+  modifyThe LakeOptions ({· with outLv? := outLv})
+| "--fail-level"  => do
+  let failLv ← takeOptArg' "--fail-level" "log level" LogLevel.ofString?
+  modifyThe LakeOptions ({· with failLv})
 | "--ansi"        => modifyThe LakeOptions ({· with ansiMode := .ansi})
 | "--no-ansi"     => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
-| "--dir"         => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
-| "--file"        => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
+| "--dir"         => do
+  let rootDir ← takeOptArg "--dir" "path"
+  modifyThe LakeOptions ({· with rootDir})
+| "--file"        => do
+  let configFile ← takeOptArg "--file" "path"
+  modifyThe LakeOptions ({· with configFile})
 | "--lean"        => do setLean <| ← takeOptArg "--lean" "path or command"
 | "--help"        => modifyThe LakeOptions ({· with wantsHelp := true})
-| "--"            => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
+| "--"            => do
+  let subArgs ← takeArgs
+  modifyThe LakeOptions ({· with subArgs})
 | opt             =>  throw <| CliError.unknownLongOption opt
 
 def lakeOption :=
@@ -320,6 +341,7 @@ protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
+  noArgsRem do
   discard <| loadWorkspace config opts.updateDeps
 
 protected def update : CliM PUnit := do

src/lake/Lake/Util/Log.lean

@@ -89,18 +89,30 @@ def LogLevel.ansiColor : LogLevel → String
 | .warning => "33"
 | .error => "31"
 
+protected def LogLevel.ofString? : String → Option LogLevel
+| "trace" => some .trace
+| "info" | "information" => some .info
+| "warn" | "warning" => some .warning
+| "error" => some .error
+| _ => none
+
 protected def LogLevel.toString : LogLevel → String
 | .trace => "trace"
 | .info => "info"
 | .warning => "warning"
 | .error => "error"
 
+instance : ToString LogLevel := ⟨LogLevel.toString⟩
+
 protected def LogLevel.ofMessageSeverity : MessageSeverity → LogLevel
 | .information => .info
 | .warning => .warning
 | .error => .error
 
-instance : ToString LogLevel := ⟨LogLevel.toString⟩
+protected def LogLevel.toMessageSeverity : LogLevel → MessageSeverity
+| .info | .trace => .information
+| .warning => .warning
+| .error => .error
 
 def Verbosity.minLogLv : Verbosity → LogLevel
 | .quiet => .warning

src/lake/tests/logLevel/Log/Error.lean

@@ -0,0 +1,2 @@
+import Lean.Elab.Command
+run_cmd Lean.logError "foo"

src/lake/tests/logLevel/Log/Info.lean

@@ -0,0 +1,2 @@
+import Lean.Elab.Command
+run_cmd Lean.logInfo "foo"

src/lake/tests/logLevel/Log/Warning.lean

@@ -0,0 +1,2 @@
+import Lean.Elab.Command
+run_cmd Lean.logWarning "foo"

src/lake/tests/logLevel/lakefile.lean

@@ -0,0 +1,49 @@
+import Lake
+open Lake DSL
+
+package test
+
+/-
+Test logging in Lake CLI
+-/
+
+def cfgLogLv? := (get_config? log).bind LogLevel.ofString?
+
+meta if cfgLogLv?.isSome then
+  run_cmd Lean.log "bar" cfgLogLv?.get!.toMessageSeverity
+
+
+/-
+Test logging in Lean
+-/
+
+lean_lib Log
+
+/-
+Test logging in job
+-/
+
+def top (level : LogLevel) : FetchM (BuildJob Unit) := Job.async do
+  logEntry {level, message := "foo"}
+  return ((), .nil)
+
+target topTrace : Unit := top .trace
+target topInfo : Unit := top .info
+target topWarning : Unit := top .warning
+target topError : Unit := top .error
+
+/--
+Test logging in build helper
+-/
+
+def art (pkg : Package) (level : LogLevel) : FetchM (BuildJob Unit) := Job.async do
+  let artFile := pkg.buildDir / s!"art_{level}"
+  (((), ·)) <$> buildFileUnlessUpToDate artFile .nil do
+    logEntry {level, message := "foo"}
+    createParentDirs artFile
+    IO.FS.writeFile artFile ""
+
+target artTrace pkg : Unit := art pkg .trace
+target artInfo pkg : Unit := art pkg .info
+target artWarning pkg : Unit := art pkg .warning
+target artError pkg : Unit := art pkg .error

src/lake/tests/logLevel/test.sh

@@ -0,0 +1,54 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# Test failure log level
+
+log_fail_target() {
+  ($LAKE build "$@" && exit 1 || true) | grep --color foo
+  ($LAKE build "$@" && exit 1 || true) | grep --color foo # test replay
+}
+
+log_fail_target topTrace --fail-level=trace
+log_fail_target artTrace --fail-level=trace
+
+log_fail() {
+  lv=$1; shift
+  log_fail_target top${lv^} "$@"
+  log_fail_target art${lv^} "$@"
+  log_fail_target Log.${lv^} "$@"
+}
+
+log_fail info --iofail
+log_fail warning --wfail
+log_fail error
+
+# Test output log level
+
+log_empty() {
+  lv=$1; shift
+  rm -f .lake/build/art_$lv
+  $LAKE build art${lv^} "$@" | grep --color foo && exit 1 || true
+  $LAKE build art${lv^} -v # test whole log was saved
+  $LAKE build art${lv^} "$@" | grep --color foo && exit 1 || true # test replay
+}
+
+log_empty info -q
+log_empty info --log-level=warning
+log_empty warning --log-level=error
+
+log_empty trace -q
+log_empty trace --log-level=info
+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 -q 2>&1 |
+  grep --color "info: bar"  && exit 1 || true
+$LAKE resolve-deps -R -Klog=warning 2>&1 | grep --color "warning: bar"
+$LAKE resolve-deps -R -Klog=warning --log-level=error 2>&1 |
+  grep --color "warning: bar" && exit 1 || true