fix: use Lake install's olean files over LEAN_PATH

tydeu · tydeu · commit 88dc993a900b · 2022-06-29T12:56:49.000-04:00
diff --git 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
@@ -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).

Original file line number	Diff line number	Diff line change
@@ -280,4 +280,4 @@ The `lake` executable needs to know where to find the `.olean` files for the mod
`280`	`280`
`281`	`281`	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`.
`282`	`282`
`283`		-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.
	`283`	+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).