From 68b81ca06580f5fad0ade4736d7262f8047c8f5d Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 11 Jul 2022 23:06:19 -0400 Subject: [PATCH] refactor: intro `Lake.Env` & add it to `Workspace` also `LakeConfig` -> `LoadConfig` --- Lake/Build/Monad.lean | 12 +-- Lake/CLI/Main.lean | 85 ++++++++++---------- Lake/Config.lean | 7 -- Lake/Config/Context.lean | 2 - Lake/Config/Env.lean | 78 +++++++++++++++++++ Lake/Config/InstallPath.lean | 53 ++++++------- Lake/Config/Monad.lean | 145 +++++++++++++++++++---------------- Lake/Config/SearchPath.lean | 41 ---------- Lake/Config/Workspace.lean | 49 ++++++++++-- Lake/Util/Lift.lean | 3 + Lake/Util/NativeLib.lean | 6 -- 11 files changed, 270 insertions(+), 211 deletions(-) create mode 100644 Lake/Config/Env.lean delete mode 100644 Lake/Config/SearchPath.lean diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean index 418d31df50..a9e767abcf 100644 --- 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 diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 84f4d97289..9629a7e34c 100644 --- 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 diff --git a/Lake/Config.lean b/Lake/Config.lean index f3555bac00..cc67357d0a 100644 --- 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 diff --git a/Lake/Config/Context.lean b/Lake/Config/Context.lean index 71b56476c6..b3bdb799c2 100644 --- 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`. -/ diff --git a/Lake/Config/Env.lean b/Lake/Config/Env.lean new file mode 100644 index 0000000000..944d9481b5 --- /dev/null +++ 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 `/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 diff --git a/Lake/Config/InstallPath.lean b/Lake/Config/InstallPath.lean index 993221775a..8b7276c5c8 100644 --- 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 `/bin`, its +Lean libraries in `/lib/lean`, and its system libraries in +`/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 `/bin` and its -libraries and `.olean` files located in `/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 `/bin` and its -libraries and `.olean` files located in `/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 `/build/bin/lake` and its static library and `.olean` files in `/build/lib`, and its source files located directly in ``. @@ -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 diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean index 4716d26197..57759d4a14 100644 --- 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) - ] diff --git a/Lake/Config/SearchPath.lean b/Lake/Config/SearchPath.lean deleted file mode 100644 index 348b597b7e..0000000000 --- a/Lake/Config/SearchPath.lean +++ /dev/null @@ -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 `/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 diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index cdad6d8515..45d4290d2d 100644 --- 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) + ] diff --git a/Lake/Util/Lift.lean b/Lake/Util/Lift.lean index c9b45a79c2..d9227013b4 100644 --- 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 diff --git a/Lake/Util/NativeLib.lean b/Lake/Util/NativeLib.lean index 672c333748..a6554d2262 100644 --- 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 []