From 17a36f89aa8ebf8e79d1a2b88eb2be9da3779fc3 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 29 Jun 2022 12:56:49 -0400
Subject: [PATCH] fix: use Lake install's olean files over LEAN_PATH

---
 Lake/Config/SearchPath.lean | 2 +-
 README.md                   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Lake/Config/SearchPath.lean b/Lake/Config/SearchPath.lean
index 1a7517698f..ccdafcf049 100644
--- a/Lake/Config/SearchPath.lean
+++ b/Lake/Config/SearchPath.lean
@@ -33,9 +33,9 @@ def setupLeanSearchPath
 (leanInstall? : Option LeanInstall) (lakeInstall? : Option LakeInstall)
 : IO Unit := do
   let mut sp : SearchPath := []
+  sp ← Lean.addSearchPathFromEnv sp
   if let some leanInstall := leanInstall? then
     sp := leanInstall.oleanDir :: sp
   if let some lakeInstall := lakeInstall? then
     sp := lakeInstall.oleanDir :: sp
-  sp ← Lean.addSearchPathFromEnv sp
   Lean.searchPathRef.set sp
diff --git a/README.md b/README.md
index 76190946ca..9a4497e864 100644
--- a/README.md
+++ b/README.md
@@ -280,4 +280,4 @@ The `lake` executable needs to know where to find the `.olean` files for the mod
 
 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 `.olean` files at `<lean-home/lib/lean`. 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>/lib`.
 
-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.
+This search path can be augmented by including other directories of `.olean` files in the `LEAN_PATH` environment variable, allowing the user to correct Lake's search if the `.olean` files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important in development, as it prevents the Lake version being used to build Lake from using the Lake version being built's `.olean` files to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors).