From f40dbbcf022a3872dd6b7eaf73a7b4409ce19604 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Mon, 8 Aug 2022 16:38:04 -0400
Subject: [PATCH] chore: remove `verbosity` from `LoadConfig`

---
 Lake/CLI/Actions.lean | 7 ++++---
 Lake/CLI/Main.lean    | 5 ++---
 Lake/Load/Config.lean | 2 --
 3 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/Lake/CLI/Actions.lean b/Lake/CLI/Actions.lean
index ef108b94c6..9977352ae5 100644
--- a/Lake/CLI/Actions.lean
+++ b/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
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 8cc4b0f8f3..7e4b853436 100644
--- a/Lake/CLI/Main.lean
+++ b/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
diff --git a/Lake/Load/Config.lean b/Lake/Load/Config.lean
index c77fbdd3d2..de31506b72 100644
--- a/Lake/Load/Config.lean
+++ b/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.