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