feat: update toolchain on lake update (leanprover#5684)

Lake will now update a package's `lean-toolchain` file on `lake update`
if it finds the package's direct dependencies use a newer compatible
toolchain. To skip this step, use the `--keep-toolchain` CLI option.

Closes leanprover#2582. Closes leanprover#2752. Closes leanprover#5615.

### Toolchain update details

To determine "newest compatible" toolchain, Lake parses the toolchain
listed in the packages' `lean-toolchain` files into four categories:
release , nightly, PR, and other. For newness, release toolchains are
compared by semantic version (e.g., `"v4.4.0" < "v4.8.0"` and
`"v4.6.0-rc1" < "v4.6.0"`) and nightlies are compared by date (e.g.,
`"nightly-2024-01-10" < "nightly-2014-10-01"`). All other toolchain
types and mixtures are incompatible. If there is not a single newest
toolchain, Lake will print a warning and continue updating without
changing the toolchain.

If Lake does find a new toolchain, Lake updates the workspace's
`lean-toolchain` file accordingly and restarts the update process on the
new Lake. If Elan is detected, it will spawn the new Lake process via
`elan run` with the same arguments Lake was initially run with. If Elan
is missing, it will prompt the user to restart Lake manually and exit
with a special error code (4).

### Other changes

To implement this new logic, various other refactors were needed. Here
are some key highlights:

* Logs emitted during package and workspace loading are now eagerly
printed.
* The Elan executable used by Lake is now configurable by the `ELAN`
environment variable.
* The `--lean` CLI option was removed. Use the `LEAN` environment
variable instead.
* `Package.deps` / `Package.opaqueDeps` have been removed. Use
`findPackage?` with a dependency's name instead.
* The dependency resolver now uses a pure breadth-first traversal to
resolve dependencies. It also resolves dependencies in reverse order,
which is done for consistency with targets. Latter targets shadow
earlier ones and latter dependencies take precedence over earlier ones.
**These changes mean the order of dependencies in a Lake manifest will
change after the first `lake update` on this version of Lake.**

src/lake/Lake/Build/Package.lean

@@ -19,7 +19,10 @@ open Lean (Name)
 
 /-- Compute a topological ordering of the package's transitive dependencies. -/
 def Package.recComputeDeps (self : Package) : FetchM (Array Package) := do
-  (·.toArray) <$> self.deps.foldlM (init := OrdPackageSet.empty) fun deps dep => do
+  (·.toArray) <$> self.depConfigs.foldlM (init := OrdPackageSet.empty) fun deps cfg => do
+    let some dep ← findPackage? cfg.name
+      | error s!"{self.name}: package not found for dependency '{cfg.name}' \
+        (this is likely a bug in Lake)"
     return (← fetch <| dep.facet `deps).foldl (·.insert ·) deps |>.insert dep
 
 /-- The `PackageFacetConfig` for the builtin `depsFacet`. -/

src/lake/Lake/Build/Topological.lean

@@ -36,6 +36,10 @@ fetch functions, but not all fetch functions need build something.
 abbrev DFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) :=
   (a : α) → m (β a)
 
+/-- A `DFetchFn` that is not dependently typed. -/
+abbrev FetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :=
+  α → m β
+
 /-!
 In order to nest builds / fetches within one another,
 we equip the monad `m` with a fetch function of its own.

src/lake/Lake/CLI/Help.lean

@@ -41,12 +41,12 @@ BASIC OPTIONS:
   --help, -h            print help of the program or a command and exit
   --dir, -d=file        use the package configuration in a specific directory
   --file, -f=file       use a specific file for the package configuration
-  --lean=cmd            specify the `lean` command used by Lake
   -K key[=value]        set the configuration file option named key
   --old                 only rebuild modified modules (ignore transitive deps)
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
-  --update, -U          update manifest before building
+  --update, -U          update dependencies on load (e.g., before a build)
   --reconfigure, -R     elaborate configuration files instead of using OLeans
+  --keep-toolchain      do not update toolchain on workspace update
   --no-build            exit immediately if a build target is not up-to-date
   --no-cache            build packages locally; do not download build caches
   --try-cache           attempt to download build caches for supported packages

src/lake/Lake/CLI/Init.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Util.Git
 import Lake.Util.Sugar
+import Lake.Util.Version
 import Lake.Config.Lang
 import Lake.Config.Package
 import Lake.Config.Workspace
@@ -18,9 +19,6 @@ open Lean (Name)
 /-- 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!"/{defaultLakeDir}
 "

src/lake/Lake/CLI/Main.lean

@@ -26,6 +26,7 @@ namespace Lake
 /-! ## General options for top-level `lake` -/
 
 structure LakeOptions where
+  args : List String := []
   rootDir : FilePath := "."
   configFile : FilePath := defaultConfigFile
   elanInstall? : Option ElanInstall := none
@@ -36,6 +37,7 @@ structure LakeOptions where
   wantsHelp : Bool := false
   verbosity : Verbosity := .normal
   updateDeps : Bool := false
+  updateToolchain : Bool := true
   reconfigure : Bool := false
   oldMode : Bool := false
   trustHash : Bool := true
@@ -72,12 +74,15 @@ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
   return {
+    lakeArgs? := opts.args.toArray
     lakeEnv := ← opts.computeEnv
     wsDir := opts.rootDir
     relConfigFile := opts.configFile
     lakeOpts := opts.configOpts
     leanOpts := Lean.Options.empty
     reconfigure := opts.reconfigure
+    updateDeps := opts.updateDeps
+    updateToolchain := opts.updateToolchain
   }
 
 /-- Make a `BuildConfig` from a `LakeOptions`. -/
@@ -101,7 +106,7 @@ abbrev CliM := ArgsT CliStateM
 
 def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
   let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
-  let main := self.run' args |>.run' {elanInstall?, leanInstall?, lakeInstall?}
+  let main := self.run' args |>.run' {args, elanInstall?, leanInstall?, lakeInstall?}
   let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
   main.run
 
@@ -111,6 +116,12 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
 
 instance (priority := low) : MonadLift LogIO CliStateM := ⟨CliStateM.runLogIO⟩
 
+@[inline] def CliStateM.runLoggerIO (x : LoggerIO α) : CliStateM α := do
+  let opts ← get
+  MainM.runLoggerIO x opts.outLv opts.ansiMode
+
+instance (priority := low) : MonadLift LoggerIO CliStateM := ⟨CliStateM.runLoggerIO⟩
+
 /-! ## Argument Parsing -/
 
 def takeArg (arg : String) : CliM String := do
@@ -141,10 +152,6 @@ def noArgsRem (act : CliStateM α) : CliM α := do
 def getWantsHelp : CliStateM Bool :=
   (·.wantsHelp) <$> get
 
-def setLean (lean : String) : CliStateM PUnit := do
-  let leanInstall? ← findLeanCmdInstall? lean
-  modify ({·  with leanInstall?})
-
 def setConfigOpt (kvPair : String) : CliM PUnit :=
   let pos := kvPair.posOf '='
   let (key, val) :=
@@ -171,6 +178,7 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--quiet"       => modifyThe LakeOptions ({· with verbosity := .quiet})
 | "--verbose"     => modifyThe LakeOptions ({· with verbosity := .verbose})
 | "--update"      => modifyThe LakeOptions ({· with updateDeps := true})
+| "--keep-toolchain" => modifyThe LakeOptions ({· with updateToolchain := false})
 | "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
 | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
 | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
@@ -193,7 +201,6 @@ def lakeLongOption : (opt : String) → CliM PUnit
 | "--file"        => do
   let configFile ← takeOptArg "--file" "path"
   modifyThe LakeOptions ({· with configFile})
-| "--lean"        => do setLean <| ← takeOptArg "--lean" "path or command"
 | "--help"        => modifyThe LakeOptions ({· with wantsHelp := true})
 | "--"            => do
   let subArgs ← takeArgs
@@ -331,7 +338,7 @@ protected def build : CliM PUnit := do
   processOptions lakeOption
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
-  let ws ← loadWorkspace config opts.updateDeps
+  let ws ← loadWorkspace config
   let targetSpecs ← takeArgs
   let specs ← parseTargetSpecs ws targetSpecs
   let buildConfig := mkBuildConfig opts (out := .stdout)
@@ -350,7 +357,7 @@ protected def resolveDeps : CliM PUnit := do
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   noArgsRem do
-  discard <| loadWorkspace config opts.updateDeps
+  discard <| loadWorkspace config
 
 protected def update : CliM PUnit := do
   processOptions lakeOption

src/lake/Lake/CLI/Serve.lean

@@ -38,7 +38,7 @@ def setupFile
       IO.eprintln s!"Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file."
       exit 1
     let outLv := buildConfig.verbosity.minLogLv
-    let ws ← MainM.runLogIO (minLv := outLv) (ansiMode := .noAnsi) do
+    let ws ← MainM.runLoggerIO (minLv := outLv) (ansiMode := .noAnsi) do
       loadWorkspace loadConfig
     let imports := imports.foldl (init := #[]) fun imps imp =>
       if let some mod := ws.findModule? imp.toName then imps.push mod else imps
@@ -71,7 +71,7 @@ with the given additional `args`.
 -/
 def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
   let (extraEnv, moreServerArgs) ← do
-    let (ws?, log) ← (loadWorkspace config).run?
+    let (ws?, log) ← (loadWorkspace config).captureLog
     log.replay (logger := MonadLog.stderr)
     if let some ws := ws? then
       let ctx := mkLakeContext ws

src/lake/Lake/Config/Env.lean

@@ -63,7 +63,7 @@ def compute
     lake, lean, elan?,
     pkgUrlMap := ← computePkgUrlMap
     reservoirApiUrl := ← getUrlD "RESERVOIR_API_URL" s!"{reservoirBaseUrl}/v1"
-    noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind toBool?).getD false
+    noCache := (noCache <|> (← IO.getEnv "LAKE_NO_CACHE").bind envToBool?).getD false
     githashOverride := (← IO.getEnv "LEAN_GITHASH").getD ""
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
@@ -72,10 +72,6 @@ def compute
     initPath := ← getSearchPath "PATH"
   }
 where
-  toBool? (o : String) : Option Bool :=
-    if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
-    else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
-    else none
   computePkgUrlMap := do
     let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
     match Json.parse urlMapStr |>.bind fromJson? with
@@ -144,14 +140,29 @@ Combines the initial path of the environment with that of the Lean installation.
 def sharedLibPath (env : Env) : SearchPath :=
   env.lean.sharedLibPath ++ env.initSharedLibPath
 
+/-- Unset toolchain-specific environment variables. -/
+def noToolchainVars : Array (String × Option String) :=
+  #[
+    ("ELAN_TOOLCHAIN", none),
+    ("LAKE", none),
+    ("LAKE_OVERRIDE_LEAN", none),
+    ("LAKE_HOME", none),
+    ("LEAN", none),
+    ("LEAN_GITHASH", none),
+    ("LEAN_SYSROOT", none),
+    ("LEAN_AR", none)
+  ]
+
 /-- Environment variable settings that are not augmented by a Lake workspace. -/
 def baseVars (env : Env) : Array (String × Option String)  :=
   #[
+    ("ELAN", env.elan?.map (·.elan.toString)),
     ("ELAN_HOME", env.elan?.map (·.home.toString)),
     ("ELAN_TOOLCHAIN", if env.toolchain.isEmpty then none else env.toolchain),
     ("LAKE", env.lake.lake.toString),
     ("LAKE_HOME", env.lake.home.toString),
     ("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
+    ("LEAN", env.lean.lean.toString),
     ("LEAN_GITHASH", env.leanGithash),
     ("LEAN_SYSROOT", env.lean.sysroot.toString),
     ("LEAN_AR", env.lean.ar.toString),

src/lake/Lake/Config/InstallPath.lean

@@ -9,16 +9,18 @@ import Lake.Config.Defaults
 open System
 namespace Lake
 
-/-! ## Data Structures -/
+/-- Convert the string value of an environment variable to a boolean. -/
+def envToBool? (o : String) : Option Bool :=
+  if ["y", "yes", "t", "true", "on", "1"].contains o.toLower then true
+  else if ["n", "no", "f", "false", "off", "0"].contains o.toLower then false
+  else none
 
-/-- Standard path of `elan` in a Elan installation. -/
-def elanExe (home : FilePath) :=
-  home / "bin" / "elan" |>.addExtension FilePath.exeExtension
+/-! ## Data Structures -/
 
 /-- Information about the local Elan setup. -/
 structure ElanInstall where
   home : FilePath
-  elan := elanExe home
+  elan : FilePath
   binDir := home / "bin"
   toolchainsDir := home / "toolchains"
   deriving Inhabited, Repr
@@ -57,7 +59,7 @@ def initSharedLib : FilePath :=
 /-- Path information about the local Lean installation. -/
 structure LeanInstall where
   sysroot : FilePath
-  githash : String
+  githash : String := ""
   srcDir := sysroot / "src" / "lean"
   leanLibDir := sysroot / "lib" / "lean"
   includeDir := sysroot / "include"
@@ -67,9 +69,9 @@ structure LeanInstall where
   leanc := leancExe sysroot
   sharedLib := leanSharedLibDir sysroot / leanSharedLib
   initSharedLib := leanSharedLibDir sysroot / initSharedLib
-  ar : FilePath
-  cc : FilePath
-  customCc : Bool
+  ar : FilePath := "ar"
+  cc : FilePath := "cc"
+  customCc : Bool := false
   deriving Inhabited, Repr
 
 /--
@@ -110,12 +112,16 @@ def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where
 /-! ## Detection Functions -/
 
 /--
-Attempt to detect a Elan installation by checking the `ELAN_HOME`
-environment variable for a installation location.
+Attempt to detect an Elan installation by checking the `ELAN` and `ELAN_HOME`
+environment variables. If `ELAN` is set but empty, Elan is considered disabled.
 -/
 def findElanInstall? : BaseIO (Option ElanInstall) := do
   if let some home ← IO.getEnv "ELAN_HOME" then
-    return some {home}
+    let elan := (← IO.getEnv "ELAN").getD "elan"
+    if elan.trim.isEmpty then
+      return none
+    else
+      return some {elan, home}
   return none
 
 /--
@@ -149,9 +155,9 @@ set to the empty string.
 
 For (2), if `LEAN_AR` or `LEAN_CC` are defined, it uses those paths.
 Otherwise, if Lean is packaged with an `llvm-ar` and/or `clang`, use them.
-If not, use the `ar` and/or `cc` in the system's `PATH`. This last step is
-needed because internal builds of Lean do not bundle these tools
-(unlike user-facing releases).
+If not, use the `ar` and/or `cc` from the `AR` / `CC` environment variables
+or the system's `PATH`. This last step is needed because internal builds of
+Lean do not bundle these tools (unlike user-facing releases).
 
 We also track whether `LEAN_CC` was set to determine whether it should
 be set in the future for `lake env`. This is because if `LEAN_CC` was not set,
@@ -187,18 +193,29 @@ where
       return FilePath.mk ar
     else
       let ar := leanArExe sysroot
-      if (← ar.pathExists) then pure ar else pure "ar"
+      if (← ar.pathExists) then
+        return ar
+      else if let some ar ← IO.getEnv "AR" then
+        return ar
+      else
+        return "ar"
   findCc := do
     if let some cc ← IO.getEnv "LEAN_CC" then
       return (FilePath.mk cc, true)
     else
       let cc := leanCcExe sysroot
-      let cc := if (← cc.pathExists) then cc else "cc"
+      let cc ←
+        if (← cc.pathExists) then
+          pure cc
+        else if let some cc ← IO.getEnv "CC" then
+          pure cc
+        else
+          pure "cc"
       return (cc, false)
 
 /--
 Attempt to detect the installation of the given `lean` command
-by calling `findLeanCmdHome?`. See `LeanInstall.get` for how it assumes the
+by calling `findLeanSysroot?`. See `LeanInstall.get` for how it assumes the
 Lean install is organized.
 -/
 def findLeanCmdInstall? (lean := "lean") : BaseIO (Option LeanInstall) :=
@@ -235,14 +252,28 @@ def getLakeInstall? (lake : FilePath) : BaseIO (Option LakeInstall) := do
   return none
 
 /--
-Attempt to detect Lean's installation by first checking the
-`LEAN_SYSROOT` environment variable and then by trying `findLeanCmdHome?`.
+Attempt to detect Lean's installation by using the `LEAN` and `LEAN_SYSROOT`
+environment variables.
+
+If `LEAN_SYSROOT` is set, use it. Otherwise, check `LEAN` for the `lean`
+executable. If `LEAN` is set but empty, Lean will be considered disabled.
+Otherwise, Lean's location will be determined by trying `findLeanSysroot?`
+using value of `LEAN` or, if unset, the `lean` in `PATH`.
+
 See `LeanInstall.get` for how it assumes the Lean install is organized.
 -/
 def findLeanInstall? : BaseIO (Option LeanInstall) := do
   if let some sysroot ← IO.getEnv "LEAN_SYSROOT" then
     return some <| ← LeanInstall.get sysroot
-  if let some sysroot ← findLeanSysroot? then
+  let lean ← do
+    if let some lean ← IO.getEnv "LEAN" then
+      if lean.trim.isEmpty then
+        return none
+      else
+        pure lean
+    else
+      pure "lean"
+  if let some sysroot ← findLeanSysroot? lean then
     return some <| ← LeanInstall.get sysroot
   return none
 
@@ -271,7 +302,8 @@ Then it attempts to detect if Lake and Lean are part of a single installation
 where the `lake` executable is co-located with the `lean` executable (i.e., they
 are in the same directory). If Lean and Lake are not co-located, Lake will
 attempt  to find the their installations separately by calling
-`findLeanInstall?` and `findLakeInstall?`.
+`findLeanInstall?` and `findLakeInstall?`. Setting `LAKE_OVERRIDE_LEAN` to true
+will force Lake to use `findLeanInstall?` even if co-located.
 
 When co-located, Lake will assume that Lean and Lake's binaries are located in
 `<sysroot>/bin`, their Lean libraries  in `<sysroot>/lib/lean`, Lean's source files
@@ -280,9 +312,13 @@ following the pattern of a regular Lean toolchain.
 -/
 def findInstall? : BaseIO (Option ElanInstall × Option LeanInstall × Option LakeInstall) := do
   let elan? ← findElanInstall?
-  if let some home ← findLakeLeanJointHome? then
-    let lean ← LeanInstall.get home (collocated := true)
-    let lake := LakeInstall.ofLean lean
-    return (elan?, lean, lake)
+  if let some sysroot ← findLakeLeanJointHome? then
+    if (← IO.getEnv "LAKE_OVERRIDE_LEAN").bind envToBool? |>.getD false then
+      let lake := LakeInstall.ofLean {sysroot}
+      return (elan?, ← findLeanInstall?, lake)
+    else
+      let lean ← LeanInstall.get sysroot (collocated := true)
+      let lake := LakeInstall.ofLean lean
+      return (elan?, lean, lake)
   else
     return (elan?, ← findLeanInstall?, ← findLakeInstall?)