feat: lake: use system cache for bootstrap (#10621)
This PR alters the Lake directory detection so that the core build (i.e., `bootstrap = true`) is stored in the user cache directory (if available) and never in a toolchain-specific directory. It is also fixes some issues with cache environment configuration discovered along the way.
This commit is contained in:
Mac Malone
GitHub
parent
5ede2bfcf2
commit
5d8498888b
4 changed files with 65 additions and 26 deletions
|
|
@ -41,19 +41,28 @@ public structure Env where
|
|||
noCache : Bool
|
||||
/-- Whether the Lake artifact cache should be enabled by default (i.e., `LAKE_ARTIFACT_CACHE`). -/
|
||||
enableArtifactCache : Bool
|
||||
/-- Whether the system cache has been disabled (`LAKE_CACHE_DIR` is set but empty). -/
|
||||
noSystemCache : Bool := false
|
||||
/--
|
||||
The system directory for the Lake cache. Set by `LAKE_CACHE_DIR`.
|
||||
The directory for the Lake cache. Customized by `LAKE_CACHE_DIR`.
|
||||
|
||||
If `none`, no suitable system directory for the cache exists.
|
||||
-/
|
||||
lakeCache? : Option Cache
|
||||
lakeCache? : Option Cache := none
|
||||
/--
|
||||
The directory for the Lake cache. Customized by `LAKE_CACHE_DIR`.
|
||||
|
||||
Unlike `lakeCache?`, this excludes the toolchain directory from consideration.
|
||||
|
||||
If `none`, no suitable system directory for the cache exists.
|
||||
-/
|
||||
lakeSystemCache? : Option Cache := none
|
||||
/-- The authentication key for cache uploads (i.e., `LAKE_CACHE_KEY`). -/
|
||||
cacheKey? : Option String
|
||||
/-- The base URL for artifact uploads and downloads from the cache (i.e., `LAKE_CACHE_ARTIFACT_ENDPOINT`). -/
|
||||
cacheArtifactEndpoint? : Option String
|
||||
/-- The base URL for revision uploads and downloads from the cache (i.e., `LAKE_CACHE_REVISION_ENDPOINT`). -/
|
||||
cacheRevisionEndpoint? : Option String
|
||||
/-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/
|
||||
initToolchain : String
|
||||
/-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/
|
||||
initLeanPath : SearchPath
|
||||
/-- The initial Lean source search path of the environment (i.e., `LEAN_SRC_PATH`). -/
|
||||
|
|
@ -65,7 +74,7 @@ public structure Env where
|
|||
/--
|
||||
The preferred toolchain of the environment. May be empty.
|
||||
|
||||
Either `initToolchain` or, if none, Lake's `Lean.toolchain`.
|
||||
Either `ELAN_TOOLCHAIN` or, if none, Lake's `Lean.toolchain`.
|
||||
-/
|
||||
toolchain : String
|
||||
deriving Inhabited
|
||||
|
|
@ -92,26 +101,45 @@ public def getSystemCacheHome? : BaseIO (Option FilePath) := do
|
|||
else
|
||||
return none
|
||||
|
||||
def ElanInstall.lakeToolchainCache (elan : ElanInstall) (toolchain : String) : Cache :=
|
||||
⟨elan.toolchainDir toolchain / "lake" / "cache"⟩
|
||||
|
||||
@[inline] def ElanInstall.lakeToolchainCache? (elan : ElanInstall) (toolchain : String) : Option Cache :=
|
||||
if toolchain.isEmpty then
|
||||
none
|
||||
else
|
||||
some (elan.lakeToolchainCache toolchain)
|
||||
|
||||
namespace Env
|
||||
|
||||
/-- Compute the Lean toolchain string used by Lake from the process environment. -/
|
||||
public def computeToolchain : BaseIO String := do
|
||||
return (← IO.getEnv "ELAN_TOOLCHAIN").getD Lean.toolchain
|
||||
|
||||
def computeEnvCache? : BaseIO (Option Cache) := OptionT.run do
|
||||
let cacheDir ← IO.getEnv "LAKE_CACHE_DIR"
|
||||
guard cacheDir.isEmpty
|
||||
return ⟨cacheDir⟩
|
||||
|
||||
def computeSystemCache? : BaseIO (Option Cache) := do
|
||||
return (← getSystemCacheHome?).map (⟨· / "lake"⟩)
|
||||
|
||||
def computeToolchainCache? (elan? : Option ElanInstall) (toolchain : String) : Option Cache := do
|
||||
let elan ← elan?
|
||||
guard !toolchain.isEmpty
|
||||
return elan.lakeToolchainCache toolchain
|
||||
|
||||
/--
|
||||
Compute the system cache location from the process environment.
|
||||
If `none`, no system directory for workspace the cache exists.
|
||||
-/
|
||||
public def computeCache? (elan? : Option ElanInstall) (toolchain : String) : BaseIO (Option Cache) := do
|
||||
if let some cacheDir ← IO.getEnv "LAKE_CACHE_DIR" then
|
||||
if cacheDir.isEmpty then
|
||||
return none
|
||||
else
|
||||
return some ⟨cacheDir⟩
|
||||
else if let some elan := elan? then
|
||||
return some ⟨elan.toolchainDir toolchain / "lake" / "cache"⟩
|
||||
else if let some cacheHome ← getSystemCacheHome? then
|
||||
return some ⟨cacheHome / "lake"⟩
|
||||
if let some cache ← computeEnvCache? then
|
||||
return some cache
|
||||
else if let some cache := computeToolchainCache? elan? toolchain then
|
||||
return some cache
|
||||
else if let some cache ← computeSystemCache? then
|
||||
return some cache
|
||||
else
|
||||
return none
|
||||
|
||||
|
|
@ -124,28 +152,36 @@ public def compute
|
|||
(noCache : Option Bool := none)
|
||||
: EIO String Env := do
|
||||
let reservoirBaseUrl ← getUrlD "RESERVOIR_API_BASE_URL" "https://reservoir.lean-lang.org/api"
|
||||
let elanToolchain? ← IO.getEnv "ELAN_TOOLCHAIN"
|
||||
let initToolchain := elanToolchain?.getD ""
|
||||
let toolchain := elanToolchain?.getD Lean.toolchain
|
||||
return {
|
||||
let toolchain ← computeToolchain
|
||||
addCacheDirs toolchain {
|
||||
lake, lean, elan?,
|
||||
pkgUrlMap := ← computePkgUrlMap
|
||||
reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
|
||||
noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
|
||||
enableArtifactCache := (← IO.getEnv "LAKE_ARTIFACT_CACHE").bind envToBool? |>.getD false
|
||||
lakeCache? := ← computeCache? elan? toolchain
|
||||
cacheKey? := (← IO.getEnv "LAKE_CACHE_KEY").map (·.trim)
|
||||
cacheArtifactEndpoint? := (← IO.getEnv "LAKE_CACHE_ARTIFACT_ENDPOINT").map normalizeUrl
|
||||
cacheRevisionEndpoint? := (← IO.getEnv "LAKE_CACHE_REVISION_ENDPOINT").map normalizeUrl
|
||||
githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
|
||||
toolchain
|
||||
initToolchain
|
||||
initLeanPath := ← getSearchPath "LEAN_PATH",
|
||||
initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
|
||||
initSharedLibPath := ← getSearchPath sharedLibPathEnvVar,
|
||||
initPath := ← getSearchPath "PATH"
|
||||
}
|
||||
where
|
||||
addCacheDirs toolchain env := do
|
||||
if let some dir ← IO.getEnv "LAKE_CACHE_DIR" then
|
||||
if dir.isEmpty then
|
||||
return {env with noSystemCache := true}
|
||||
else
|
||||
return {env with lakeCache? := some ⟨dir⟩, lakeSystemCache? := some ⟨dir⟩}
|
||||
else if let some cache := computeToolchainCache? elan? toolchain then
|
||||
return {env with lakeCache? := some cache, lakeSystemCache? := ← computeSystemCache?}
|
||||
else if let some cache ← computeSystemCache? then
|
||||
return {env with lakeCache? := some cache, lakeSystemCache? := some cache}
|
||||
else
|
||||
return env
|
||||
computePkgUrlMap := do
|
||||
let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
|
||||
match Json.parse urlMapStr |>.bind fromJson? with
|
||||
|
|
@ -210,10 +246,11 @@ public def sharedLibPath (env : Env) : SearchPath :=
|
|||
env.lean.sharedLibPath ++ env.initSharedLibPath
|
||||
|
||||
/-- Unset toolchain-specific environment variables. -/
|
||||
public def noToolchainVars : Array (String × Option String) :=
|
||||
public def noToolchainVars (env : Env) : Array (String × Option String) :=
|
||||
#[
|
||||
("ELAN_TOOLCHAIN", none),
|
||||
("LAKE", none),
|
||||
("LAKE_CACHE_DIR", if env.noSystemCache then some "" else env.lakeSystemCache?.map (·.dir.toString)),
|
||||
("LAKE_OVERRIDE_LEAN", none),
|
||||
("LAKE_HOME", none),
|
||||
("LEAN", none),
|
||||
|
|
|
|||
|
|
@ -25,6 +25,10 @@ public structure Workspace : Type where
|
|||
root : Package
|
||||
/-- The detected `Lake.Env` of the workspace. -/
|
||||
lakeEnv : Lake.Env
|
||||
/-- The Lake cache. -/
|
||||
lakeCache : Cache :=
|
||||
if root.bootstrap then lakeEnv.lakeSystemCache?.getD ⟨root.lakeDir / "cache"⟩
|
||||
else lakeEnv.lakeCache?.getD ⟨root.lakeDir / "cache"⟩
|
||||
/--
|
||||
The CLI arguments Lake was run with.
|
||||
Used by `lake update` to perform a restart of Lake on a toolchain update.
|
||||
|
|
@ -69,10 +73,6 @@ namespace Workspace
|
|||
@[inline] public def lakeDir (self : Workspace) : FilePath :=
|
||||
self.root.lakeDir
|
||||
|
||||
/-- The Lake cache. -/
|
||||
@[inline] public def lakeCache (ws : Workspace) : Cache :=
|
||||
ws.lakeEnv.lakeCache?.getD ⟨ws.lakeDir⟩
|
||||
|
||||
/-- Whether the Lake artifact cache should be enabled by default for packages in the workspace. -/
|
||||
@[inline] public def enableArtifactCache (ws : Workspace) : Bool :=
|
||||
ws.lakeEnv.enableArtifactCache
|
||||
|
|
|
|||
|
|
@ -256,7 +256,7 @@ def Workspace.updateToolchain
|
|||
let child ← IO.Process.spawn {
|
||||
cmd := elanInstall.elan.toString
|
||||
args := #["run", "--install", tc.toString, "lake"] ++ lakeArgs
|
||||
env := Env.noToolchainVars
|
||||
env := ws.lakeEnv.noToolchainVars
|
||||
}
|
||||
IO.Process.exit (← child.wait).toUInt8
|
||||
else
|
||||
|
|
|
|||
2
src/lake/tests/env/test.sh
vendored
2
src/lake/tests/env/test.sh
vendored
|
|
@ -36,6 +36,8 @@ LAKE_CACHE_DIR= test_run env -d ../../examples/hello env printenv LAKE_CACHE_DIR
|
|||
# Test that `env` preserves the input environment for certain variables
|
||||
echo "# TEST: Setting variables for lake env"
|
||||
test_eq "foo" env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN
|
||||
test_out "foo" env env -u LAKE_CACHE_DIR ELAN_HOME=/ ELAN_TOOLCHAIN=foo \
|
||||
$LAKE env printenv LAKE_CACHE_DIR
|
||||
LAKE_CACHE_DIR=foo test_eq "foo" env printenv LAKE_CACHE_DIR
|
||||
LEAN_GITHASH=foo test_eq "foo" env printenv LEAN_GITHASH
|
||||
LEAN_AR=foo test_eq "foo" env printenv LEAN_AR
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue