From f3274d375a553462268b4d5ce0610ab60392248e Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 12 Jun 2024 23:22:47 -0400 Subject: [PATCH] refactor: lake: simplify load code (#4371) Simplifies the Lake dependency resolution code. Largely split from #3998. --- src/lake/Lake/CLI/Translate.lean | 2 +- src/lake/Lake/Config/Monad.lean | 24 +- src/lake/Lake/Config/Workspace.lean | 12 +- src/lake/Lake/Load.lean | 2 +- src/lake/Lake/Load/Lean.lean | 34 +++ src/lake/Lake/Load/{ => Lean}/Elab.lean | 9 +- src/lake/Lake/Load/Lean/Eval.lean | 168 ++++++++++++ src/lake/Lake/Load/Main.lean | 339 ------------------------ src/lake/Lake/Load/Materialize.lean | 26 +- src/lake/Lake/Load/Package.lean | 203 ++++---------- src/lake/Lake/Load/Resolve.lean | 304 +++++++++++++++++++++ src/lake/Lake/Load/Toml.lean | 7 +- src/lake/Lake/Load/Workspace.lean | 58 ++++ src/lake/Lake/Util/StoreInsts.lean | 6 +- src/lake/tests/order/bar/lakefile.lean | 4 +- src/lake/tests/order/clean.sh | 4 +- src/lake/tests/order/foo/lakefile.lean | 4 +- src/lake/tests/order/lakefile.lean | 2 + src/lake/tests/order/leaf/Z.lean | 0 src/lake/tests/order/leaf/lakefile.lean | 9 + src/lake/tests/order/test.sh | 3 +- 21 files changed, 685 insertions(+), 535 deletions(-) create mode 100644 src/lake/Lake/Load/Lean.lean rename src/lake/Lake/Load/{ => Lean}/Elab.lean (98%) create mode 100644 src/lake/Lake/Load/Lean/Eval.lean delete mode 100644 src/lake/Lake/Load/Main.lean create mode 100644 src/lake/Lake/Load/Resolve.lean create mode 100644 src/lake/Lake/Load/Workspace.lean create mode 100644 src/lake/tests/order/leaf/Z.lean create mode 100644 src/lake/tests/order/leaf/lakefile.lean diff --git a/src/lake/Lake/CLI/Translate.lean b/src/lake/Lake/CLI/Translate.lean index 41175786bf..9a75e638cf 100644 --- a/src/lake/Lake/CLI/Translate.lean +++ b/src/lake/Lake/CLI/Translate.lean @@ -3,11 +3,11 @@ 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.Load.Elab import Lake.Config.Lang import Lake.Config.Package import Lake.CLI.Translate.Toml import Lake.CLI.Translate.Lean +import Lake.Load.Lean.Elab import Lean.PrettyPrinter namespace Lake diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index 72e04134ed..0ac8db9607 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/src/lake/Lake/Config/Monad.lean @@ -26,8 +26,16 @@ abbrev LakeEnvT := ReaderT Lake.Env ReaderT.run self env /-- A monad equipped with a (read-only) Lake `Workspace`. -/ -abbrev MonadWorkspace (m : Type → Type u) := - MonadReaderOf Workspace m +class MonadWorkspace (m : Type → Type u) where + getWorkspace : m Workspace + +export MonadWorkspace (getWorkspace) + +instance [MonadReaderOf Workspace m] : MonadWorkspace m where + getWorkspace := read + +instance [MonadStateOf Workspace m] : MonadWorkspace m where + getWorkspace := get /-- A monad equipped with a (read-only) Lake context. -/ abbrev MonadLake (m : Type → Type u) := @@ -38,31 +46,27 @@ abbrev MonadLake (m : Type → Type u) := opaqueWs := ws instance [MonadWorkspace m] [Functor m] : MonadLake m where - read := (mkLakeContext ·) <$> read + read := (mkLakeContext ·) <$> getWorkspace @[inline] def Context.workspace (self : Context) := self.opaqueWs.get instance [MonadLake m] [Functor m] : MonadWorkspace m where - read := (·.workspace) <$> read + getWorkspace := (·.workspace) <$> read instance [MonadWorkspace m] [Functor m] : MonadLakeEnv m where - read := (·.lakeEnv) <$> read + read := (·.lakeEnv) <$> getWorkspace section variable [MonadWorkspace m] /-! ## Workspace Helpers -/ -/-- Get the workspace of the context. -/ -@[inline] def getWorkspace : m Workspace := - read - variable [Functor m] /-- Get the root package of the context's workspace. -/ @[inline] def getRootPackage : m Package := - (·.root) <$> read + (·.root) <$> getWorkspace @[inherit_doc Workspace.findPackage?, inline] def findPackage? (name : Name) : m (Option (NPackage name)) := diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index ac3acca4ba..36a9d2637e 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -71,11 +71,11 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace := {self with packages := self.packages.push pkg, packageMap := self.packageMap.insert pkg.name pkg} /-- Try to find a package within the workspace with the given name. -/ -@[inline] def findPackage? (name : Name) (self : Workspace) : Option (NPackage name) := +@[inline] protected def findPackage? (name : Name) (self : Workspace) : Option (NPackage name) := self.packageMap.find? name /-- Try to find a script in the workspace with the given name. -/ -def findScript? (script : Name) (self : Workspace) : Option Script := +protected def findScript? (script : Name) (self : Workspace) : Option Script := self.packages.findSomeRev? (·.scripts.find? script) /-- Check if the module is local to any package in the workspace. -/ @@ -87,7 +87,7 @@ def isBuildableModule (mod : Name) (self : Workspace) : Bool := self.packages.any fun pkg => pkg.isBuildableModule mod /-- Locate the named, buildable, importable, local module in the workspace. -/ -def findModule? (mod : Name) (self : Workspace) : Option Module := +protected def findModule? (mod : Name) (self : Workspace) : Option Module := self.packages.findSomeRev? (·.findModule? mod) /-- Locate the named, buildable, but not necessarily importable, module in the workspace. -/ @@ -95,15 +95,15 @@ def findTargetModule? (mod : Name) (self : Workspace) : Option Module := self.packages.findSomeRev? (·.findTargetModule? mod) /-- Try to find a Lean library in the workspace with the given name. -/ -def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib := +protected def findLeanLib? (name : Name) (self : Workspace) : Option LeanLib := self.packages.findSomeRev? fun pkg => pkg.findLeanLib? name /-- Try to find a Lean executable in the workspace with the given name. -/ -def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe := +protected def findLeanExe? (name : Name) (self : Workspace) : Option LeanExe := self.packages.findSomeRev? fun pkg => pkg.findLeanExe? name /-- Try to find an external library in the workspace with the given name. -/ -def findExternLib? (name : Name) (self : Workspace) : Option ExternLib := +protected def findExternLib? (name : Name) (self : Workspace) : Option ExternLib := self.packages.findSomeRev? fun pkg => pkg.findExternLib? name /-- Try to find a target configuration in the workspace with the given name. -/ diff --git a/src/lake/Lake/Load.lean b/src/lake/Lake/Load.lean index 11a8de7964..9b71d35bb7 100644 --- a/src/lake/Lake/Load.lean +++ b/src/lake/Lake/Load.lean @@ -3,4 +3,4 @@ Copyright (c) 2022 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ -import Lake.Load.Main +import Lake.Load.Workspace diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean new file mode 100644 index 0000000000..95fc736774 --- /dev/null +++ b/src/lake/Lake/Load/Lean.lean @@ -0,0 +1,34 @@ +/- +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.Load.Lean.Elab +import Lake.Load.Lean.Eval + +/-! # Lean Loader + +This module contains the main definitions to load a package from a +Lake configuration file written in Lake's Lean DSL. +-/ + +open Lean + +namespace Lake + +/-- +Elaborate a Lean configuration file into a `Package`. +The resulting package does not yet include any dependencies. +-/ +def loadLeanConfig (cfg : LoadConfig) +: LogIO (Package × Environment) := do + let configEnv ← importConfigFile cfg + let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv cfg.leanOpts + let pkg : Package := { + dir := cfg.pkgDir + relDir := cfg.relPkgDir + config := pkgConfig + relConfigFile := cfg.relConfigFile + remoteUrl? := cfg.remoteUrl? + } + return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv) diff --git a/src/lake/Lake/Load/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean similarity index 98% rename from src/lake/Lake/Load/Elab.lean rename to src/lake/Lake/Load/Lean/Elab.lean index 67cc4cb2b0..ae057ac421 100644 --- a/src/lake/Lake/Load/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -10,8 +10,15 @@ import Lake.Load.Config import Lake.Build.Trace import Lake.Util.Log +/-! # Lean Configuration Elaborator + +This module contains the definitions to elaborate a Lake configuration file. +-/ + + +open System Lean + namespace Lake -open Lean System deriving instance BEq, Hashable for Import diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean new file mode 100644 index 0000000000..2b3f6cc1ed --- /dev/null +++ b/src/lake/Lake/Load/Lean/Eval.lean @@ -0,0 +1,168 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.DSL.Attributes +import Lake.Config.Workspace + +/-! # Lean Configuration Evaluator + +This module contains the definitions to load Lake configuration objects from +a Lean environment elaborated from a Lake configuration file. +-/ + +open System Lean + +namespace Lake + +/-- Unsafe implementation of `evalConstCheck`. -/ +unsafe def unsafeEvalConstCheck (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α := + match env.find? const with + | none => throw s!"unknown constant '{const}'" + | some info => + match info.type with + | Expr.const c _ => + if c != type then + throwUnexpectedType + else + env.evalConst α opts const + | _ => throwUnexpectedType +where + throwUnexpectedType : Except String α := + throw s!"unexpected type at '{const}', `{type}` expected" + +/-- Like `Lean.Environment.evalConstCheck`, but with plain universe-polymorphic `Except`. -/ +@[implemented_by unsafeEvalConstCheck] opaque evalConstCheck +(env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α + +/-- Construct a `DNameMap` from the declarations tagged with `attr`. -/ +def mkTagMap +(env : Environment) (attr : OrderedTagAttribute) +[Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) := + let entries := attr.getAllEntries env + entries.foldlM (init := {}) fun map declName => + return map.insert declName <| ← f declName + +/-- Construct a `OrdNameMap` from the declarations tagged with `attr`. -/ +def mkOrdTagMap +(env : Environment) (attr : OrderedTagAttribute) +[Monad m] (f : (n : Name) → m β) : m (OrdNameMap β) := + let entries := attr.getAllEntries env + entries.foldlM (init := .mkEmpty entries.size) fun map declName => + return map.insert declName <| ← f declName + +/-- Load a `PackageConfig` from a configuration environment. -/ +def PackageConfig.loadFromEnv +(env : Environment) (opts := Options.empty) : Except String PackageConfig := do + let declName ← + match packageAttr.getAllEntries env |>.toList with + | [] => error s!"configuration file is missing a `package` declaration" + | [name] => pure name + | _ => error s!"configuration file has multiple `package` declarations" + evalConstCheck env opts _ ``PackageConfig declName + +/-- +Load the optional elements of a `Package` from the Lean environment. +This is done after loading its core configuration but before resolving +its dependencies. +-/ +def Package.loadFromEnv + (self : Package) (env : Environment) (opts : Options) +: LogIO Package := do + let strName := self.name.toString (escape := false) + + -- Load Script, Facet, Target, and Hook Configurations + let scripts ← mkTagMap env scriptAttr fun scriptName => do + let name := strName ++ "/" ++ scriptName.toString (escape := false) + let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn scriptName + return {name, fn, doc? := ← findDocString? env scriptName : Script} + let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name => + if let some script := scripts.find? name then pure script else + error s!"package is missing script `{name}` marked as a default" + let leanLibConfigs ← IO.ofExcept <| mkOrdTagMap env leanLibAttr fun name => + evalConstCheck env opts LeanLibConfig ``LeanLibConfig name + let leanExeConfigs ← IO.ofExcept <| mkOrdTagMap env leanExeAttr fun name => + evalConstCheck env opts LeanExeConfig ``LeanExeConfig name + let externLibConfigs ← mkTagMap env externLibAttr fun name => + match evalConstCheck env opts ExternLibDecl ``ExternLibDecl name with + | .ok decl => + if h : decl.pkg = self.config.name ∧ decl.name = name then + return h.1 ▸ h.2 ▸ decl.config + else + error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`" + | .error e => error e + let opaqueTargetConfigs ← mkTagMap env targetAttr fun name => + match evalConstCheck env opts TargetDecl ``TargetDecl name with + | .ok decl => + if h : decl.pkg = self.config.name ∧ decl.name = name then + return OpaqueTargetConfig.mk <| h.1 ▸ h.2 ▸ decl.config + else + error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`" + | .error e => error e + let defaultTargets := defaultTargetAttr.getAllEntries env + let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name => + match evalConstCheck env opts PostUpdateHookDecl ``PostUpdateHookDecl name with + | .ok decl => + if h : decl.pkg = self.config.name then + return OpaquePostUpdateHook.mk ⟨h ▸ decl.fn⟩ + else + error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`" + | .error e => error e + let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name => + evalConstCheck env opts Dependency ``Dependency name + let testDrivers := testDriverAttr.getAllEntries env + let testDriver ← + if testDrivers.size > 1 then + error s!"{self.name}: only one script, executable, or library can be tagged @[test_driver]" + else if h : testDrivers.size > 0 then + if self.config.testDriver.isEmpty then + pure (testDrivers[0]'h |>.toString) + else + error s!"{self.name}: cannot both set testDriver and use @[test_driver]" + else + pure self.config.testDriver + let lintDrivers := lintDriverAttr.getAllEntries env + let lintDriver ← + if lintDrivers.size > 1 then + error s!"{self.name}: only one script or executable can be tagged @[linter]" + else if h : lintDrivers.size > 0 then + if self.config.lintDriver.isEmpty then + pure (lintDrivers[0]'h |>.toString) + else + error s!"{self.name}: cannot both set linter and use @[linter]" + else + pure self.config.lintDriver + + -- Deprecation warnings + unless self.config.manifestFile.isNone do + logWarning s!"{self.name}: package configuration option `manifestFile` is deprecated" + unless self.config.moreServerArgs.isEmpty do + logWarning s!"{self.name}: package configuration option `moreServerArgs` is deprecated in favor of `moreServerOptions`" + + -- Fill in the Package + return {self with + depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs + opaqueTargetConfigs, defaultTargets, scripts, defaultScripts + testDriver, lintDriver, postUpdateHooks + } + +/-- +Load module/package facets into a `Workspace` from a configuration environment. +-/ +def Workspace.addFacetsFromEnv +(env : Environment) (opts : Options) (self : Workspace) : Except String Workspace := do + let mut ws := self + for name in moduleFacetAttr.getAllEntries env do + match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with + | .ok decl => ws := ws.addModuleFacetConfig <| decl.config + | .error e => error e + for name in packageFacetAttr.getAllEntries env do + match evalConstCheck env opts PackageFacetDecl ``PackageFacetDecl name with + | .ok decl => ws := ws.addPackageFacetConfig <| decl.config + | .error e => error e + for name in libraryFacetAttr.getAllEntries env do + match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with + | .ok decl => ws := ws.addLibraryFacetConfig <| decl.config + | .error e => error e + return ws diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean deleted file mode 100644 index 3620cbb81b..0000000000 --- a/src/lake/Lake/Load/Main.lean +++ /dev/null @@ -1,339 +0,0 @@ -/- -Copyright (c) 2022 Mac Malone. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mac Malone, Gabriel Ebner --/ -import Lake.Util.EStateT -import Lake.Util.StoreInsts -import Lake.Config.Workspace -import Lake.Build.Topological -import Lake.Build.Module -import Lake.Build.Package -import Lake.Build.Library -import Lake.Load.Materialize -import Lake.Load.Package -import Lake.Load.Elab -import Lake.Load.Toml - -open System Lean - -/-! # Loading a Workspace -The main definitions for loading a workspace and resolving dependencies. --/ - -namespace Lake - -/-- -Elaborate a dependency's Lean configuration file into a `Package`. -The resulting package does not yet include any dependencies. --/ -def loadLeanConfig (cfg : LoadConfig) -: LogIO (Package × Environment) := do - let configEnv ← importConfigFile cfg - let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv cfg.leanOpts - let pkg : Package := { - dir := cfg.pkgDir - relDir := cfg.relPkgDir - config := pkgConfig - relConfigFile := cfg.relConfigFile - remoteUrl? := cfg.remoteUrl? - } - return (← pkg.loadFromEnv configEnv cfg.leanOpts, configEnv) - -/-- -Return whether a configuration file with the given name -and/or a supported extension exists. --/ -def configFileExists (cfgFile : FilePath) : BaseIO Bool := - if cfgFile.extension.isSome then - cfgFile.pathExists - else - let leanFile := cfgFile.addExtension "lean" - let tomlFile := cfgFile.addExtension "toml" - leanFile.pathExists <||> tomlFile.pathExists - -/-- Loads a Lake package configuration (either Lean or TOML). -/ -def loadPackageCore - (name : String) (cfg : LoadConfig) -: LogIO (Package × Option Environment) := do - if let some ext := cfg.relConfigFile.extension then - unless (← cfg.configFile.pathExists) do - error s!"{name}: configuration file not found: {cfg.configFile}" - match ext with - | "lean" => (·.map id some) <$> loadLeanConfig cfg - | "toml" => ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir cfg.relConfigFile - | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}" - else - let relLeanFile := cfg.relConfigFile.addExtension "lean" - let relTomlFile := cfg.relConfigFile.addExtension "toml" - let leanFile := cfg.pkgDir / relLeanFile - let tomlFile := cfg.pkgDir / relTomlFile - let leanExists ← leanFile.pathExists - let tomlExists ← tomlFile.pathExists - if leanExists then - if tomlExists then - logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}" - (·.map id some) <$> loadLeanConfig {cfg with relConfigFile := relLeanFile} - else - if tomlExists then - ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir relTomlFile - else - error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}" - -/-- -Loads the package configuration of a materialized dependency. -Adds the facets defined in the package to the `Workspace`. --/ -def loadDepPackage - (dep : MaterializedDep) (leanOpts : Options) (reconfigure : Bool) -: StateT Workspace LogIO Package := fun ws => do - let name := dep.name.toString (escape := false) - let (pkg, env?) ← loadPackageCore name { - lakeEnv := ws.lakeEnv - wsDir := ws.dir - relPkgDir := dep.relPkgDir - relConfigFile := dep.configFile - lakeOpts := dep.configOpts - leanOpts - reconfigure - remoteUrl? := dep.remoteUrl? - } - if let some env := env? then - let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts - return (pkg, ws) - else - return (pkg, ws) - -/-- -Load a `Workspace` for a Lake package by elaborating its configuration file. -Does not resolve dependencies. --/ -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 - moduleFacetConfigs := initModuleFacetConfigs - packageFacetConfigs := initPackageFacetConfigs - libraryFacetConfigs := initLibraryFacetConfigs - } - if let some env := env? then - IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts - else - return ws - -/-- Loads a Lake package as a single independent object (without dependencies). -/ -def loadPackage (config : LoadConfig) : LogIO Package := do - Lean.searchPathRef.set config.lakeEnv.leanSearchPath - (·.1) <$> loadPackageCore "[root]" config - -/-- Recursively visits a package dependency graph, avoiding cycles. -/ -private def resolveDepsAcyclic - [Monad m] [MonadError m] - (root : Package) (f : RecFetchFn Package α (CycleT Name m)) -: m α := do - match (← ExceptT.run <| recFetchAcyclic (·.name) f root []) with - | .ok s => pure s - | .error cycle => - let cycle := cycle.map (s!" {·}") - error s!"dependency cycle detected:\n{"\n".intercalate cycle}" - -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} - -" - -/-- -Rebuild the workspace's Lake manifest and materialize missing dependencies. - -Packages 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. - -If `reconfigure`, elaborate configuration files while updating, do not use OLeans. --/ -def Workspace.updateAndMaterialize - (ws : Workspace) (leanOpts : Options := {}) - (toUpdate : NameSet := {}) (reconfigure := true) -: LogIO Workspace := do - let ((root, deps), ws) ← - StateT.run (s := ws) <| StateT.run (s := mkNameMap MaterializedDep) <| - StateT.run' (s := mkNameMap PackageEntry) <| StateT.run' (s := mkNameMap Package) do - -- Use manifest versions of root packages that should not be updated - let rootName := ws.root.name.toString (escape := false) - match (← Manifest.load ws.manifestFile |>.toBaseIO) with - | .ok manifest => - unless toUpdate.isEmpty do - manifest.packages.forM fun entry => do - unless entry.inherited || toUpdate.contains entry.name do - modifyThe (NameMap PackageEntry) (·.insert entry.name entry) - if let some oldRelPkgsDir := manifest.packagesDir? then - let oldPkgsDir := ws.dir / oldRelPkgsDir - if oldRelPkgsDir.normalize != ws.relPkgsDir.normalize && (← oldPkgsDir.pathExists) then - logInfo s!"workspace packages directory changed; renaming '{oldPkgsDir}' to '{ws.pkgsDir}'" - let doRename : IO Unit := do - createParentDirs ws.pkgsDir - IO.FS.rename oldPkgsDir ws.pkgsDir - if let .error e ← doRename.toBaseIO then - error s!"could not rename workspace packages directory: {e}" - | .error (.noFileOrDirectory ..) => - logInfo s!"{rootName}: no previous manifest, creating one from scratch" - | .error e => - unless toUpdate.isEmpty do - liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update` - logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}" - resolveDepsAcyclic ws.root fun pkg resolve => do - if let some pkg := (← getThe Workspace).findPackage? pkg.name then - return pkg - let inherited := pkg.name != ws.root.name - -- Materialize this package's dependencies first - let deps ← pkg.depConfigs.mapM fun dep => fetchOrCreate dep.name do - if let some entry := (← getThe (NameMap PackageEntry)).find? dep.name then - entry.materialize dep ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap - else - dep.materialize inherited ws.dir ws.relPkgsDir pkg.relDir ws.lakeEnv.pkgUrlMap - -- Load dependency packages and materialize their locked dependencies - let deps ← deps.mapM fun dep => do - if let some pkg := (← getThe (NameMap Package)).find? dep.name then - return pkg - else - -- Load the package - let depPkg ← liftM <| loadDepPackage dep leanOpts reconfigure - if depPkg.name ≠ dep.name then - if dep.name = .mkSimple "std" then - let rev := - match dep.manifestEntry.src with - | .git (inputRev? := some rev) .. => s!" @ {repr rev}" - | _ => "" - logError (stdMismatchError depPkg.name.toString rev) - try - IO.FS.removeDirAll depPkg.dir -- cleanup - catch e => - -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows - 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}'" - -- Materialize locked dependencies - match (← Manifest.load depPkg.manifestFile |>.toBaseIO) with - | .ok manifest => - manifest.packages.forM fun entry => do - unless (← getThe (NameMap PackageEntry)).contains entry.name do - let entry := entry.setInherited.inDirectory dep.relPkgDir - modifyThe (NameMap PackageEntry) (·.insert entry.name entry) - | .error (.noFileOrDirectory ..) => - logWarning s!"{depPkg.name}: ignoring missing dependency manifest '{depPkg.manifestFile}'" - | .error e => - logWarning s!"{depPkg.name}: ignoring dependency manifest because it failed to load: {e}" - modifyThe (NameMap Package) (·.insert dep.name depPkg) - return depPkg - -- Resolve dependencies's dependencies recursively - let pkg := {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)} - modifyThe Workspace (·.addPackage pkg) - return pkg - let ws : Workspace := {ws with root} - let manifest : Manifest := { - name := ws.root.name - lakeDir := ws.relLakeDir - packagesDir? := ws.relPkgsDir - } - let manifest := ws.packages.foldl (init := manifest) fun manifest pkg => - match deps.find? pkg.name with - | some dep => manifest.addPackage <| - dep.manifestEntry.setManifestFile pkg.relManifestFile |>.setConfigFile pkg.relConfigFile - | none => manifest -- should only be the case for the root - 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 - return ws - -/-- -Resolving a workspace's dependencies using a manifest, -downloading and/or updating them as necessary. --/ -def Workspace.materializeDeps - (ws : Workspace) (manifest : Manifest) - (leanOpts : Options := {}) (reconfigure := false) -: LogIO Workspace := do - if !manifest.packages.isEmpty && manifest.packagesDir? != some (mkRelPathString ws.relPkgsDir) then - logWarning <| - "manifest out of date: packages directory changed; " ++ - "use `lake update` to rebuild the manifest (warning: this will update ALL workspace dependencies)" - let relPkgsDir := manifest.packagesDir?.getD ws.relPkgsDir - let pkgEntries := manifest.packages.foldl (init := mkNameMap PackageEntry) - fun map entry => map.insert entry.name entry - let rootPkg := ws.root - let (root, ws) ← StateT.run (s := ws) <| StateT.run' (s := mkNameMap Package) do - resolveDepsAcyclic rootPkg fun pkg resolve => do - if let some pkg := (← getThe Workspace).findPackage? pkg.name then - return pkg - let topLevel := pkg.name = rootPkg.name - let deps := pkg.depConfigs - if topLevel then - if manifest.packages.isEmpty && !deps.isEmpty then - error "missing manifest; use `lake update` to generate one" - for dep in deps do - let warnOutOfDate (what : String) := - logWarning <| - s!"manifest out of date: {what} of dependency '{dep.name}' changed; " ++ - s!"use `lake update {dep.name}` to update it" - if let .some entry := pkgEntries.find? dep.name then - match dep.src, entry.src with - | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev') .. => - if url ≠ url' then warnOutOfDate "git url" - if rev ≠ rev' then warnOutOfDate "git revision" - | .path .., .path .. => pure () - | _, _ => warnOutOfDate "source kind (git/path)" - let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do - if let some entry := pkgEntries.find? dep.name then - let ws ← getThe Workspace - let result ← entry.materialize dep ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap - liftM <| loadDepPackage result leanOpts reconfigure - else if topLevel then - error <| - s!"dependency '{dep.name}' not in manifest; " ++ - s!"use `lake update {dep.name}` to add it" - else - error <| - s!"dependency '{dep.name}' of '{pkg.name}' not in manifest; " ++ - "this suggests that the manifest is corrupt;" ++ - "use `lake update` to generate a new, complete file (warning: this will update ALL workspace dependencies)" - let pkg := {pkg with opaqueDeps := ← depPkgs.mapM (.mk <$> resolve ·)} - modifyThe Workspace (·.addPackage pkg) - return pkg - return {ws with root} - -/-- -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 - let ws ← loadWorkspaceRoot config - if updateDeps then - ws.updateAndMaterialize leanOpts {} rc - else if let some manifest ← Manifest.load? ws.manifestFile then - ws.materializeDeps manifest leanOpts rc - else - ws.updateAndMaterialize leanOpts {} rc - -/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/ -def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do - let rc := config.reconfigure - let leanOpts := config.leanOpts - let ws ← loadWorkspaceRoot config - discard <| ws.updateAndMaterialize leanOpts toUpdate rc diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean index a3df21c913..0ae5975811 100644 --- a/src/lake/Lake/Load/Materialize.lean +++ b/src/lake/Lake/Load/Materialize.lean @@ -81,8 +81,6 @@ structure MaterializedDep where remoteUrl? : Option String /-- The manifest entry for the dependency. -/ manifestEntry : PackageEntry - /-- The configuration-specified dependency. -/ - configDep : Dependency deriving Inhabited @[inline] def MaterializedDep.name (self : MaterializedDep) := @@ -96,16 +94,13 @@ structure MaterializedDep where @[inline] def MaterializedDep.configFile (self : MaterializedDep) := self.manifestEntry.configFile - /-- Lake configuration options for the dependency. -/ -@[inline] def MaterializedDep.configOpts (self : MaterializedDep) := - self.configDep.opts - /-- Materializes a configuration dependency. For Git dependencies, updates it to the latest input revision. -/ -def Dependency.materialize (dep : Dependency) (inherited : Bool) -(wsDir relPkgsDir relParentDir : FilePath) (pkgUrlMap : NameMap String) +def Dependency.materialize + (dep : Dependency) (inherited : Bool) + (lakeEnv : Env) (wsDir relPkgsDir relParentDir : FilePath) : LogIO MaterializedDep := match dep.src with | .path dir => @@ -114,13 +109,12 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool) relPkgDir remoteUrl? := none manifestEntry := mkEntry <| .path relPkgDir - configDep := dep } | .git url inputRev? subDir? => do let sname := dep.name.toString (escape := false) let relGitDir := relPkgsDir / sname let repo := GitRepo.mk (wsDir / relGitDir) - let materializeUrl := pkgUrlMap.find? dep.name |>.getD url + let materializeUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD url materializeGitRepo sname repo materializeUrl inputRev? let rev ← repo.getHeadRevision let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir @@ -128,7 +122,6 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool) relPkgDir remoteUrl? := Git.filterUrl? url manifestEntry := mkEntry <| .git url rev inputRev? subDir? - configDep := dep } where mkEntry src : PackageEntry := {name := dep.name, inherited, src} @@ -136,8 +129,9 @@ where /-- Materializes a manifest package entry, cloning and/or checking it out as necessary. -/ -def PackageEntry.materialize (manifestEntry : PackageEntry) -(configDep : Dependency) (wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String) +def PackageEntry.materialize + (manifestEntry : PackageEntry) + (lakeEnv : Env) (wsDir relPkgsDir : FilePath) : LogIO MaterializedDep := match manifestEntry.src with | .path (dir := relPkgDir) .. => @@ -145,7 +139,6 @@ def PackageEntry.materialize (manifestEntry : PackageEntry) relPkgDir remoteUrl? := none manifestEntry - configDep } | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do let sname := manifestEntry.name.toString (escape := false) @@ -163,15 +156,14 @@ def PackageEntry.materialize (manifestEntry : PackageEntry) if (← repo.hasDiff) then logWarning s!"{sname}: repository '{repo.dir}' has local changes" else - let url := pkgUrlMap.find? manifestEntry.name |>.getD url + let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url updateGitRepo sname repo url rev else - let url := pkgUrlMap.find? manifestEntry.name |>.getD url + 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 manifestEntry - configDep } diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index a536baf906..b287e0fd5f 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/src/lake/Lake/Load/Package.lean @@ -1,166 +1,65 @@ /- -Copyright (c) 2021 Mac Malone. All rights reserved. +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.DSL.Attributes -import Lake.Config.Workspace +import Lake.Load.Lean +import Lake.Load.Toml -/-! -This module contains definitions to load configuration objects from -a package configuration file (e.g., `lakefile.lean`). +/-! # Package Loader + +This module contains the main definitions to load a package +from Lake configuration file (either Lean or TOML). -/ +open Lean + namespace Lake -open Lean System - -/-- Unsafe implementation of `evalConstCheck`. -/ -unsafe def unsafeEvalConstCheck (env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α := - match env.find? const with - | none => throw s!"unknown constant '{const}'" - | some info => - match info.type with - | Expr.const c _ => - if c != type then - throwUnexpectedType - else - env.evalConst α opts const - | _ => throwUnexpectedType -where - throwUnexpectedType : Except String α := - throw s!"unexpected type at '{const}', `{type}` expected" - -/-- Like `Lean.Environment.evalConstCheck`, but with plain universe-polymorphic `Except`. -/ -@[implemented_by unsafeEvalConstCheck] opaque evalConstCheck -(env : Environment) (opts : Options) (α) (type : Name) (const : Name) : Except String α - -/-- Construct a `DNameMap` from the declarations tagged with `attr`. -/ -def mkTagMap -(env : Environment) (attr : OrderedTagAttribute) -[Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) := - let entries := attr.getAllEntries env - entries.foldlM (init := {}) fun map declName => - return map.insert declName <| ← f declName - -/-- Construct a `OrdNameMap` from the declarations tagged with `attr`. -/ -def mkOrdTagMap -(env : Environment) (attr : OrderedTagAttribute) -[Monad m] (f : (n : Name) → m β) : m (OrdNameMap β) := - let entries := attr.getAllEntries env - entries.foldlM (init := .mkEmpty entries.size) fun map declName => - return map.insert declName <| ← f declName - -/-- Load a `PackageConfig` from a configuration environment. -/ -def PackageConfig.loadFromEnv -(env : Environment) (opts := Options.empty) : Except String PackageConfig := do - let declName ← - match packageAttr.getAllEntries env |>.toList with - | [] => error s!"configuration file is missing a `package` declaration" - | [name] => pure name - | _ => error s!"configuration file has multiple `package` declarations" - evalConstCheck env opts _ ``PackageConfig declName /-- -Load the optional elements of a `Package` from the Lean environment. -This is done after loading its core configuration but before resolving -its dependencies. +Return whether a configuration file with the given name +and/or a supported extension exists. -/ -def Package.loadFromEnv - (self : Package) (env : Environment) (opts : Options) -: LogIO Package := do - let strName := self.name.toString (escape := false) - - -- Load Script, Facet, Target, and Hook Configurations - let scripts ← mkTagMap env scriptAttr fun scriptName => do - let name := strName ++ "/" ++ scriptName.toString (escape := false) - let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn scriptName - return {name, fn, doc? := ← findDocString? env scriptName : Script} - let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name => - if let some script := scripts.find? name then pure script else - error s!"package is missing script `{name}` marked as a default" - let leanLibConfigs ← IO.ofExcept <| mkOrdTagMap env leanLibAttr fun name => - evalConstCheck env opts LeanLibConfig ``LeanLibConfig name - let leanExeConfigs ← IO.ofExcept <| mkOrdTagMap env leanExeAttr fun name => - evalConstCheck env opts LeanExeConfig ``LeanExeConfig name - let externLibConfigs ← mkTagMap env externLibAttr fun name => - match evalConstCheck env opts ExternLibDecl ``ExternLibDecl name with - | .ok decl => - if h : decl.pkg = self.config.name ∧ decl.name = name then - return h.1 ▸ h.2 ▸ decl.config - else - error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`" - | .error e => error e - let opaqueTargetConfigs ← mkTagMap env targetAttr fun name => - match evalConstCheck env opts TargetDecl ``TargetDecl name with - | .ok decl => - if h : decl.pkg = self.config.name ∧ decl.name = name then - return OpaqueTargetConfig.mk <| h.1 ▸ h.2 ▸ decl.config - else - error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`" - | .error e => error e - let defaultTargets := defaultTargetAttr.getAllEntries env - let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name => - match evalConstCheck env opts PostUpdateHookDecl ``PostUpdateHookDecl name with - | .ok decl => - if h : decl.pkg = self.config.name then - return OpaquePostUpdateHook.mk ⟨h ▸ decl.fn⟩ - else - error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`" - | .error e => error e - let depConfigs ← IO.ofExcept <| packageDepAttr.getAllEntries env |>.mapM fun name => - evalConstCheck env opts Dependency ``Dependency name - let testDrivers := testDriverAttr.getAllEntries env - let testDriver ← - if testDrivers.size > 1 then - error s!"{self.name}: only one script, executable, or library can be tagged @[test_driver]" - else if h : testDrivers.size > 0 then - if self.config.testDriver.isEmpty then - pure (testDrivers[0]'h |>.toString) - else - error s!"{self.name}: cannot both set testDriver and use @[test_driver]" - else - pure self.config.testDriver - let lintDrivers := lintDriverAttr.getAllEntries env - let lintDriver ← - if lintDrivers.size > 1 then - error s!"{self.name}: only one script or executable can be tagged @[linter]" - else if h : lintDrivers.size > 0 then - if self.config.lintDriver.isEmpty then - pure (lintDrivers[0]'h |>.toString) - else - error s!"{self.name}: cannot both set linter and use @[linter]" - else - pure self.config.lintDriver - - -- Deprecation warnings - unless self.config.manifestFile.isNone do - logWarning s!"{self.name}: package configuration option `manifestFile` is deprecated" - unless self.config.moreServerArgs.isEmpty do - logWarning s!"{self.name}: package configuration option `moreServerArgs` is deprecated in favor of `moreServerOptions`" - - -- Fill in the Package - return {self with - depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs - opaqueTargetConfigs, defaultTargets, scripts, defaultScripts - testDriver, lintDriver, postUpdateHooks - } +def configFileExists (cfgFile : FilePath) : BaseIO Bool := + if cfgFile.extension.isSome then + cfgFile.pathExists + else + let leanFile := cfgFile.addExtension "lean" + let tomlFile := cfgFile.addExtension "toml" + leanFile.pathExists <||> tomlFile.pathExists /-- -Load module/package facets into a `Workspace` from a configuration environment. +Loads a Lake package configuration (either Lean or TOML). +The resulting package does not yet include any dependencies. -/ -def Workspace.addFacetsFromEnv -(env : Environment) (opts : Options) (self : Workspace) : Except String Workspace := do - let mut ws := self - for name in moduleFacetAttr.getAllEntries env do - match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with - | .ok decl => ws := ws.addModuleFacetConfig <| decl.config - | .error e => error e - for name in packageFacetAttr.getAllEntries env do - match evalConstCheck env opts PackageFacetDecl ``PackageFacetDecl name with - | .ok decl => ws := ws.addPackageFacetConfig <| decl.config - | .error e => error e - for name in libraryFacetAttr.getAllEntries env do - match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with - | .ok decl => ws := ws.addLibraryFacetConfig <| decl.config - | .error e => error e - return ws +def loadPackageCore + (name : String) (cfg : LoadConfig) +: LogIO (Package × Option Environment) := do + if let some ext := cfg.relConfigFile.extension then + unless (← cfg.configFile.pathExists) do + error s!"{name}: configuration file not found: {cfg.configFile}" + match ext with + | "lean" => (·.map id some) <$> loadLeanConfig cfg + | "toml" => ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir cfg.relConfigFile + | _ => error s!"{name}: configuration has unsupported file extension: {cfg.configFile}" + else + let relLeanFile := cfg.relConfigFile.addExtension "lean" + let relTomlFile := cfg.relConfigFile.addExtension "toml" + let leanFile := cfg.pkgDir / relLeanFile + let tomlFile := cfg.pkgDir / relTomlFile + let leanExists ← leanFile.pathExists + let tomlExists ← tomlFile.pathExists + if leanExists then + if tomlExists then + logInfo s!"{name}: {relLeanFile} and {relTomlFile} are both present; using {relLeanFile}" + (·.map id some) <$> loadLeanConfig {cfg with relConfigFile := relLeanFile} + else + if tomlExists then + ((·,none)) <$> loadTomlConfig cfg.pkgDir cfg.relPkgDir relTomlFile + else + error s!"{name}: no configuration file with a supported extension:\n{leanFile}\n{tomlFile}" + +/-- Loads a Lake package as a single independent object (without dependencies). -/ +def loadPackage (config : LoadConfig) : LogIO Package := do + Lean.searchPathRef.set config.lakeEnv.leanSearchPath + (·.1) <$> loadPackageCore "[root]" config diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean new file mode 100644 index 0000000000..921549875a --- /dev/null +++ b/src/lake/Lake/Load/Resolve.lean @@ -0,0 +1,304 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone, Gabriel Ebner +-/ +import Lake.Config.Monad +import Lake.Util.StoreInsts +import Lake.Build.Topological +import Lake.Load.Materialize +import Lake.Load.Package + +open System Lean + +/-! # Dependency Resolution + +This module contains definitions for resolving the dependencies of a package. +-/ + +namespace Lake + +/-- +Loads the package configuration of a materialized dependency. +Adds the facets defined in the package to the `Workspace`. +-/ +def loadDepPackage + (dep : MaterializedDep) + (lakeOpts : NameMap String) + (leanOpts : Options) (reconfigure : Bool) +: StateT Workspace LogIO Package := fun ws => do + let name := dep.name.toString (escape := false) + let (pkg, env?) ← loadPackageCore name { + lakeEnv := ws.lakeEnv + wsDir := ws.dir + relPkgDir := dep.relPkgDir + relConfigFile := dep.configFile + lakeOpts, leanOpts, reconfigure + remoteUrl? := dep.remoteUrl? + } + if let some env := env? then + let ws ← IO.ofExcept <| ws.addFacetsFromEnv env leanOpts + return (pkg, ws) + else + return (pkg, ws) + +/-- The monad of the dependency resolver. -/ +abbrev ResolveT m := CallStackT Name <| StateT Workspace m + +@[inline] nonrec def ResolveT.run (ws : Workspace) (x : ResolveT m α) (stack : CallStack Name := {}) : m (α × Workspace) := + x.run stack |>.run ws + +/-- 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 + throwCycle := depCycleError + +/-- +Recursively visits the workspace dependency graph, starting from `root`. +At each package, performs `f` to resolve the dependencies of a package, +recurses, then adds the package to workspace's package set. +Errors if a cycle is encountered. + +**Traversal Order** + +All dependencies of a package are visited in order before recursing to the +dependencies' dependencies. For example, given the dependency graph: + +``` +R +|- A +|- B + |- X + |- Y +|- C +``` + +Lake follows the order `R`, `A`, `B`, `C`, `X`, `Y`. + +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. + +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. +-/ +@[inline] def Workspace.resolveDeps + [Monad m] [MonadError m] (ws : Workspace) + (f : Package → Dependency → ResolveT m Package) +: m Workspace := do + let (root, ws) ← ResolveT.run ws <| StateT.run' (s := {}) <| + recFetchAcyclic (·.name) go ws.root + return {ws with root} +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 + if pkg.name = dep.name then + error s!"{pkg.name}: package requires itself (or a package with the same name)" + let dep ← f pkg dep -- package w/o dependencies + store dep.name dep + let deps ← pkg.depConfigs.mapM fun dep => do + if let some dep ← fetch? dep.name then + modifyThe (NameMap Package) (·.erase dep.name) -- for `dep` linearity + return OpaquePackage.mk (← resolve dep) + 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} + +" + +/-- +The monad of the manifest updater. +It is equipped with and entry map entries for the updated manifest. +-/ +abbrev UpdateT := StateT (NameMap PackageEntry) + +@[inline] nonrec def UpdateT.run (x : UpdateT m α) (init : NameMap PackageEntry := {}) : m (α × NameMap PackageEntry) := + x.run init + +/-- +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 + let rootName := ws.root.name.toString (escape := false) + match (← Manifest.load ws.manifestFile |>.toBaseIO) with + | .ok manifest => + -- Reuse manifest versions + unless toUpdate.isEmpty do + manifest.packages.forM fun entry => do + unless entry.inherited || toUpdate.contains entry.name do + store entry.name entry + -- Move packages directory + if let some oldRelPkgsDir := manifest.packagesDir? then + let oldPkgsDir := ws.dir / oldRelPkgsDir + if oldRelPkgsDir.normalize != ws.relPkgsDir.normalize && (← oldPkgsDir.pathExists) then + logInfo s!"workspace packages directory changed; \ + renaming '{oldPkgsDir}' to '{ws.pkgsDir}'" + let doRename : IO Unit := do + createParentDirs ws.pkgsDir + IO.FS.rename oldPkgsDir ws.pkgsDir + if let .error e ← doRename.toBaseIO then + error s!"could not rename workspace packages directory: {e}" + | .error (.noFileOrDirectory ..) => + logInfo s!"{rootName}: no previous manifest, creating one from scratch" + | .error e => + unless toUpdate.isEmpty do + liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update` + logWarning s!"{rootName}: ignoring previous 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 + if depPkg.name ≠ dep.name then + if dep.name = .mkSimple "std" then + let rev := + match matDep.manifestEntry.src with + | .git (inputRev? := some rev) .. => s!" @ {repr rev}" + | _ => "" + logError (stdMismatchError depPkg.name.toString rev) + if let .error e ← IO.FS.removeDirAll depPkg.dir |>.toBaseIO then -- cleanup + -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows + 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}'" + -- Add the dependencies' locked dependencies to the manifest + match (← Manifest.load depPkg.manifestFile |>.toBaseIO) with + | .ok manifest => + manifest.packages.forM fun entry => do + unless (← getThe (NameMap PackageEntry)).contains entry.name do + let entry := entry.setInherited.inDirectory depPkg.relDir + store entry.name entry + | .error (.noFileOrDirectory ..) => + logWarning s!"{depPkg.name}: ignoring missing dependency manifest '{depPkg.manifestFile}'" + | .error e => + logWarning s!"{depPkg.name}: ignoring dependency manifest because it failed to load: {e}" + return depPkg + +/-- +Rebuild the workspace's Lake manifest and materialize missing dependencies. + +Packages 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. + +Package are always reconfigured when updated. +-/ +def Workspace.updateAndMaterialize + (ws : Workspace) (toUpdate : NameSet := {}) (leanOpts : Options := {}) +: LogIO Workspace := do + let (ws, entries) ← UpdateT.run do + reuseManifest ws toUpdate + ws.resolveDeps fun pkg dep => updateDep pkg dep leanOpts + let manifestEntries := ws.packages.foldl (init := #[]) fun arr pkg => + match entries.find? pkg.name with + | some entry => arr.push <| + entry.setManifestFile pkg.relManifestFile |>.setConfigFile pkg.relConfigFile + | none => arr -- should only be the case for the root + let manifest : Manifest := { + name := ws.root.name + lakeDir := ws.relLakeDir + packagesDir? := ws.relPkgsDir + 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 + return ws + +/-- +Check whether the manifest exists and +whether entries in the manifest are up-to-date, +reporting warnings and/or errors as appropriate. +-/ +def validateManifest + (pkgEntries : NameMap PackageEntry) (deps : Array Dependency) +: LogIO PUnit := do + if pkgEntries.isEmpty && !deps.isEmpty then + error "missing manifest; use `lake update` to generate one" + deps.forM fun dep => do + let warnOutOfDate (what : String) := + logWarning <| + s!"manifest out of date: {what} of dependency '{dep.name}' changed; \ + use `lake update {dep.name}` to update it" + if let .some entry := pkgEntries.find? dep.name then + match dep.src, entry.src with + | .git (url := url) (rev := rev) .., .git (url := url') (inputRev? := rev') .. => + if url ≠ url' then warnOutOfDate "git url" + if rev ≠ rev' then warnOutOfDate "git revision" + | .path .., .path .. => pure () + | _, _ => warnOutOfDate "source kind (git/path)" + +/-- +Resolving a workspace's dependencies using a manifest, +downloading and/or updating them as necessary. +-/ +def Workspace.materializeDeps + (ws : Workspace) (manifest : Manifest) + (leanOpts : Options := {}) (reconfigure := false) +: LogIO Workspace := do + if !manifest.packages.isEmpty && manifest.packagesDir? != some (mkRelPathString ws.relPkgsDir) then + logWarning <| + "manifest out of date: packages directory changed; \ + use `lake update` to rebuild the manifest \ + (warning: this will update ALL workspace dependencies)" + let relPkgsDir := manifest.packagesDir?.getD ws.relPkgsDir + 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 + if let some entry := pkgEntries.find? dep.name then + let result ← entry.materialize ws.lakeEnv ws.dir relPkgsDir + loadDepPackage result dep.opts leanOpts reconfigure + else + if pkg.name = ws.root.name then + error <| + s!"dependency '{dep.name}' not in manifest; \ + use `lake update {dep.name}` to add it" + else + error <| + s!"dependency '{dep.name}' of '{pkg.name}' not in manifest; \ + this suggests that the manifest is corrupt; \ + use `lake update` to generate a new, complete file \ + (warning: this will update ALL workspace dependencies)" diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 46854e1e97..b345cad61b 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -12,7 +12,8 @@ open Lean Parser /-! # TOML Loader -Load a package from a TOML Lake configuration file. +This module contains the main definitions to load a package from a +Lake configuration file written in TOML. -/ namespace Lake @@ -255,6 +256,10 @@ instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v. /-! ## Root Loader -/ +/-- +Load a `Package` from a TOML Lake configuration file. +The resulting package does not yet include any dependencies. +-/ def loadTomlConfig (dir relDir relConfigFile : FilePath) : LogIO Package := do let configFile := dir / relConfigFile let input ← IO.FS.readFile configFile diff --git a/src/lake/Lake/Load/Workspace.lean b/src/lake/Lake/Load/Workspace.lean new file mode 100644 index 0000000000..b9b334bf52 --- /dev/null +++ b/src/lake/Lake/Load/Workspace.lean @@ -0,0 +1,58 @@ +/- +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.Load.Resolve +import Lake.Build.Module +import Lake.Build.Package +import Lake.Build.Library + +/-! # Workspace Loader + +This module contains the main definitions for loading a complete Lake workspace. +-/ + +open Lean + +namespace Lake + +/-- +Load a `Workspace` for a Lake package by elaborating its configuration file. +Does not resolve dependencies. +-/ +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 + moduleFacetConfigs := initModuleFacetConfigs + packageFacetConfigs := initPackageFacetConfigs + libraryFacetConfigs := initLibraryFacetConfigs + } + if let some env := env? then + IO.ofExcept <| ws.addFacetsFromEnv env config.leanOpts + else + return ws + +/-- +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 + let ws ← loadWorkspaceRoot config + if updateDeps then + ws.updateAndMaterialize {} leanOpts + else if let some manifest ← Manifest.load? ws.manifestFile then + ws.materializeDeps manifest leanOpts rc + else + ws.updateAndMaterialize {} leanOpts + +/-- Updates the manifest for the loaded Lake workspace (see `updateAndMaterialize`). -/ +def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do + let leanOpts := config.leanOpts + let ws ← loadWorkspaceRoot config + discard <| ws.updateAndMaterialize toUpdate leanOpts diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean index 7723ed5224..05fb570901 100644 --- a/src/lake/Lake/Util/StoreInsts.lean +++ b/src/lake/Lake/Util/StoreInsts.lean @@ -23,8 +23,10 @@ instance [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m) where fetch? k := return (← get).find? k store k a := modify (·.insert k a) -instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) := - inferInstanceAs (MonadStore _ _ (StateT (RBMap ..) _)) +-- uses the eagerly specialized `RBMap` functions in `NameMap` +instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) where + fetch? k := return (← get).find? k + store k a := modify (·.insert k a) @[inline] instance [MonadDStore κ β m] [t : FamilyOut β k α] : MonadStore1Of k α m where fetch? := cast (by rw [t.family_key_eq_type]) <| fetch? (m := m) k diff --git a/src/lake/tests/order/bar/lakefile.lean b/src/lake/tests/order/bar/lakefile.lean index 611efef4c4..e168034539 100644 --- a/src/lake/tests/order/bar/lakefile.lean +++ b/src/lake/tests/order/bar/lakefile.lean @@ -2,7 +2,9 @@ import Lake open Lake DSL package bar where - moreLeanArgs := #["-DmaxHeartbeats=555000"] + moreLeanArgs := #["-DmaxHeartbeats=888000"] + +require leaf from ".." / "leaf" with NameMap.empty.insert `val "888000" lean_lib X lean_exe Y diff --git a/src/lake/tests/order/clean.sh b/src/lake/tests/order/clean.sh index 2df4b795d7..46d55ed9cc 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 -rm -f lake-manifest.json foo/lake-manifest.json bar/lake-manifest.json +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 -f lake-manifest-1.json diff --git a/src/lake/tests/order/foo/lakefile.lean b/src/lake/tests/order/foo/lakefile.lean index 0716154187..520e4235fa 100644 --- a/src/lake/tests/order/foo/lakefile.lean +++ b/src/lake/tests/order/foo/lakefile.lean @@ -2,7 +2,9 @@ import Lake open Lake DSL package foo where - moreLeanArgs := #["-DmaxHeartbeats=555000"] + moreLeanArgs := #["-DmaxHeartbeats=777000"] + +require leaf from ".." / "leaf" with NameMap.empty.insert `val "777000" lean_lib X lean_exe Y diff --git a/src/lake/tests/order/lakefile.lean b/src/lake/tests/order/lakefile.lean index 08ef2281d6..91e3dfc616 100644 --- a/src/lake/tests/order/lakefile.lean +++ b/src/lake/tests/order/lakefile.lean @@ -9,6 +9,8 @@ lean_exe Y require foo from "foo" require bar from "bar" +require leaf from "leaf" with NameMap.empty.insert `val "666000" + lean_lib A where moreLeanArgs := #["-DmaxHeartbeats=222000"] diff --git a/src/lake/tests/order/leaf/Z.lean b/src/lake/tests/order/leaf/Z.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/lake/tests/order/leaf/lakefile.lean b/src/lake/tests/order/leaf/lakefile.lean new file mode 100644 index 0000000000..6fc273f830 --- /dev/null +++ b/src/lake/tests/order/leaf/lakefile.lean @@ -0,0 +1,9 @@ +import Lake +open Lake DSL + +def val := get_config? val |>.getD "0" + +package leaf where + moreLeanArgs := #[s!"-DmaxHeartbeats={val}"] + +lean_lib Z diff --git a/src/lake/tests/order/test.sh b/src/lake/tests/order/test.sh index b0e834e4e8..9f94ecf765 100755 --- a/src/lake/tests/order/test.sh +++ b/src/lake/tests/order/test.sh @@ -14,8 +14,9 @@ $LAKE update $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 555000 +$LAKE build +X -v | grep --color 888000 $LAKE build +Y -v | grep --color 666000 +$LAKE build +Z -v | grep --color 666000 $LAKE exe Y | grep --color root # Tests that `lake update` does not reorder packages in the manifest