From 123dcb964ce8fd5fade53626fd8daa88150fd470 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 8 Mar 2024 10:03:07 -0500 Subject: [PATCH] feat: lake: `LEAN_GITHASH` override (#3609) If the `LEAN_GITHASH` environment variable is set, Lake will now use it instead of the detected Lean's githash when computing traces for builds and the elaborated Lake configuration. This override allows one to replace the Lean version used by a library (e.g., Mathlib) without completely rebuilding it, which is useful for testing custom builds of Lean. --- src/lake/Lake/Build/Monad.lean | 2 +- src/lake/Lake/Config/Env.lean | 17 ++++++++++++++++- src/lake/Lake/Load/Elab.lean | 7 +++---- src/lake/Lake/Load/Main.lean | 10 +++++----- src/lake/tests/env/test.sh | 2 ++ 5 files changed, 27 insertions(+), 11 deletions(-) diff --git a/src/lake/Lake/Build/Monad.lean b/src/lake/Lake/Build/Monad.lean index 9ca09286fc..cb42d7a082 100644 --- a/src/lake/Lake/Build/Monad.lean +++ b/src/lake/Lake/Build/Monad.lean @@ -17,7 +17,7 @@ def mkBuildContext (ws : Workspace) (config : BuildConfig) : IO BuildContext := toBuildConfig := config, startedBuilds := ← IO.mkRef 0 finishedBuilds := ← IO.mkRef 0, - leanTrace := Hash.ofString ws.lakeEnv.lean.githash + leanTrace := Hash.ofString ws.lakeEnv.leanGithash } def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index 305afc7166..09677b1abd 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -25,7 +25,9 @@ structure Env where lean : LeanInstall /-- The Elan installation (if any) of the environment. -/ elan? : Option ElanInstall - /-- A name-to-URL mapping of URL overwrites for the named packages. -/ + /-- Overrides the detected Lean's githash as the string Lake uses for Lean traces. -/ + githashOverride : String + /-- A name-to-URL mapping of URL overrides for the named packages. -/ pkgUrlMap : NameMap String /-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/ initToolchain : String @@ -46,6 +48,7 @@ def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstal return { lake, lean, elan?, pkgUrlMap := ← computePkgUrlMap + githashOverride := (← IO.getEnv "LEAN_GITHASH").getD "" initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD "" initLeanPath := ← getSearchPath "LEAN_PATH", initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH", @@ -59,6 +62,17 @@ where | .ok urlMap => return urlMap | .error e => throw s!"'LAKE_PKG_URL_MAP' has invalid JSON: {e}" +/-- +The string Lake uses to identify Lean in traces. +Either the environment-specified `LEAN_GITHASH` or the detected Lean's githash. + +The override allows one to replace the Lean version used by a library +(e.g., Mathlib) without completely rebuilding it, which is useful for testing +custom builds of Lean. +-/ +def leanGithash (env : Env) : String := + if env.githashOverride.isEmpty then env.lean.githash else env.githashOverride + /-- The preferred toolchain of the environment. May be empty. Tries `env.initToolchain` first and then Lake's `Lean.toolchain`. @@ -113,6 +127,7 @@ def baseVars (env : Env) : Array (String × Option String) := ("LAKE", env.lake.lake.toString), ("LAKE_HOME", env.lake.home.toString), ("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress), + ("LEAN_GITHASH", env.leanGithash), ("LEAN_SYSROOT", env.lean.sysroot.toString), ("LEAN_AR", env.lean.ar.toString), ("LEAN_CC", env.lean.leanCc?) diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Elab.lean index 9cdf455227..c3f64016d1 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/src/lake/Lake/Load/Elab.lean @@ -156,7 +156,7 @@ Import the `.olean` for the configuration file if `reconfigure` is not set and an up-to-date one exists (i.e., one with matching configuration and on the same toolchain). Otherwise, elaborate the configuration and save it to the `.olean`. -/ -def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) +def importConfigFile (pkgDir lakeDir : FilePath) (lakeEnv : Lake.Env) (lakeOpts : NameMap String) (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do let some configName := FilePath.mk <$> configFile.fileName | error "invalid configuration file name" @@ -181,7 +181,6 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) handle, and acquires an exclusive lock on the trace. It then releases its lock on the lock file. writes the new lock data. -/ - let acquireTrace h : IO IO.FS.Handle := id do let hLock ← IO.FS.Handle.mk lockFile .write /- @@ -223,7 +222,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) match (← IO.FS.removeFile olean |>.toBaseIO) with | .ok _ | .error (.noFileOrDirectory ..) => h.putStrLn <| Json.pretty <| toJson - {platform := System.Platform.target, leanHash := Lean.githash, + {platform := System.Platform.target, leanHash := lakeEnv.leanGithash, configHash, options := lakeOpts : ConfigTrace} h.truncate let env ← elabConfigFile pkgDir lakeOpts leanOpts configFile @@ -245,7 +244,7 @@ def importConfigFile (pkgDir lakeDir : FilePath) (lakeOpts : NameMap String) | error "compiled configuration is invalid; run with '-R' to reconfigure" let upToDate := (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧ - trace.leanHash = Lean.githash ∧ trace.configHash = configHash + trace.leanHash = lakeEnv.leanGithash ∧ trace.configHash = configHash if upToDate then let env ← importConfigFileCore olean leanOpts h.unlock diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index c865d7c3f2..658a99aea6 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -31,10 +31,10 @@ Elaborate a dependency's configuration file into a `Package`. The resulting package does not yet include any dependencies. -/ def MaterializedDep.loadPackage (dep : MaterializedDep) -(wsDir : FilePath) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do +(wsDir : FilePath) (lakeEnv : Lake.Env) (leanOpts : Options) (reconfigure : Bool) : LogIO Package := do let dir := wsDir / dep.relPkgDir let lakeDir := dir / defaultLakeDir - let configEnv ← importConfigFile dir lakeDir dep.configOpts leanOpts (dir / dep.configFile) reconfigure + let configEnv ← importConfigFile dir lakeDir lakeEnv dep.configOpts leanOpts (dir / dep.configFile) reconfigure let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts return { dir @@ -51,7 +51,7 @@ Does not resolve dependencies. def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do Lean.searchPathRef.set config.env.leanSearchPath let configEnv ← importConfigFile - config.rootDir (config.rootDir / defaultLakeDir) + config.rootDir (config.rootDir / defaultLakeDir) config.env config.configOpts config.leanOpts config.configFile config.reconfigure let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts let root := { @@ -145,7 +145,7 @@ def Workspace.updateAndMaterialize (ws : Workspace) return pkg else -- Load the package - let depPkg ← dep.loadPackage ws.dir pkg.leanOpts reconfigure + let depPkg ← dep.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure if depPkg.name ≠ dep.name then logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'" -- Materialize locked dependencies @@ -220,7 +220,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do if let some entry := pkgEntries.find? dep.name then let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap - result.loadPackage ws.dir pkg.leanOpts reconfigure + result.loadPackage ws.dir ws.lakeEnv pkg.leanOpts reconfigure else if topLevel then error <| s!"dependency '{dep.name}' not in manifest; " ++ diff --git a/src/lake/tests/env/test.sh b/src/lake/tests/env/test.sh index a3036f1d3b..4401738c5e 100755 --- a/src/lake/tests/env/test.sh +++ b/src/lake/tests/env/test.sh @@ -13,6 +13,7 @@ $LAKE env | grep ".*=.*" # NOTE: `printenv` exits with code 1 if the variable is not set $LAKE env printenv LAKE $LAKE env printenv LAKE_HOME +$LAKE env printenv LEAN_GITHASH $LAKE env printenv LEAN_SYSROOT $LAKE env printenv LEAN_AR | grep ar $LAKE env printenv LEAN_PATH @@ -23,6 +24,7 @@ $LAKE -d ../../examples/hello env printenv PATH | grep examples/hello # Test that `env` preserves the input environment for certain variables test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo +test "`LEAN_GITHASH=foo $LAKE env printenv LEAN_GITHASH`" = foo test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo