chore: address review comments

tydeu · tydeu · commit 27b90140987f · 2025-06-10T17:49:56.000+02:00
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Module
-import Lean.Util.Paths
 import Lean.CoreM
 
 namespace Lean.Elab
diff --git a/src/Lean/Server/Completion/ImportCompletion.lean b/src/Lean/Server/Completion/ImportCompletion.lean
@@ -5,7 +5,6 @@ Authors: Marc Huisinga
 -/
 prelude
 import Lean.Data.NameTrie
-import Lean.Util.Paths
 import Lean.Util.LakePath
 import Lean.Server.Completion.CompletionItemData
 import Lean.Parser.Module
diff --git a/src/Lean/Server/FileWorker/SetupFile.lean b/src/Lean/Server/FileWorker/SetupFile.lean
@@ -38,8 +38,7 @@ partial def runLakeSetupFile
   }
   let lakeProc ← Process.spawn spawnArgs
   let (stdin, lakeProc) ← lakeProc.takeStdin
-  stdin.putStr (toJson header).compress
-  stdin.putStr "\n"
+  stdin.putStrLn (toJson header).compress
 
   let rec processStderr (acc : String) : IO String := do
     let line ← lakeProc.stderr.getLine
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
@@ -11,8 +11,6 @@ import Std.Data.TreeMap
 import Init.Data.ByteArray
 import Lean.Data.RBMap
 
-import Lean.Util.Paths
-
 import Lean.Data.FuzzyMatching
 import Lean.Data.Json
 import Lean.Data.Lsp
diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean
@@ -28,7 +28,6 @@ import Lean.Util.SCC
 import Lean.Util.TestExtern
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
-import Lean.Util.FileSetupInfo
 import Lean.Util.Heartbeats
 import Lean.Util.SearchPath
 import Lean.Util.SafeExponentiation
diff --git a/src/Lean/Util/FileSetupInfo.lean b/src/Lean/Util/FileSetupInfo.lean
diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marc Huisinga
 -/
 prelude
-import Lean.Util.Paths
+import Lean.Data.Json
 
 namespace Lean
 
diff --git a/src/Lean/Util/Paths.lean b/src/Lean/Util/Paths.lean
diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
@@ -57,7 +57,7 @@ def setupFile
   if configFile.toString.isEmpty then
     exit noConfigFileCode
   else if configFile == path then do
-    let header ← header?.getDM <|
+    let header ← header?.getDM do
       Lean.parseImports' (← IO.FS.readFile path) leanFile.toString
     let setup : ModuleSetup := {
       name := configModuleName
diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 prelude
-import Lean.Util.Paths
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
 import Lake.Config.Env

Original file line number	Diff line number	Diff line change
`@@ -38,8 +38,7 @@ partial def runLakeSetupFile`
`38`	`38`	`}`
`39`	`39`	`let lakeProc ← Process.spawn spawnArgs`
`40`	`40`	`let (stdin, lakeProc) ← lakeProc.takeStdin`
`41`		`- stdin.putStr (toJson header).compress`
`42`		`- stdin.putStr "\n"`
	`41`	`+ stdin.putStrLn (toJson header).compress`
`43`	`42`
`44`	`43`	`let rec processStderr (acc : String) : IO String := do`
`45`	`44`	`let line ← lakeProc.stderr.getLine`