feat: setup lean/lake env for server even if config has errors

Lake/CLI/Main.lean

@@ -228,8 +228,9 @@ def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do
       let ctx := mkLakeContext ws config
       pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
     catch _ =>
+      let installEnv := mkInstallEnv config.leanInstall config.lakeInstall
       logWarning "package configuration has errors, falling back to plain `lean --server`"
-      pure (#[(invalidConfigEnvVar, "1")], #[])
+      pure (installEnv.push (invalidConfigEnvVar, "1"), #[])
   (← IO.Process.spawn {
     cmd := config.leanInstall.lean.toString
     args := #["--server"] ++ moreServerArgs ++ args

Lake/Config/InstallPath.lean

@@ -49,6 +49,10 @@ structure LeanInstall where
   customCc : Bool
   deriving Inhabited, Repr
 
+/-- The `LEAN_CC` of the Lean installation. -/
+def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
+  if self.customCc then self.cc.toString else none
+
 /-- Standard path of `lake` in a Lake installation. -/
 def lakeExe (buildHome : FilePath) :=
   buildHome / "bin" / "lake" |>.withExtension FilePath.exeExtension
@@ -61,6 +65,16 @@ structure LakeInstall where
   lake := lakeExe <| home / "build"
   deriving Inhabited, Repr
 
+/-- Environment variable settings based on the given Lean and Lake installations. -/
+def mkInstallEnv (lean : LeanInstall) (lake : LakeInstall) : Array (String × Option String)  :=
+  #[
+    ("LAKE", lake.lake.toString),
+    ("LAKE_HOME", lake.home.toString),
+    ("LEAN_SYSROOT", lean.sysroot.toString),
+    ("LEAN_AR", lean.ar.toString),
+    ("LEAN_CC", lean.leanCc?)
+  ]
+
 /--
 Try to find the sysroot of the given `lean` command (if it exists)
 by calling `lean --print-prefix` and returning the path it prints.

Lake/Config/Monad.lean

@@ -104,7 +104,7 @@ variable [MonadLake m] [Functor m]
   (·.cc) <$> getLeanInstall
 
 @[inline] def getLeanCc? : m (Option String) :=
-  (fun lean => if lean.customCc then lean.cc.toString else none) <$> getLeanInstall
+  (·.leanCc?) <$> getLeanInstall
 
 /- ## Lake Install Helpers -/
 
@@ -147,13 +147,8 @@ Otherwise, it may fall back on whatever the default Lake instance is.
   return (← getSearchPath sharedLibPathEnvVar) ++ (← getLibPath)
 
 def getAugmentedEnv : LakeT BaseIO (Array (String × Option String)) :=
-  return #[
-    ("LAKE", (← getLake).toString),
-    ("LAKE_HOME", (← getLakeHome).toString),
-    ("LEAN_SYSROOT", (← getLeanSysroot).toString),
-    ("LEAN_AR", (← getLeanAr).toString),
-    ("LEAN_CC", ← getLeanCc?),
-    ("LEAN_PATH", (← getAugmentedLeanPath).toString),
-    ("LEAN_SRC_PATH", (← getAugmentedLeanSrcPath).toString),
-    (sharedLibPathEnvVar, (← getAugmentedLibPath).toString)
+  return mkInstallEnv (← getLeanInstall) (← getLakeInstall) ++ #[
+    ("LEAN_PATH", some (← getAugmentedLeanPath).toString),
+    ("LEAN_SRC_PATH", some (← getAugmentedLeanSrcPath).toString),
+    (sharedLibPathEnvVar, some (← getAugmentedLibPath).toString)
   ]