feat: LAKE_OVERRIDE_LEAN

src/lake/Lake/Config/Env.lean

@@ -63,7 +63,7 @@ def compute
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
     reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
-    noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind toBool?).getD false
+    noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
     githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
@@ -72,10 +72,6 @@ def compute
     initPath := ← getSearchPath "PATH"
   }
 where
-  toBool? (o : String) : Option Bool :=
-    if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
-    else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
-    else none
   computePkgUrlMap := do
     let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
     match Json.parse urlMapStr |>.bind fromJson? with
@@ -149,6 +145,7 @@ def noToolchainVars : Array (String × Option String) :=
   #[
     ("ELAN_TOOLCHAIN", none),
     ("LAKE", none),
+    ("LAKE_OVERRIDE_LEAN", none),
     ("LAKE_HOME", none),
     ("LEAN", none),
     ("LEAN_GITHASH", none),

src/lake/Lake/Config/InstallPath.lean

@@ -9,6 +9,12 @@ import Lake.Config.Defaults
 open System
 namespace Lake
 
+/-- Convert the string value of an environment variable to a boolean. -/
+def envToBool? (o : String) : Option Bool :=
+  if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
+  else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
+  else none
+
 /-! ## Data Structures -/
 
 /-- Information about the local Elan setup. -/
@@ -296,7 +302,8 @@ Then it attempts to detect if Lake and Lean are part of a single installation
 where the `lake` executable is co-located with the `lean` executable (i.e., they
 are in the same directory). If Lean and Lake are not co-located, Lake will
 attempt  to find the their installations separately by calling
-`findLeanInstall?` and `findLakeInstall?`.
+`findLeanInstall?` and `findLakeInstall?`. This behavior can be forced even
+when Lake is co-located by setting `LAKE_OVERRIDE_LEAN` to true.
 
 When co-located, Lake will assume that Lean and Lake's binaries are located in
 `<sysroot>/bin`, their Lean libraries  in `<sysroot>/lib/lean`, Lean's source files
@@ -305,9 +312,9 @@ following the pattern of a regular Lean toolchain.
 -/
 def findInstall? : BaseIO (Option ElanInstall × Option LeanInstall × Option LakeInstall) := do
   let elan? ← findElanInstall?
-  if let some home ← findLakeLeanJointHome? then
-    let lean ← LeanInstall.get home (collocated := true)
-    let lake := LakeInstall.ofLean lean
-    return (elan?, lean, lake)
-  else
-    return (elan?, ← findLeanInstall?, ← findLakeInstall?)
+  unless (← IO.getEnv "LAKE_OVERRIDE_LEAN").bind envToBool? |>.getD false do
+    if let some home ← findLakeLeanJointHome? then
+      let lean ← LeanInstall.get home (collocated := true)
+      let lake := LakeInstall.ofLean lean
+      return (elan?, lean, lake)
+  return (elan?, ← findLeanInstall?, ← findLakeInstall?)