chore: prefer LEAN_SRC_PATH

nix/buildLeanPackage.nix

@@ -222,7 +222,7 @@ in rec {
   };
 
   lean-package = writeShellScriptBin "lean" ''
-    LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=${src}:$LEAN_SRC_PATH ${lean-final}/bin/lean "$@"
+    LEAN_PATH=${modRoot}:$LEAN_PATH LEAN_SRC_PATH=$LEAN_SRC_PATH:${src} exec ${lean-final}/bin/lean "$@"
   '';
   emacs-package = makeEmacsWrapper "emacs-package" lean-package;
   vscode-package = makeVSCodeWrapper "vscode-package" lean-package;

src/Lean/Server/FileWorker.lean

@@ -207,7 +207,7 @@ section Initialization
         -- NOTE: lake does not exist in stage 0 (yet?)
         if path.fileName != "lakefile.lean" && (← System.FilePath.pathExists lakePath) then
           let pkgSearchPath ← lakeSetupSearchPath lakePath m (Lean.Elab.headerToImports headerStx).toArray hOut
-          srcSearchPath := pkgSearchPath ++ srcSearchPath
+          srcSearchPath ← initSrcSearchPath (← getBuildDir) pkgSearchPath
       Elab.processHeader headerStx opts msgLog m.mkInputContext
     catch e =>  -- should be from `lake print-paths`
       let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -70,7 +70,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
   let hoverPos := text.lspPosToUtf8Pos p.position
 
   let documentUriFromModule (modName : Name) : MetaM (Option DocumentUri) := do
-    let some modFname ← rc.srcSearchPath.findWithExt "lean" modName
+    let some modFname ← rc.srcSearchPath.findModuleWithExt "lean" modName
       | pure none
     -- resolve symlinks (such as `src` in the build dir) so that files are opened
     -- in the right folder

src/Lean/Util/Paths.lean

@@ -26,6 +26,6 @@ def initSrcSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Sea
     else []
   let srcPath := (← IO.appDir) / ".." / "src" / "lean"
   -- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
-  return srcSearchPath ++ [srcPath / "lake", srcPath]
+  return srcSearchPath ++ sp ++ [srcPath / "lake", srcPath]
 
 end Lean