From 3abb70dbb58a85404da4f5870ff995a242a6960f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 18 Jan 2022 18:21:09 +0100
Subject: [PATCH] refactor: factor out common source search path logic

---
 src/Lean/Server/FileWorker.lean |  6 +-----
 src/Lean/Server/Watchdog.lean   | 13 ++-----------
 src/Lean/Util/Paths.lean        | 11 +++++++++++
 3 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 0b9ba562c2..62b6331ab2 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -182,6 +182,7 @@ section Initialization
   def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) : IO (Snapshot × SearchPath) := do
     let inputCtx := Parser.mkInputContext m.text.source "<input>"
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
+    let mut srcSearchPath ← initSrcSearchPath (← getBuildDir)
     let lakePath ← match (← IO.getEnv "LAKE") with
       | some path => System.FilePath.mk path
       | none =>
@@ -193,9 +194,6 @@ section Initialization
           | some path => pure <| System.FilePath.mk path / "bin" / lakePath
           | _         => pure <| (← appDir) / lakePath
         lakePath.withExtension System.FilePath.exeExtension
-    let srcPath := (← appDir) / ".." / "lib" / "lean" / "src"
-    -- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
-    let mut srcSearchPath := [srcPath / "lake", srcPath]
     let (headerEnv, msgLog) ← try
       if let some path := m.uri.toPath? then
         -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps
@@ -212,8 +210,6 @@ section Initialization
       if let some path := m.uri.toPath? then
         headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
     catch _ => ()
-    if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
-      srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
     let cmdState := Elab.Command.mkState headerEnv msgLog opts
     let cmdState := { cmdState with infoState := {
       enabled := true
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index f7627ceaa1..770e607272 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -9,6 +9,7 @@ import Init.Data.ByteArray
 import Std.Data.RBMap
 
 import Lean.Elab.Import
+import Lean.Util.Paths
 
 import Lean.Data.Json
 import Lean.Data.Lsp
@@ -649,16 +650,6 @@ def findWorkerPath : IO System.FilePath := do
     workerPath := System.FilePath.mk path
   workerPath
 
--- TODO Combine with FileWorker.lean#compileHeader to deduplicate logic
--- TODO Support lake projects (src and olean paths)
-def findSrcSearchPath : IO System.SearchPath := do
-  let srcPath := (← appDir) / ".." / "lib" / "lean" / "src"
-  -- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
-  let mut srcSearchPath := [srcPath / "lake", srcPath]
-  if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
-    srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
-  srcSearchPath
-
 def loadReferences : IO References := do
   let oleanSearchPath ← Lean.searchPathRef.get
   let mut refs := References.empty
@@ -668,7 +659,7 @@ def loadReferences : IO References := do
 
 def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let workerPath ← findWorkerPath
-  let srcSearchPath ← findSrcSearchPath
+  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
   let references ← IO.mkRef (← loadReferences)
   let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
   let i ← maybeTee "wdIn.txt" false i
diff --git a/src/Lean/Util/Paths.lean b/src/Lean/Util/Paths.lean
index fcf7c02a48..b677425726 100644
--- a/src/Lean/Util/Paths.lean
+++ b/src/Lean/Util/Paths.lean
@@ -11,9 +11,20 @@ import Lean.Util.Path
 
 namespace Lean
 
+open System
+
 structure LeanPaths where
   oleanPath : SearchPath
   srcPath   : SearchPath
   deriving ToJson, FromJson
 
+def initSrcSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO SearchPath := do
+  let srcSearchPath :=
+    if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
+      System.SearchPath.parse p
+    else []
+  let srcPath := (← IO.appDir) / ".." / "lib" / "lean" / "src"
+  -- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
+  return srcSearchPath ++ [srcPath / "lake", srcPath]
+
 end Lean