feat: search path now first checks IO.appPath for lean

Lake/SearchPath.lean

@@ -6,9 +6,12 @@ Authors: Mac Malone
 import Lean.Util.Path
 
 open System
-
 namespace Lake
 
+/--
+  Try to find the home of Lean by calling
+  `lean --print-prefix` and returning the path it prints.
+-/
 def getLeanHome? : IO (Option FilePath) := do
   let out ← IO.Process.output {
     cmd := "lean",
@@ -19,9 +22,26 @@ def getLeanHome? : IO (Option FilePath) := do
   else
     none
 
+/--
+  Try to get Lake's home by assuming
+  this executable is located at `<lake-home>/bin/lake`.
+-/
 def getLakeHome? : IO (Option FilePath) := do
   (← IO.appPath).parent.bind FilePath.parent
 
+
+/--
+  Check if Lake's executable is co-located with Lean, and, if so,
+  try to return their joint home by assuming they are located at `<app-home>/bin`.
+-/
+def getAppHome? : IO (Option FilePath) := do
+  let appPath ← IO.appPath
+  if let some appDir := appPath.parent then
+    let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension
+    if (← leanExe.pathExists) then
+      return appDir.parent
+  return none
+
 /--
   Initializes the search path the Lake executable
   uses when interpreting package configuration files.
@@ -36,16 +56,28 @@ def getLakeHome? : IO (Option FilePath) := do
   the necessary directories, Lake also intelligently derives an initial
   search path from the location of the `lean` executable and itself.
 
-  It will assume that `lean` is located at `<lean-home>/bin/lean`
-  with its `.olean` files at `<lean-home>/lib/lean` and that `lake`
+  If Lake is co-located with `lean` (i.e., there is `lean` executable
+  in the same directory as itself), it will assume it was installed with
+  Lean and that both Lean and Lake are located in `<lean-home>/bin` with
+  Lean's `.olean` files at `<lean-home/lib/lean` and Lake's at `.olean` files
+  at `<lean-home/lib/lake`.
+
+  Otherwise, it will run `lean --print-prefix` to find Lean's home and
+  assume that its `.olean` files are at `<lean-home>/lib/lean` and that `lake`
   is at `<lake-home>/bin/lake` with its `.olean` files at `<lake-home>`.
   If this is correct, the user will not need to augment `LEAN_PATH`.
 -/
 def setupLeanSearchPath : IO Unit := do
   let mut sp : SearchPath := []
-  if let some lakeHome ← getLakeHome? then
-    sp := lakeHome :: sp
-  if let some leanHome ← getLeanHome? then
-    sp := leanHome / "lib" / "lean" :: sp
+  if let some appHome ← getAppHome? then
+    -- we are co-located with Lean
+    let libDir := appHome / "lib"
+    sp := libDir / "lean" :: libDir / "lake" :: sp
+  else
+    -- we are a custom installation
+    if let some lakeHome ← getLakeHome? then
+      sp := lakeHome :: sp
+    if let some leanHome ← getLeanHome? then
+      sp := leanHome / "lib" / "lean" :: sp
   sp ← Lean.addSearchPathFromEnv sp
   Lean.searchPathRef.set sp

README.md

@@ -15,7 +15,9 @@ After building, the `lake` binary will be located at `build/bin/lake` and the li
 
 ### Augmenting Lake's Search Path
 
-The `lake` executable needs to know where to find the `.olean` files for the modules used in the package configuration file. Lake will intelligently setup an initial search path based on the location of its own executable and `lean`. It will assume that `lean` is located at `<lean-home>/bin/lean` with its `.olean` files (e.g., for `Init`) at `<lean-home>/lib/lean` and that `lake` is at `<lake-home>/bin/lake` with its `.olean` files at `<lake-home>`.
+The `lake` executable needs to know where to find the `.olean` files for the modules used in the package configuration file. Lake will intelligently setup an initial search path based on the location of its own executable and `lean`.
+
+Specifically, if Lake is co-located with `lean` (i.e., there is `lean` executable in the same directory as itself), it will assume it was installed with Lean and that both Lean and Lake are located in `<lean-home>/bin` with Lean's `.olean` files at `<lean-home/lib/lean` and Lake's at `.olean` files at `<lean-home/lib/lake`. Otherwise, it will run `lean --print-prefix` to find Lean's home and assume that its `.olean` files are at `<lean-home>/lib/lean` and that `lake` is at `<lake-home>/bin/lake` with its `.olean` files at `<lake-home>`.
 
 This search path can be augmented by including other directories of `.olean` files in the `LEAN_PATH` environment variable. Such directories will take precedence over the initial search path, so `LEAN_PATH` can also be used to correct Lake's search if the `.olean` files for Lean (or Lake itself) are in non-standard locations.