From fbb1184f256c4e36fb87afe0122dc99c8993a1e1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 21 Jan 2021 14:12:51 +0100
Subject: [PATCH] feat: auto-add stdlib to LEAN_SRC_PATH for installed Lean

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

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 8f1f87a304..7b12db1b65 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -204,9 +204,9 @@ section Initialization
     let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with
       | some path => s!"{path}/bin/leanpkg{System.FilePath.exeSuffix}"
       | _         => s!"{← appDir}/leanpkg{System.FilePath.exeSuffix}"
-    let mut srcSearchPath := match (← IO.getEnv "LEAN_SRC_PATH") with
-      | some p => parseSearchPath p
-      | none   => []
+    let mut srcSearchPath := [s!"{← appDir}/../lib/lean/src"]
+    if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
+      srcSearchPath := srcSearchPath ++ parseSearchPath p
     -- NOTE: leanpkg does not exist in stage 0 (yet?)
     if (← fileExists leanpkgPath) then
       let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut