From 6a7111ed0e1964faa3ca1c8a07853c863d01510b Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 20 Aug 2025 22:44:36 -0400
Subject: [PATCH] fix: lake: no `LEAN_GITHASH` for bootstrap (#10012)

This PR changes Lake to not set `LEAN_GITHASH` when in core (i.e.
`bootstrap = true`). This avoids Lake rebuilding modules when the Lake
watchdog is on one build of Lean/Lake and the command line is on a
different one.
---
 src/lake/Lake/Config/Env.lean       | 2 +-
 src/lake/Lake/Config/Workspace.lean | 8 +++++++-
 stage0/src/stdlib_flags.h           | 2 ++
 3 files changed, 10 insertions(+), 2 deletions(-)

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;