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

@@ -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 α

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?)

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

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; " ++

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