From b3c8ee292396b93ebad04090c99700cfca1b13e5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 19 Oct 2021 10:56:38 +0200
Subject: [PATCH] fix: add Lake to built-in search path

---
 src/Lean/Server/FileWorker.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 5d1b002122..7f19870558 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -170,7 +170,8 @@ section Initialization
           | some path => pure <| System.FilePath.mk path / "bin" / lakePath
           | _         => pure <| (← appDir) / lakePath
         lakePath.withExtension System.FilePath.exeExtension
-    let mut srcSearchPath := [(← appDir) / ".." / "lib" / "lean" / "src"]
+    let srcPath := (← appDir) / ".." / "lib" / "lean" / "src"
+    let mut srcSearchPath := [srcPath, srcPath / "lake"]
     if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
       srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
     let (headerEnv, msgLog) ← try