diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index dec54acdca..aa437c7cf7 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -215,7 +215,6 @@ def baseVars (env : Env) : Array (String × Option String) := ("LAKE_ARTIFACT_CACHE", toString env.enableArtifactCache), ("LAKE_CACHE_DIR", if env.lakeCache.isDisabled then none else env.lakeCache.dir.toString), ("LEAN", env.lean.lean.toString), - ("LEAN_GITHASH", env.leanGithash), ("LEAN_SYSROOT", env.lean.sysroot.toString), ("LEAN_AR", env.lean.ar.toString), ("LEAN_CC", env.lean.leanCc?) @@ -226,6 +225,7 @@ def vars (env : Env) : Array (String × Option String) := let vars := env.baseVars ++ #[ ("LEAN_PATH", some env.leanPath.toString), ("LEAN_SRC_PATH", some env.leanSrcPath.toString), + ("LEAN_GITHASH", env.leanGithash), ("PATH", some env.path.toString) ] if Platform.isWindows then diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index a217b995d9..5cc0146b15 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -41,6 +41,10 @@ hydrate_opaque_type OpaqueWorkspace Workspace namespace Workspace +/-- **For internal use.** Whether this workspace is Lean itself. -/ +@[inline] def bootstrap (ws : Workspace) : Bool := + ws.root.bootstrap + /-- The Lake cache. May be disabled. -/ @[inline] def lakeCache (ws : Workspace) : Cache := ws.lakeEnv.lakeCache @@ -234,13 +238,15 @@ def augmentedSharedLibPath (self : Workspace) : SearchPath := self.lakeEnv.lean.sharedLibPath ++ self.sharedLibPath ++ self.lakeEnv.initSharedLibPath /-- -The detected environment augmented with Lake's and the workspace's paths. +The detected environment augmented with Lake's and the workspace's configuration. These are the settings use by `lake env` / `Lake.env` to run executables. -/ def augmentedEnvVars (self : Workspace) : Array (String × Option String) := let vars := self.lakeEnv.baseVars ++ #[ ("LEAN_PATH", some self.augmentedLeanPath.toString), ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString), + -- Allow the Lean version to change dynamically within core + ("LEAN_GITHASH", if self.bootstrap then none else some self.lakeEnv.leanGithash), ("PATH", some self.augmentedPath.toString) ] if Platform.isWindows then diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..cff0f06afc 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// dear bot, please update stage0 + namespace lean { options get_default_options() { options opts;