refactor: intro Lake.Env & add it to Workspace

also `LakeConfig` -> `LoadConfig`
2022-07-11 23:06:19 -04:00 · 2022-07-11 23:06:19 -04:00 · 68b81ca065
commit 68b81ca065
parent 2e38df619c
11 changed files with 270 additions and 211 deletions
--- a/Lake/Build/Monad.lean
+++ b/Lake/Build/Monad.lean
@ -12,21 +12,17 @@ namespace Lake

 deriving instance Inhabited for BuildContext

-def mkBuildContext (ws : Workspace) (lean : LeanInstall) (lake : LakeInstall) : IO BuildContext := do
+def mkBuildContext (ws : Workspace) : IO BuildContext := do
+  let lean := ws.env.lean
  let leanTrace :=
    if lean.githash.isEmpty then
      mixTrace (← computeTrace lean.lean) (← computeTrace lean.sharedLib)
    else
      Hash.ofString lean.githash
-  return {opaqueWs := ws, lean, lake, leanTrace}
-
-instance [Monad m] : MonadLake (BuildT m) where
-  getLeanInstall := (·.lean) <$> read
-  getLakeInstall := (·.lake) <$> read
-  getWorkspace := (·.workspace) <$> read
+  return {opaqueWs := ws, leanTrace}

@[inline] def getLeanTrace : BuildM BuildTrace :=
-  (·.leanTrace) <$> read
+  (·.leanTrace) <$> readThe BuildContext

 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
 | Except.ok a => pure a
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Config.Load
-import Lake.Config.SearchPath
-import Lake.Config.InstallPath
 import Lake.Config.Manifest
 import Lake.Config.Resolve
 import Lake.Util.Error
@ -21,23 +19,16 @@ open Lean (Json toJson fromJson?)

 namespace Lake

-- # Loading Lake Config
+-- # Loading a Workspace

-structure LakeConfig where
+structure LoadConfig where
+  env : Lake.Env
  rootDir : FilePath
  configFile : FilePath
-  leanInstall : LeanInstall
-  lakeInstall : LakeInstall
  options : NameMap String

-/-- Make a Lake `Context` from a `Workspace` and `LakeConfig`. -/
-def mkLakeContext (ws : Workspace) (config : LakeConfig) : Context where
-  lean := config.leanInstall
-  lake := config.lakeInstall
-  opaqueWs := ws
-
-def loadPkg (config : LakeConfig) : LogIO Package := do
-  setupLeanSearchPath config.leanInstall config.lakeInstall
+def loadPkg (config : LoadConfig) : LogIO Package := do
+  Lean.searchPathRef.set config.env.leanSearchPath
  Package.load config.rootDir config.options config.configFile

 def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do
@ -56,14 +47,14 @@ def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry
  else
    return {}

-def loadWorkspace (config : LakeConfig) (updateDeps := false) : LogIO Workspace := do
-  let pkg ← loadPkg config
-  let ws := Workspace.ofPackage pkg
+def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do
+  let root ← loadPkg config
+  let ws : Workspace := {root, env := config.env}
  let manifestMap ← loadManifestMap ws.manifestFile
-  let (packageMap, resolvedMap) ← resolveDeps ws pkg updateDeps |>.run manifestMap
+  let (packageMap, resolvedMap) ← resolveDeps ws root updateDeps |>.run manifestMap
  unless resolvedMap.isEmpty do
    IO.FS.writeFile ws.manifestFile <| Json.pretty <| toJson <| Manifest.fromMap resolvedMap
-  let packageMap := packageMap.insert pkg.name pkg
+  let packageMap := packageMap.insert root.name root
  return {ws with packageMap}

 -- # CLI
@ -95,16 +86,21 @@ def LakeOptions.getLakeInstall (opts : LakeOptions) : Except CliError LakeInstal
 def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall × LakeInstall) := do
  return (← opts.getLeanInstall, ← opts.getLakeInstall)

-/-- Make a `LakeConfig` from a `LakeOptions`. -/
-def mkLakeConfig (opts : LakeOptions) : Except CliError LakeConfig :=
+/-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
+def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
+  Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall)
+
+/-- Make a `LoadConfig` from a `LakeOptions`. -/
+def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
  return {
    rootDir := opts.rootDir,
    configFile := opts.rootDir / opts.configFile,
-    leanInstall := ← opts.getLeanInstall,
-    lakeInstall := ← opts.getLakeInstall,
+    env := ← opts.computeEnv
    options := opts.configOptions
  }

+export LakeOptions (mkLoadConfig)
+
 -- ## Monad

 abbrev CliMainM := ExceptT CliError MainM
@ -209,14 +205,14 @@ If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).

 The `print-paths` command is used internally by Lean 4 server.
 -/
-def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit := do
+def printPaths (config : LoadConfig) (imports : List String := []) : MainM PUnit := do
  let configFile := config.rootDir / config.configFile
  if (← configFile.pathExists) then
    if (← IO.getEnv invalidConfigEnvVar) matches some .. then
      IO.eprintln s!"Error parsing '{configFile}'.  Please restart the lean server after fixing the Lake configuration file."
      exit 1
    let ws ← loadWorkspace config
-    let ctx ← mkBuildContext ws config.leanInstall config.lakeInstall
+    let ctx ← mkBuildContext ws
    let dynlibs ← ws.root.buildImportsAndDeps imports |>.run MonadLog.eio ctx
    IO.println <| Json.compress <| toJson {ws.leanPaths with loadDynlibPaths := dynlibs}
  else
@ -225,18 +221,17 @@ def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
  IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait)

-def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do
+def serve (config : LoadConfig) (args : Array String) : LogIO UInt32 := do
  let (extraEnv, moreServerArgs) ←
    try
      let ws ← loadWorkspace config
-      let ctx := mkLakeContext ws config
+      let ctx := mkLakeContext ws
      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 (installEnv.push (invalidConfigEnvVar, "1"), #[])
+      pure (config.env.installVars.push (invalidConfigEnvVar, "1"), #[])
  (← IO.Process.spawn {
-    cmd := config.leanInstall.lean.toString
+    cmd := config.env.lean.lean.toString
    args := #["--server"] ++ moreServerArgs ++ args
    env := extraEnv
  }).wait
@ -244,7 +239,7 @@ def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do
 def exe (name : Name) (args  : Array String := #[]) : LakeT IO UInt32 := do
  let ws ← getWorkspace
  if let some exe := ws.findLeanExe? name then
-    let ctx ← mkBuildContext ws (← getLeanInstall) (← getLakeInstall)
+    let ctx ← mkBuildContext ws
    let exeFile ← (exe.build >>= (·.build)).run MonadLog.eio ctx
    env exeFile.toString args
  else
@ -274,7 +269,7 @@ namespace script

 protected def list : CliM PUnit := do
  processOptions lakeOption
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  noArgsRem do
    let ws ← loadWorkspace config
    ws.packageMap.forM fun _ pkg => do
@ -286,13 +281,11 @@ protected def list : CliM PUnit := do
 protected nonrec def run : CliM PUnit := do
  processOptions lakeOption
  let spec ← takeArg "script name"; let args ← takeArgs
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  let ws ← loadWorkspace config
  let (pkg, scriptName) ← parseScriptSpec ws spec
  if let some script := pkg.scripts.find? scriptName then
    exit <| ← script.run args |>.run {
-      lean := config.leanInstall,
-      lake := config.lakeInstall,
      opaqueWs := ws
    }
  else do
@ -301,7 +294,7 @@ protected nonrec def run : CliM PUnit := do
 protected def doc : CliM PUnit := do
  processOptions lakeOption
  let spec ← takeArg "script name"
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  noArgsRem do
    let ws ← loadWorkspace config
    let (pkg, scriptName) ← parseScriptSpec ws spec
@ -341,7 +334,7 @@ protected def init : CliM PUnit := do
 protected def build : CliM PUnit := do
  processOptions lakeOption
  let opts ← getThe LakeOptions
-  let config ← mkLakeConfig opts
+  let config ← mkLoadConfig opts
  let ws ← loadWorkspace config
  let targetSpecs ← takeArgs
  let target ← show Except _ _ from do
@ -350,22 +343,22 @@ protected def build : CliM PUnit := do
      resolveDefaultPackageTarget ws ws.root
    else
      return Target.collectOpaqueList targets
-  let ctx ← mkBuildContext ws config.leanInstall config.lakeInstall
+  let ctx ← mkBuildContext ws
  BuildM.run MonadLog.io ctx target.build

 protected def update : CliM PUnit := do
  processOptions lakeOption
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  noArgsRem <| discard <| loadWorkspace config (updateDeps := true)

 protected def printPaths : CliM PUnit := do
  processOptions lakeOption
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  printPaths config (← takeArgs)

 protected def clean : CliM PUnit := do
  processOptions lakeOption
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  noArgsRem (← loadPkg config).clean

 protected def script : CliM PUnit := do
@ -382,21 +375,21 @@ protected def serve : CliM PUnit := do
  processOptions lakeOption
  let opts ← getThe LakeOptions
  let args := opts.subArgs.toArray
-  let config ← mkLakeConfig opts
+  let config ← mkLoadConfig opts
  noArgsRem do exit <| ← serve config args

 protected def env : CliM PUnit := do
  let cmd ← takeArg "command"; let args ← takeArgs
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  let ws ← loadWorkspace config
-  let ctx := mkLakeContext ws config
+  let ctx := mkLakeContext ws
  exit <| ← (env cmd args.toArray).run ctx

 protected def exe : CliM PUnit := do
  let exeName ← takeArg "executable name"; let args ← takeArgs
-  let config ← mkLakeConfig (← getThe LakeOptions)
+  let config ← mkLoadConfig (← getThe LakeOptions)
  let ws ← loadWorkspace config
-  let ctx := mkLakeContext ws config
+  let ctx := mkLakeContext ws
  exit <| ← (exe exeName args.toArray).run ctx

 protected def selfCheck : CliM PUnit := do
--- a/Lake/Config.lean
+++ b/Lake/Config.lean
@ -3,11 +3,4 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lake.Config.Glob
-import Lake.Config.InstallPath
-import Lake.Config.Workspace
-import Lake.Config.Script
-import Lake.Config.Package
-import Lake.Config.Module
 import Lake.Config.Monad
-import Lake.Config.SearchPath
--- a/Lake/Config/Context.lean
+++ b/Lake/Config/Context.lean
@ -11,8 +11,6 @@ namespace Lake

 /-- A Lake configuration. -/
 structure Context where
-  lean : LeanInstall
-  lake : LakeInstall
  opaqueWs : OpaqueWorkspace

 /-- A transformer to equip a monad with a `Lake.Context`. -/
--- a/Lake/Config/Env.lean
+++ b/Lake/Config/Env.lean
@ -0,0 +1,78 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Util.NativeLib
+import Lake.Config.InstallPath
+
+open System
+
+namespace Lake
+
+/-- The detected Lake environment. -/
+structure Env where
+  lake : LakeInstall
+  lean : LeanInstall
+  leanPath : SearchPath
+  leanSrcPath : SearchPath
+  sharedLibPath : SearchPath
+  deriving Inhabited, Repr
+
+/-- Gets a `SearchPath` from an environment variable. -/
+def getSearchPath (envVar : String) : BaseIO SearchPath := do
+  match (← IO.getEnv envVar) with
+  | some path => pure <| SearchPath.parse path
+  | none => pure []
+
+namespace Env
+
+/-- Compute an `Lake.Env` object from the given installs and set environment variables. -/
+def compute (lake : LakeInstall) (lean : LeanInstall) : BaseIO Env :=
+  return {
+    lake, lean
+    leanPath := ← getSearchPath "LEAN_PATH",
+    leanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
+    sharedLibPath := ← getSearchPath sharedLibPathEnvVar
+  }
+
+/-- Environment variable settings based only on the given Lean and Lake installations. -/
+def installVars (env : Env) : Array (String × Option String)  :=
+  #[
+    ("LAKE", env.lake.lake.toString),
+    ("LAKE_HOME", env.lake.home.toString),
+    ("LEAN_SYSROOT", env.lean.sysroot.toString),
+    ("LEAN_AR", env.lean.ar.toString),
+    ("LEAN_CC", env.lean.leanCc?)
+  ]
+
+/-- Environment variable settings for the `Lake.Env`. -/
+def vars (env : Env) : Array (String × Option String)  :=
+  env.installVars ++ #[
+    ("LEAN_PATH", some env.leanPath.toString),
+    ("LEAN_SRC_PATH", some env.leanSrcPath.toString),
+    (sharedLibPathEnvVar, some env.sharedLibPath.toString)
+  ]
+
+/--
+The default search path the Lake executable
+uses when interpreting package configuration files.
+
+In order to use the Lean stdlib (e.g., `Init`),
+the executable needs the search path to include the directory
+with the stdlib's `.olean` files (e.g., from `<lean-sysroot>/lib/lean`).
+In order to use Lake's modules as well, the search path also
+needs to include Lake's `.olean` files (e.g., from `build`).
+
+While this can be done by having the user augment `LEAN_PATH` with
+the necessary directories, Lake also intelligently augments the initial
+search path with the `.olean` directories of the provided Lean and Lake
+installations.
+
+See `findInstall?` for more information on how Lake determines those
+directories. If everything is configured as expected, the user will not
+need to augment `LEAN_PATH`. Otherwise, they will need to provide Lake
+with more information (either through `LEAN_PATH` or through other options).
+-/
+def leanSearchPath (env : Lake.Env) : SearchPath :=
+  env.lake.libDir :: env.lean.leanLibDir :: env.leanPath
--- a/Lake/Config/InstallPath.lean
+++ b/Lake/Config/InstallPath.lean
@ -38,9 +38,9 @@ structure LeanInstall where
  sysroot : FilePath
  githash : String
  srcDir := sysroot / "src" / "lean"
-  oleanDir := sysroot / "lib" / "lean"
+  leanLibDir := sysroot / "lib" / "lean"
  includeDir := sysroot / "include"
-  libDir := sysroot / "lib"
+  systemLibDir := sysroot / "lib"
  lean := leanExe sysroot
  leanc := leancExe sysroot
  sharedLib := leanSharedLib sysroot
@ -61,20 +61,10 @@ def lakeExe (buildHome : FilePath) :=
 structure LakeInstall where
  home : FilePath
  srcDir := home
-  oleanDir := home / "build" / "lib"
+  libDir := home / "build" / "lib"
  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.
@ -95,9 +85,10 @@ def findLeanSysroot? (lean := "lean") : BaseIO (Option FilePath) := do
 /--
 Construct the `LeanInstall` object for the given Lean sysroot.

-Does two things:
+Does the following:
 1. Invokes `lean` to find out its `githash`.
 2. Finds the  `ar` and `cc` to use with Lean.
+3. Computes the sub-paths of the Lean install.

 For (1), if the invocation fails, `githash` is set to the empty string.

@ -106,10 +97,17 @@ Otherwise, if Lean is packaged with an `llvm-ar` and/or `clang`, use them.
 If not, use the `ar` and/or `cc` in the system's `PATH`. This last step is
 needed because internal builds of Lean do not bundle these tools
 (unlike user-facing releases).
+
 We also track whether `LEAN_CC` was set to determine whether it should
 be set in the future for `lake env`. This is because if `LEAN_CC` was not set,
-it needs to remain not set for `leanc` to work (even setting it to the bundled
-compiler will break it -- see https://github.com/leanprover/lean4/issues/1281).
+it needs to remain not set for `leanc` to work.
+Even setting it to the bundled compiler will break `leanc` -- see
+[leanprover/lean4#1281](https://github.com/leanprover/lean4/issues/1281).
+
+For (3), it assumes that the Lean installation is organized the normal way.
+That is, with its binaries located in `<lean-sysroot>/bin`, its
+Lean libraries in `<lean-sysroot>/lib/lean`, and its system libraries in
+`<lean-sysroot>/lib`.
 -/
 def LeanInstall.get (sysroot : FilePath) : BaseIO LeanInstall := do
  let (cc, customCc) ← findCc
@ -144,11 +142,8 @@ where

 /--
 Try to find the installation of the given `lean` command
-by calling `findLeanCmdHome?`.
-
-It assumes that the Lean installation is setup the normal way.
-That is, with its binaries located in `<lean-home>/bin` and its
-libraries and `.olean` files located in `<lean-home>/lib/lean`.
+by calling `findLeanCmdHome?`. See `LeanInstall.get` for how it assumes the
+Lean install is organized.
 -/
 def findLeanCmdInstall? (lean := "lean") : BaseIO (Option LeanInstall) :=
  OptionT.run do LeanInstall.get (← findLeanSysroot? lean)
@ -173,13 +168,9 @@ def lakePackageHome? (lake : FilePath) : Option FilePath := do
  (← (← lake.parent).parent).parent

 /--
-Try to find Lean's installation by
-first checking the `LEAN_SYSROOT` environment variable
-and then by trying `findLeanCmdHome?`.
-
-It assumes that the Lean installation is setup the normal way.
-That is, with its binaries located in `<lean-home>/bin` and its
-libraries and `.olean` files located in `<lean-home>/lib/lean`.
+Try to find Lean's installation by first checking the
+`LEAN_SYSROOT` environment variable and then by trying `findLeanCmdHome?`.
+See `LeanInstall.get` for how it assumes the Lean install is organized.
 -/
 def findLeanInstall? : BaseIO (Option LeanInstall) := do
  if let some sysroot ← IO.getEnv "LEAN_SYSROOT" then
@ -193,7 +184,7 @@ Try to find Lake's installation by
 first checking the `LAKE_HOME` environment variable
 and then by trying the `lakePackageHome?` of the running executable.

-It assumes that the Lake installation is setup the same way it is built.
+It assumes that the Lake installation is organized the same way it is built.
 That is, with its binary located at `<lake-home>/build/bin/lake` and its static
 library and `.olean` files in `<lake-home>/build/lib`, and its source files
 located directly in `<lake-home>`.
@ -227,8 +218,8 @@ def findInstall? : BaseIO (Option LeanInstall × Option LakeInstall) := do
      some {
        home,
        srcDir := lean.srcDir / "lake",
-        oleanDir := lean.oleanDir,
-        lake := lakeExe lean.sysroot
+        libDir := lean.leanLibDir,
+        lake := lakeExe home
      }
    )
  else
--- a/Lake/Config/Monad.lean
+++ b/Lake/Config/Monad.lean
@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 import Lake.Config.Context
-import Lake.Config.InstallPath
 import Lake.Config.Workspace

 open System
@ -12,41 +11,38 @@ open Lean (Name)

 namespace Lake

+abbrev MonadLakeEnv (m : Type → Type u) :=
+  MonadReaderOf Lake.Env m
+
+abbrev MonadWorkspace (m : Type → Type u) :=
+  MonadReaderOf Workspace m
+
+abbrev MonadLake (m : Type → Type u) :=
+  MonadReaderOf Context m
+
 deriving instance Inhabited for Context

-class MonadLake (m : Type → Type u) where
-  getLeanInstall : m LeanInstall
-  getLakeInstall : m LakeInstall
-  getWorkspace : m Workspace
-
-export MonadLake (getLeanInstall getLakeInstall getWorkspace)
-
-instance [MonadLift m n] [MonadLake m] : MonadLake n where
-  getLeanInstall := liftM (m := m) <| getLeanInstall
-  getLakeInstall := liftM (m := m) <| getLakeInstall
-  getWorkspace := liftM (m := m) <| getWorkspace
+/-- Make a `Lake.Context` from a `Workspace`. -/
+def mkLakeContext (ws : Workspace) : Context where
+  opaqueWs := ws

@[inline] def Context.workspace (self : Context) :=
  self.opaqueWs.get

-instance [Monad m] : MonadLake (LakeT m) where
-  getLeanInstall := (·.lean) <$> read
-  getLakeInstall := (·.lake) <$> read
-  getWorkspace := (·.workspace) <$> read
-
-instance [MonadLake m] [Monad m] [MonadLiftT n m] : MonadLiftT (LakeT n) m where
-  monadLift x := do
-    liftM <| x {
-      lean := ← getLeanInstall
-      lake := ← getLakeInstall
-      opaqueWs := ← getWorkspace
-    }
+instance [MonadLake m] [Functor m] : MonadWorkspace m where
+  read := (·.workspace) <$> read

 section
-variable [MonadLake m] [Functor m]
+variable [MonadWorkspace m] [Functor m]
+
+instance : MonadLakeEnv m where
+  read := (·.env) <$> read

 /- ## Workspace Helpers -/

+@[inline] def getWorkspace : m Workspace :=
+  read
+
@[inline] def findPackage? (name : Name) : m (Option Package) :=
  (·.findPackage? name) <$> getWorkspace

@ -62,16 +58,48 @@ variable [MonadLake m] [Functor m]
@[inline] def findExternLib? (mod : Name) : m (Option ExternLib) :=
  (·.findExternLib? mod) <$> getWorkspace

+/-- Get the `leanPath` of the `Workspace`. -/
@[inline] def getLeanPath : m SearchPath :=
-  (·.oleanPath) <$> getWorkspace
+  (·.leanPath) <$> getWorkspace

+/-- Get the `leanSrcPath` of the `Workspace`. -/
@[inline] def getLeanSrcPath : m SearchPath :=
  (·.leanSrcPath) <$> getWorkspace

+/-- Get the `libPath` value of the `Workspace`. -/
@[inline] def getLibPath : m SearchPath :=
  (·.libPath) <$> getWorkspace

-/- ## Lean Install Helpers -/
+/-- Get the `augmentedLeanPath` of the `Workspace`. -/
+@[inline] def getAugmentedLeanPath : m SearchPath :=
+  (·.augmentedLeanPath) <$> getWorkspace
+
+/-- Get the `augmentedLeanSrcPath` value of the `Workspace`. -/
+@[inline] def getAugmentedLeanSrcPath  : m SearchPath :=
+  (·.augmentedLeanSrcPath) <$> getWorkspace
+
+/-- Get the `augmentedSharedLibPath` value of the `Workspace`. -/
+@[inline] def getAugmentedSharedLibPath  : m SearchPath :=
+  (·.augmentedSharedLibPath) <$> getWorkspace
+
+/-- Get the `augmentedEnvVars` of the `Workspace`. -/
+@[inline]  def getAugmentedEnv : m (Array (String × Option String)) :=
+  (·.augmentedEnvVars) <$> getWorkspace
+
+end
+
+section
+variable [MonadLakeEnv m] [Functor m]
+
+/- ## Environment Helpers -/
+
+@[inline] def getLakeEnv : m Lake.Env :=
+  read
+
+/- ### Lean Install Helpers -/
+
+@[inline] def getLeanInstall : m LeanInstall :=
+  (·.lean) <$> getLakeEnv

@[inline] def getLeanSysroot : m FilePath :=
  (·.sysroot) <$> getLeanInstall
@ -79,14 +107,15 @@ variable [MonadLake m] [Functor m]
@[inline] def getLeanSrcDir : m FilePath :=
  (·.srcDir) <$> getLeanInstall

-@[inline] def getLeanOleanDir : m FilePath :=
-  (·.oleanDir) <$> getLeanInstall
+/-- Get the `leanLibDir` of the detected `LeanInstall`. -/
+@[inline] def getLeanLibDir : m FilePath :=
+  (·.leanLibDir) <$> getLeanInstall

@[inline] def getLeanIncludeDir : m FilePath :=
  (·.includeDir) <$> getLeanInstall

-@[inline] def getLeanLibDir : m FilePath :=
-  (·.libDir) <$> getLeanInstall
+@[inline] def getLeanSystemLibDir : m FilePath :=
+  (·.systemLibDir) <$> getLeanInstall

@[inline] def getLean : m FilePath :=
  (·.lean) <$> getLeanInstall
@ -106,7 +135,10 @@ variable [MonadLake m] [Functor m]
@[inline] def getLeanCc? : m (Option String) :=
  (·.leanCc?) <$> getLeanInstall

-/- ## Lake Install Helpers -/
+/- ### Lake Install Helpers -/
+
+@[inline] def getLakeInstall : m LakeInstall :=
+  (·.lake) <$> getLakeEnv

@[inline] def getLakeHome : m FilePath :=
  (·.home) <$> getLakeInstall
@ -114,41 +146,24 @@ variable [MonadLake m] [Functor m]
@[inline] def getLakeSrcDir : m FilePath :=
  (·.srcDir) <$> getLakeInstall

-@[inline] def getLakeOleanDir : m FilePath :=
-  (·.oleanDir) <$> getLakeInstall
+@[inline] def getLakeLibDir : m FilePath :=
+  (·.libDir) <$> getLakeInstall

@[inline] def getLake : m FilePath :=
  (·.lake) <$> getLakeInstall

+/- ### Search Path Helpers -/
+
+/-- Get the detected `LEAN_PATH` value of the Lake environment. -/
+@[inline] def getEnvLeanPath : m SearchPath :=
+  (·.leanPath) <$> getLakeEnv
+
+/-- Get the detected `LEAN_SRC_PATH` value of the Lake environment. -/
+@[inline] def getEnvLeanSrcPath : m SearchPath :=
+  (·.leanSrcPath) <$> getLakeEnv
+
+/-- Get the detected `sharedLibPathEnvVar` value of the Lake environment. -/
+@[inline] def getEnvSharedLibPath : m SearchPath :=
+  (·.sharedLibPath) <$> getLakeEnv
+
 end
-
-/--
-Get `LEAN_PATH` augmented with the workspace's `leanPath` and Lake's `oleanDir`.
-
-Including Lake's `oleanDir` at the end ensures that same Lake package being
-used to build is available to the environment (and thus, e.g., the Lean server).
-Otherwise, it may fall back on whatever the default Lake instance is.
-/
-@[inline] def getAugmentedLeanPath : LakeT BaseIO SearchPath := do
-  return (← getSearchPath "LEAN_PATH") ++ (← getLeanPath) ++ [← getLakeOleanDir]
-
-/--
-Get `LEAN_SRC_PATH` augmented with the workspace's `leanSrcPath` and Lake's `srcDir`.
-
-Including Lake's `srcDir` at the end ensures that same Lake package being
-used to build is available to the environment (and thus, e.g., the Lean server).
-Otherwise, it may fall back on whatever the default Lake instance is.
-/
-@[inline] def getAugmentedLeanSrcPath : LakeT BaseIO SearchPath := do
-  return (← getSearchPath "LEAN_SRC_PATH") ++ (← getLeanSrcPath) ++ [← getLakeSrcDir]
-
-/- Get `sharedLibPathEnv` augmented with the workspace's `libPath`. -/
-@[inline] def getAugmentedLibPath : LakeT BaseIO SearchPath := do
-  return (← getSearchPath sharedLibPathEnvVar) ++ (← getLibPath)
-
-def getAugmentedEnv : LakeT BaseIO (Array (String × Option String)) :=
-  return mkInstallEnv (← getLeanInstall) (← getLakeInstall) ++ #[
-    ("LEAN_PATH", some (← getAugmentedLeanPath).toString),
-    ("LEAN_SRC_PATH", some (← getAugmentedLeanSrcPath).toString),
-    (sharedLibPathEnvVar, some (← getAugmentedLibPath).toString)
-  ]
--- a/Lake/Config/SearchPath.lean
+++ b/Lake/Config/SearchPath.lean
@ -1,41 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
-/
-import Lean.Util.Path
-import Lake.Config.InstallPath
-
-open System
-namespace Lake
-
-/--
-Initializes the search path the Lake executable
-uses when interpreting package configuration files.
-
-In order to use the Lean stdlib (e.g., `Init`),
-the executable needs the search path to include the directory
-with the stdlib's `.olean` files (e.g., from `<lean-sysroot>/lib/lean`).
-In order to use Lake's modules as well, the search path also
-needs to include Lake's `.olean` files (e.g., from `build`).
-
-While this can be done by having the user augment `LEAN_PATH` with
-the necessary directories, Lake also intelligently augments the initial
-search path with the `.olean` directories of the provided Lean and Lake
-installations.
-
-See `findInstall?` for more information on how Lake determines those
-directories. If everything is configured as expected, the user will not
-need to augment `LEAN_PATH`. Otherwise, they will need to provide Lake
-with more information (either through `LEAN_PATH` or through other options).
-/
-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
-  Lean.searchPathRef.set sp
--- a/Lake/Config/Workspace.lean
+++ b/Lake/Config/Workspace.lean
@ -6,6 +6,7 @@ Authors: Mac Malone
 import Lean.Util.Paths
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
+import Lake.Config.Env

 open System
 open Lean (LeanPaths)
@ -19,6 +20,8 @@ def manifestFileName := "manifest.json"
 structure Workspace where
  /-- The root package of the workspace. -/
  root : Package
+  /-- The detect `Lake.Env` of the workspace. -/
+  env : Lake.Env
  /-- Name-package map of packages within the workspace. -/
  packageMap : NameMap Package := {}
  deriving Inhabited
@ -27,10 +30,6 @@ hydrate_opaque_type OpaqueWorkspace Workspace

 namespace Workspace

-/-- Create a `Workspace` from a package using its directory and `WorkspaceConfig`. -/
-def ofPackage (pkg : Package) : Workspace :=
-  {root := pkg}
-
 /-- The path to the workspace's directory (i.e., the directory of the root package). -/
 def dir (self : Workspace) : FilePath :=
  self.root.dir
@ -100,7 +99,7 @@ def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × Targ
  self.packageArray.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)

 /-- The `LEAN_PATH` of the workspace. -/
-def oleanPath (self : Workspace) : SearchPath :=
+def leanPath (self : Workspace) : SearchPath :=
  self.packageList.map (·.oleanDir)

 /-- The `LEAN_SRC_PATH` of the workspace. -/
@ -118,3 +117,43 @@ def libPath (self : Workspace) : SearchPath :=
 def leanPaths (self : Workspace) : LeanPaths where
  oleanPath := self.packageList.map (·.oleanDir)
  srcPath := self.packageList.map (·.srcDir)
+
+/--
+Rhe detected `LEAN_PATH` of the environment
+augmented with the workspace's `leanPath` and Lake's `libDir`.
+
+We include Lake's `oleanDir` at the end to ensure that same Lake package being
+used to build is available to the environment (and thus, e.g., the Lean server).
+Otherwise, it may fall back on whatever the default Lake instance is.
+-/
+def augmentedLeanPath (self : Workspace) : SearchPath :=
+  self.env.leanPath ++ self.leanPath ++ [self.env.lake.libDir]
+
+/--
+The detected `LEAN_SRC_PATH` of the environment
+augmented with the workspace's `leanSrcPath` and Lake's `srcDir`.
+
+We include Lake's `srcDir` at the end to ensure that same Lake package being
+used to build is available to the environment (and thus, e.g., the Lean server).
+Otherwise, it may fall back on whatever the default Lake instance is.
+-/
+def augmentedLeanSrcPath (self : Workspace) : SearchPath :=
+  self.env.leanSrcPath ++ self.leanSrcPath ++ [self.env.lake.srcDir]
+
+/-
+The detected `sharedLibPathEnv` value of the environment
+augmented with the workspace's `libPath`.
+-/
+def augmentedSharedLibPath (self : Workspace) : SearchPath :=
+  self.env.sharedLibPath ++ self.libPath
+
+/--
+The detected environment augmented with the Workspace's paths.
+These are the settings use by `lake env` / `Lake.env` to run executables.
+-/
+def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
+  self.env.installVars ++ #[
+    ("LEAN_PATH", some self.augmentedLeanPath.toString),
+    ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
+    (sharedLibPathEnvVar, some self.augmentedSharedLibPath.toString)
+  ]
--- a/Lake/Util/Lift.lean
+++ b/Lake/Util/Lift.lean
@ -30,3 +30,6 @@ instance [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m w

 instance [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where
  monadLift act := act.run >>= liftM
+
+instance [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where
+  monadLift act := act.toBaseIO >>= liftM
--- a/Lake/Util/NativeLib.lean
+++ b/Lake/Util/NativeLib.lean
@ -34,9 +34,3 @@ def sharedLibPathEnvVar :=
    "DYLD_LIBRARY_PATH"
  else
    "LD_LIBRARY_PATH"
-
-/-- Gets a `SearchPath` from an environment variable. -/
-def getSearchPath (envVar : String) : BaseIO SearchPath := do
-  match (← IO.getEnv envVar) with
-  | some path => pure <| SearchPath.parse path
-  | none => pure []