From 7aabb48549e01c93916838c2e50a2b12df01e26f Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 4 Nov 2024 09:31:40 -0500 Subject: [PATCH] feat: update toolchain on `lake update` (#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 #2582. Closes #2752. Closes #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 | 5 +- src/lake/Lake/Build/Topological.lean | 4 + src/lake/Lake/CLI/Help.lean | 4 +- src/lake/Lake/CLI/Init.lean | 4 +- src/lake/Lake/CLI/Main.lean | 23 +- src/lake/Lake/CLI/Serve.lean | 4 +- src/lake/Lake/Config/Env.lean | 21 +- src/lake/Lake/Config/InstallPath.lean | 88 +++-- src/lake/Lake/Config/Monad.lean | 4 + src/lake/Lake/Config/Opaque.lean | 3 - src/lake/Lake/Config/Package.lean | 12 +- src/lake/Lake/Config/Workspace.lean | 28 +- src/lake/Lake/Load/Config.lean | 16 +- src/lake/Lake/Load/Materialize.lean | 62 ++- src/lake/Lake/Load/Resolve.lean | 365 ++++++++++++------ src/lake/Lake/Load/Workspace.lean | 22 +- src/lake/Lake/Toml/Data/DateTime.lean | 55 +-- src/lake/Lake/Util/Date.lean | 69 ++++ src/lake/Lake/Util/Lift.lean | 22 +- src/lake/Lake/Util/Log.lean | 52 ++- src/lake/Lake/Util/MainM.lean | 9 + src/lake/Lake/Util/Version.lean | 110 +++++- .../deps/bar/lake-manifest.expected.json | 20 +- src/lake/examples/scripts/expected.out | 4 +- src/lake/tests/clone/test.sh | 5 +- src/lake/tests/depTree/test.sh | 11 +- src/lake/tests/env/test.sh | 1 + .../tests/manifest/lake-manifest-v1.1.0.json | 16 +- src/lake/tests/online/test.sh | 8 +- src/lake/tests/order/bar/lakefile.lean | 1 + src/lake/tests/order/baz/X.lean | 0 src/lake/tests/order/baz/lakefile.lean | 7 + src/lake/tests/order/clean.sh | 4 +- src/lake/tests/order/test.sh | 8 +- src/lake/tests/toolchain/.gitignore | 1 + src/lake/tests/toolchain/clean.sh | 1 + src/lake/tests/toolchain/lakefile.lean | 6 + src/lake/tests/toolchain/test.sh | 27 +- src/lake/tests/updateToolchain/.gitignore | 1 + .../tests/updateToolchain/a/lakefile.toml | 1 + .../tests/updateToolchain/b/lakefile.toml | 1 + src/lake/tests/updateToolchain/clean.sh | 1 + src/lake/tests/updateToolchain/lakefile.toml | 9 + src/lake/tests/updateToolchain/test.lean | 35 ++ src/lake/tests/updateToolchain/test.sh | 68 ++++ 45 files changed, 886 insertions(+), 332 deletions(-) create mode 100644 src/lake/Lake/Util/Date.lean create mode 100644 src/lake/tests/order/baz/X.lean create mode 100644 src/lake/tests/order/baz/lakefile.lean create mode 100644 src/lake/tests/toolchain/lakefile.lean create mode 100644 src/lake/tests/updateToolchain/.gitignore create mode 100644 src/lake/tests/updateToolchain/a/lakefile.toml create mode 100644 src/lake/tests/updateToolchain/b/lakefile.toml create mode 100755 src/lake/tests/updateToolchain/clean.sh create mode 100644 src/lake/tests/updateToolchain/lakefile.toml create mode 100644 src/lake/tests/updateToolchain/test.lean create mode 100755 src/lake/tests/updateToolchain/test.sh diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean index ae1a753da882..08e74c1a6de1 100644 --- a/src/lake/Lake/Build/Package.lean +++ b/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`. -/ diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean index d0e34890f04b..b5bb54ee00c4 100644 --- a/src/lake/Lake/Build/Topological.lean +++ b/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. diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 23c01a5b1bbc..1ef1390e24f5 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 94a8cbf684c9..07e0e492b618 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/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} " diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index cea688b6453e..7ce6fa9cdeac 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/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 diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 9748ae83720f..eab1b99439b0 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/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 diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index d15081823618..e50343c480e1 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/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), diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index 83681cf3bc49..a0877ef9316f 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/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 `/bin`, their Lean libraries in `/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?) diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index 4fd3148ea056..a548520a303b 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/src/lake/Lake/Config/Monad.lean @@ -45,6 +45,10 @@ abbrev MonadLake (m : Type → Type u) := @[inline] def mkLakeContext (ws : Workspace) : Lake.Context where opaqueWs := ws +/-- Run a `LakeT` monad in the context of this workspace. -/ +@[inline] def Workspace.runLakeT (ws : Workspace) (x : LakeT m α) : m α := + x.run (mkLakeContext ws) + instance [MonadWorkspace m] [Functor m] : MonadLake m where read := (mkLakeContext ·) <$> getWorkspace diff --git a/src/lake/Lake/Config/Opaque.lean b/src/lake/Lake/Config/Opaque.lean index 93b708c09184..9f3e2eba19de 100644 --- a/src/lake/Lake/Config/Opaque.lean +++ b/src/lake/Lake/Config/Opaque.lean @@ -8,9 +8,6 @@ import Lake.Util.Opaque namespace Lake -/-- Opaque reference to a `Package` used for forward declaration. -/ -declare_opaque_type OpaquePackage - /-- Opaque reference to a `Workspace` used for forward declaration. -/ declare_opaque_type OpaqueWorkspace diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 7629bc04492e..21c186bb8b26 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -380,11 +380,9 @@ structure Package where /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/ relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile /-- The package's scope (e.g., in Reservoir). -/ - scope : String := "" + scope : String /-- The URL to this package's Git remote. -/ - remoteUrl : String := "" - /-- (Opaque references to) the package's direct dependencies. -/ - opaqueDeps : Array OpaquePackage := #[] + remoteUrl : String /-- Dependency configurations for the package. -/ depConfigs : Array Dependency := #[] /-- Lean library configurations for the package. -/ @@ -419,8 +417,6 @@ instance : Nonempty Package := have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance ⟨by constructor <;> exact default⟩ -hydrate_opaque_type OpaquePackage Package - instance : Hashable Package where hash pkg := hash pkg.config.name instance : BEq Package where beq p1 p2 := p1.config.name == p2.config.name @@ -508,10 +504,6 @@ namespace Package @[inline] def readmeFile (self : Package) : FilePath := self.dir / self.config.readmeFile -/-- The package's direct dependencies. -/ -@[inline] def deps (self : Package) : Array Package := - self.opaqueDeps.map (·.get) - /-- The path to the package's Lake directory relative to `dir` (e.g., `.lake`). -/ @[inline] def relLakeDir (_ : Package) : FilePath := defaultLakeDir diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index cbd19304308b..29638b2c9df5 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -18,8 +18,14 @@ open Lean (Name) structure Workspace : Type where /-- The root package of the workspace. -/ root : Package - /-- The detect `Lake.Env` of the workspace. -/ + /-- The detected `Lake.Env` of the workspace. -/ lakeEnv : Lake.Env + /-- + The CLI arguments Lake was run with. + Used by `lake update` to perform a restart of Lake on a toolchain update. + A value of `none` means that Lake is not restartable via the CLI. + -/ + lakeArgs? : Option (Array String) := none /-- The packages within the workspace (in `require` declaration order). -/ packages : Array Package := {} /-- Name-package map of packages within the workspace. -/ @@ -77,7 +83,7 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace := /-- Try to find a script in the workspace with the given name. -/ protected def findScript? (script : Name) (self : Workspace) : Option Script := - self.packages.findSomeRev? (·.scripts.find? script) + self.packages.findSome? (·.scripts.find? script) /-- Check if the module is local to any package in the workspace. -/ def isLocalModule (mod : Name) (self : Workspace) : Bool := @@ -89,27 +95,27 @@ def isBuildableModule (mod : Name) (self : Workspace) : Bool := /-- Locate the named, buildable, importable, local module in the workspace. -/ protected def findModule? (mod : Name) (self : Workspace) : Option Module := - self.packages.findSomeRev? (·.findModule? mod) + self.packages.findSome? (·.findModule? mod) /-- Locate the named, buildable, but not necessarily importable, module in the workspace. -/ def findTargetModule? (mod : Name) (self : Workspace) : Option Module := - self.packages.findSomeRev? (·.findTargetModule? mod) + self.packages.findSome? (·.findTargetModule? mod) /-- Try to find a Lean library in the workspace with the given name. -/ protected def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib := - self.packages.findSomeRev? fun pkg => pkg.findLeanLib? name + self.packages.findSome? fun pkg => pkg.findLeanLib? name /-- Try to find a Lean executable in the workspace with the given name. -/ protected def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe := - self.packages.findSomeRev? fun pkg => pkg.findLeanExe? name + self.packages.findSome? fun pkg => pkg.findLeanExe? name /-- Try to find an external library in the workspace with the given name. -/ protected def findExternLib? (name : Name) (self : Workspace) : Option ExternLib := - self.packages.findSomeRev? fun pkg => pkg.findExternLib? name + self.packages.findSome? fun pkg => pkg.findExternLib? name /-- Try to find a target configuration in the workspace with the given name. -/ def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) := - self.packages.findSomeRev? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩) + self.packages.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩) /-- Add a module facet to the workspace. -/ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace := @@ -137,15 +143,15 @@ def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFa /-- The workspace's binary directories (which are added to `Path`). -/ def binPath (self : Workspace) : SearchPath := - self.packages.foldr (fun pkg dirs => pkg.binDir :: dirs) [] + self.packages.foldl (fun dirs pkg => pkg.binDir :: dirs) [] /-- The workspace's Lean library directories (which are added to `LEAN_PATH`). -/ def leanPath (self : Workspace) : SearchPath := - self.packages.foldr (fun pkg dirs => pkg.leanLibDir :: dirs) [] + self.packages.foldl (fun dirs pkg => pkg.leanLibDir :: dirs) [] /-- The workspace's source directories (which are added to `LEAN_SRC_PATH`). -/ def leanSrcPath (self : Workspace) : SearchPath := - self.packages.foldr (init := {}) fun pkg dirs => + self.packages.foldl (init := {}) fun dirs pkg => pkg.leanLibConfigs.foldr (init := dirs) fun cfg dirs => pkg.srcDir / cfg.srcDir :: dirs diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean index 237578cd8c36..d5929bf8cd4b 100644 --- a/src/lake/Lake/Load/Config.lean +++ b/src/lake/Lake/Load/Config.lean @@ -8,6 +8,7 @@ import Lean.Data.Options import Lake.Config.Defaults import Lake.Config.Env import Lake.Util.Log +import Lake.Util.Version namespace Lake open System Lean @@ -16,6 +17,12 @@ open System Lean structure LoadConfig where /-- The Lake environment of the load process. -/ lakeEnv : Lake.Env + /-- + The CLI arguments Lake was run with. + Used to perform a restart of Lake on a toolchain update. + A value of `none` means that Lake is not restartable via the CLI. + -/ + lakeArgs? : Option (Array String) := none /-- The root directory of the Lake workspace. -/ wsDir : FilePath /-- The directory of the loaded package (relative to the root). -/ @@ -26,8 +33,15 @@ structure LoadConfig where lakeOpts : NameMap String := {} /-- The Lean options with which to elaborate the configuration file. -/ leanOpts : Options := {} - /-- If `true`, Lake will elaborate configuration files instead of using OLeans. -/ + /-- Whether Lake should re-elaborate configuration files instead of using cached OLeans. -/ reconfigure : Bool := false + /-- Whether to update dependencies when loading the workspace. -/ + updateDeps : Bool := false + /-- + Whether to update the workspace's `lean-toolchain` when dependencies are updated. + If `true` and a toolchain update occurs, Lake will need to be restarted. + -/ + updateToolchain : Bool := true /-- The package's scope (e.g., in Reservoir). -/ scope : String := "" /-- The URL to this package's Git remote (if any). -/ diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index cf618aaf5342..4882a4af9750 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/src/lake/Lake/Load/Materialize.lean @@ -20,31 +20,36 @@ or resolve a local path dependency. namespace Lake /-- Update the Git package in `repo` to `rev` if not already at it. -/ -def updateGitPkg (name : String) (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do +def updateGitPkg + (name : String) (repo : GitRepo) (rev? : Option String) +: LogIO PUnit := do let rev ← repo.findRemoteRevision rev? if (← repo.getHeadRevision) = rev then if (← repo.hasDiff) then logWarning s!"{name}: repository '{repo.dir}' has local changes" else - logInfo s!"{name}: updating repository '{repo.dir}' to revision '{rev}'" + logInfo s!"{name}: checking out revision '{rev}'" repo.checkoutDetach rev /-- Clone the Git package as `repo`. -/ -def cloneGitPkg (name : String) (repo : GitRepo) -(url : String) (rev? : Option String) : LogIO PUnit := do - logInfo s!"{name}: cloning {url} to '{repo.dir}'" +def cloneGitPkg + (name : String) (repo : GitRepo) (url : String) (rev? : Option String) +: LogIO PUnit := do + logInfo s!"{name}: cloning {url}" repo.clone url if let some rev := rev? then - let hash ← repo.resolveRemoteRevision rev - repo.checkoutDetach hash + let rev ← repo.resolveRemoteRevision rev + logInfo s!"{name}: checking out revision '{rev}'" + repo.checkoutDetach rev /-- Update the Git repository from `url` in `repo` to `rev?`. If `repo` is already from `url`, just checkout the new revision. Otherwise, delete the local repository and clone a fresh copy from `url`. -/ -def updateGitRepo (name : String) (repo : GitRepo) -(url : String) (rev? : Option String) : LogIO Unit := do +def updateGitRepo + (name : String) (repo : GitRepo) (url : String) (rev? : Option String) +: LogIO Unit := do let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do let some remoteUrl ← repo.getRemoteUrl? | return false if remoteUrl = url then return true @@ -65,8 +70,9 @@ def updateGitRepo (name : String) (repo : GitRepo) Materialize the Git repository from `url` into `repo` at `rev?`. Clone it if no local copy exists, otherwise update it. -/ -def materializeGitRepo (name : String) (repo : GitRepo) -(url : String) (rev? : Option String) : LogIO Unit := do +def materializeGitRepo + (name : String) (repo : GitRepo) (url : String) (rev? : Option String) +: LogIO Unit := do if (← repo.dirExists) then updateGitRepo name repo url rev? else @@ -110,11 +116,7 @@ def Dependency.materialize match src with | .path dir => let relPkgDir := relParentDir / dir - return { - relPkgDir - remoteUrl := "" - manifestEntry := mkEntry <| .path relPkgDir - } + return mkDep relPkgDir "" (.path relPkgDir) | .git url inputRev? subDir? => do let sname := dep.name.toString (escape := false) let repoUrl := Git.filterUrl? url |>.getD "" @@ -127,7 +129,7 @@ def Dependency.materialize if ver.startsWith "git#" then return ver.drop 4 else - error s!"{dep.name} unsupported dependency version format '{ver}' (should be \"git#>rev>\")" + error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#>rev>\")" let depName := dep.name.toString (escape := false) let some pkg ← Reservoir.fetchPkg? lakeEnv dep.scope depName | error s!"{dep.scope}/{depName}: could not materialize package: \ @@ -139,18 +141,17 @@ def Dependency.materialize (githubUrl?.getD "") (verRev? <|> defaultBranch?) subDir? | _ => error s!"{pkg.fullName}: Git source not found on Reservoir" where - mkEntry src : PackageEntry := - {name := dep.name, scope := dep.scope, inherited, src} materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LogIO MaterializedDep := do let repo := GitRepo.mk (wsDir / relPkgDir) let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl materializeGitRepo name repo gitUrl inputRev? let rev ← repo.getHeadRevision let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir - return { - relPkgDir, remoteUrl - manifestEntry := mkEntry <| .git gitUrl rev inputRev? subDir? - } + return mkDep relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir? + @[inline] mkDep relPkgDir remoteUrl src : MaterializedDep := { + relPkgDir, remoteUrl, + manifestEntry := {name := dep.name, scope := dep.scope, inherited, src} + } /-- Materializes a manifest package entry, cloning and/or checking it out as necessary. @@ -161,11 +162,7 @@ def PackageEntry.materialize : LogIO MaterializedDep := match manifestEntry.src with | .path (dir := relPkgDir) .. => - return { - relPkgDir - remoteUrl := "" - manifestEntry - } + return mkDep relPkgDir "" | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do let sname := manifestEntry.name.toString (escape := false) let relGitDir := relPkgsDir / sname @@ -188,8 +185,7 @@ def PackageEntry.materialize let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url cloneGitPkg sname repo url rev let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir - return { - relPkgDir - remoteUrl := Git.filterUrl? url |>.getD "" - manifestEntry - } + return mkDep relPkgDir (Git.filterUrl? url |>.getD "") +where + @[inline] mkDep relPkgDir remoteUrl : MaterializedDep := + {relPkgDir, remoteUrl, manifestEntry} diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index e92c77d2f765..d56f4bc79848 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -18,6 +18,21 @@ This module contains definitions for resolving the dependencies of a package. namespace Lake +def stdMismatchError (newName : String) (rev : String) := +s!"the 'std' package has been renamed to '{newName}' and moved to the +'leanprover-community' organization; downstream packages which wish to +update to the new std should replace + + require std from + git \"https://github.com/leanprover/std4\"{rev} + +in their Lake configuration file with + + require {newName} from + git \"https://github.com/leanprover-community/{newName}\"{rev} + +" + /-- Loads the package configuration of a materialized dependency. Adds the facets defined in the package to the `Workspace`. @@ -43,100 +58,82 @@ def loadDepPackage else return (pkg, ws) -/-- The monad of the dependency resolver. -/ -abbrev ResolveT m := CallStackT Name <| StateT Workspace m +/-- +The resolver's call stack of dependencies. +That is, the dependency currently being resolved plus its parents. +-/ +abbrev DepStack := CallStack Name -@[inline] nonrec def ResolveT.run (ws : Workspace) (x : ResolveT m α) (stack : CallStack Name := {}) : m (α × Workspace) := - x.run stack |>.run ws +/-- +A monad transformer for recursive dependency resolution. +It equips the monad with the stack of dependencies currently being resolved. +-/ +abbrev DepStackT m := CallStackT Name m + +@[inline] nonrec def DepStackT.run + (x : DepStackT m α) (stack : DepStack := {}) +: m α := + x.run stack /-- Log dependency cycle and error. -/ @[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α := error s!"dependency cycle detected:\n{"\n".intercalate <| cycle.map (s!" {·}")}" -instance [Monad m] [MonadError m] : MonadCycleOf Name (ResolveT m) where +instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where throwCycle := depCycleError -/-- -Recursively visits the workspace dependency graph, starting from `root`. -At each package, loops through each direct dependency performing just `breath`. -Them, loops again through the results applying `depth`, recursing, and adding -the package to workspace's package set. Errors if a cycle is encountered. - -**Traversal Order** +/-- The monad of the dependency resolver. -/ +abbrev ResolveT m := DepStackT <| StateT Workspace m -All dependencies of a package are visited in order before recursing to the -dependencies' dependencies. For example, given the dependency graph: +@[inline] nonrec def ResolveT.run + (ws : Workspace) (x : ResolveT m α) (stack : DepStack := {}) +: m (α × Workspace) := + x.run stack |>.run ws -``` -R -|- A -|- B - |- X - |- Y -|- C -``` +/-- Recursively run a `ResolveT` monad starting from the workspace's root. -/ +@[specialize] private def Workspace.runResolveT + [Monad m] [MonadError m] (ws : Workspace) + (go : RecFetchFn Package PUnit (ResolveT m)) + (root := ws.root) (stack : DepStack := {}) +: m Workspace := do + let (_, ws) ← ResolveT.run ws (stack := stack) do + inline <| recFetchAcyclic (·.name) go root + return ws -Lake follows the order `R`, `A`, `B`, `C`, `X`, `Y`. +/- +Recursively visits each node in a package's dependency graph, starting from +the workspace package `root`. Each dependency missing from the workspace is +resolved using the `resolve` function and added into the workspace. -The logic behind this design is that users would expect the dependencies -they write in a package configuration to be resolved accordingly and would be -surprised if they are overridden by nested dependencies referring to the same -package. +Recursion occurs breadth-first. Each direct dependency of a package is +resolved in reverse order before recursing to the dependencies' dependencies. -For example, were Lake to use a pure depth-first traversal, Lake would follow -the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package -`foo`, Lake would use the configuration of `foo` found in `B` rather than in -the root `R`, which would likely confuse the user. +See `Workspace.updateAndMaterializeCore` for more details. -/ -@[specialize] def Workspace.resolveDeps +@[inline] private def Workspace.resolveDepsCore [Monad m] [MonadError m] (ws : Workspace) - (breadth : Package → Dependency → ResolveT m Package) - (depth : Package → m PUnit := fun _ => pure ()) + (load : Package → Dependency → StateT Workspace m Package) + (root : Package := ws.root) (stack : DepStack := {}) : m Workspace := do - let (root, ws) ← ResolveT.run ws <| StateT.run' (s := {}) <| - inline <| recFetchAcyclic (·.name) go ws.root - return {ws with root} + ws.runResolveT go root stack where - @[specialize] go pkg resolve : StateT (NameMap Package) (ResolveT m) Package := do - pkg.depConfigs.forM fun dep => do - if (← getThe (NameMap Package)).contains dep.name then - return - if (← getThe Workspace).packageMap.contains dep.name then - return -- already resolved in another branch + @[specialize] go pkg recurse : ResolveT m Unit := do + let start := (← getWorkspace).packages.size + -- Materialize and load the missing direct dependencies of `pkg` + pkg.depConfigs.forRevM fun dep => do + let ws ← getWorkspace + if ws.packageMap.contains dep.name then + return -- already handled in another branch if pkg.name = dep.name then error s!"{pkg.name}: package requires itself (or a package with the same name)" - let pre ← breadth pkg dep -- package w/o dependencies - store dep.name pre - let deps ← pkg.depConfigs.mapM fun dep => do - if let some pre ← fetch? dep.name then - modifyThe (NameMap Package) (·.erase dep.name) -- for `dep` linearity - depth pre - return OpaquePackage.mk (← resolve pre) - if let some dep ← findPackage? dep.name then - return OpaquePackage.mk dep -- already resolved in another branch - error s!"{dep.name}: impossible resolution state reached" - let pkg := {pkg with opaqueDeps := deps} - modifyThe Workspace (·.addPackage pkg) - return pkg - -def stdMismatchError (newName : String) (rev : String) := -s!"the 'std' package has been renamed to '{newName}' and moved to the -'leanprover-community' organization; downstream packages which wish to -update to the new std should replace - - require std from - git \"https://github.com/leanprover/std4\"{rev} - -in their Lake configuration file with - - require {newName} from - git \"https://github.com/leanprover-community/{newName}\"{rev} - -" + let depPkg ← load pkg dep + modifyThe Workspace (·.addPackage depPkg) + -- Recursively load the dependencies' dependencies + (← getWorkspace).packages.forM recurse start /-- -The monad of the manifest updater. -It is equipped with and entry map entries for the updated manifest. +Adds monad state used to update the manifest. +It equips the monad with a map of locked dependencies. -/ abbrev UpdateT := StateT (NameMap PackageEntry) @@ -147,7 +144,9 @@ abbrev UpdateT := StateT (NameMap PackageEntry) Reuse manifest versions of root packages that should not be updated. Also, move the packages directory if its location has changed. -/ -def reuseManifest (ws : Workspace) (toUpdate : NameSet) : UpdateT LogIO PUnit := do +private def reuseManifest + (ws : Workspace) (toUpdate : NameSet) +: UpdateT LogIO PUnit := do let rootName := ws.root.name.toString (escape := false) match (← Manifest.load ws.manifestFile |>.toBaseIO) with | .ok manifest => @@ -175,7 +174,7 @@ def reuseManifest (ws : Workspace) (toUpdate : NameSet) : UpdateT LogIO PUnit := logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}" /-- Add a package dependency's manifest entries to the update state. -/ -def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do +private def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do match (← Manifest.load pkg.manifestFile |>.toBaseIO) with | .ok manifest => manifest.packages.forM fun entry => do @@ -187,22 +186,31 @@ def addDependencyEntries (pkg : Package) : UpdateT LogIO PUnit := do | .error e => logWarning s!"{pkg.name}: ignoring manifest because it failed to load: {e}" -/-- Update a single dependency. -/ -def updateDep - (pkg : Package) (dep : Dependency) (leanOpts : Options := {}) -: ResolveT (UpdateT LogIO) Package := do - let ws ← getThe Workspace - let inherited := pkg.name != ws.root.name - -- Materialize the dependency - let matDep ← id do - if let some entry ← fetch? dep.name then - entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir - else - let matDep ← dep.materialize inherited ws.lakeEnv ws.dir ws.relPkgsDir pkg.relDir - store matDep.name matDep.manifestEntry - return matDep - -- Load the package - let depPkg ← loadDepPackage matDep dep.opts leanOpts true +/-- Materialize a single dependency, updating it if desired. -/ +private def updateAndMaterializeDep + (ws : Workspace) (pkg : Package) (dep : Dependency) +: UpdateT LogIO MaterializedDep := do + if let some entry ← fetch? dep.name then + entry.materialize ws.lakeEnv ws.dir ws.relPkgsDir + else + let inherited := pkg.name ≠ ws.root.name + /- + NOTE: A path dependency inherited from another dependency's manifest + will always be of the form a `./` (i.e., be relative to its + workspace). Thus, when relativized to this workspace, it will have the + path `/./`. However, if defining dependency lacks + a manifest, it will instead be locked as `/`. + Adding a `.` here eliminates this difference. + -/ + let relPkgDir := if pkg.relDir == "." then pkg.relDir else pkg.relDir / "." + let matDep ← dep.materialize inherited ws.lakeEnv ws.dir ws.relPkgsDir relPkgDir + store matDep.name matDep.manifestEntry + return matDep + +/-- Verify that a dependency was loaded with the correct name. -/ +private def validateDep + (pkg : Package) (dep : Dependency) (matDep : MaterializedDep) (depPkg : Package) +: LogIO PUnit := do if depPkg.name ≠ dep.name then if dep.name = .mkSimple "std" then let rev := @@ -216,24 +224,144 @@ def updateDep logError s!"'{dep.name}' was downloaded incorrectly; \ you will need to manually delete '{depPkg.dir}': {e}" error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'" - return depPkg /-- -Rebuild the workspace's Lake manifest and materialize missing dependencies. +Exit code returned if Lake needs a manual restart. +Used, for instance, if the toolchain is updated and no Elan is detected. +-/ +def restartCode : ExitCode := 4 -Packages are updated to latest specific revision matching that in `require` +/-- +Update the workspace's `lean-toolchain` if necessary. + +Compares the root's toolchain with that of its direct dependencies to find the +best match. If none can be found, issue warning and return normally. If an +update is found +-/ +def Workspace.updateToolchain + (ws : Workspace) (rootDeps : Array MaterializedDep) +: LoggerIO PUnit := do + let rootToolchainFile := ws.root.dir / toolchainFileName + let rootTc? ← ToolchainVer.ofDir? ws.dir + let (src, tc?, tcs) ← rootDeps.foldlM (init := (ws.root.name, rootTc?, #[])) fun s dep => do + let depTc? ← ToolchainVer.ofDir? (ws.dir / dep.relPkgDir) + let some depTc := depTc? + | return s + let (src, tc?, tcs) := s + let some tc := tc? + | return (dep.name, depTc?, tcs) + if depTc ≤ tc then + return (src, tc, tcs) + else if tc < depTc then + return (dep.name, depTc, tcs) + else + return (src, tc, tcs.push (dep.name, depTc)) + if 0 < tcs.size then + let s := "toolchain not updated; multiple toolchain candidates:" + let s := if let some tc := tc? then s!"{s}\n {tc}\n from {src}" else s + let s := tcs.foldl (init := s) fun s (d, tc) => s!"{s}\n {tc}\n from {d}" + logWarning s + else if let some tc := tc? then + if rootTc?.any (· == tc) then + logInfo "toolchain not updated; already up-to-date" + return + logInfo s!"updating toolchain to '{tc}'" + IO.FS.writeFile rootToolchainFile tc.toString + let some lakeArgs := ws.lakeArgs? + | logInfo s!"cannot auto-restart; you will need to manually restart Lake" + IO.Process.exit restartCode.toUInt8 + let some elanInstall := ws.lakeEnv.elan? + | logInfo s!"no Elan detected; you will need to manually restart Lake" + IO.Process.exit restartCode.toUInt8 + logInfo s!"restarting Lake via Elan" + let child ← IO.Process.spawn { + cmd := elanInstall.elan.toString + args := #["run", "--install", tc.toString, "lake"] ++ lakeArgs + env := Env.noToolchainVars + } + IO.Process.exit (← child.wait).toUInt8 + else + logInfo s!"toolchain not updated; no toolchain information found" + +/-- +Updates the workspace, materializing and reconfiguring dependencies. + +Dependencies are updated to latest specific revision matching that in `require` (e.g., if the `require` is `@master`, update to latest commit on master) or -removed if the `require` is removed. If `tuUpdate` is empty, update/remove all -root dependencies. Otherwise, only update the root dependencies specified. +removed if the `require` is removed. +If `tuUpdate` is empty, all direct dependencies of the workspace's root will be +updated and/or remove. Otherwise, only those specified will be updated. + +If `updateToolchain := true`, the workspace's toolchain is also updated to the +latest toolchain compatible with the root and its direct dependencies. +If there are multiple incomparable toolchain versions across them, +a warning will be issued and no update performed. +If an update is performed, Lake will automatically restart the update on the new +toolchain (via `elan`). If `elan` is missing, it will instead request a manual +restart from the user and exit immediately with `restartCode`. + +**Dependency Traversal Order** -Package are always reconfigured when updated. +All dependencies of a package are visited in reverse order before recursing +to the dependencies' dependencies. For example, given the dependency graph: + +``` +R +|- A +|- B + |- X + |- Y +|- C +``` + +Lake follows the order `R`, `C`, `A`, `B`, `Y`, `X`. + +The reason for this is two-fold: +1. Like targets, later requires should shadow earlier definitions. +2. Requires written by a user should take priority over those inherited +from dependencies. + +Were Lake to use a depth-first traversal, for example, Lake would follow +the order `R`, `A`, `B`, `X`, `Y`, `C`. If `X` and `C` are both the package +`foo`, Lake would use the configuration of `foo` found in `B` rather than in +the root `R`, which would likely confuse the user. -/ -def Workspace.updateAndMaterialize - (ws : Workspace) (toUpdate : NameSet := {}) (leanOpts : Options := {}) -: LogIO Workspace := do - let (ws, entries) ← UpdateT.run do - reuseManifest ws toUpdate - ws.resolveDeps (updateDep · · leanOpts) (addDependencyEntries ·) +def Workspace.updateAndMaterializeCore + (ws : Workspace) + (toUpdate : NameSet := {}) (leanOpts : Options := {}) + (updateToolchain := true) +: LoggerIO (Workspace × NameMap PackageEntry) := UpdateT.run do + reuseManifest ws toUpdate + let ws := ws.addPackage ws.root + if updateToolchain then + let deps := ws.root.depConfigs.reverse + let matDeps ← deps.mapM fun dep => do + logVerbose s!"{ws.root.name}: updating '{dep.name}' with {toJson dep.opts}" + updateAndMaterializeDep ws ws.root dep + ws.updateToolchain matDeps + let start := ws.packages.size + let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do + let (depPkg, ws) ← loadUpdatedDep ws.root dep matDep ws + let ws := ws.addPackage depPkg + return ws + ws.packages.foldlM (init := ws) (start := start) fun ws pkg => + ws.resolveDepsCore (stack := [ws.root.name]) updateAndLoadDep pkg + else + ws.resolveDepsCore updateAndLoadDep +where + @[inline] updateAndLoadDep pkg dep := do + let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep + loadUpdatedDep pkg dep matDep + @[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LogIO) Package := do + let depPkg ← loadDepPackage matDep dep.opts leanOpts true + validateDep pkg dep matDep depPkg + addDependencyEntries depPkg + return depPkg + +/-- Write package entries to the workspace manifest. -/ +def Workspace.writeManifest + (ws : Workspace) (entries : NameMap PackageEntry) +: LogIO PUnit := do let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg => match entries.find? pkg.name with | some entry => arr.push <| @@ -246,10 +374,28 @@ def Workspace.updateAndMaterialize packages := manifestEntries } manifest.saveToFile ws.manifestFile - LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do - unless pkg.postUpdateHooks.isEmpty do - logInfo s!"{pkg.name}: running post-update hooks" - pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg + +/-- Run a package's `post_update` hooks. -/ +def Package.runPostUpdateHooks (pkg : Package) : LakeT LogIO PUnit := do + unless pkg.postUpdateHooks.isEmpty do + logInfo s!"{pkg.name}: running post-update hooks" + pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg + +/-- +Updates the workspace, writes the new Lake manifest, and runs package +post-update hooks. + +See `Workspace.updateAndMaterializeCore` for details on the update process. +-/ +def Workspace.updateAndMaterialize + (ws : Workspace) + (toUpdate : NameSet := {}) (leanOpts : Options := {}) + (updateToolchain := true) +: LoggerIO Workspace := do + let (ws, entries) ← + ws.updateAndMaterializeCore toUpdate leanOpts updateToolchain + ws.writeManifest entries + ws.runLakeT do ws.packages.forM (·.runPostUpdateHooks) return ws /-- @@ -293,8 +439,9 @@ def Workspace.materializeDeps let pkgEntries : NameMap PackageEntry := manifest.packages.foldl (init := {}) fun map entry => map.insert entry.name entry validateManifest pkgEntries ws.root.depConfigs - ws.resolveDeps fun pkg dep => do - let ws ← getThe Workspace + let ws := ws.addPackage ws.root + ws.resolveDepsCore fun pkg dep => do + let ws ← getWorkspace if let some entry := pkgEntries.find? dep.name then let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir loadDepPackage result dep.opts leanOpts reconfigure diff --git a/src/lake/Lake/Load/Workspace.lean b/src/lake/Lake/Load/Workspace.lean index b9b334bf52f6..c17adecbc17a 100644 --- a/src/lake/Lake/Load/Workspace.lean +++ b/src/lake/Lake/Load/Workspace.lean @@ -25,7 +25,9 @@ def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do Lean.searchPathRef.set config.lakeEnv.leanSearchPath let (root, env?) ← loadPackageCore "[root]" config let ws : Workspace := { - root, lakeEnv := config.lakeEnv + root + lakeEnv := config.lakeEnv + lakeArgs? := config.lakeArgs? moduleFacetConfigs := initModuleFacetConfigs packageFacetConfigs := initPackageFacetConfigs libraryFacetConfigs := initLibraryFacetConfigs @@ -40,19 +42,19 @@ Load a `Workspace` for a Lake package by elaborating its configuration file and resolving its dependencies. If `updateDeps` is true, updates the manifest before resolving dependencies. -/ -def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace := do - let rc := config.reconfigure - let leanOpts := config.leanOpts +def loadWorkspace (config : LoadConfig) : LoggerIO Workspace := do + let {reconfigure, leanOpts, updateDeps, updateToolchain, ..} := config let ws ← loadWorkspaceRoot config if updateDeps then - ws.updateAndMaterialize {} leanOpts + ws.updateAndMaterialize {} leanOpts updateToolchain else if let some manifest ← Manifest.load? ws.manifestFile then - ws.materializeDeps manifest leanOpts rc + ws.materializeDeps manifest leanOpts reconfigure else - ws.updateAndMaterialize {} leanOpts + ws.updateAndMaterialize {} leanOpts updateToolchain /-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/ -def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do - let leanOpts := config.leanOpts +def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) +: LoggerIO Unit := do + let {leanOpts, updateToolchain, ..} := config let ws ← loadWorkspaceRoot config - discard <| ws.updateAndMaterialize toUpdate leanOpts + discard <| ws.updateAndMaterialize toUpdate leanOpts updateToolchain diff --git a/src/lake/Lake/Toml/Data/DateTime.lean b/src/lake/Lake/Toml/Data/DateTime.lean index d201f3ce458e..4b4c9a7b3856 100644 --- a/src/lake/Lake/Toml/Data/DateTime.lean +++ b/src/lake/Lake/Toml/Data/DateTime.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +import Lake.Util.Date /-! # TOML Date-Time @@ -22,62 +23,10 @@ optionally left out, creating four distinct variants. namespace Lake.Toml -def lpad (s : String) (c : Char) (len : Nat) : String := - "".pushn c (len - s.length) ++ s - -def rpad (s : String) (c : Char) (len : Nat) : String := - s.pushn c (len - s.length) - -def zpad (n : Nat) (len : Nat) : String := - lpad (toString n) '0' len - -/-- A TOML date (year-month-day). -/ -structure Date where - year : Nat - month : Nat - day : Nat - deriving Inhabited, DecidableEq, Ord - -namespace Date - -abbrev IsLeapYear (y : Nat) : Prop := - y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0) - -abbrev IsValidMonth (m : Nat) : Prop := - m ≥ 1 ∧ m ≤ 12 - -def maxDay (y m : Nat) : Nat := - if m = 2 then - if IsLeapYear y then 29 else 28 - else if m ≤ 7 then - 30 + (m % 2) - else - 31 - (m % 2) - -abbrev IsValidDay (y m d : Nat) : Prop := - d ≥ 1 ∧ d ≤ maxDay y m - -def ofValid? (year month day : Nat) : Option Date := do - guard (IsValidMonth month ∧ IsValidDay year month day) - return {year, month, day} - -def ofString? (t : String) : Option Date := do - match t.split (· == '-') with - | [y,m,d] => - ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?) - | _ => none - -protected def toString (d : Date) : String := - s!"{zpad d.year 4}-{zpad d.month 2}-{zpad d.day 2}" - -instance : ToString Date := ⟨Date.toString⟩ - -end Date - /-- A TOML time (hour:minute:second.fraction). -We do not represent whole time as seconds to due to the possibility +We do not represent the whole time as seconds to due to the possibility of leap seconds in RFC 3339 times. -/ structure Time where diff --git a/src/lake/Lake/Util/Date.lean b/src/lake/Lake/Util/Date.lean new file mode 100644 index 000000000000..e49a21def12c --- /dev/null +++ b/src/lake/Lake/Util/Date.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2024 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ + +/-! +# Date + +A year-mont-day date. Used by Lake's TOML parser and its toolchain version +parser (for nightlies). +-/ + +namespace Lake + +def lpad (s : String) (c : Char) (len : Nat) : String := + "".pushn c (len - s.length) ++ s + +def rpad (s : String) (c : Char) (len : Nat) : String := + s.pushn c (len - s.length) + +def zpad (n : Nat) (len : Nat) : String := + lpad (toString n) '0' len + +/-- A date (year-month-day). -/ +structure Date where + year : Nat + month : Nat + day : Nat + deriving Inhabited, DecidableEq, Ord, Repr + +namespace Date + +instance : LT Date := ltOfOrd +instance : LE Date := leOfOrd +instance : Min Date := minOfLe +instance : Max Date := maxOfLe + +abbrev IsLeapYear (y : Nat) : Prop := + y % 4 = 0 ∧ (y % 100 ≠ 0 ∨ y % 400 = 0) + +abbrev IsValidMonth (m : Nat) : Prop := + m ≥ 1 ∧ m ≤ 12 + +def maxDay (y m : Nat) : Nat := + if m = 2 then + if IsLeapYear y then 29 else 28 + else if m ≤ 7 then + 30 + (m % 2) + else + 31 - (m % 2) + +abbrev IsValidDay (y m d : Nat) : Prop := + d ≥ 1 ∧ d ≤ maxDay y m + +def ofValid? (year month day : Nat) : Option Date := do + guard (IsValidMonth month ∧ IsValidDay year month day) + return {year, month, day} + +def ofString? (t : String) : Option Date := do + match t.split (· == '-') with + | [y,m,d] => + ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?) + | _ => none + +protected def toString (d : Date) : String := + s!"{zpad d.year 4}-{zpad d.month 2}-{zpad d.day 2}" + +instance : ToString Date := ⟨Date.toString⟩ diff --git a/src/lake/Lake/Util/Lift.lean b/src/lake/Lake/Util/Lift.lean index ae2a45d9d9f0..7dd0a21f83f3 100644 --- a/src/lake/Lake/Util/Lift.lean +++ b/src/lake/Lake/Util/Lift.lean @@ -5,33 +5,39 @@ Authors: Mac Malone -/ namespace Lake +instance (priority := low) [Monad m] [MonadExceptOf PUnit m] : Alternative m where + failure := throw () + orElse := tryCatch + /-- Ensure direct lifts are preferred over indirect ones. -/ instance (priority := high) [MonadLift α β] : MonadLiftT α β := ⟨MonadLift.monadLift⟩ -instance [Pure m] : MonadLiftT Id m where +instance (priority := low) [Pure m] : MonadLiftT Id m where monadLift act := pure act.run -instance [Alternative m] : MonadLiftT Option m where +instance (priority := low) [Alternative m] : MonadLiftT Option m where monadLift | some a => pure a | none => failure -instance [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m where +instance (priority := low) [Pure m] [MonadExceptOf ε m] : MonadLiftT (Except ε) m where monadLift | .ok a => pure a | .error e => throw e -instance [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m where +-- Remark: not necessarily optimal; uses context non-linearly +instance (priority := low) [Bind m] [MonadReaderOf ρ m] [MonadLiftT n m] : MonadLiftT (ReaderT ρ n) m where monadLift act := do act (← read) -instance [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m where +-- Remark: not necessarily optimal; uses state non-linearly +instance (priority := low) [Monad m] [MonadStateOf σ m] [MonadLiftT n m] : MonadLiftT (StateT σ n) m where monadLift act := do let (a, s) ← act (← get); set s; pure a -instance [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m where +instance (priority := low) [Monad m] [Alternative m] [MonadLiftT n m] : MonadLiftT (OptionT n) m where monadLift act := act.run >>= liftM -instance [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where +instance (priority := low) [Monad m] [MonadExceptOf ε m] [MonadLiftT n m] : MonadLiftT (ExceptT ε n) m where monadLift act := act.run >>= liftM -instance [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where +instance (priority := low) [Monad m] [MonadExceptOf ε m] [MonadLiftT BaseIO m] : MonadLiftT (EIO ε) m where monadLift act := act.toBaseIO >>= liftM diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean index dd34583cb9d4..2abf76ac54b5 100644 --- a/src/lake/Lake/Util/Log.lean +++ b/src/lake/Lake/Util/Log.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ import Lake.Util.Error import Lake.Util.EStateT +import Lake.Util.Lift import Lean.Data.Json import Lean.Message @@ -195,6 +196,9 @@ abbrev stream [MonadLiftT BaseIO m] (out : IO.FS.Stream) (minLv := LogLevel.info) (useAnsi := false) : MonadLog m where logEntry e := logToStream e out minLv useAnsi +@[inline] def error [Alternative m] [MonadLog m] (msg : String) : m α := + logError msg *> failure + end MonadLog def OutStream.logEntry @@ -404,7 +408,7 @@ from an `ELogT` (e.g., `LogIO`). (msg : String) : m α := errorWithLog (logError msg) -/-- `Alternative` instance for monads with `Log` state and `Log.Pos` errors. -/ +/-- `MonadError` instance for monads with `Log` state and `Log.Pos` errors. -/ abbrev ELog.monadError [Monad m] [MonadLog m] [MonadStateOf Log m] [MonadExceptOf Log.Pos m] : MonadError m := ⟨ELog.error⟩ @@ -505,7 +509,7 @@ abbrev run?' [Functor m] (self : ELogT m α) (log : Log := {}) : m (Option α) : Run `self` with the log taken from the state of the monad `n`, **Warning:** If lifting `self` from `m` to `n` fails, the log will be lost. -Thus, this is best used when the lift cannot fail. Note excludes the +Thus, this is best used when the lift cannot fail. This excludes the native log position failure of `ELogT`, which are lifted safely. -/ @[inline] def takeAndRun @@ -545,8 +549,6 @@ instance : MonadLift IO LogIO := ⟨MonadError.runIO⟩ namespace LogIO -@[deprecated ELogT.run? (since := "2024-05-18")] abbrev captureLog := @ELogT.run? - /-- Runs a `LogIO` action in `BaseIO`. Prints log entries of at least `minLv` to `out`. @@ -563,4 +565,46 @@ where replay (log : Log) (logger : MonadLog BaseIO) : BaseIO Unit := log.replay (logger := logger) +-- deprecated 2024-05-18, reversed 2024-10-18 +abbrev captureLog := @ELogT.run? + end LogIO + +/-- +A monad equipped with a log function and the ability to perform I/O. +Unlike `LogIO`, log entries are not retained by the monad but instead eagerly +passed to the log function. +-/ +abbrev LoggerIO := MonadLogT BaseIO (EIO PUnit) + +instance : MonadError LoggerIO := ⟨MonadLog.error⟩ +instance : MonadLift IO LoggerIO := ⟨MonadError.runIO⟩ +instance : MonadLift LogIO LoggerIO := ⟨ELogT.replayLog⟩ + +namespace LoggerIO + +/-- +Runs a `LoggerIO` action in `BaseIO`. +Prints log entries of at least `minLv` to `out`. +-/ +@[inline] def toBaseIO + (self : LoggerIO α) + (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr) +: BaseIO (Option α) := do + (·.toOption) <$> (self.run (← out.getLogger minLv ansiMode)).toBaseIO + +def captureLog (self : LoggerIO α) : BaseIO (Option α × Log) := do + let ref ← IO.mkRef ({} : Log) + let e ← self.run ⟨fun e => ref.modify (·.push e)⟩ |>.toBaseIO + return (e.toOption, ← ref.get) + +-- For parity with `LogIO.run?` +abbrev run? := @captureLog + +-- For parity with `LogIO.run?'` +@[inline] def run?' + (self : LoggerIO α) (logger : LogEntry → BaseIO PUnit := fun _ => pure ()) +: BaseIO (Option α) := do + (·.toOption) <$> (self.run ⟨logger⟩).toBaseIO + +end LoggerIO diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean index 72cb37b60277..24dcea7a0717 100644 --- a/src/lake/Lake/Util/MainM.lean +++ b/src/lake/Lake/Util/MainM.lean @@ -88,3 +88,12 @@ where log.replay (logger := logger) instance (priority := low) : MonadLift LogIO MainM := ⟨runLogIO⟩ + +@[inline] def runLoggerIO (x : LoggerIO α) + (minLv := LogLevel.info) (ansiMode := AnsiMode.auto) (out := OutStream.stderr) +: MainM α := do + let some a ← x.run (← out.getLogger minLv ansiMode) |>.toBaseIO + | exit 1 + return a + +instance (priority := low) : MonadLift LoggerIO MainM := ⟨runLoggerIO⟩ diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean index 1a96a5d3644c..8c16fec1e853 100644 --- a/src/lake/Lake/Util/Version.lean +++ b/src/lake/Lake/Util/Version.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lean.Elab.Eval +import Lake.Util.Date /-! # Version @@ -11,7 +12,7 @@ This module contains useful definitions for manipulating versions. It also defines a `v!""` syntax for version literals. -/ -open Lean +open System Lean namespace Lake @@ -117,6 +118,112 @@ instance : ToExpr StdVer where #[toExpr ver.toSemVerCore, toExpr ver.specialDescr] toTypeExpr := mkConst ``StdVer +/-- A Lean toolchain version. -/ +inductive ToolchainVer +| release (ver : LeanVer) +| nightly (date : Date) +| pr (no : Nat) +| other (name : String) +deriving Repr, DecidableEq + +instance : Coe LeanVer ToolchainVer := ⟨ToolchainVer.release⟩ + +def ToolchainVer.defaultOrigin := "leanprover/lean4" +def ToolchainVer.prOrigin := "leanprover/lean4-pr-releases" + +def ToolchainVer.ofString (ver : String) : ToolchainVer := Id.run do + let colonPos := ver.posOf ':' + let (origin, tag) := + if h : colonPos < ver.endPos then + let pos := ver.next' colonPos (by simp_all [h, String.endPos, String.atEnd]) + (ver.extract 0 colonPos, ver.extract pos ver.endPos) + else + ("", ver) + if tag.startsWith "v" then + if let .ok ver := StdVer.parse (tag.drop 1) then + if origin.isEmpty || origin == defaultOrigin then + return .release ver + return .other ver + else if tag.startsWith "nightly-" then + if let some date := Date.ofString? (tag.drop "nightly-".length) then + if origin.isEmpty || origin == defaultOrigin then + return .nightly date + else if tag.startsWith "pr-release-" then + if let some n := (tag.drop "pr-release-".length).toNat? then + if origin.isEmpty || origin == prOrigin then + return .pr n + else + if let .ok ver := StdVer.parse ver then + if origin.isEmpty || origin == defaultOrigin then + return .release ver + return .other ver + +/-- Parse a toolchain from a `lean-toolchain` file. -/ +def ToolchainVer.ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do + try + let toolchainString ← IO.FS.readFile toolchainFile + return some <| ToolchainVer.ofString toolchainString.trim + catch + | .noFileOrDirectory .. => + return none + | e => throw e + +/-- The `elan` toolchain file name (i.e., `lean-toolchain`). -/ +def toolchainFileName : FilePath := "lean-toolchain" + +/-- Parse a toolchain from the `lean-toolchain` file of the directory `dir`. -/ +@[inline] def ToolchainVer.ofDir? (dir : FilePath) : IO (Option ToolchainVer) := + ToolchainVer.ofFile? (dir / toolchainFileName) + +protected def ToolchainVer.toString (ver : ToolchainVer) : String := + match ver with + | .release ver => s!"{defaultOrigin}:v{ver}" + | .nightly date => s!"{defaultOrigin}:nightly-{date}" + | .pr n => s!"{prOrigin}:pr-release-{n}" + | .other s => s + +instance : ToString ToolchainVer := ⟨ToolchainVer.toString⟩ +instance : ToJson ToolchainVer := ⟨(·.toString)⟩ +instance : FromJson ToolchainVer := ⟨(ToolchainVer.ofString <$> fromJson? ·)⟩ + +protected def ToolchainVer.lt (a b : ToolchainVer) : Prop := + match a, b with + | .release v1, .release v2 => v1 < v2 + | .nightly d1, .nightly d2 => d1 < d2 + | _, _ => False + +instance : LT ToolchainVer := ⟨ToolchainVer.lt⟩ + +instance ToolchainVer.decLt (a b : ToolchainVer) : Decidable (a < b) := + match a, b with + | .release v1, .release v2 => inferInstanceAs (Decidable (v1 < v2)) + | .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 < d2)) + | .release _, .pr _ | .release _, .nightly _ | .release _, .other _ + | .nightly _, .release _ | .nightly _, .pr _ | .nightly _, .other _ + | .pr _, _ | .other _, _ => .isFalse (by simp [LT.lt, ToolchainVer.lt]) + +protected def ToolchainVer.le (a b : ToolchainVer) : Prop := + match a, b with + | .release v1, .release v2 => v1 ≤ v2 + | .nightly d1, .nightly d2 => d1 ≤ d2 + | .pr n1, .pr n2 => n1 = n2 + | .other v1, .other v2 => v1 = v2 + | _, _ => False + +instance : LE ToolchainVer := ⟨ToolchainVer.le⟩ + +instance ToolchainVer.decLe (a b : ToolchainVer) : Decidable (a ≤ b) := + match a, b with + | .release v1, .release v2 => inferInstanceAs (Decidable (v1 ≤ v2)) + | .nightly d1, .nightly d2 => inferInstanceAs (Decidable (d1 ≤ d2)) + | .pr n1, .pr n2 => inferInstanceAs (Decidable (n1 = n2)) + | .other v1, .other v2 => inferInstanceAs (Decidable (v1 = v2)) + | .release _, .pr _ | .release _, .nightly _ | .release _, .other _ + | .nightly _, .release _ | .nightly _, .pr _ | .nightly _, other _ + | .pr _, .release _ | .pr _, .nightly _ | .pr _, .other _ + | .other _, .release _ | .other _, .nightly _ | .other _, .pr _ => + .isFalse (by simp [LE.le, ToolchainVer.le]) + /-! ## Version Literals Defines the `v!""` syntax for version literals. @@ -134,6 +241,7 @@ export DecodeVersion (decodeVersion) instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩ @[default_instance] instance : DecodeVersion StdVer := ⟨StdVer.parse⟩ +instance : DecodeVersion ToolchainVer := ⟨(pure <| ToolchainVer.ofString ·)⟩ private def toResultExpr [ToExpr α] (x : Except String α) : Except String Expr := Functor.map toExpr x diff --git a/src/lake/examples/deps/bar/lake-manifest.expected.json b/src/lake/examples/deps/bar/lake-manifest.expected.json index 0313121dfd1d..068c60e836f5 100644 --- a/src/lake/examples/deps/bar/lake-manifest.expected.json +++ b/src/lake/examples/deps/bar/lake-manifest.expected.json @@ -3,31 +3,31 @@ "packages": [{"type": "path", "scope": "", - "name": "root", + "name": "foo", "manifestFile": "lake-manifest.json", - "inherited": true, - "dir": "./../foo/../a/../root", + "inherited": false, + "dir": "./../foo", "configFile": "lakefile.lean"}, {"type": "path", "scope": "", - "name": "a", + "name": "b", "manifestFile": "lake-manifest.json", "inherited": true, - "dir": "./../foo/../a", + "dir": "./../foo/./../b", "configFile": "lakefile.lean"}, {"type": "path", "scope": "", - "name": "b", + "name": "a", "manifestFile": "lake-manifest.json", "inherited": true, - "dir": "./../foo/../b", + "dir": "./../foo/./../a", "configFile": "lakefile.lean"}, {"type": "path", "scope": "", - "name": "foo", + "name": "root", "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "./../foo", + "inherited": true, + "dir": "./../foo/./../b/./../root", "configFile": "lakefile.lean"}], "name": "bar", "lakeDir": ".lake"} diff --git a/src/lake/examples/scripts/expected.out b/src/lake/examples/scripts/expected.out index bdd43a01fdb8..2a02d1f5e2eb 100644 --- a/src/lake/examples/scripts/expected.out +++ b/src/lake/examples/scripts/expected.out @@ -1,6 +1,6 @@ -dep/hello scripts/say-goodbye scripts/greet +dep/hello Hello, world! Hello, me! Hello, --me! @@ -16,8 +16,8 @@ Hello from Dep! Goodbye! error: unknown script nonexistent error: unknown script nonexistent -dep/hello scripts/say-goodbye scripts/greet +dep/hello Hello, world! Goodbye! diff --git a/src/lake/tests/clone/test.sh b/src/lake/tests/clone/test.sh index 102a454353b3..9b2a67bc08ce 100755 --- a/src/lake/tests/clone/test.sh +++ b/src/lake/tests/clone/test.sh @@ -17,6 +17,7 @@ fi mkdir hello pushd hello $LAKE init hello +rm -f lean-toolchain $LAKE update git init git checkout -b master @@ -34,7 +35,7 @@ cd test LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | grep --color "file://" # test that a second `lake update` is a no-op (with URLs) # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901 -LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update 2>&1 | diff - /dev/null +LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update --keep-toolchain 2>&1 | diff - /dev/null rm -rf .lake/packages # Test that Lake produces no warnings on a `lake build` after a `lake update` @@ -42,7 +43,7 @@ rm -rf .lake/packages $LAKE update # test that a second `lake update` is a no-op (with file paths) -$LAKE update 2>&1 | diff - /dev/null +$LAKE update --keep-toolchain 2>&1 | diff - /dev/null test -d .lake/packages/hello # test that Lake produces no warnings $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null diff --git a/src/lake/tests/depTree/test.sh b/src/lake/tests/depTree/test.sh index 46fd67b2172c..a5379ec0212f 100755 --- a/src/lake/tests/depTree/test.sh +++ b/src/lake/tests/depTree/test.sh @@ -75,8 +75,8 @@ pushd d git init git checkout -b master cat >>lakefile.lean <&1 | grep --color 'first commit in a' @@ -129,13 +129,20 @@ $LAKE update a -v git commit -am 'second commit in b' popd pushd a -# a@4 +# a@4/main sed_i 's/third commit/fourth commit/' A.lean git commit -am 'fourth commit in a' popd +pushd c +# c@2 +echo '-- second commit in c' >>C.lean +git commit -am 'second commit in c' +popd pushd d # d: b@1 -> b@2 => a@1 -> a@3 $LAKE update b -v +# test that Lake does not update c +grep --color 'second commit in c' .lake/packages/c/C.lean && exit 1 || true # test 119: pickup a@3 and not a@4 grep --color 'third commit in a' .lake/packages/a/A.lean # test the removal of `c` from the manifest diff --git a/src/lake/tests/env/test.sh b/src/lake/tests/env/test.sh index d1588a430e8b..f833ce74cea1 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 $LAKE env printenv LEAN_GITHASH $LAKE env printenv LEAN_SYSROOT $LAKE env printenv LEAN_AR | grep --color ar diff --git a/src/lake/tests/manifest/lake-manifest-v1.1.0.json b/src/lake/tests/manifest/lake-manifest-v1.1.0.json index 58b965f03bf6..595c92827bfe 100644 --- a/src/lake/tests/manifest/lake-manifest-v1.1.0.json +++ b/src/lake/tests/manifest/lake-manifest-v1.1.0.json @@ -1,14 +1,7 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"type": "path", - "scope": "", - "name": "foo", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "./foo", - "configFile": "lakefile.lean"}, - {"url": "bar", + [{"url": "bar", "type": "git", "subDir": null, "scope": "foo", @@ -17,6 +10,13 @@ "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "foo", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "./foo", "configFile": "lakefile.lean"}], "name": "«foo-bar»", "lakeDir": ".lake"} diff --git a/src/lake/tests/online/test.sh b/src/lake/tests/online/test.sh index 0b54313672a6..50ef0c2fd7b6 100755 --- a/src/lake/tests/online/test.sh +++ b/src/lake/tests/online/test.sh @@ -11,13 +11,13 @@ export ELAN_TOOLCHAIN=test grep --color "error: bogus/bogus: could not materialize package: dependency has no explicit source and was not found on Reservoir" ./clean.sh -$LAKE -f git.toml update +$LAKE -f git.toml update --keep-toolchain # Test that barrels are not fetched for non-Reservoir dependencies $LAKE -v -f git.toml build @Cli:extraDep | grep --color "Cli:optBarrel" && exit 1 || true ./clean.sh -$LAKE -f barrel.lean update +$LAKE -f barrel.lean update --keep-toolchain # Test that a barrel is not fetched for an unbuilt dependency $LAKE -v -f barrel.lean build @test:extraDep | grep --color "Cli:optBarrel" && exit 1 || true @@ -53,11 +53,11 @@ LEAN_GITHASH=ec3042d94bd11a42430f9e14d39e26b1f880f99b \ $LAKE -f barrel.lean build Cli --no-build ./clean.sh -$LAKE -f require.lean update -v +$LAKE -f require.lean update -v --keep-toolchain test -d .lake/packages/doc-gen4 $LAKE -f require.lean resolve-deps # validate manifest ./clean.sh -$LAKE -f require.toml update v +$LAKE -f require.toml update -v --keep-toolchain test -d .lake/packages/doc-gen4 $LAKE -f require.toml resolve-deps # validate manifest diff --git a/src/lake/tests/order/bar/lakefile.lean b/src/lake/tests/order/bar/lakefile.lean index e1680345396e..28c2ca1b65af 100644 --- a/src/lake/tests/order/bar/lakefile.lean +++ b/src/lake/tests/order/bar/lakefile.lean @@ -4,6 +4,7 @@ open Lake DSL package bar where moreLeanArgs := #["-DmaxHeartbeats=888000"] +require baz from ".." / "baz" require leaf from ".." / "leaf" with NameMap.empty.insert `val "888000" lean_lib X diff --git a/src/lake/tests/order/baz/X.lean b/src/lake/tests/order/baz/X.lean new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/src/lake/tests/order/baz/lakefile.lean b/src/lake/tests/order/baz/lakefile.lean new file mode 100644 index 000000000000..2ebcf3525454 --- /dev/null +++ b/src/lake/tests/order/baz/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package baz where + moreLeanArgs := #["-DmaxHeartbeats=999000"] + +lean_lib X diff --git a/src/lake/tests/order/clean.sh b/src/lake/tests/order/clean.sh index 46d55ed9cca7..3974b61a733e 100755 --- a/src/lake/tests/order/clean.sh +++ b/src/lake/tests/order/clean.sh @@ -1,3 +1,3 @@ -rm -rf .lake foo/.lake bar/.lake leaf/.lake -rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json leaf/lake-manifest.json +rm -rf .lake foo/.lake bar/.lake baz/.lake leaf/.lake +rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json baz/lake-manifest.json leaf/lake-manifest.json rm -f lake-manifest-1.json diff --git a/src/lake/tests/order/test.sh b/src/lake/tests/order/test.sh index f69f93e99456..8a99b861d93c 100755 --- a/src/lake/tests/order/test.sh +++ b/src/lake/tests/order/test.sh @@ -10,13 +10,13 @@ LAKE=${LAKE:-../../.lake/build/bin/lake} # Later packages and libraries in the dependency tree shadow earlier ones. # https://github.com/leanprover/lean4/issues/2548 -$LAKE update +$LAKE update -v $LAKE build +A -v | grep --color 222000 $LAKE build +A.B -v | grep --color 333000 $LAKE build +A.B.C -v | grep --color 333000 -$LAKE build +X -v | grep --color 888000 -$LAKE build +Y -v | grep --color 666000 -$LAKE build +Z -v | grep --color 666000 +$LAKE build +X -v | grep --color 888000 # bar +$LAKE build +Y -v | grep --color 666000 # order +$LAKE build +Z -v | grep --color 666000 # leaf from order $LAKE exe Y | grep --color root # Tests that `lake update` does not reorder packages in the manifest diff --git a/src/lake/tests/toolchain/.gitignore b/src/lake/tests/toolchain/.gitignore index 0661686d611d..afbd2ae7327f 100644 --- a/src/lake/tests/toolchain/.gitignore +++ b/src/lake/tests/toolchain/.gitignore @@ -1 +1,2 @@ /foo +lean-toolchain diff --git a/src/lake/tests/toolchain/clean.sh b/src/lake/tests/toolchain/clean.sh index 1cfb9dabe486..b635730fb08e 100755 --- a/src/lake/tests/toolchain/clean.sh +++ b/src/lake/tests/toolchain/clean.sh @@ -1 +1,2 @@ rm -rf foo +rm -f lake-manifest.json lean-toolchain diff --git a/src/lake/tests/toolchain/lakefile.lean b/src/lake/tests/toolchain/lakefile.lean new file mode 100644 index 000000000000..ec992f1b95c0 --- /dev/null +++ b/src/lake/tests/toolchain/lakefile.lean @@ -0,0 +1,6 @@ +import Lake +open System Lake DSL + +package test + +require foo from "foo" diff --git a/src/lake/tests/toolchain/test.sh b/src/lake/tests/toolchain/test.sh index f88356c3edae..16e86fe650cd 100755 --- a/src/lake/tests/toolchain/test.sh +++ b/src/lake/tests/toolchain/test.sh @@ -1,9 +1,9 @@ #!/usr/bin/env bash set -euxo pipefail -# Tests that Lake rebuilds when toolchain changes -# See https://github.com/leanprover/lake/issues/62 -# Requires Elan to download a toolchain +LAKE=${LAKE:-../../../.lake/build/bin/lake} + +# Tests which require Elan to download a toolchain # skip if no elan found if ! command -v elan > /dev/null; then @@ -11,9 +11,20 @@ if ! command -v elan > /dev/null; then exit 0 fi +# Test that Lake rebuilds when toolchain changes +# See https://github.com/leanprover/lake/issues/62 + +TOOLCHAIN=leanprover/lean4:v4.0.0 ./clean.sh -elan run --install leanprover/lean4:v4.0.0 lake new foo -cd foo -elan run leanprover/lean4:v4.0.0 lake build +Foo:olean -v | grep --color Foo.olean -rm lean-toolchain -${LAKE:-../../../.lake/build/bin/lake} build -v | grep --color Foo.olean +elan run --install $TOOLCHAIN lake new foo +pushd foo +elan run $TOOLCHAIN lake build +Foo:olean -v | grep --color Foo.olean +rm lean-toolchain # switch to Lake under test +$LAKE build -v | grep --color Foo.olean +popd + +# Test Lake runs under the new toolchain after Lake updates it +rm -f foo/lake-manifest.json +echo $TOOLCHAIN > foo/lean-toolchain +$LAKE update +grep --color -F '"version": 5' lake-manifest.json diff --git a/src/lake/tests/updateToolchain/.gitignore b/src/lake/tests/updateToolchain/.gitignore new file mode 100644 index 000000000000..12bf8dcaf61e --- /dev/null +++ b/src/lake/tests/updateToolchain/.gitignore @@ -0,0 +1 @@ +lean-toolchain diff --git a/src/lake/tests/updateToolchain/a/lakefile.toml b/src/lake/tests/updateToolchain/a/lakefile.toml new file mode 100644 index 000000000000..26f6be51c262 --- /dev/null +++ b/src/lake/tests/updateToolchain/a/lakefile.toml @@ -0,0 +1 @@ +name = "a" diff --git a/src/lake/tests/updateToolchain/b/lakefile.toml b/src/lake/tests/updateToolchain/b/lakefile.toml new file mode 100644 index 000000000000..0a8c2a67a5c4 --- /dev/null +++ b/src/lake/tests/updateToolchain/b/lakefile.toml @@ -0,0 +1 @@ +name = "b" diff --git a/src/lake/tests/updateToolchain/clean.sh b/src/lake/tests/updateToolchain/clean.sh new file mode 100755 index 000000000000..1ba7c542cc11 --- /dev/null +++ b/src/lake/tests/updateToolchain/clean.sh @@ -0,0 +1 @@ +rm -f lean-toolchain a/lean-toolchain b/lean-toolchain diff --git a/src/lake/tests/updateToolchain/lakefile.toml b/src/lake/tests/updateToolchain/lakefile.toml new file mode 100644 index 000000000000..4d6374a94fc5 --- /dev/null +++ b/src/lake/tests/updateToolchain/lakefile.toml @@ -0,0 +1,9 @@ +name = "test" + +[[require]] +name = "a" +path = "a" + +[[require]] +name = "b" +path = "b" diff --git a/src/lake/tests/updateToolchain/test.lean b/src/lake/tests/updateToolchain/test.lean new file mode 100644 index 000000000000..c15208018283 --- /dev/null +++ b/src/lake/tests/updateToolchain/test.lean @@ -0,0 +1,35 @@ +import Lake.Util.Version + +open Lake + +def checkParse (tc : String) := + IO.println <| repr <| ToolchainVer.ofString tc + +def checkLt (tc1 tc2 : String) := + IO.println <| decide <| ToolchainVer.ofString tc1 < ToolchainVer.ofString tc2 + +def test := do + IO.println "" + checkParse "leanprover/lean4:v4.13.0-rc1" + checkParse "leanprover/lean4:nightly-2024-09-15" + checkParse "leanprover/lean4-pr-releases:pr-release-101" + checkParse "leanprover/lean:v4.1.0" + checkParse "4.12.0" + checkLt "4.6.0-rc1" "v4.6.0" + checkLt "4.12.0" "leanprover/lean4:v4.13.0-rc1" + checkLt "nightly-2024-09-08" "nightly-2024-10-09" + checkLt "nightly-2024-09-08" "4.0.0" + +/-- +info: +Lake.ToolchainVer.release { toSemVerCore := { major := 4, minor := 13, patch := 0 }, specialDescr := "rc1" } +Lake.ToolchainVer.nightly { year := 2024, month := 9, day := 15 } +Lake.ToolchainVer.pr 101 +Lake.ToolchainVer.other "leanprover/lean:v4.1.0" +Lake.ToolchainVer.release { toSemVerCore := { major := 4, minor := 12, patch := 0 }, specialDescr := "" } +true +true +true +false +-/ +#guard_msgs in #eval test diff --git a/src/lake/tests/updateToolchain/test.sh b/src/lake/tests/updateToolchain/test.sh new file mode 100755 index 000000000000..094ca86e25fb --- /dev/null +++ b/src/lake/tests/updateToolchain/test.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LAKE=${LAKE:-../../.lake/build/bin/lake} + +# Ensure Lake thinks there is a elan environment configured +export ELAN_HOME= + +# Tests the toolchain update functionality of `lake update` + +RESTART_CODE=4 + +test_update(){ + ELAN=true $LAKE update 2>&1 | grep --color "updating toolchain to '$1'" + cat lean-toolchain | diff - <(echo -n "$1") +} + +# Test toolchain version API +$LAKE lean test.lean + +# Test no toolchain information +./clean.sh +$LAKE update 2>&1 | grep --color "toolchain not updated; no toolchain information found" + +# Test a single unknown candidate +./clean.sh +echo lean-a > a/lean-toolchain +test_update lean-a + +# Test a single known (PR) candidate +./clean.sh +echo pr-release-101 > a/lean-toolchain +test_update leanprover/lean4-pr-releases:pr-release-101 + +# Test release comparison +./clean.sh +echo v4.4.0 > a/lean-toolchain +echo v4.8.0 > b/lean-toolchain +test_update leanprover/lean4:v4.8.0 + +# Test nightly comparison +./clean.sh +echo nightly-2024-10-01 > a/lean-toolchain +echo nightly-2024-01-10 > b/lean-toolchain +test_update leanprover/lean4:nightly-2024-10-01 + +# Test up-to-date root +./clean.sh +echo v4.4.0 > a/lean-toolchain +echo v4.8.0 > b/lean-toolchain +echo v4.10.0 > lean-toolchain +$LAKE update 2>&1 | grep --color "toolchain not updated; already up-to-date" + +# Test multiple candidates +./clean.sh +echo lean-a > a/lean-toolchain +echo lean-b > b/lean-toolchain +$LAKE update 2>&1 | grep --color "toolchain not updated; multiple toolchain candidates" + +# Test manual restart +./clean.sh +echo lean-a > a/lean-toolchain +ELAN= $LAKE update 2>&1 && exit 1 || [ $? = $RESTART_CODE ] + +# Test elan restart +./clean.sh +echo lean-a > a/lean-toolchain +ELAN=echo $LAKE update | grep --color "run --install lean-a lake update"