diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean index d658c7da76f5..39ca7951656c 100644 --- a/src/lake/Lake/Build/Basic.lean +++ b/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. diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean index d2899bf05ea5..221b91193e02 100644 --- a/src/lake/Lake/CLI/Error.lean +++ b/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}" diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 5bc0902d57c1..042614704922 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/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 ` for more information on a specific command." def templateHelp := diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 8e3b3df4f1c1..3c2621b519ad 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index b6185e1b456a..c106fe817271 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -89,18 +89,31 @@ def LogLevel.ansiColor : LogLevel → String | .warning => "33" | .error => "31" +protected def LogLevel.ofString? (s : String) : Option LogLevel := + match s.toLower with + | "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 diff --git a/src/lake/tests/logLevel/Log/Error.lean b/src/lake/tests/logLevel/Log/Error.lean new file mode 100644 index 000000000000..137301e9a005 --- /dev/null +++ b/src/lake/tests/logLevel/Log/Error.lean @@ -0,0 +1,2 @@ +import Lean.Elab.Command +run_cmd Lean.logError "foo" diff --git a/src/lake/tests/logLevel/Log/Info.lean b/src/lake/tests/logLevel/Log/Info.lean new file mode 100644 index 000000000000..eea08cf07ccf --- /dev/null +++ b/src/lake/tests/logLevel/Log/Info.lean @@ -0,0 +1,2 @@ +import Lean.Elab.Command +run_cmd Lean.logInfo "foo" diff --git a/src/lake/tests/logLevel/Log/Warning.lean b/src/lake/tests/logLevel/Log/Warning.lean new file mode 100644 index 000000000000..14d0a780eb11 --- /dev/null +++ b/src/lake/tests/logLevel/Log/Warning.lean @@ -0,0 +1,2 @@ +import Lean.Elab.Command +run_cmd Lean.logWarning "foo" diff --git a/src/lake/tests/wfail/clean.sh b/src/lake/tests/logLevel/clean.sh similarity index 100% rename from src/lake/tests/wfail/clean.sh rename to src/lake/tests/logLevel/clean.sh diff --git a/src/lake/tests/logLevel/lakefile.lean b/src/lake/tests/logLevel/lakefile.lean new file mode 100644 index 000000000000..8fa2e1328315 --- /dev/null +++ b/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.toString.capitalize}" + (((), ·)) <$> 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 diff --git a/src/lake/tests/logLevel/test.sh b/src/lake/tests/logLevel/test.sh new file mode 100755 index 000000000000..0ae448062073 --- /dev/null +++ b/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 diff --git a/src/lake/tests/wfail/Warn.lean b/src/lake/tests/wfail/Warn.lean deleted file mode 100644 index 534874a20d5c..000000000000 --- a/src/lake/tests/wfail/Warn.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Lean.Elab.Command - -run_cmd Lean.logWarning "bar" diff --git a/src/lake/tests/wfail/lakefile.lean b/src/lake/tests/wfail/lakefile.lean deleted file mode 100644 index a7bd9aafd2f6..000000000000 --- a/src/lake/tests/wfail/lakefile.lean +++ /dev/null @@ -1,17 +0,0 @@ -import Lake -open Lake DSL - -package test - -lean_lib Warn - -target warn : PUnit := Job.async do - logWarning "foo" - return ((), .nil) - -target warnArt pkg : PUnit := Job.async do - let warnArtFile := pkg.buildDir / "warn_art" - (((), ·)) <$> buildFileUnlessUpToDate warnArtFile .nil do - logWarning "foo-file" - createParentDirs warnArtFile - IO.FS.writeFile warnArtFile "" diff --git a/src/lake/tests/wfail/test.sh b/src/lake/tests/wfail/test.sh deleted file mode 100755 index 8c53757eae06..000000000000 --- a/src/lake/tests/wfail/test.sh +++ /dev/null @@ -1,22 +0,0 @@ -#!/usr/bin/env bash -set -euxo pipefail - -LAKE=${LAKE:-../../.lake/build/bin/lake} - -./clean.sh - -# Test Lake warnings produce build failures with `--wfail` - -$LAKE build warn | grep --color foo -$LAKE build warn | grep --color foo # test idempotent -$LAKE build warn --wfail && exit 1 || true - -$LAKE build warnArt | grep --color foo-file -$LAKE build warnArt | grep --color foo-file # test `buildFileUpToDate` cache -$LAKE build warnArt --wfail && exit 1 || true - -# Test Lean warnings produce build failures with `--wfail` - -$LAKE build Warn | grep --color bar -$LAKE build Warn | grep --color bar # test Lean module build log cache -$LAKE build Warn --wfail && exit 1 || true