diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean
index b650517f82..2b3376dc4e 100644
--- a/Lake/Build/Actions.lean
+++ b/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
diff --git a/Lake/Build/Executable.lean b/Lake/Build/Executable.lean
index 7cfdd560f2..cbda3d8746 100644
--- a/Lake/Build/Executable.lean
+++ b/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
diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
index 1ebdc58859..4c551bd2f1 100644
--- a/Lake/Build/Index.lean
+++ b/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
diff --git a/Lake/Build/Library.lean b/Lake/Build/Library.lean
index 023e66e270..a6239c9163 100644
--- a/Lake/Build/Library.lean
+++ b/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 :=
diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index cef5c27ac3..6cbe7e1858 100644
--- a/Lake/Build/Module.lean
+++ b/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`. -/
diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean
index 948e6f2d26..04707fe247 100644
--- a/Lake/Build/Targets.lean
+++ b/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 :=
diff --git a/Lake/CLI/Help.lean b/Lake/CLI/Help.lean
index 8e278e3940..782a077036 100644
--- a/Lake/CLI/Help.lean
+++ b/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
 
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 8b787337d3..a76a102f9e 100644
--- a/Lake/CLI/Main.lean
+++ b/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
diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean
index 20774adfa1..c0ebfb1104 100644
--- a/Lake/Config/Workspace.lean
+++ b/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)
diff --git a/Lake/Load/Config.lean b/Lake/Load/Config.lean
index ec59d26673..c77fbdd3d2 100644
--- a/Lake/Load/Config.lean
+++ b/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.
diff --git a/Lake/Util/Log.lean b/Lake/Util/Log.lean
index 8813adf445..423c349af8 100644
--- a/Lake/Util/Log.lean
+++ b/Lake/Util/Log.lean
@@ -12,13 +12,28 @@ inductive LogLevel
 | warning
 | error
 
+inductive Verbosity
+| quiet
+| normal
+| verbose
+deriving BEq
+
+instance : Inhabited Verbosity := ⟨.normal⟩
+
 /-! # Class -/
 
 class MonadLog (m : Type u → Type v) where
+  verbosity : m (ULift Verbosity)
   log (message : String) (level : LogLevel) : m PUnit
 
 export MonadLog (log)
 
+abbrev logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do
+  if (← MonadLog.verbosity (m := m)).1 == .verbose then log message .info
+
+abbrev logAuxInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do
+  if (← MonadLog.verbosity (m := m)).1 != .quiet then log message .info
+
 abbrev logInfo [MonadLog m] (message : String) : m PUnit :=
   log message .info
 
@@ -31,26 +46,29 @@ abbrev logError  [MonadLog m] (message : String) : m PUnit :=
 namespace MonadLog
 
 def nop [Pure m] : MonadLog m :=
-  ⟨fun _ _ => pure ()⟩
+  ⟨pure ⟨.normal⟩, fun _ _ => pure ()⟩
 
 instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
 
-def io [MonadLiftT BaseIO m] : MonadLog m where
+def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+  verbosity := (pure ⟨verbosity⟩ : BaseIO _)
   log msg
     | .info => IO.println msg.trim |>.catchExceptions fun _ => pure ()
     | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
 
-def eio [MonadLiftT BaseIO m] : MonadLog m where
+def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
+  verbosity := (pure ⟨verbosity⟩ : BaseIO _)
   log msg
-    | .info => IO.eprintln s!"info: {msg.trim}"  |>.catchExceptions fun _ => pure ()
+    | .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
     | .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
 
 def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
+  verbosity := liftM <| self.verbosity
   log msg lv := liftM <| self.log msg lv
 
-instance [MonadLift m n] [methods : MonadLog m] : MonadLog n  := lift methods
+instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
 
 /-- Log the given error message and then fail. -/
 protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
@@ -67,6 +85,7 @@ instance [Pure n] [Inhabited α] : Inhabited (MonadLogT m n α) :=
   ⟨fun _ => pure Inhabited.default⟩
 
 instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
+  verbosity := do (← read).verbosity
   log msg lv := do (← read).log msg lv
 
 namespace MonadLogT
diff --git a/Lake/Util/MainM.lean b/Lake/Util/MainM.lean
index f1416c6f76..d9f8d9904a 100644
--- a/Lake/Util/MainM.lean
+++ b/Lake/Util/MainM.lean
@@ -75,4 +75,8 @@ protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
 instance : MonadError MainM := ⟨MainM.error⟩
 instance [ToString ε] : MonadLift (EIO ε) MainM := ⟨MonadError.runEIO⟩
 instance : MonadLift IO MainM := inferInstance -- necessary, but don't know why
-instance : MonadLift LogIO MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩
+
+def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
+  liftM <| MonadLogT.run (MonadLog.eio verbosity) x
+
+instance : MonadLift LogIO MainM := ⟨runLogIO⟩
diff --git a/examples/ffi/lib/lakefile.lean b/examples/ffi/lib/lakefile.lean
index c99b5e3dac..70209dc7e9 100644
--- a/examples/ffi/lib/lakefile.lean
+++ b/examples/ffi/lib/lakefile.lean
@@ -20,8 +20,8 @@ def ffiOTarget : FileTarget :=
   let oFile := cBuildDir / "ffi.o"
   let srcTarget := inputFileTarget <| cSrcDir / "ffi.cpp"
   fileTargetWithDep oFile srcTarget fun srcFile => do
-    compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"] "c++"
+    compileO `ffi oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"] "c++"
 
 extern_lib cLib :=
   let libFile := cBuildDir / nameToStaticLib "leanffi"
-  staticLibTarget libFile #[ffiOTarget]
+  staticLibTarget `leanffi libFile #[ffiOTarget]
diff --git a/test/50/test.sh b/test/50/test.sh
index 157f314f33..b05221cb64 100755
--- a/test/50/test.sh
+++ b/test/50/test.sh
@@ -5,7 +5,7 @@ LAKE=${LAKE:-../../../build/bin/lake}
 
 cd foo
 rm -rf build
-${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m2 foo.c
-${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAZ | grep -m2 foo.c
-${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAR | grep -m1 foo.o
-${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m1 foo.olean
+${LAKE} build -v -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m2 foo.c
+${LAKE} build -v -KleanArgs=-Dhygiene=false -K leancArgs=-DBAZ | grep -m2 foo.c
+${LAKE} build -v -KleanArgs=-Dhygiene=false -K leancArgs=-DBAR | grep -m1 foo.o
+${LAKE} build -v -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m1 foo.olean
diff --git a/test/62/test.sh b/test/62/test.sh
index 7fe1b12cb5..8074d2bd59 100755
--- a/test/62/test.sh
+++ b/test/62/test.sh
@@ -9,4 +9,4 @@ lake +leanprover/lean4:nightly-2022-06-30 new foo
 cd foo
 lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo
 cp ../../../lean-toolchain lean-toolchain
-${LAKE:-../../../build/bin/lake} build | grep -m1 foo
+${LAKE:-../../../build/bin/lake} build -v | grep -m1 foo
diff --git a/test/84/test.sh b/test/84/test.sh
index c7af6425f0..569f8f851f 100755
--- a/test/84/test.sh
+++ b/test/84/test.sh
@@ -32,6 +32,6 @@ git commit -am 'second commit in a'
 popd
 
 pushd b
-$LAKE1 update
+$LAKE1 update -v
 git diff | grep -m1 manifest
 popd