feat: verbosity options for logging + neater build progress

Lake/Build/Actions.lean

@@ -16,7 +16,7 @@ def proc (args : IO.Process.SpawnArgs) : JobM Unit := do
   let envStr := String.join <| args.env.toList.filterMap fun (k, v) =>
     if k == "PATH" then none else some s!"{k}={v.getD ""} " -- PATH too big
   let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
-  logInfo <| "> " ++ envStr ++
+  logVerbose <| "> " ++ envStr ++
     match args.cwd with
     | some cwd => s!"{cmdStr}    # in directory {cwd}"
     | none     => cmdStr
@@ -33,12 +33,13 @@ def proc (args : IO.Process.SpawnArgs) : JobM Unit := do
     logError s!"external command {args.cmd} exited with status {out.exitCode}"
     failure
 
-def compileLeanModule (leanFile : FilePath)
+def compileLeanModule (name : Name) (leanFile : FilePath)
 (oleanFile? ileanFile? cFile? : Option FilePath)
 (leanPath : SearchPath := []) (rootDir : FilePath := ".")
 (dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
 (leanArgs : Array String := #[]) (lean : FilePath := "lean")
 : JobM PUnit := do
+  logAuxInfo s!"Building {name}"
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
   if let some oleanFile := oleanFile? then
@@ -61,32 +62,36 @@ def compileLeanModule (leanFile : FilePath)
     ]
   }
 
-def compileO (oFile srcFile : FilePath)
+def compileO (name : Name) (oFile srcFile : FilePath)
 (moreArgs : Array String := #[]) (compiler : FilePath := "cc") : JobM Unit := do
+  logAuxInfo s!"Compiling {name}"
   createParentDirs oFile
   proc {
     cmd := compiler.toString
     args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
   }
 
-def compileStaticLib (libFile : FilePath)
+def compileStaticLib (name : Name) (libFile : FilePath)
 (oFiles : Array FilePath) (ar : FilePath := "ar") : JobM Unit := do
+  logAuxInfo s!"Linking {name}"
   createParentDirs libFile
   proc {
     cmd := ar.toString
     args := #["rcs", libFile.toString] ++ oFiles.map toString
   }
 
-def compileSharedLib (libFile : FilePath)
+def compileSharedLib (name : Name) (libFile : FilePath)
 (linkArgs : Array String) (linker : FilePath := "cc") : JobM Unit := do
+  logAuxInfo s!"Linking {name}"
   createParentDirs libFile
   proc {
     cmd := linker.toString
     args := #["-shared", "-o", libFile.toString] ++ linkArgs
   }
 
-def compileExe (binFile : FilePath) (linkFiles : Array FilePath)
+def compileExe (name : Name) (binFile : FilePath) (linkFiles : Array FilePath)
 (linkArgs : Array String := #[]) (linker : FilePath := "cc") : JobM Unit := do
+  logAuxInfo s!"Linking {name}"
   createParentDirs binFile
   proc {
     cmd := linker.toString

Lake/Build/Executable.lean

@@ -21,4 +21,4 @@ protected def LeanExe.recBuildExe
   let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do
     linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
-  leanExeTarget self.file linkTargets self.linkArgs |>.activate
+  leanExeTarget self.name self.file linkTargets self.linkArgs |>.activate

Lake/Build/Index.lean

@@ -59,7 +59,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
 | .sharedExternLib lib =>
   mkTargetFacetBuild ExternLib.sharedFacet do
     let staticTarget := Target.active <| ← lib.static.recBuild
-    staticToLeanSharedLibTarget staticTarget |>.activate
+    staticToLeanSharedLibTarget lib.name staticTarget |>.activate
 | .dynlibExternLib lib =>
   mkTargetFacetBuild ExternLib.dynlibFacet do
     let sharedTarget := Target.active <| ← lib.shared.recBuild

Lake/Build/Library.lean

@@ -37,7 +37,7 @@ def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
 protected def LeanLib.recBuildStatic
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
   let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
-  staticLibTarget self.staticLibFile oTargets |>.activate
+  staticLibTarget self.name self.staticLibFile oTargets |>.activate
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
@@ -79,7 +79,7 @@ def LeanLib.recBuildLinks
 protected def LeanLib.recBuildShared
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
   let linkJobs := (← self.recBuildLinks).map Target.active
-  leanSharedLibTarget self.sharedLibFile linkJobs self.linkArgs |>.activate
+  leanSharedLibTarget self.name self.sharedLibFile linkJobs self.linkArgs |>.activate
 
 /-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
 def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=

Lake/Build/Module.lean

@@ -19,12 +19,12 @@ def Module.buildUnlessUpToDate (mod : Module)
   let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
   if leanOnly then
     unless modUpToDate do
-      compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
+      compileLeanModule mod.name mod.leanFile mod.oleanFile mod.ileanFile none
         (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
   else
     let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
     unless modUpToDate && cUpToDate do
-      compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
+      compileLeanModule mod.name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
         (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
     modTrace.writeToFile mod.cTraceFile
   modTrace.writeToFile mod.traceFile
@@ -143,7 +143,7 @@ def Module.cFacetConfig : ModuleFacetConfig cFacet :=
 /-- Recursively build the module's object file from its C file produced by `lean`. -/
 def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
   let cJob := Target.active (← self.c.recBuild)
-  leanOFileTarget self.oFile cJob self.leancArgs |>.activate
+  leanOFileTarget self.name self.oFile cJob self.leancArgs |>.activate
 
 /-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
 def Module.oFacetConfig : ModuleFacetConfig oFacet :=
@@ -215,7 +215,7 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do
     let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
       let args := links.map toString ++
         libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}")
-      compileSharedLib mod.dynlibFile args (← getLeanc)
+      compileSharedLib mod.name mod.dynlibFile args (← getLeanc)
     return (mod.dynlibName, trace)
 
 /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/

Lake/Build/Targets.lean

@@ -47,44 +47,44 @@ def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget ι
 
 /-! # Specific Targets -/
 
-def oFileTarget (oFile : FilePath) (srcTarget : FileTarget)
+def oFileTarget (name : Name) (oFile : FilePath) (srcTarget : FileTarget)
 (args : Array String := #[]) (compiler : FilePath := "c++") : FileTarget :=
   fileTargetWithDep oFile srcTarget (extraDepTrace := computeHash args) fun srcFile => do
-    compileO oFile srcFile args compiler
+    compileO name oFile srcFile args compiler
 
-def leanOFileTarget (oFile : FilePath)
+def leanOFileTarget (name : Name) (oFile : FilePath)
 (srcTarget : FileTarget) (args : Array String := #[]) : FileTarget :=
   fileTargetWithDep oFile srcTarget (extraDepTrace := computeHash args) fun srcFile => do
-    compileO oFile srcFile args (← getLeanc)
+    compileO name oFile srcFile args (← getLeanc)
 
-def staticLibTarget (libFile : FilePath)
+def staticLibTarget (name : Name) (libFile : FilePath)
 (oFileTargets : Array FileTarget) (ar : Option FilePath := none) : FileTarget :=
   fileTargetWithDepArray libFile oFileTargets fun oFiles => do
-    compileStaticLib libFile oFiles (ar.getD (← getLeanAr))
+    compileStaticLib name libFile oFiles (ar.getD (← getLeanAr))
 
-def cSharedLibTarget (libFile : FilePath)
+def cSharedLibTarget (name : Name) (libFile : FilePath)
 (linkTargets : Array FileTarget) (linkArgs : Array String := #[])
 (linker : FilePath := "cc"): FileTarget :=
   fileTargetWithDepArray libFile linkTargets fun links => do
-    compileSharedLib libFile (links.map toString ++ linkArgs) linker
+    compileSharedLib name libFile (links.map toString ++ linkArgs) linker
 
-def leanSharedLibTarget (libFile : FilePath)
+def leanSharedLibTarget (name : Name) (libFile : FilePath)
 (linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
   fileTargetWithDepArray libFile linkTargets fun links => do
-    compileSharedLib libFile (links.map toString ++ linkArgs) (← getLeanc)
+    compileSharedLib name libFile (links.map toString ++ linkArgs) (← getLeanc)
 
-def cExeTarget (exeFile : FilePath) (linkTargets : Array FileTarget)
+def cExeTarget (name : Name) (exeFile : FilePath) (linkTargets : Array FileTarget)
 (linkArgs : Array String := #[]) (linker : FilePath := "cc") : FileTarget :=
   fileTargetWithDepArray exeFile linkTargets (extraDepTrace := computeHash linkArgs) fun links => do
-    compileExe exeFile links linkArgs linker
+    compileExe name exeFile links linkArgs linker
 
-def leanExeTarget (exeFile : FilePath)
+def leanExeTarget (name : Name) (exeFile : FilePath)
 (linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
   fileTargetWithDepArray exeFile linkTargets
   (extraDepTrace := getLeanTrace <&> (·.mix <| pureHash linkArgs)) fun links => do
-    compileExe exeFile links linkArgs (← getLeanc)
+    compileExe name exeFile links linkArgs (← getLeanc)
 
-def staticToLeanSharedLibTarget (staticLibTarget : FileTarget) : FileTarget :=
+def staticToLeanSharedLibTarget (name : Name) (staticLibTarget : FileTarget) : FileTarget :=
   .mk <| staticLibTarget.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let trace ← buildFileUnlessUpToDate dynlib staticTrace do
@@ -93,7 +93,7 @@ def staticToLeanSharedLibTarget (staticLibTarget : FileTarget) : FileTarget :=
           #[s!"-Wl,-force_load,{staticLib}"]
         else
           #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
-      compileSharedLib dynlib args (← getLeanc)
+      compileSharedLib name dynlib args (← getLeanc)
     return (dynlib, trace)
 
 def sharedToLeanDynlibTarget (sharedLibTarget : FileTarget) : DynlibTarget :=

Lake/CLI/Help.lean

@@ -18,6 +18,8 @@ OPTIONS:
   --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
 

Lake/CLI/Main.lean

@@ -30,6 +30,7 @@ structure LakeOptions where
   configOpts : NameMap String := {}
   subArgs : List String := []
   wantsHelp : Bool := false
+  verbosity : Verbosity := .normal
 
 /-- Get the Lean installation. Error if missing. -/
 def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
@@ -60,6 +61,7 @@ def LakeOptions.mkLoadConfig
     configFile := opts.rootDir / opts.configFile
     configOpts := opts.configOpts
     leanOpts := Lean.Options.empty
+    verbosity := opts.verbosity
     updateDeps
   }
 
@@ -77,6 +79,9 @@ 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
 
+instance : MonadLift LogIO CliStateM :=
+  ⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
+
 /-! ## Argument Parsing -/
 
 def takeArg (arg : String) : CliM String := do
@@ -119,18 +124,22 @@ def setConfigOpt (kvPair : String) : CliM PUnit :=
 
 def lakeShortOption : (opt : Char) → CliM PUnit
 | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
+| 'q' => modifyThe LakeOptions ({· with verbosity := .quiet})
+| 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
 | 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
 | 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
 | 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
 | opt => throw <| CliError.unknownShortOption opt
 
 def lakeLongOption : (opt : String) → CliM PUnit
-| "--help"  => modifyThe LakeOptions ({· with wantsHelp := true})
-| "--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"
-| "--"      => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
-| opt       => throw <| CliError.unknownLongOption opt
+| "--help"    => modifyThe LakeOptions ({· with wantsHelp := true})
+| "--quiet"   => modifyThe LakeOptions ({· with verbosity := .quiet})
+| "--verbose" => modifyThe LakeOptions ({· with verbosity := .verbose})
+| "--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"
+| "--"        => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
+| opt         => throw <| CliError.unknownLongOption opt
 
 def lakeOption :=
   option {
@@ -175,9 +184,9 @@ def printPaths (config : LoadConfig) (imports : List String := []) : MainM PUnit
     if (← IO.getEnv invalidConfigEnvVar) matches some .. then
       IO.eprintln s!"Error parsing '{configFile}'.  Please restart the lean server after fixing the Lake configuration file."
       exit 1
-    let ws ← loadWorkspace config
+    let ws ← MainM.runLogIO (loadWorkspace config) config.verbosity
     let ctx ← mkBuildContext ws
-    let dynlibs ← ws.root.buildImportsAndDeps imports |>.run MonadLog.eio ctx
+    let dynlibs ← ws.root.buildImportsAndDeps imports |>.run (MonadLog.eio config.verbosity) ctx
     IO.println <| Json.compress <| toJson {ws.leanPaths with loadDynlibPaths := dynlibs}
   else
     exit noConfigFileCode
@@ -200,11 +209,11 @@ def serve (config : LoadConfig) (args : Array String) : LogIO UInt32 := do
     env := extraEnv
   }).wait
 
-def exe (name : Name) (args  : Array String := #[]) : LakeT IO UInt32 := do
+def exe (name : Name) (args  : Array String := #[]) (verbosity : Verbosity) : LakeT IO UInt32 := do
   let ws ← getWorkspace
   if let some exe := ws.findLeanExe? name then
     let ctx ← mkBuildContext ws
-    let exeFile ← (exe.build >>= (·.await)).run MonadLog.eio ctx
+    let exeFile ← (exe.build >>= (·.await)).run (MonadLog.eio verbosity) ctx
     env exeFile.toString args
   else
     error s!"unknown executable `{name}`"
@@ -287,13 +296,13 @@ protected def new : CliM PUnit := do
   processOptions lakeOption
   let pkgName ← takeArg "package name"
   let template ← parseTemplateSpec <| (← takeArg?).getD ""
-  noArgsRem <| new pkgName template
+  noArgsRem <| MainM.runLogIO (new pkgName template) (← getThe LakeOptions).verbosity
 
 protected def init : CliM PUnit := do
   processOptions lakeOption
   let pkgName ← takeArg "package name"
   let template ← parseTemplateSpec <| (← takeArg?).getD ""
-  noArgsRem <| init pkgName template
+  noArgsRem <| MainM.runLogIO (init pkgName template) (← getThe LakeOptions).verbosity
 
 protected def build : CliM PUnit := do
   processOptions lakeOption
@@ -303,7 +312,7 @@ protected def build : CliM PUnit := do
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
   let ctx ← mkBuildContext ws
-  BuildM.run MonadLog.io ctx <| buildSpecs specs
+  BuildM.run (MonadLog.io config.verbosity) ctx <| buildSpecs specs
 
 protected def update : CliM PUnit := do
   processOptions lakeOption
@@ -349,7 +358,7 @@ protected def exe : CliM PUnit := do
   let config ← mkLoadConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   let ctx := mkLakeContext ws
-  exit <| ← (exe exeName args.toArray).run ctx
+  exit <| ← (exe exeName args.toArray config.verbosity).run ctx
 
 protected def selfCheck : CliM PUnit := do
   processOptions lakeOption

Lake/Config/Workspace.lean

@@ -7,6 +7,7 @@ import Lean.Util.Paths
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
 import Lake.Config.Env
+import Lake.Util.Log
 
 open System
 open Lean (LeanPaths)

Lake/Load/Config.lean

@@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lean.Data.Name
 import Lean.Data.Options
 import Lake.Config.Env
+import Lake.Util.Log
 
 namespace Lake
 open System Lean
@@ -25,6 +26,8 @@ structure LoadConfig where
   configOpts : NameMap String := {}
   /-- The Lean options with which to elaborate the configuration file. -/
   leanOpts : Options := {}
+  /-- The verbosity setting for logging messages. -/
+  verbosity : Verbosity := .normal
   /--
   Whether to update dependencies during resolution
   or fallback to the ones listed in the manifest.