chore: remove verbosity from LoadConfig

Lake/CLI/Actions.lean

@@ -26,15 +26,16 @@ If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).
 
 The `print-paths` command is used internally by Lean 4 server.
 -/
-def printPaths (config : LoadConfig) (imports : List String := []) (oldMode : Bool := false) : MainM PUnit := do
+def printPaths (config : LoadConfig) (imports : List String := [])
+(oldMode : Bool := false) (verbosity : Verbosity := .normal) : MainM PUnit := do
   let configFile := config.rootDir / config.configFile
   if (← configFile.pathExists) then
     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 ← MainM.runLogIO (loadWorkspace config) config.verbosity
+    let ws ← MainM.runLogIO (loadWorkspace config) verbosity
     let dynlibs ← ws.runBuild (buildImportsAndDeps imports) oldMode
-      |>.run (MonadLog.eio config.verbosity)
+      |>.run (MonadLog.eio verbosity)
     IO.println <| Json.compress <| toJson {
       oleanPath := ws.leanPath
       srcPath := ws.leanSrcPath

Lake/CLI/Main.lean

@@ -63,7 +63,6 @@ def LakeOptions.mkLoadConfig
     configFile := opts.rootDir / opts.configFile
     configOpts := opts.configOpts
     leanOpts := Lean.Options.empty
-    verbosity := opts.verbosity
     updateDeps
   }
 
@@ -261,7 +260,7 @@ protected def build : CliM PUnit := do
   let ws ← loadWorkspace config
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
-  ws.runBuild (buildSpecs specs) opts.oldMode |>.run (MonadLog.io config.verbosity)
+  ws.runBuild (buildSpecs specs) opts.oldMode |>.run (MonadLog.io opts.verbosity)
 
 protected def resolveDeps : CliM PUnit := do
   processOptions lakeOption
@@ -290,7 +289,7 @@ protected def printPaths : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
-  printPaths config (← takeArgs) opts.oldMode
+  printPaths config (← takeArgs) opts.oldMode opts.verbosity
 
 protected def clean : CliM PUnit := do
   processOptions lakeOption

Lake/Load/Config.lean

@@ -26,8 +26,6 @@ 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.