fix: lake: reconfigure if toolchain changes

src/lake/Lake/CLI/Init.lean

@@ -16,10 +16,6 @@ open Git System
 /-- The default module of an executable in `std` package. -/
 def defaultExeRoot : Name := `Main
 
-/-- `elan` toolchain file name -/
-def toolchainFileName : FilePath :=
-  "lean-toolchain"
-
 def gitignoreContents :=
 s!"/{defaultBuildDir}
 /{defaultConfigFile.withExtension "olean"}

src/lake/Lake/Load/Config.lean

@@ -11,6 +11,9 @@ import Lake.Util.Log
 namespace Lake
 open System Lean
 
+/-- `elan` toolchain file name -/
+def toolchainFileName : FilePath := "lean-toolchain"
+
 /-- The default name of the Lake configuration file (i.e., `lakefile.lean`). -/
 def defaultConfigFile : FilePath := "lakefile.lean"
 

src/lake/Lake/Load/Elab.lean

@@ -78,17 +78,20 @@ def elabConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
     return s.commandState.env
 
 /--
-If `reconfigure` is not set and up-to-date OLean for the configuration file exists,
-import it. Otherwise, elaborate the configuration and store save it to the OLean.
+Import the OLean for the configuration file if `reconfigure` is not set
+and an up-to-date one exists (i.e., one newer than the configuration and the
+toolchain). Otherwise, elaborate the configuration and save it to the OLean.
 -/
-def importConfigFile (pkgDir : FilePath) (lakeOpts : NameMap String)
+def importConfigFile (wsDir pkgDir : FilePath) (lakeOpts : NameMap String)
 (leanOpts := Options.empty) (configFile := pkgDir / defaultConfigFile) (reconfigure := true) : LogIO Environment := do
   let olean := configFile.withExtension "olean"
   let useOLean ← id do
     if reconfigure then return false
-    unless (← olean.pathExists) do return false
-    unless (← getMTime olean) > (← getMTime configFile) do return false
-    return true
+    let .ok oleanMTime ← getMTime olean |>.toBaseIO | return false
+    unless oleanMTime > (← getMTime configFile) do return false
+    let toolchainFile := wsDir / toolchainFileName
+    let .ok toolchainMTime ← getMTime toolchainFile |>.toBaseIO | return true
+    return oleanMTime > toolchainMTime
   if useOLean then
     withImporting do
     let (mod, region) ← readModuleData olean

src/lake/Lake/Load/Main.lean

@@ -33,7 +33,7 @@ The resulting package does not yet include any dependencies.
 def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
 (leanOpts : Options) (lakeOpts : NameMap String) (reconfigure : Bool) : LogIO Package := do
   let dir := wsDir / dep.relPkgDir
-  let configEnv ← importConfigFile dir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
+  let configEnv ← importConfigFile wsDir dir lakeOpts leanOpts (dir / defaultConfigFile) reconfigure
   let config ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv leanOpts
   return {
     dir, config, configEnv, leanOpts
@@ -100,7 +100,7 @@ Does not resolve dependencies.
 -/
 def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
   Lean.searchPathRef.set config.env.leanSearchPath
-  let configEnv ← importConfigFile config.rootDir
+  let configEnv ← importConfigFile config.rootDir config.rootDir
     config.configOpts config.leanOpts config.configFile config.reconfigure
   let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
   let repo := GitRepo.mk config.rootDir