refactor: lake: simplify load code (#4371)
Simplifies the Lake dependency resolution code. Largely split from #3998.
This commit is contained in:
Mac Malone
GitHub
parent
a8de4b3b06
commit
f3274d375a
21 changed files with 685 additions and 535 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)) :=
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
34
src/lake/Lake/Load/Lean.lean
Normal file
34
src/lake/Lake/Load/Lean.lean
Normal file
|
|
@ -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)
|
||||
|
|
@ -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
|
||||
|
||||
168
src/lake/Lake/Load/Lean/Eval.lean
Normal file
168
src/lake/Lake/Load/Lean/Eval.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
304
src/lake/Lake/Load/Resolve.lean
Normal file
304
src/lake/Lake/Load/Resolve.lean
Normal file
|
|
@ -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)"
|
||||
|
|
@ -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
|
||||
|
|
|
|||
58
src/lake/Lake/Load/Workspace.lean
Normal file
58
src/lake/Lake/Load/Workspace.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"]
|
||||
|
||||
|
|
|
|||
0
src/lake/tests/order/leaf/Z.lean
Normal file
0
src/lake/tests/order/leaf/Z.lean
Normal file
9
src/lake/tests/order/leaf/lakefile.lean
Normal file
9
src/lake/tests/order/leaf/lakefile.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue