refactor: pattern TargetConfig off FacetConfig
This commit is contained in:
tydeu
parent
bc8c809d66
commit
6bb5101256
18 changed files with 106 additions and 110 deletions
|
|
@ -3,8 +3,6 @@ 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.Build.Info
|
||||
import Lake.Build.Store
|
||||
import Lake.Build.Targets
|
||||
|
||||
namespace Lake
|
||||
|
|
|
|||
|
|
@ -44,13 +44,9 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
|
|||
error s!"do not know how to build package facet `{facet}`"
|
||||
| .customTarget pkg target =>
|
||||
if let some config := pkg.findTargetConfig? target then
|
||||
if h : pkg.name = config.package ∧ target = config.name then
|
||||
have h' : CustomData (pkg.name, target) = BuildJob config.resultType := by simp [h]
|
||||
liftM <| cast (by rw [← h']) <| config.target.activate
|
||||
else
|
||||
error "target's name in the configuration does not match the name it was registered with"
|
||||
config.build pkg
|
||||
else
|
||||
error s!"could not build `{target}` of `{pkg.name}` -- target not found"
|
||||
error s!"could not build `{target}` of `{pkg.name}` -- target not found"
|
||||
| .libraryFacet lib facet => do
|
||||
if let some config := (← getWorkspace).findLibraryFacetConfig? facet then
|
||||
config.build lib
|
||||
|
|
@ -98,12 +94,6 @@ export BuildInfo (build)
|
|||
[FamilyDef BuildData self.key (BuildJob α)] : BuildTarget α :=
|
||||
Target.mk <| self.build |>.catchFailure fun _ => pure failure
|
||||
|
||||
/-- A smart constructor for facet configurations that generate CLI targets. -/
|
||||
@[inline] def mkFacetTargetConfig (build : ι → IndexBuildM (BuildJob α))
|
||||
[h : FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
|
||||
build := cast (by rw [← h.family_key_eq_type]) build
|
||||
getJob? := some fun data => discard <| ofFamily data
|
||||
|
||||
/-! ### Lean Executable Builds -/
|
||||
|
||||
@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ 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.Build.Index
|
||||
import Lake.Build.Targets
|
||||
|
||||
namespace Lake
|
||||
|
||||
|
|
@ -32,7 +32,7 @@ protected def LeanLib.recBuildLean
|
|||
|
||||
/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/
|
||||
def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean)
|
||||
mkFacetJobConfig (·.recBuildLean)
|
||||
|
||||
protected def LeanLib.recBuildStatic
|
||||
(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
|
||||
|
|
@ -41,7 +41,7 @@ protected def LeanLib.recBuildStatic
|
|||
|
||||
/-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
|
||||
def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
|
||||
mkFacetTargetConfig (·.recBuildStatic)
|
||||
mkFacetJobConfig (·.recBuildStatic)
|
||||
|
||||
/-! # Build Shared Lib -/
|
||||
|
||||
|
|
@ -83,7 +83,7 @@ protected def LeanLib.recBuildShared
|
|||
|
||||
/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
|
||||
def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
|
||||
mkFacetTargetConfig (·.recBuildShared)
|
||||
mkFacetJobConfig (·.recBuildShared)
|
||||
|
||||
open LeanLib in
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Sebastian Ullrich, Mac Malone
|
||||
-/
|
||||
import Lean.Elab.Import
|
||||
import Lake.Build.Index
|
||||
import Lake.Build.Targets
|
||||
|
||||
open System
|
||||
|
||||
|
|
@ -126,19 +126,19 @@ def Module.recBuildLean (mod : Module) (art : LeanArtifact)
|
|||
|
||||
/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/
|
||||
def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean .leanBin)
|
||||
mkFacetJobConfig (·.recBuildLean .leanBin)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/
|
||||
def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean .olean)
|
||||
mkFacetJobConfig (·.recBuildLean .olean)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/
|
||||
def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean .ilean)
|
||||
mkFacetJobConfig (·.recBuildLean .ilean)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
|
||||
def Module.cFacetConfig : ModuleFacetConfig cFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLean .c)
|
||||
mkFacetJobConfig (·.recBuildLean .c)
|
||||
|
||||
/-- Recursively build the module's object file from its C file produced by `lean`. -/
|
||||
def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
|
||||
|
|
@ -147,7 +147,7 @@ def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
|
|||
|
||||
/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
|
||||
def Module.oFacetConfig : ModuleFacetConfig oFacet :=
|
||||
mkFacetTargetConfig (·.recBuildLeanO)
|
||||
mkFacetJobConfig (·.recBuildLeanO)
|
||||
|
||||
/--
|
||||
Recursively parse the Lean files of a module and its imports
|
||||
|
|
@ -220,7 +220,7 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do
|
|||
|
||||
/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet :=
|
||||
mkFacetTargetConfig (·.recBuildDynlib)
|
||||
mkFacetJobConfig (·.recBuildDynlib)
|
||||
|
||||
open Module in
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ 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.Build.Index
|
||||
import Lake.Build.Targets
|
||||
|
||||
namespace Lake
|
||||
|
||||
|
|
@ -34,7 +34,7 @@ def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Uni
|
|||
|
||||
/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
|
||||
mkFacetTargetConfig (·.recBuildExtraDepTargets)
|
||||
mkFacetJobConfig (·.recBuildExtraDepTargets)
|
||||
|
||||
open Package in
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -27,15 +27,15 @@ structure BuildSpec where
|
|||
(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet)
|
||||
: Except CliError BuildSpec := do
|
||||
let some getJob := config.getJob?
|
||||
| throw <| CliError.nonTargetFacet facetType facet
|
||||
| throw <| CliError.nonCliFacet facetType facet
|
||||
return {info, getJob := h ▸ getJob}
|
||||
|
||||
def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) := do
|
||||
return self.getJob <| ← buildIndexTop' self.info
|
||||
def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) :=
|
||||
self.getJob <$> buildIndexTop' self.info
|
||||
|
||||
def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do
|
||||
let jobs ← RecBuildM.run do specs.mapM (·.build)
|
||||
jobs.forM (discard <| liftM <| await ·)
|
||||
jobs.forM (discard <| ·.await)
|
||||
|
||||
/-! ## Parsing CLI Build Target Specifiers -/
|
||||
|
||||
|
|
@ -79,15 +79,15 @@ def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError Bu
|
|||
throw <| CliError.unknownFacet "external library" facet
|
||||
|
||||
def resolveCustomTarget (pkg : Package)
|
||||
(target facet : Name) (config : TargetConfig) : Except CliError BuildSpec :=
|
||||
(name facet : Name) (config : TargetConfig pkg.name name) : Except CliError BuildSpec :=
|
||||
if !facet.isAnonymous then
|
||||
throw <| CliError.invalidFacet target facet
|
||||
else if h : pkg.name = config.package then
|
||||
have : FamilyDef CustomData (pkg.name, config.name) (BuildJob config.resultType) :=
|
||||
⟨by simp [h]⟩
|
||||
return mkBuildSpec <| pkg.customTarget config.name
|
||||
else
|
||||
throw <| CliError.badTarget pkg.name target config.package config.name
|
||||
throw <| CliError.invalidFacet name facet
|
||||
else do
|
||||
let info := pkg.customTarget name
|
||||
let some getJob := config.getJob?
|
||||
| throw <| CliError.nonCliTarget name
|
||||
have h : BuildData info.key = CustomData (pkg.name, name) := rfl
|
||||
return {info, getJob := h ▸ getJob}
|
||||
|
||||
def resolveTargetInPackage (ws : Workspace)
|
||||
(pkg : Package) (target facet : Name) : Except CliError BuildSpec :=
|
||||
|
|
@ -117,7 +117,7 @@ def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Excep
|
|||
|
||||
def resolveTargetInWorkspace (ws : Workspace)
|
||||
(target : Name) (facet : Name) : Except CliError (Array BuildSpec) :=
|
||||
if let some (pkg, config) := ws.findTargetConfig? target then
|
||||
if let some ⟨pkg, config⟩ := ws.findTargetConfig? target then
|
||||
Array.singleton <$> resolveCustomTarget pkg target facet config
|
||||
else if let some exe := ws.findLeanExe? target then
|
||||
Array.singleton <$> resolveExeTarget exe facet
|
||||
|
|
|
|||
|
|
@ -25,8 +25,8 @@ inductive CliError
|
|||
| unknownTarget (target : Name)
|
||||
| missingModule (pkg : Name) (mod : Name)
|
||||
| missingTarget (pkg : Name) (spec : String)
|
||||
| badTarget (pkg target cfgPkg cfgName : Name)
|
||||
| nonTargetFacet (type : String) (facet : Name)
|
||||
| nonCliTarget (target : Name)
|
||||
| nonCliFacet (type : String) (facet : Name)
|
||||
| invalidTargetSpec (spec : String) (tooMany : Char)
|
||||
| invalidFacet (target : Name) (facet : Name)
|
||||
/- Script CLI Error -/
|
||||
|
|
@ -56,8 +56,8 @@ def toString : CliError → String
|
|||
| unknownTarget t => s!"unknown target `{t.toString false}`"
|
||||
| missingModule pkg mod => s!"package '{pkg.toString false}' has no module '{mod.toString false}'"
|
||||
| missingTarget pkg spec => s!"package '{pkg.toString false}' has no target '{spec}'"
|
||||
| badTarget p t p' t' => s!"target registered as `{p.toString false}/{t.toString false}` but configured as `{p'.toString false}/{t'.toString false}` "
|
||||
| nonTargetFacet t f => s!"{t} facet `{f.toString false}` is not a buildable target"
|
||||
| nonCliTarget t => s!"target `{t.toString false}` is not a buildable via `lake`"
|
||||
| nonCliFacet t f => s!"{t} facet `{f.toString false}` is not a buildable via `lake`"
|
||||
| invalidTargetSpec s c => s!"invalid script spec '{s}' (too many '{c}')"
|
||||
| invalidFacet t f => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets"
|
||||
| unknownScript s => s!"unknown script {s}"
|
||||
|
|
|
|||
|
|
@ -24,6 +24,12 @@ protected abbrev FacetConfig.name (_ : FacetConfig DataFam ι name) := name
|
|||
build := cast (by rw [← h.family_key_eq_type]) build
|
||||
getJob? := none
|
||||
|
||||
/-- A smart constructor for facet configurations that generate jobs for the CLI. -/
|
||||
@[inline] def mkFacetJobConfig (build : ι → IndexBuildM (BuildJob α))
|
||||
[h : FamilyDef Fam facet (BuildJob α)] : FacetConfig Fam ι facet where
|
||||
build := cast (by rw [← h.family_key_eq_type]) build
|
||||
getJob? := some fun data => discard <| ofFamily data
|
||||
|
||||
/-- A dependently typed configuration based on its registered name. -/
|
||||
structure NamedConfigDecl (β : Name → Type u) where
|
||||
name : Name
|
||||
|
|
|
|||
|
|
@ -15,4 +15,4 @@ declare_opaque_type OpaquePackage
|
|||
declare_opaque_type OpaqueWorkspace
|
||||
|
||||
/-- Opaque reference to a `TargetConfig` used for forward declaration. -/
|
||||
declare_opaque_type OpaqueTargetConfig
|
||||
declare_opaque_type OpaqueTargetConfig (pkgName name : Name)
|
||||
|
|
|
|||
|
|
@ -125,7 +125,7 @@ deriving Inhabited
|
|||
/-! # Package -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp
|
||||
abbrev DNameMap α := DRBMap Name α Name.quickCmp
|
||||
@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty
|
||||
|
||||
/-- A Lake package -- its location plus its configuration. -/
|
||||
|
|
@ -147,7 +147,7 @@ structure Package where
|
|||
/-- External library targets for the package. -/
|
||||
externLibConfigs : NameMap ExternLibConfig := {}
|
||||
/-- (Opaque references to) targets defined in the package. -/
|
||||
opaqueTargetConfigs : NameMap OpaqueTargetConfig := {}
|
||||
opaqueTargetConfigs : DNameMap (OpaqueTargetConfig config.name) := {}
|
||||
/--
|
||||
The names of the package's targets to build by default
|
||||
(i.e., on a bare `lake build` of the package).
|
||||
|
|
@ -165,7 +165,7 @@ abbrev PackageSet := RBTree Package (·.config.name.quickCmp ·.config.name)
|
|||
namespace Package
|
||||
|
||||
/-- The package's name. -/
|
||||
@[inline] def name (self : Package) : Name :=
|
||||
abbrev name (self : Package) : Name :=
|
||||
self.config.name
|
||||
|
||||
/-- An `Array` of the package's direct dependencies. -/
|
||||
|
|
|
|||
|
|
@ -9,34 +9,27 @@ import Lake.Build.Store
|
|||
namespace Lake
|
||||
|
||||
/-- A custom target's declarative configuration. -/
|
||||
structure TargetConfig where
|
||||
/-- The name of the target. -/
|
||||
name : Name
|
||||
/-- The name of the target's package. -/
|
||||
package : Name
|
||||
/-- The type of the target's build result. -/
|
||||
resultType : Type
|
||||
structure TargetConfig (pkgName name : Name) : Type where
|
||||
/-- The target's build function. -/
|
||||
target : BuildTarget resultType
|
||||
/-- Proof that target's build result is the correctly typed target.-/
|
||||
data_eq_target : CustomData (package, name) = BuildJob resultType
|
||||
build : Package → IndexBuildM (CustomData (pkgName, name))
|
||||
/-- Does this target produce an associated asynchronous job? -/
|
||||
getJob? : Option (CustomData (pkgName, name) → Job Unit)
|
||||
deriving Inhabited
|
||||
|
||||
family_def _nil_ : CustomData (.anonymous, .anonymous) := BuildJob Unit
|
||||
/-- A smart constructor for target configurations that generate CLI targets. -/
|
||||
@[inline] def mkTargetJobConfig (build : Package → IndexBuildM (BuildJob α))
|
||||
[h : FamilyDef CustomData (pkgName, name) (BuildJob α)] : TargetConfig pkgName name where
|
||||
build := cast (by rw [← h.family_key_eq_type]) build
|
||||
getJob? := some fun data => discard <| ofFamily data
|
||||
|
||||
instance : Inhabited TargetConfig := ⟨{
|
||||
name := .anonymous
|
||||
package := .anonymous
|
||||
resultType := PUnit
|
||||
target := default
|
||||
data_eq_target := family_key_eq_type
|
||||
}⟩
|
||||
/-- A dependently typed configuration based on its registered package and name. -/
|
||||
structure TargetDecl where
|
||||
pkg : Name
|
||||
name : Name
|
||||
config : TargetConfig pkg name
|
||||
|
||||
hydrate_opaque_type OpaqueTargetConfig TargetConfig
|
||||
|
||||
instance FamilyDefOfTargetConfig {cfg : TargetConfig}
|
||||
: FamilyDef CustomData (cfg.package, cfg.name) (BuildJob cfg.resultType) :=
|
||||
⟨cfg.data_eq_target⟩
|
||||
hydrate_opaque_type OpaqueTargetConfig TargetConfig pkgName name
|
||||
|
||||
/-- Try to find a target configuration in the package with the given name . -/
|
||||
def Package.findTargetConfig? (name : Name) (self : Package) : Option TargetConfig :=
|
||||
def Package.findTargetConfig? (name : Name) (self : Package) : Option (TargetConfig self.name name) :=
|
||||
self.opaqueTargetConfigs.find? name |>.map (·.get)
|
||||
|
|
|
|||
|
|
@ -93,12 +93,12 @@ def findExternLib? (name : Name) (self : Workspace) : Option ExternLib :=
|
|||
self.packageArray.findSome? fun pkg => pkg.findExternLib? name
|
||||
|
||||
/-- Try to find a target configuration in the workspace with the given name. -/
|
||||
def findTargetConfig? (name : Name) (self : Workspace) : Option (Package × TargetConfig) :=
|
||||
def findTargetConfig? (name : Name) (self : Workspace) : Option ((pkg : Package) × TargetConfig pkg.name name) :=
|
||||
self.packageArray.findSome? fun pkg => pkg.findTargetConfig? name <&> (⟨pkg, ·⟩)
|
||||
|
||||
/-- Add a module facet to the workspace. -/
|
||||
def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace :=
|
||||
{self with moduleFacetConfigs := self.moduleFacetConfigs.insert cfg.name cfg}
|
||||
{self with moduleFacetConfigs := self.moduleFacetConfigs.insert name cfg}
|
||||
|
||||
/-- Try to find a module facet configuration in the workspace with the given name. -/
|
||||
def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) :=
|
||||
|
|
@ -106,7 +106,7 @@ def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFace
|
|||
|
||||
/-- Add a package facet to the workspace. -/
|
||||
def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace :=
|
||||
{self with packageFacetConfigs := self.packageFacetConfigs.insert cfg.name cfg}
|
||||
{self with packageFacetConfigs := self.packageFacetConfigs.insert name cfg}
|
||||
|
||||
/-- Try to find a package facet configuration in the workspace with the given name. -/
|
||||
def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) :=
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do
|
|||
`(module_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
config := Lake.mkFacetJobConfig $defn
|
||||
})
|
||||
| stx => Macro.throwErrorAt stx "ill-formed module facet declaration"
|
||||
|
||||
|
|
@ -41,7 +41,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do
|
|||
`(package_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
config := Lake.mkFacetJobConfig $defn
|
||||
})
|
||||
| stx => Macro.throwErrorAt stx "ill-formed package facet declaration"
|
||||
|
||||
|
|
@ -56,7 +56,7 @@ kw:"library_facet " sig:simpleDeclSig : command => do
|
|||
`(library_data $id : BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : LibraryFacetDecl := {
|
||||
name := $name
|
||||
config := Lake.mkFacetTargetConfig $defn
|
||||
config := Lake.mkFacetJobConfig $defn
|
||||
})
|
||||
| stx => Macro.throwErrorAt stx "ill-formed library facet declaration"
|
||||
|
||||
|
|
@ -67,15 +67,12 @@ kw:"target " sig:simpleDeclSig : command => do
|
|||
| `(simpleDeclSig| $id:ident : $ty := $defn $[$wds?]?) =>
|
||||
let attr ← withRef kw `(Term.attrInstance| target)
|
||||
let attrs := #[attr] ++ expandAttrs attrs?
|
||||
let axm := mkIdentFrom id <| ``CustomData ++ id.getId
|
||||
let name := Name.quoteFrom id id.getId
|
||||
let pkgName := mkIdentFrom id `_package.name
|
||||
`(family_def $id : CustomData ($pkgName, $name) := BuildJob $ty
|
||||
$[$doc?]? @[$attrs,*] def $id : TargetConfig := {
|
||||
$[$doc?]? @[$attrs,*] def $id : TargetDecl := {
|
||||
pkg := $pkgName
|
||||
name := $name
|
||||
package := $pkgName
|
||||
resultType := $ty
|
||||
target := $defn
|
||||
data_eq_target := $axm
|
||||
config := Lake.mkTargetJobConfig $defn
|
||||
})
|
||||
| stx => Macro.throwErrorAt stx "ill-formed target declaration"
|
||||
|
|
|
|||
|
|
@ -75,9 +75,13 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
|
|||
evalConstCheck env opts LeanExeConfig ``LeanExeConfig name
|
||||
let externLibConfigs ← IO.ofExcept <| mkTagMap env externLibAttr fun name =>
|
||||
evalConstCheck env opts ExternLibConfig ``ExternLibConfig name
|
||||
let opaqueTargetConfigs ← mkTagMap env targetAttr fun declName =>
|
||||
match evalConstCheck env opts TargetConfig ``TargetConfig declName with
|
||||
| .ok a => pure <| OpaqueTargetConfig.mk a
|
||||
let opaqueTargetConfigs ← mkDTagMap 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.ext.getState env |>.fold (·.push ·) #[]
|
||||
|
||||
|
|
@ -101,26 +105,14 @@ def Workspace.addFacetsFromEnv
|
|||
let mut ws := self
|
||||
for name in moduleFacetAttr.ext.getState env do
|
||||
match evalConstCheck env opts ModuleFacetDecl ``ModuleFacetDecl name with
|
||||
| .ok decl =>
|
||||
if h : name = decl.name then
|
||||
ws := ws.addModuleFacetConfig <| h ▸ decl.config
|
||||
else
|
||||
error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
|
||||
| .ok decl => ws := ws.addModuleFacetConfig <| decl.config
|
||||
| .error e => error e
|
||||
for name in packageFacetAttr.ext.getState env do
|
||||
match evalConstCheck env opts PackageFacetDecl ``PackageFacetDecl name with
|
||||
| .ok decl =>
|
||||
if h : name = decl.name then
|
||||
ws := ws.addPackageFacetConfig <| h ▸ decl.config
|
||||
else
|
||||
error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
|
||||
| .ok decl => ws := ws.addPackageFacetConfig <| decl.config
|
||||
| .error e => error e
|
||||
for name in libraryFacetAttr.ext.getState env do
|
||||
match evalConstCheck env opts LibraryFacetDecl ``LibraryFacetDecl name with
|
||||
| .ok decl =>
|
||||
if h : name = decl.name then
|
||||
ws := ws.addLibraryFacetConfig <| h ▸ decl.config
|
||||
else
|
||||
error s!"facet was defined as `{decl.name}`, but was registered as `{name}`"
|
||||
| .ok decl => ws := ws.addLibraryFacetConfig <| decl.config
|
||||
| .error e => error e
|
||||
return ws
|
||||
|
|
|
|||
|
|
@ -46,7 +46,6 @@ instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
|
|||
instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
|
||||
eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
|
||||
|
||||
|
||||
-- ## Basic Instances
|
||||
|
||||
theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
|
||||
|
|
@ -108,3 +107,20 @@ instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp)
|
|||
intro o
|
||||
unfold Option.compareWith
|
||||
cases o <;> simp
|
||||
|
||||
def Prod.compareWith
|
||||
(cmpA : α → α → Ordering) (cmpB : β → β → Ordering)
|
||||
: (α × β) → (α × β) → Ordering :=
|
||||
fun (a, b) (a', b') => match cmpA a a' with | .eq => cmpB b b' | ord => ord
|
||||
|
||||
instance [EqOfCmp α cmpA] [EqOfCmp β cmpB]
|
||||
: EqOfCmp (α × β) (Prod.compareWith cmpA cmpB) where
|
||||
eq_of_cmp := by
|
||||
intro (a, b) (a', b')
|
||||
dsimp only [Prod.compareWith]
|
||||
split; next ha => intro hb; rw [eq_of_cmp ha, eq_of_cmp hb]
|
||||
intros; contradiction
|
||||
|
||||
instance [LawfulCmpEq α cmpA] [LawfulCmpEq β cmpB]
|
||||
: LawfulCmpEq (α × β) (Prod.compareWith cmpA cmpB) where
|
||||
cmp_rfl := by simp [Prod.compareWith]
|
||||
|
|
|
|||
|
|
@ -18,3 +18,5 @@ instance : Monad BaseIOTask := inferInstanceAs <| Monad Task
|
|||
|
||||
abbrev EIOTask ε := ExceptT ε BaseIOTask
|
||||
abbrev OptionIOTask := OptionT BaseIOTask
|
||||
|
||||
instance : Inhabited (OptionIOTask α) := ⟨failure⟩
|
||||
|
|
|
|||
|
|
@ -17,14 +17,14 @@ lean_exe b
|
|||
lean_exe c
|
||||
|
||||
@[defaultTarget]
|
||||
target meow : PUnit := Target.mk <| sync (m := BuildM) do
|
||||
IO.FS.writeFile (_package.buildDir / "meow.txt") "Meow!"
|
||||
return default
|
||||
target meow : Unit := fun pkg => do
|
||||
IO.FS.writeFile (pkg.buildDir / "meow.txt") "Meow!"
|
||||
return .nil
|
||||
|
||||
target bark : PUnit := Target.mk <| sync (m := BuildM) do
|
||||
target bark : Unit := fun _pkg => do
|
||||
logInfo "Bark!"
|
||||
return default
|
||||
return .nil
|
||||
|
||||
package_facet print_name : PUnit := fun pkg => do
|
||||
package_facet print_name : Unit := fun pkg => do
|
||||
IO.println pkg.name
|
||||
return BuildJob.nil
|
||||
return .nil
|
||||
|
|
|
|||
|
|
@ -47,3 +47,5 @@ test -f ./build/lib/${LIB_PREFIX}Bar.$SHARED_LIB_EXT
|
|||
$LAKE build bark | grep -m1 Bark!
|
||||
|
||||
$LAKE build targets:print_name | grep -m1 targets
|
||||
|
||||
$LAKE build targets:deps && exit 1 || true
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue