feat: lake: input dependencies (#7703)
This PR adds `input_file` and `input_dir` as new target types. It also adds the `needs` configuration option for Lean libraries and executables. This option generalizes `extraDepTargets` (which will be deprecated in the future), providing much richer support for declaring dependencies across package and target type boundaries. Closes #2761.
This commit is contained in:
Mac Malone
GitHub
parent
bb23713542
commit
2d28331cb6
37 changed files with 1357 additions and 181 deletions
|
|
@ -306,6 +306,28 @@ rebuilds across platforms.
|
|||
@[inline] def inputFile (path : FilePath) (text : Bool) : SpawnM (Job FilePath) :=
|
||||
if text then inputTextFile path else inputBinFile path
|
||||
|
||||
/--
|
||||
A build job for a directory of files that are expected to already exist.
|
||||
Returns an array of the files in the directory that match the filter.
|
||||
|
||||
If `text := true`, the files are handled as text files rather than a binary files.
|
||||
Any byte difference in a binary file will trigger a rebuild of its dependents.
|
||||
In contrast, text file traces have normalized line endings to avoid unnecessary
|
||||
rebuilds across platforms.
|
||||
-/
|
||||
def inputDir
|
||||
(path : FilePath) (text : Bool) (filter : FilePath → Bool)
|
||||
: SpawnM (Job (Array FilePath)) := do
|
||||
let job ← Job.async do
|
||||
let fs ← path.readDir
|
||||
let ps := fs.filterMap fun f =>
|
||||
if filter f.path then some f.path else none
|
||||
-- Makes the order of files consistent across platforms
|
||||
let ps := ps.qsort (toString · < toString ·)
|
||||
return ps
|
||||
job.bindM fun ps =>
|
||||
Job.collectArray <$> ps.mapM (inputFile · text)
|
||||
|
||||
/--
|
||||
Build an object file from a source file job using `compiler`. The invocation is:
|
||||
|
||||
|
|
|
|||
|
|
@ -103,9 +103,6 @@ as needed (via `package_data`).
|
|||
-/
|
||||
abbrev PackageData := FacetData Package.facetKind
|
||||
|
||||
/-- The kind identifier for facets of a Lean library. -/
|
||||
@[match_pattern] abbrev LeanLib.facetKind : Name := `lean_lib
|
||||
|
||||
/--
|
||||
The open type family which maps a Lean library facet's name to its output type.
|
||||
For example, the `FilePath` pf the generated static library for the `static` facet.
|
||||
|
|
@ -118,12 +115,6 @@ abbrev LibraryData := FacetData LeanLib.facetKind
|
|||
@[inherit_doc LibraryData]
|
||||
abbrev LeanLibData := LibraryData
|
||||
|
||||
/-- The kind identifier for facets of a Lean executable. -/
|
||||
@[match_pattern] abbrev LeanExe.facetKind : Name := `lean_exe
|
||||
|
||||
/-- The kind identifier for facets of an external library. -/
|
||||
@[match_pattern] abbrev ExternLib.facetKind : Name := `extern_lib
|
||||
|
||||
/--
|
||||
The open type family which maps a custom package target
|
||||
(package × target name) to its output type.
|
||||
|
|
@ -197,13 +188,11 @@ scoped macro (name := builtinFacetCommand)
|
|||
id?:optional(atomic(group(ident " @ "))) name:ident " : " ns:ident " => " ty:term
|
||||
: command => withRef tk do
|
||||
let fam := mkCIdentFrom tk ``FacetOut
|
||||
let kindName ← match ns.getId with
|
||||
| `Package => pure Package.facetKind
|
||||
| `Module => pure Module.facetKind
|
||||
| `LeanLib => pure LeanLib.facetKind
|
||||
| `LeanExe => pure LeanExe.facetKind
|
||||
| `ExternLib => pure ExternLib.facetKind
|
||||
| _ => Macro.throwErrorAt ns "unknown facet kind"
|
||||
let nsName :: _ ← Macro.resolveNamespace ns.getId
|
||||
| Macro.throwErrorAt ns s!"unknown or ambiguous target namespace '{ns.getId}'"
|
||||
let kindName := facetKindForNamespace nsName
|
||||
if kindName.isAnonymous then
|
||||
Macro.throwErrorAt ns s!"unknown target namespace '{ns.getId}'"
|
||||
let nameLit := Name.quoteFrom name name.getId (canonical := id?.isSome)
|
||||
let kindLit := Name.quoteFrom ns kindName (canonical := true)
|
||||
let facet := kindName ++ name.getId
|
||||
|
|
@ -218,7 +207,7 @@ scoped macro (name := builtinFacetCommand)
|
|||
| .str .anonymous n => pure <| mkIdentFrom name (ns.getId.str s!"{n}Facet") (canonical := true)
|
||||
| _ => Macro.throwErrorAt name "cannot generate facet declaration name from facet name"
|
||||
`(
|
||||
$[$doc?]? abbrev $id := $facetLit
|
||||
$[$doc?]? @[reducible] def $id := $facetLit
|
||||
family_def $facetId : $fam $facetLit := $ty
|
||||
instance : FamilyDef FacetOut ($kindLit ++ $nameLit) $ty :=
|
||||
inferInstanceAs (FamilyDef FacetOut $facetLit $ty)
|
||||
|
|
|
|||
|
|
@ -190,3 +190,12 @@ builtin_facet shared : ExternLib => FilePath
|
|||
|
||||
/-- A external library's dynlib. -/
|
||||
builtin_facet dynlib : ExternLib => Dynlib
|
||||
|
||||
/-- The default facet for an input file. Produces the file path. -/
|
||||
builtin_facet default : InputFile => FilePath
|
||||
|
||||
/--
|
||||
The default facet for an input directory.
|
||||
Produces the matching files in the directory.
|
||||
-/
|
||||
builtin_facet default : InputDir => Array FilePath
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Mac Malone
|
|||
prelude
|
||||
import Lake.Config.LeanExe
|
||||
import Lake.Config.ExternLib
|
||||
import Lake.Config.InputFile
|
||||
import Lake.Build.Facets
|
||||
|
||||
/-!
|
||||
|
|
@ -30,54 +31,63 @@ inductive BuildInfo
|
|||
|
||||
/-! ### Build Key Helper Constructors -/
|
||||
|
||||
abbrev Module.key (self : Module) : BuildKey :=
|
||||
.module self.keyName
|
||||
|
||||
@[deprecated Module.key (since := "2025-03-28")]
|
||||
abbrev Module.buildKey (self : Module) : BuildKey :=
|
||||
.module self.keyName
|
||||
|
||||
@[deprecated BuildKey.facet (since := "2025-03-28")]
|
||||
abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey :=
|
||||
.moduleFacet self.keyName facet
|
||||
self.key.facet facet
|
||||
|
||||
abbrev Package.key (self : Package) : BuildKey :=
|
||||
.package self.name
|
||||
|
||||
@[deprecated Package.key (since := "2025-03-28")]
|
||||
abbrev Package.buildKey (self : Package) : BuildKey :=
|
||||
.package self.name
|
||||
|
||||
@[deprecated BuildKey.facet (since := "2025-03-28")]
|
||||
abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey :=
|
||||
.packageFacet self.name facet
|
||||
self.key.facet facet
|
||||
|
||||
abbrev Package.targetBuildKey
|
||||
(target : Name) (self : Package)
|
||||
: BuildKey := .packageTarget self.name target
|
||||
abbrev Package.targetKey (target : Name) (self : Package) : BuildKey :=
|
||||
.packageTarget self.name target
|
||||
|
||||
abbrev LeanLib.buildKey (self : LeanLib) : BuildKey :=
|
||||
@[deprecated Package.targetKey (since := "2025-03-28")]
|
||||
abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey :=
|
||||
.packageTarget self.name target
|
||||
|
||||
abbrev ConfigTarget.key (self : ConfigTarget kind) : BuildKey :=
|
||||
.packageTarget self.pkg.name self.name
|
||||
|
||||
abbrev LeanLib.facetBuildKey (self : LeanLib) (facet : Name) : BuildKey :=
|
||||
.targetFacet self.pkg.name self.name facet
|
||||
|
||||
abbrev LeanExe.buildKey (self : LeanExe) : BuildKey :=
|
||||
@[deprecated ConfigTarget.key (since := "2025-03-28")]
|
||||
abbrev ConfigTarget.buildKey (self : ConfigTarget kind) : BuildKey :=
|
||||
.packageTarget self.pkg.name self.name
|
||||
|
||||
@[deprecated BuildKey.facet (since := "2025-03-28")]
|
||||
abbrev ConfigTarget.facetBuildKey (self : ConfigTarget kind) (facet : Name) : BuildKey :=
|
||||
self.key.facet facet
|
||||
|
||||
abbrev LeanExe.exeBuildKey (self : LeanExe) : BuildKey :=
|
||||
.targetFacet self.pkg.name self.name exeFacet
|
||||
|
||||
abbrev ExternLib.buildKey (self : ExternLib) : BuildKey :=
|
||||
.packageTarget self.pkg.name self.name
|
||||
|
||||
abbrev ExternLib.facetBuildKey (facet : Name) (self : ExternLib) : BuildKey :=
|
||||
.targetFacet self.pkg.name self.name facet
|
||||
self.key.facet exeFacet
|
||||
|
||||
abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey :=
|
||||
self.facetBuildKey staticFacet
|
||||
self.key.facet staticFacet
|
||||
|
||||
abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey :=
|
||||
self.facetBuildKey sharedFacet
|
||||
self.key.facet sharedFacet
|
||||
|
||||
abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey :=
|
||||
self.facetBuildKey dynlibFacet
|
||||
self.key.facet dynlibFacet
|
||||
|
||||
/-! ### Build Info to Key -/
|
||||
|
||||
/-- The key that identifies the build in the Lake build store. -/
|
||||
@[reducible] def BuildInfo.key : (self : BuildInfo) → BuildKey
|
||||
| target p t => p.targetBuildKey t
|
||||
| target p t => p.targetKey t
|
||||
| facet (target := t) (facet := f) .. => .facet t f
|
||||
|
||||
instance : ToString BuildInfo := ⟨(toString ·.key)⟩
|
||||
|
|
@ -93,7 +103,7 @@ instance {p : NPackage n} [FamilyOut (CustomData n) t α]
|
|||
|
||||
instance {p : NPackage n} [FamilyOut BuildData (.packageTarget n t) α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.target p.toPackage t)) α where
|
||||
fam_eq := by unfold BuildInfo.key Package.targetBuildKey; simp
|
||||
fam_eq := by unfold BuildInfo.key Package.targetKey; simp
|
||||
|
||||
instance [FamilyOut FacetOut f α]
|
||||
: FamilyDef BuildData (BuildInfo.key (.facet t k d f)) α where
|
||||
|
|
@ -117,6 +127,8 @@ data_type package : Package
|
|||
data_type lean_lib : LeanLib
|
||||
data_type lean_exe : LeanExe
|
||||
data_type extern_lib : ExternLib
|
||||
data_type input_file : InputFile
|
||||
data_type input_dir : InputDir
|
||||
|
||||
/-- The direct local imports of the Lean module. -/
|
||||
builtin_facet imports : Module => Array Module
|
||||
|
|
@ -146,12 +158,14 @@ Definitions to easily construct `BuildInfo` values for module, package,
|
|||
and target facets.
|
||||
-/
|
||||
|
||||
/-! #### Module Infos -/
|
||||
|
||||
/--
|
||||
Build info for applying the specified facet to the module.
|
||||
It is the user's obiligation to ensure the facet in question is a module facet.
|
||||
-/
|
||||
abbrev Module.facetCore (facet : Name) (self : Module) : BuildInfo :=
|
||||
.facet self.buildKey facetKind (toFamily self) facet
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info for a module facet. -/
|
||||
abbrev Module.facet (facet : Name) (self : Module) : BuildInfo :=
|
||||
|
|
@ -216,6 +230,8 @@ namespace Module
|
|||
|
||||
end Module
|
||||
|
||||
/-! #### Package Infos -/
|
||||
|
||||
/-- Build info for a package target (e.g., a library, executable, or custom target). -/
|
||||
abbrev Package.target (target : Name) (self : Package) : BuildInfo :=
|
||||
.target self target
|
||||
|
|
@ -225,7 +241,7 @@ Build info for applying the specified facet to the package.
|
|||
It is the user's obiligation to ensure the facet in question is a package facet.
|
||||
-/
|
||||
abbrev Package.facetCore (facet : Name) (self : Package) : BuildInfo :=
|
||||
.facet self.buildKey facetKind (toFamily self) facet
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info for a package facet. -/
|
||||
abbrev Package.facet (facet : Name) (self : Package) : BuildInfo :=
|
||||
|
|
@ -281,12 +297,14 @@ abbrev transDeps (self : Package) : BuildInfo :=
|
|||
|
||||
end Package
|
||||
|
||||
/-! #### Lean Library Infos -/
|
||||
|
||||
/-
|
||||
Build info for applying the specified facet to the library.
|
||||
It is the user's obiligation to ensure the facet in question is a library facet.
|
||||
-/
|
||||
abbrev LeanLib.facetCore (facet : Name) (self : LeanLib) : BuildInfo :=
|
||||
.facet self.buildKey facetKind (toFamily self) facet
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info for a facet of a Lean library. -/
|
||||
abbrev LeanLib.facet (facet : Name) (self : LeanLib) : BuildInfo :=
|
||||
|
|
@ -324,12 +342,14 @@ abbrev extraDep (self : LeanLib) : BuildInfo :=
|
|||
|
||||
end LeanLib
|
||||
|
||||
/-! #### Lean Executable Infos -/
|
||||
|
||||
/-
|
||||
Build info for applying the specified facet to the executable.
|
||||
It is the user's obiligation to ensure the facet in question is the executable facet.
|
||||
-/
|
||||
abbrev LeanExe.facetCore (facet : Name) (self : LeanExe) : BuildInfo :=
|
||||
.facet self.buildKey facetKind (toFamily self) facet
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info of the Lean executable. -/
|
||||
abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=
|
||||
|
|
@ -339,12 +359,14 @@ abbrev LeanExe.exe (self : LeanExe) : BuildInfo :=
|
|||
abbrev BuildInfo.leanExe (exe : LeanExe) : BuildInfo :=
|
||||
exe.exe
|
||||
|
||||
/-! #### External Library Infos -/
|
||||
|
||||
/-
|
||||
Build info for applying the specified facet to the external library.
|
||||
It is the user's obiligation to ensure the facet in question is an external library facet.
|
||||
-/
|
||||
abbrev ExternLib.facetCore (facet : Name) (self : ExternLib) : BuildInfo :=
|
||||
.facet self.buildKey facetKind (toFamily self) facet
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info of the external library's static binary. -/
|
||||
abbrev ExternLib.static (self : ExternLib) : BuildInfo :=
|
||||
|
|
@ -369,3 +391,27 @@ abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo :=
|
|||
@[deprecated ExternLib.dynlib (since := "2025-03-04")]
|
||||
abbrev BuildInfo.dynlibExternLib (lib : ExternLib) : BuildInfo :=
|
||||
lib.facetCore ExternLib.dynlibFacet
|
||||
|
||||
/-! #### Input File & Directory Infos -/
|
||||
|
||||
/-
|
||||
Build info for applying the specified facet to the input file.
|
||||
It is the user's obiligation to ensure the facet in question is an external library facet.
|
||||
-/
|
||||
abbrev InputFile.facetCore (facet : Name) (self : InputFile) : BuildInfo :=
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info of the input file's default facet. -/
|
||||
abbrev InputFile.default (self : InputFile) : BuildInfo :=
|
||||
self.facetCore InputFile.defaultFacet
|
||||
|
||||
/-
|
||||
Build info for applying the specified facet to the input directory.
|
||||
It is the user's obiligation to ensure the facet in question is an external library facet.
|
||||
-/
|
||||
abbrev InputDir.facetCore (facet : Name) (self : InputDir) : BuildInfo :=
|
||||
.facet self.key facetKind (toFamily self) facet
|
||||
|
||||
/-- Build info of the input directory's default facet. -/
|
||||
abbrev InputDir.default (self : InputDir) : BuildInfo :=
|
||||
self.facetCore InputDir.defaultFacet
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ import Lake.Build.Package
|
|||
import Lake.Build.Library
|
||||
import Lake.Build.Executable
|
||||
import Lake.Build.ExternLib
|
||||
import Lake.Build.InputFile
|
||||
|
||||
/-! # Initial Facets -/
|
||||
|
||||
|
|
@ -22,6 +23,8 @@ def initFacetConfigs : DNameMap FacetConfig :=
|
|||
|> insert LeanLib.initFacetConfigs
|
||||
|> insert LeanExe.initFacetConfigs
|
||||
|> insert ExternLib.initFacetConfigs
|
||||
|> insert InputFile.initFacetConfigs
|
||||
|> insert InputDir.initFacetConfigs
|
||||
where
|
||||
insert {k} (group : DNameMap (KFacetConfig k)) map :=
|
||||
group.fold (init := map) fun m k v => m.insert k v.toFacetConfig
|
||||
|
|
|
|||
52
src/lake/Lake/Build/InputFile.lean
Normal file
52
src/lake/Lake/Build/InputFile.lean
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Common
|
||||
import Lake.Config.InputFile
|
||||
|
||||
/-! # Input File Build
|
||||
Build function definitions for input files and directories.
|
||||
-/
|
||||
|
||||
open System (FilePath)
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-! ## Input File -/
|
||||
|
||||
private def InputFile.recFetch (t : InputFile) : FetchM (Job FilePath) :=
|
||||
withRegisterJob s!"{t.name}" do
|
||||
inputFile t.config.path t.config.text
|
||||
|
||||
/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
|
||||
def InputFile.defaultFacetConfig : KFacetConfig InputFile.facetKind defaultFacet :=
|
||||
mkFacetJobConfig recFetch
|
||||
|
||||
/--
|
||||
A name-configuration map for the initial set of
|
||||
input file facets (e.g., `default`).
|
||||
-/
|
||||
def InputFile.initFacetConfigs : DNameMap (KFacetConfig InputFile.facetKind) :=
|
||||
DNameMap.empty
|
||||
|>.insert defaultFacet defaultFacetConfig
|
||||
|
||||
/-! ## Input Directory -/
|
||||
|
||||
private def InputDir.recFetch (t : InputDir) : FetchM (Job (Array FilePath)) :=
|
||||
withRegisterJob s!"{t.name}" do
|
||||
inputDir t.config.path t.config.text t.config.filter.matches
|
||||
|
||||
/-- The facet configuration for the builtin `ExternLib.staticFacet`. -/
|
||||
def InputDir.defaultFacetConfig : KFacetConfig InputDir.facetKind defaultFacet :=
|
||||
mkFacetJobConfig recFetch
|
||||
|
||||
/--
|
||||
A name-configuration map for the initial set of
|
||||
input directory facets (e.g., `default`).
|
||||
-/
|
||||
def InputDir.initFacetConfigs : DNameMap (KFacetConfig InputDir.facetKind) :=
|
||||
DNameMap.empty
|
||||
|>.insert defaultFacet defaultFacetConfig
|
||||
|
|
@ -5,6 +5,7 @@ Authors: Mac Malone
|
|||
-/
|
||||
prelude
|
||||
import Lake.Util.Name
|
||||
import Lake.Config.Kinds
|
||||
|
||||
namespace Lake
|
||||
open Lean (Name)
|
||||
|
|
@ -17,11 +18,84 @@ inductive BuildKey
|
|||
| facet (target : BuildKey) (facet : Name)
|
||||
deriving Inhabited, Repr, DecidableEq, Hashable
|
||||
|
||||
/-- The kind identifier for facets of a package. -/
|
||||
@[match_pattern] abbrev Package.facetKind : Name := `package
|
||||
def PartialBuildKey.moduleTargetIndicator := `«_+»
|
||||
|
||||
/-- The kind identifier for facets of a (Lean) module. -/
|
||||
@[match_pattern] abbrev Module.facetKind : Name := `module
|
||||
/--
|
||||
A build key with some missing info.
|
||||
|
||||
* Package names may be elided (replaced by `Name.anonymous`).
|
||||
* Facet names are unqualified (they do not include the input target kind)
|
||||
and may also be ellided.
|
||||
* Module package targets are supported via a fake `packageTarget` with
|
||||
a target name ending in `moduleTargetIndicator`.
|
||||
-/
|
||||
def PartialBuildKey := BuildKey
|
||||
|
||||
/--
|
||||
Parses a `PartialBuildKey` from a `String`.
|
||||
Uses the same syntax as the `lake build` / `lake query` CLI.
|
||||
-/
|
||||
def PartialBuildKey.parse (s : String) : Except String PartialBuildKey := do
|
||||
if s.isEmpty then
|
||||
throw "ill-formed target: empty string"
|
||||
match s.splitOn ":" with
|
||||
| target :: facets =>
|
||||
let target ← parseTarget target
|
||||
facets.foldlM (init := target) fun target facet => do
|
||||
if facet.isEmpty then
|
||||
throw "ill-formed target: empty facet"
|
||||
else
|
||||
return .facet target (stringToLegalOrSimpleName facet)
|
||||
| [] =>
|
||||
-- ∀ str, length (str.splitOn sep) > 0
|
||||
unreachable!
|
||||
where
|
||||
parseTarget s := do
|
||||
match s.splitOn "/" with
|
||||
| [target] =>
|
||||
if target.isEmpty then
|
||||
return .package .anonymous
|
||||
if target.startsWith "@" then
|
||||
let pkg := target.drop 1
|
||||
if pkg.isEmpty then
|
||||
return .package .anonymous
|
||||
else
|
||||
return .package (stringToLegalOrSimpleName pkg)
|
||||
else if target.startsWith "+" then
|
||||
return .module (stringToLegalOrSimpleName (target.drop 1))
|
||||
else
|
||||
parsePackageTarget .anonymous target
|
||||
| [pkg, target] =>
|
||||
let pkg := if pkg.startsWith "@" then pkg.drop 1 else pkg
|
||||
if pkg.isEmpty then
|
||||
parsePackageTarget .anonymous target
|
||||
else
|
||||
parsePackageTarget (stringToLegalOrSimpleName pkg) target
|
||||
| _ =>
|
||||
throw "ill-formed target: too many '/'"
|
||||
parsePackageTarget pkg target :=
|
||||
if target.isEmpty then
|
||||
throw s!"ill-formed target: default package targets are not supported in partial build keys"
|
||||
else if target.startsWith "+" then
|
||||
let target := target.drop 1 |> stringToLegalOrSimpleName
|
||||
let target := target ++ moduleTargetIndicator
|
||||
return .packageTarget pkg target
|
||||
else
|
||||
let target := stringToLegalOrSimpleName target
|
||||
return .packageTarget pkg target
|
||||
|
||||
def PartialBuildKey.toString : (self : PartialBuildKey) → String
|
||||
| .module m => s!"+{m}"
|
||||
| .package p => if p.isAnonymous then "" else s!"@{p}"
|
||||
| .packageTarget p t =>
|
||||
let t :=
|
||||
if let some t := t.eraseSuffix? moduleTargetIndicator then
|
||||
s!"+{t}"
|
||||
else t.toString
|
||||
if p.isAnonymous then t else s!"{p}/{t}"
|
||||
| .facet t f => if f.isAnonymous then toString t else s!"{toString t}:{f}"
|
||||
|
||||
instance : ToString PartialBuildKey := ⟨PartialBuildKey.toString⟩
|
||||
|
||||
namespace BuildKey
|
||||
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Mac Malone
|
|||
prelude
|
||||
import Lake.Build.Common
|
||||
import Lake.Build.Targets
|
||||
import Lake.Build.Target.Fetch
|
||||
|
||||
/-! # Library Facet Builds
|
||||
Build function definitions for a library's builtin facets.
|
||||
|
|
@ -96,12 +97,16 @@ protected def LeanLib.recBuildShared
|
|||
def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
|
||||
mkFacetJobConfig LeanLib.recBuildShared
|
||||
|
||||
/-! ## Build `extraDepTargets` -/
|
||||
/-! ## Other -/
|
||||
|
||||
/-- Build the `extraDepTargets` for the library and its package. -/
|
||||
/--
|
||||
Build extra target dependencies of the library (e.g., `extraDepTargets`, `needs`). -/
|
||||
def LeanLib.recBuildExtraDepTargets (self : LeanLib) : FetchM (Job Unit) := do
|
||||
self.extraDepTargets.foldlM (init := ← self.pkg.extraDep.fetch) fun job target => do
|
||||
let job ← self.extraDepTargets.foldlM (init := ← self.pkg.extraDep.fetch) fun job target => do
|
||||
return job.mix <| ← self.pkg.fetchTargetJob target
|
||||
let job ← self.config.needs.foldlM (init := job) fun job key => do
|
||||
return job.mix <| ← key.fetchIn self.pkg
|
||||
return job
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `extraDepFacet`. -/
|
||||
def LeanLib.extraDepFacetConfig : LibraryFacetConfig extraDepFacet :=
|
||||
|
|
|
|||
|
|
@ -7,21 +7,95 @@ prelude
|
|||
import Lake.Build.Job
|
||||
import Lake.Config.Monad
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Lake
|
||||
|
||||
private def BuildKey.fetchCore (self : BuildKey) : FetchM (Job (BuildData self)) := do
|
||||
variable (defaultPkg : Package) (root : BuildKey) in
|
||||
private def PartialBuildKey.fetchInCore
|
||||
(self : PartialBuildKey) (facetless : Bool := false)
|
||||
: FetchM ((key : BuildKey) × Job (BuildData key)) := do
|
||||
match self with
|
||||
| .module modName =>
|
||||
let some mod ← findModule? modName
|
||||
| error s!"invalid target '{root}': module '{modName}' not found in workspace"
|
||||
return ⟨.module modName, cast (by simp) <| Job.pure mod⟩
|
||||
| .package pkgName =>
|
||||
let pkg ← resolveTargetPackageD pkgName
|
||||
return ⟨.package pkg.name, cast (by simp) <| Job.pure pkg⟩
|
||||
| .packageTarget pkgName target =>
|
||||
let pkg ← resolveTargetPackageD pkgName
|
||||
if let some modName := target.eraseSuffix? PartialBuildKey.moduleTargetIndicator then
|
||||
let some mod := pkg.findTargetModule? modName
|
||||
| error s!"invalid target '{root}': module target '{modName}' not found in package '{pkg.name}'"
|
||||
return ⟨.module mod.keyName, cast (by simp) <| Job.pure mod⟩
|
||||
else
|
||||
let key := BuildKey.packageTarget pkg.name target
|
||||
if facetless then
|
||||
if let some decl := pkg.findTargetDecl? target then
|
||||
if h : decl.kind.isAnonymous then
|
||||
let job ← ( pkg.target target).fetch
|
||||
return ⟨key, cast (by simp) job⟩
|
||||
else
|
||||
let facet := decl.kind.str "default"
|
||||
let tgt := decl.mkConfigTarget pkg
|
||||
let tgt := cast (by simp [decl.target_eq_type h]) tgt
|
||||
let info := BuildInfo.facet key decl.kind tgt facet
|
||||
return ⟨key.facet facet, ← info.fetch⟩
|
||||
else
|
||||
error s!"invalid target '{root}': target not found in package '{pkg.name}'"
|
||||
else
|
||||
let job ← (pkg.target target).fetch
|
||||
return ⟨key, cast (by simp) job⟩
|
||||
| .facet target shortFacet =>
|
||||
let ⟨key, job⟩ ← PartialBuildKey.fetchInCore target false
|
||||
let kind := job.kind
|
||||
if h : kind.isAnonymous then
|
||||
error s!"invalid target '{root}': targets of opaque data kinds do not support facets"
|
||||
else
|
||||
let shortFacet := if shortFacet.isAnonymous then `default else shortFacet
|
||||
have facet := kind ++ shortFacet
|
||||
let job ← (job.cast h).bindM fun data =>
|
||||
fetch (.facet target kind data facet)
|
||||
return ⟨.facet target facet, cast (by simp) job⟩
|
||||
where
|
||||
@[inline] resolveTargetPackageD (name : Name) : FetchM Package := do
|
||||
if name.isAnonymous then
|
||||
pure defaultPkg
|
||||
else
|
||||
let some pkg ← findPackage? name
|
||||
| error s!"invalid target '{root}': package '{name}' not found in workspace"
|
||||
return pkg
|
||||
|
||||
/--
|
||||
Fetches the target specified by this key, resolving gaps as needed.
|
||||
|
||||
* A missing package (i.e., `Name.anoanmoyus`) is filled in with `defaultPkg`.
|
||||
* Facets are qualified by the their input target's kind, and missing facets
|
||||
are replaced by their kind's `default`.
|
||||
* Package targets ending in `moduleTargetIndicator` are converted to module package targets.
|
||||
* Package targets for non-dynamic targets (i.e., non-`target`) produce their default facet
|
||||
rather than their configuration.
|
||||
-/
|
||||
@[inline] def PartialBuildKey.fetchIn (defaultPkg : Package) (self : PartialBuildKey) : FetchM OpaqueJob :=
|
||||
(·.2.toOpaque) <$> fetchInCore defaultPkg self self true
|
||||
|
||||
variable (root : BuildKey) in
|
||||
private def BuildKey.fetchCore
|
||||
(self : BuildKey)
|
||||
: FetchM (Job (BuildData self)) := do
|
||||
match self with
|
||||
| module modName =>
|
||||
let some mod ← findModule? modName
|
||||
| error s!"invalid target '{self}': module '{modName}' not found in workspace"
|
||||
return Job.pure <| toFamily mod
|
||||
| error s!"invalid target '{root}': module '{modName}' not found in workspace"
|
||||
return cast (by simp) <| Job.pure mod
|
||||
| package pkgName =>
|
||||
let some pkg ← findPackage? pkgName
|
||||
| error s!"invalid target '{self}': package '{pkgName}' not found in workspace"
|
||||
return Job.pure <| toFamily pkg.toPackage
|
||||
| error s!"invalid target '{root}': package '{pkgName}' not found in workspace"
|
||||
return cast (by simp) <| Job.pure pkg.toPackage
|
||||
| packageTarget pkgName target =>
|
||||
let some pkg ← findPackage? pkgName
|
||||
| error s!"invalid target '{self}': package '{pkgName}' not found in workspace"
|
||||
| error s!"invalid target '{root}': package '{pkgName}' not found in workspace"
|
||||
fetch <| pkg.target target
|
||||
| facet target facetName =>
|
||||
let job ← target.fetchCore
|
||||
|
|
@ -33,7 +107,7 @@ private def BuildKey.fetchCore (self : BuildKey) : FetchM (Job (BuildData self))
|
|||
|
||||
@[inline] protected def BuildKey.fetch
|
||||
(self : BuildKey) [FamilyOut BuildData self α] : FetchM (Job α)
|
||||
:= cast (by simp) self.fetchCore
|
||||
:= cast (by simp) <| fetchCore self self
|
||||
|
||||
@[inline] protected def Target.fetch (self : Target α) : FetchM (Job α) := do
|
||||
have := self.data_def; self.key.fetch
|
||||
|
|
|
|||
|
|
@ -15,6 +15,15 @@ open System (FilePath)
|
|||
|
||||
namespace Lake
|
||||
|
||||
/-- Get the target in the workspace corresponding to this configuration. -/
|
||||
@[inline] def KConfigDecl.get
|
||||
[Monad m] [MonadError m] [MonadLake m] (self : KConfigDecl kind)
|
||||
: m (ConfigTarget kind) := do
|
||||
let some pkg ← findPackage? self.pkg
|
||||
| error s!"package of target '{self.pkg}/{self.name}' not found in workspace"
|
||||
let config := cast (by rw [self.kind_eq, pkg.name_eq]) self.config
|
||||
return ConfigTarget.mk pkg self.name config
|
||||
|
||||
/-! ## Package Facets & Targets -/
|
||||
|
||||
/-- Fetch the build job of the specified package target. -/
|
||||
|
|
@ -74,13 +83,10 @@ def Module.fetchFacetJob (name : Name) (self : Module) : FetchM OpaqueJob :=
|
|||
|
||||
/-! ## Lean Library Facets -/
|
||||
|
||||
/-- Get the Lean library in the workspace with the configuration's name. -/
|
||||
/-- Get the Lean library in the workspace corresponding to this configuration. -/
|
||||
@[inline] def LeanLibDecl.get
|
||||
(self : LeanLibDecl) [Monad m] [MonadError m] [MonadLake m] : m LeanLib
|
||||
:= do
|
||||
let some lib ← findLeanLib? self.name
|
||||
| error s!"Lean library '{self.name}' does not exist in the workspace"
|
||||
return lib
|
||||
:= KConfigDecl.get self
|
||||
|
||||
/-- Fetch the build result of a library facet. -/
|
||||
@[inline] protected def LibraryFacetDecl.fetch
|
||||
|
|
@ -100,18 +106,43 @@ def LeanLib.fetchFacetJob
|
|||
|
||||
/-! ## Lean Executable Target -/
|
||||
|
||||
/-- Get the Lean executable in the workspace with the configuration's name. -/
|
||||
/-- Get the Lean executable in the workspace corresponding to this configuration. -/
|
||||
@[inline] def LeanExeDecl.get
|
||||
(self : LeanExeDecl) [Monad m] [MonadError m] [MonadLake m]
|
||||
: m LeanExe := do
|
||||
let some exe ← findLeanExe? self.name
|
||||
| error s!"Lean executable '{self.name}' does not exist in the workspace"
|
||||
return exe
|
||||
|
||||
/-- Fetch the build of the Lean executable. -/
|
||||
@[inline] def LeanExeDecl.fetch (self : LeanExeDecl) : FetchM (Job FilePath) := do
|
||||
(← self.get).exe.fetch
|
||||
(self : LeanExeDecl) [Monad m] [MonadError m] [MonadLake m] : m LeanExe
|
||||
:= KConfigDecl.get self
|
||||
|
||||
/-- Fetch the build of the Lean executable. -/
|
||||
@[inline] def LeanExe.fetch (self : LeanExe) : FetchM (Job FilePath) :=
|
||||
self.exe.fetch
|
||||
|
||||
/-- Fetch the build of the Lean executable. -/
|
||||
@[inline] def LeanExeDecl.fetch (self : LeanExeDecl) : FetchM (Job FilePath) := do
|
||||
(← self.get).fetch
|
||||
|
||||
/-! ## Input File / Directory Targets -/
|
||||
|
||||
/-- Fetch the input file. -/
|
||||
@[inline] def InputFile.fetch (self : InputFile) : FetchM (Job FilePath) :=
|
||||
self.default.fetch
|
||||
|
||||
/-- Get the input file in the workspace corresponding to this configuration. -/
|
||||
@[inline] def InputFileDecl.get
|
||||
(self : InputFileDecl) [Monad m] [MonadError m] [MonadLake m] : m InputFile
|
||||
:= KConfigDecl.get self
|
||||
|
||||
/-- Fetch the input file. -/
|
||||
@[inline] def InputFileDecl.fetch (self : InputFileDecl) : FetchM (Job FilePath) := do
|
||||
(← self.get).default.fetch
|
||||
|
||||
/-- Fetch the files in the input directory. -/
|
||||
@[inline] def InputDir.fetch (self : InputDir) : FetchM (Job (Array FilePath)) :=
|
||||
self.default.fetch
|
||||
|
||||
/-- Get the input directory in the workspace corresponding to this configuration. -/
|
||||
@[inline] def InputDirDecl.get
|
||||
(self : InputDirDecl) [Monad m] [MonadError m] [MonadLake m] : m InputDir
|
||||
:= KConfigDecl.get self
|
||||
|
||||
/-- Fetch the files in the input directory. -/
|
||||
@[inline] def InputDirDecl.fetch (self : InputDirDecl) : FetchM (Job (Array FilePath)) := do
|
||||
(← self.get).default.fetch
|
||||
|
|
|
|||
|
|
@ -41,6 +41,23 @@ instance [ToLean α] : ToLean (Array α) where
|
|||
instance : ToLean Bool where
|
||||
toLean b := mkIdent <| if b then `true else `false
|
||||
|
||||
class ToLean? (α : Type u) where
|
||||
toLean? : α → Option Term
|
||||
|
||||
export ToLean? (toLean?)
|
||||
|
||||
instance (priority := high) [ToLean α] : ToLean? α where
|
||||
toLean? a := some (toLean a)
|
||||
|
||||
def quoteArray? [ToLean? α] (as : Array α) : Option Term :=
|
||||
toLean <$> as.foldl (init := some #[]) fun vs? a => do
|
||||
let vs ← vs?
|
||||
let v ← toLean? a
|
||||
return vs.push v
|
||||
|
||||
instance [ToLean? α] : ToLean? (Array α) where
|
||||
toLean? as := quoteArray? as
|
||||
|
||||
class AddDeclField (σ : Type u) (name : Name) where
|
||||
addDeclField : σ → Array DeclField → Array DeclField
|
||||
|
||||
|
|
@ -52,6 +69,9 @@ def addDeclFieldCore
|
|||
: Array DeclField :=
|
||||
fs.push <| Unhygienic.run `(declField|$(mkIdent name) := $val)
|
||||
|
||||
instance [ToLean? α] [field : ConfigField σ name α] : AddDeclField σ name where
|
||||
addDeclField cfg fs := if let some v := toLean? (field.get cfg) then addDeclFieldCore name v fs else fs
|
||||
|
||||
@[inline] def addDeclFieldNotEmpty
|
||||
[ToLean α] (name : Name) (val : Array α) (fs : Array DeclField)
|
||||
: Array DeclField :=
|
||||
|
|
@ -144,16 +164,74 @@ protected def Glob.toLean (glob : Glob) : Term := Unhygienic.run do
|
|||
|
||||
instance : ToLean Glob := ⟨Glob.toLean⟩
|
||||
|
||||
def quoteVerTags? (pat : StrPat) : Option Term :=
|
||||
match pat with
|
||||
| .mem xs => if xs.isEmpty then Unhygienic.run `(∅) else some (toLean xs)
|
||||
| .startsWith pre => Unhygienic.run `(.$(mkIdent `startsWith) $(toLean pre))
|
||||
| .satisfies _ n =>
|
||||
if n.isAnonymous || n == `default then none else
|
||||
@[inline] private def quoteSingleton? [ToLean? α] (name : Name) (a : α) : Option Term :=
|
||||
toLean? a |>.map fun a => Unhygienic.run `(.$(mkIdent name) $a)
|
||||
|
||||
protected def Pattern.toLean? [ToLean? (PatternDescr α β)] (p : Pattern α β) : Option Term :=
|
||||
match p.name with
|
||||
| .anonymous =>
|
||||
p.descr?.bind toLean?
|
||||
| `default =>
|
||||
none
|
||||
| n =>
|
||||
Unhygienic.run `(.$(mkIdent n))
|
||||
|
||||
instance : AddDeclField (PackageConfig n) `versionTags where
|
||||
addDeclField cfg := addDeclField? `versionTags (quoteVerTags? cfg.versionTags)
|
||||
instance [ToLean? (PatternDescr α β)] : ToLean? (Pattern α β) := ⟨Pattern.toLean?⟩
|
||||
|
||||
protected partial def PattternDescr.toLean? [ToLean? β] (p : PatternDescr α β) : Option Term :=
|
||||
have : ToLean? (PatternDescr α β) := ⟨PattternDescr.toLean?⟩
|
||||
match p with
|
||||
| .not p => quoteSingleton? `not p
|
||||
| .any p => quoteSingleton? `any p
|
||||
| .all p => quoteSingleton? `all p
|
||||
| .coe p => toLean? p
|
||||
|
||||
instance [ToLean? β] : ToLean? (PatternDescr α β) := ⟨PattternDescr.toLean?⟩
|
||||
|
||||
protected def StrPatDescr.toLean (pat : StrPatDescr) : Term :=
|
||||
match pat with
|
||||
| .mem xs => if xs.isEmpty then Unhygienic.run `(∅) else (toLean xs)
|
||||
| .startsWith affix => Unhygienic.run `(.$(mkIdent `startsWith) $(toLean affix))
|
||||
| .endsWith affix => Unhygienic.run `(.$(mkIdent `endsWith) $(toLean affix))
|
||||
|
||||
instance : ToLean StrPatDescr := ⟨StrPatDescr.toLean⟩
|
||||
|
||||
protected def PathPatDescr.toLean? (p : PathPatDescr) : Option Term :=
|
||||
match p with
|
||||
| .path p => quoteSingleton? `path p
|
||||
| .extension p => quoteSingleton? `extension p
|
||||
| .fileName p => quoteSingleton? `fileName p
|
||||
|
||||
instance : ToLean? PathPatDescr := ⟨PathPatDescr.toLean?⟩
|
||||
|
||||
@[inline] protected def PartialBuildKey.toLean (k : BuildKey) : Term :=
|
||||
go k []
|
||||
where
|
||||
go k (fs : List Name) := Unhygienic.run do
|
||||
match k with
|
||||
| .module n =>
|
||||
`(`+$(mkIdent n)$(mkSuffixes fs)*)
|
||||
| .package n =>
|
||||
if n.isAnonymous then
|
||||
`(`@$(mkSuffixes fs):facetSuffix*)
|
||||
else
|
||||
`(`@$(mkIdent n)$(mkSuffixes fs)*)
|
||||
| .packageTarget p t =>
|
||||
let t ←
|
||||
if let some t := t.eraseSuffix? moduleTargetIndicator then
|
||||
`(packageTargetLit|+$(mkIdent t))
|
||||
else
|
||||
`(packageTargetLit|$(mkIdent t):ident)
|
||||
if p.isAnonymous then
|
||||
`(`@/$t$(mkSuffixes fs)*)
|
||||
else
|
||||
`(`@$(mkIdent p)/$t$(mkSuffixes fs)*)
|
||||
| .facet k f =>
|
||||
return go k (f :: fs)
|
||||
mkSuffixes facets : Array (TSyntax ``facetSuffix) :=
|
||||
facets.toArray.map fun f => Unhygienic.run `(facetSuffix|:$(mkIdent f))
|
||||
|
||||
instance : ToLean PartialBuildKey := ⟨PartialBuildKey.toLean⟩
|
||||
|
||||
/-! ## Dependency Configuration Encoder -/
|
||||
|
||||
|
|
@ -208,6 +286,8 @@ local macro "gen_lean_encoders%" : command => do
|
|||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genMkDeclFields cmds ``LeanExeConfig true
|
||||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genMkDeclFields cmds ``InputFileConfig true
|
||||
let cmds ← genMkDeclFields cmds ``InputDirConfig true
|
||||
-- Package
|
||||
let cmds ← genMkDeclFields cmds ``WorkspaceConfig false
|
||||
let cmds ← genMkDeclFields cmds ``PackageConfig true
|
||||
|
|
@ -234,6 +314,20 @@ protected def LeanExeConfig.mkCommand
|
|||
let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
|
||||
`(leanExeCommand|$[$attrs?:attributes]? lean_exe $(mkIdent n):ident $[$declVal?]?)
|
||||
|
||||
protected def InputFileConfig.mkCommand
|
||||
(cfg : InputFileConfig n) (defaultTarget : Bool)
|
||||
: Command := Unhygienic.run do
|
||||
let declVal? := mkDeclValWhere? (mkDeclFields cfg)
|
||||
let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
|
||||
`(inputFileCommand|$[$attrs?:attributes]? input_file $(mkIdent n):ident $[$declVal?]?)
|
||||
|
||||
protected def InputDirConfig.mkCommand
|
||||
(cfg : InputDirConfig n) (defaultTarget : Bool)
|
||||
: Command := Unhygienic.run do
|
||||
let declVal? := mkDeclValWhere? (mkDeclFields cfg)
|
||||
let attrs? ← if defaultTarget then some <$> `(Term.attributes|@[default_target]) else pure none
|
||||
`(inputDirCommand|$[$attrs?:attributes]? input_dir $(mkIdent n):ident $[$declVal?]?)
|
||||
|
||||
@[inline] def Package.mkTargetCommands
|
||||
(pkg : Package) (defaultTargets : NameSet) (kind : Name)
|
||||
(mkCommand : {n : Name} → ConfigType kind pkg.name n → Bool → Command)
|
||||
|
|
@ -255,4 +349,6 @@ def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
|
|||
$[$(pkg.depConfigs.map (·.mkRequire)):command]*
|
||||
$[$(pkg.mkTargetCommands defaultTargets LeanLib.configKind LeanLibConfig.mkCommand):command]*
|
||||
$[$(pkg.mkTargetCommands defaultTargets LeanExe.configKind LeanExeConfig.mkCommand):command]*
|
||||
$[$(pkg.mkTargetCommands defaultTargets InputFile.configKind InputFileConfig.mkCommand):command]*
|
||||
$[$(pkg.mkTargetCommands defaultTargets InputDir.configKind InputDirConfig.mkCommand):command]*
|
||||
)
|
||||
|
|
|
|||
|
|
@ -63,22 +63,62 @@ def Toml.encodeLeanOptions (opts : Array LeanOption) : Table :=
|
|||
instance : ToToml (Array LeanOption) where
|
||||
toToml opts := .table .missing <| encodeLeanOptions opts
|
||||
|
||||
def smartInsertVerTags (pat : StrPat) (t : Table) : Table :=
|
||||
match pat with
|
||||
| .mem s => t.insert `versionTags (toToml s)
|
||||
| .startsWith p => t.insert `versionTags.startsWith (toToml p)
|
||||
| .satisfies _ n =>
|
||||
if n.isAnonymous || n == `default then t else
|
||||
t.insert `versionTags.preset (toToml n)
|
||||
@[inline] private def encodeSingleton? [ToToml? α] (name : Name) (a : α) : Option Value :=
|
||||
toToml? a |>.map fun v => toToml <| Table.empty.insert name v
|
||||
|
||||
instance : InsertField (PackageConfig n) `versionTags where
|
||||
insertField cfg := smartInsertVerTags cfg.versionTags
|
||||
mutual
|
||||
|
||||
partial def Pattern.toToml? [ToToml? β] (p : Pattern α β) : Option Value :=
|
||||
have : ToToml? (PatternDescr α β) := ⟨PattternDescr.toToml?⟩
|
||||
match p.name with
|
||||
| .anonymous =>
|
||||
p.descr?.bind toToml?
|
||||
| `default =>
|
||||
none
|
||||
| `star =>
|
||||
toToml "*"
|
||||
| n =>
|
||||
toToml <| Table.empty.insert `preset n
|
||||
|
||||
partial def PattternDescr.toToml?
|
||||
[ToToml? β] (p : PatternDescr α β) : Option Value
|
||||
:=
|
||||
have : ToToml? (Pattern α β) := ⟨Pattern.toToml?⟩
|
||||
match p with
|
||||
| .not p => encodeSingleton? `not p
|
||||
| .any p => encodeSingleton? `any p
|
||||
| .all p => encodeSingleton? `all p
|
||||
| .coe p => toToml? p
|
||||
|
||||
end
|
||||
|
||||
instance [ToToml? β] : ToToml? (Pattern α β) := ⟨Pattern.toToml?⟩
|
||||
instance [ToToml? β] : ToToml? (PatternDescr α β) := ⟨PattternDescr.toToml?⟩
|
||||
|
||||
protected def StrPatDescr.toToml (p : StrPatDescr) : Value :=
|
||||
match p with
|
||||
| .mem xs => toToml xs
|
||||
| .startsWith affix => toToml <| Table.empty.insert `startsWith (toToml affix)
|
||||
| .endsWith affix => toToml <| Table.empty.insert `endsWith (toToml affix)
|
||||
|
||||
instance : ToToml StrPatDescr := ⟨StrPatDescr.toToml⟩
|
||||
|
||||
protected def PathPatDescr.toToml? (p : PathPatDescr) : Option Value :=
|
||||
match p with
|
||||
| .path p => encodeSingleton? `path p
|
||||
| .extension p => encodeSingleton? `extension p
|
||||
| .fileName p => encodeSingleton? `fileName p
|
||||
|
||||
instance : ToToml? PathPatDescr := ⟨PathPatDescr.toToml?⟩
|
||||
|
||||
def encodeFacets (facets : Array Name) : Value :=
|
||||
toToml <| facets.map (toToml <| Name.eraseHead ·)
|
||||
|
||||
instance : EncodeField (LeanLibConfig n) `defaultFacets (Array Name) := ⟨encodeFacets⟩
|
||||
|
||||
instance : ToToml BuildKey := ⟨(toToml ·.toString)⟩
|
||||
instance : ToToml PartialBuildKey := ⟨(toToml ·.toString)⟩
|
||||
|
||||
/-! ## Dependency Configuration Encoders -/
|
||||
|
||||
protected def Dependency.toToml (dep : Dependency) (t : Table := {}) : Table :=
|
||||
|
|
@ -129,6 +169,8 @@ local macro "gen_toml_encoders%" : command => do
|
|||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genToToml cmds ``LeanExeConfig true
|
||||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genToToml cmds ``InputFileConfig true
|
||||
let cmds ← genToToml cmds ``InputDirConfig true
|
||||
-- Package
|
||||
let cmds ← genToToml cmds ``WorkspaceConfig false
|
||||
let cmds ← genToToml cmds ``PackageConfig true
|
||||
|
|
@ -154,3 +196,5 @@ def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
|
|||
|>.smartInsert `require pkg.depConfigs
|
||||
|>.smartInsert LeanLib.keyword (pkg.mkTomlTargets LeanLib.configKind LeanLibConfig.toToml)
|
||||
|>.smartInsert LeanExe.keyword (pkg.mkTomlTargets LeanExe.configKind LeanExeConfig.toToml)
|
||||
|>.smartInsert InputFile.keyword (pkg.mkTomlTargets InputFile.configKind InputFileConfig.toToml)
|
||||
|>.smartInsert InputDir.keyword (pkg.mkTomlTargets InputDir.configKind InputDirConfig.toToml)
|
||||
|
|
|
|||
|
|
@ -8,35 +8,20 @@ import Lake.Config.Opaque
|
|||
import Lake.Config.LeanLibConfig
|
||||
import Lake.Config.LeanExeConfig
|
||||
import Lake.Config.ExternLibConfig
|
||||
import Lake.Config.InputFileConfig
|
||||
|
||||
open Lean (Name)
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- The keyword for Lean library configurations. -/
|
||||
abbrev LeanLib.keyword : Name := `lean_lib
|
||||
|
||||
/-- The type kind for Lean library configurations. -/
|
||||
@[match_pattern] abbrev LeanLib.configKind := facetKind
|
||||
|
||||
/-- The keyword for Lean executable configurations. -/
|
||||
abbrev LeanExe.keyword : Name := `lean_exe
|
||||
|
||||
/-- The type kind for Lean executable configurations. -/
|
||||
@[match_pattern] abbrev LeanExe.configKind := facetKind
|
||||
|
||||
/-- The keyword for external library configurations. -/
|
||||
abbrev ExternLib.keyword : Name := `extern_lib
|
||||
|
||||
/-- The type kind for external library configurations. -/
|
||||
@[match_pattern] abbrev ExternLib.configKind := facetKind
|
||||
|
||||
abbrev ConfigType (kind : Name) (pkgName name : Name) : Type :=
|
||||
match kind with
|
||||
| LeanLib.configKind => LeanLibConfig name
|
||||
| LeanExe.configKind => LeanExeConfig name
|
||||
| ExternLib.configKind => ExternLibConfig pkgName name
|
||||
| .anonymous => OpaqueTargetConfig pkgName name
|
||||
| InputFile.configKind => InputFileConfig name
|
||||
| InputDir.configKind => InputDirConfig name
|
||||
| _ => Empty
|
||||
|
||||
/-- Forward declared `ConfigTarget` to work around recursion issues (e.g., with `Package`). -/
|
||||
|
|
@ -62,6 +47,11 @@ structure KConfigDecl (k : Name) extends ConfigDecl where
|
|||
instance : Nonempty (NConfigDecl pkg name) :=
|
||||
⟨{pkg, name, kind := .anonymous, config := Classical.ofNonempty, wf_data := by simp [Name.isAnonymous]}⟩
|
||||
|
||||
@[inline] def ConfigDecl.partialKey (self : ConfigDecl) : PartialBuildKey :=
|
||||
.packageTarget .anonymous self.name
|
||||
|
||||
instance : CoeOut (KConfigDecl k) PartialBuildKey := ⟨(·.partialKey)⟩
|
||||
|
||||
@[inline] def PConfigDecl.config' (self : PConfigDecl p) : ConfigType self.kind p self.name :=
|
||||
cast (by rw [self.pkg_eq]) self.config
|
||||
|
||||
|
|
@ -94,7 +84,7 @@ theorem NConfigDecl.data_eq_target (self : NConfigDecl p n)
|
|||
@[inline] def NConfigDecl.leanLibConfig? (self : NConfigDecl p n) : Option (LeanLibConfig n) :=
|
||||
self.config? LeanLib.configKind
|
||||
|
||||
/-- A Lean library declaration from a configuration written in Lean. -/
|
||||
/-- A Lean library declaration from a configuration written in Lean. -/
|
||||
abbrev LeanLibDecl := KConfigDecl LeanLib.configKind
|
||||
|
||||
@[inline] def ConfigDecl.leanExeConfig? (self : ConfigDecl) : Option (LeanExeConfig self.name) :=
|
||||
|
|
@ -130,4 +120,12 @@ abbrev ExternLibDecl := KConfigDecl ExternLib.configKind
|
|||
@[inline] def NConfigDecl.opaqueTargetConfig? (self : NConfigDecl p n) : Option (OpaqueTargetConfig p n) :=
|
||||
cast (by rw [self.name_eq]) self.toPConfigDecl.opaqueTargetConfig?
|
||||
|
||||
deriving instance TypeName for LeanLibDecl, LeanExeDecl
|
||||
/-- A input file declaration from a configuration written in Lean. -/
|
||||
abbrev InputFileDecl := KConfigDecl InputFile.configKind
|
||||
|
||||
/-- A inpurt directory declaration from a configuration written in Lean. -/
|
||||
abbrev InputDirDecl := KConfigDecl InputDir.configKind
|
||||
|
||||
deriving instance TypeName for
|
||||
LeanLibDecl, LeanExeDecl,
|
||||
InputFileDecl, InputDirDecl
|
||||
|
|
|
|||
16
src/lake/Lake/Config/InputFile.lean
Normal file
16
src/lake/Lake/Config/InputFile.lean
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Config.ConfigTarget
|
||||
|
||||
namespace Lake
|
||||
open Lean System
|
||||
|
||||
/-- An input file -- its package plus its configuration. -/
|
||||
abbrev InputFile := ConfigTarget InputFile.configKind
|
||||
|
||||
/-- An input directory -- its package plus its configuration. -/
|
||||
abbrev InputDir := ConfigTarget InputDir.configKind
|
||||
57
src/lake/Lake/Config/InputFileConfig.lean
Normal file
57
src/lake/Lake/Config/InputFileConfig.lean
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Config.Meta
|
||||
import Lake.Config.Pattern
|
||||
|
||||
open Lean System
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- The declarative configuration for a single input file. -/
|
||||
configuration InputFileConfig (name : Name) where
|
||||
/--
|
||||
The path to the input file (relative to the package root).
|
||||
|
||||
Defaults to the name of the target.
|
||||
-/
|
||||
path : FilePath := name.toString (escape := false)
|
||||
/--
|
||||
Whether this is a text file.
|
||||
If so, Lake normalize line endings for its trace.
|
||||
This avoids rebuilds across platforms with different line endings.
|
||||
|
||||
Defaults to `false`.
|
||||
-/
|
||||
text : Bool := false
|
||||
|
||||
instance : EmptyCollection (InputFileConfig name) := ⟨{}⟩
|
||||
|
||||
/-- The declarative configuration for an input directory. -/
|
||||
configuration InputDirConfig (name : Name) where
|
||||
/--
|
||||
The path to the input directory (relative to the package root).
|
||||
|
||||
Defaults to the name of the target.
|
||||
-/
|
||||
path : FilePath := name.toString (escape := false)
|
||||
/--
|
||||
Whether the directory is composed of text files.
|
||||
If so, Lake normalize line endings for their traces.
|
||||
This avoids rebuilds across platforms with different line endings.
|
||||
|
||||
Defaults to `false`.
|
||||
-/
|
||||
text : Bool := false
|
||||
/-
|
||||
Includes only the files from the directory
|
||||
whose paths statisify the pattern.
|
||||
|
||||
Defaults to including every file.
|
||||
-/
|
||||
filter : PathPat := .star
|
||||
|
||||
instance : EmptyCollection (InputDirConfig name) := ⟨{}⟩
|
||||
89
src/lake/Lake/Config/Kinds.lean
Normal file
89
src/lake/Lake/Config/Kinds.lean
Normal file
|
|
@ -0,0 +1,89 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Init.Prelude
|
||||
|
||||
open Lean (Name)
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-- The keyword for package declarations. -/
|
||||
@[reducible] def Package.keyword : Name := `package
|
||||
|
||||
/-- The kind identifier for facets of a package. -/
|
||||
@[match_pattern] abbrev Package.facetKind : Name := keyword
|
||||
|
||||
/--
|
||||
The would-be keyword for module declarations.
|
||||
|
||||
Such declarations do not currently exist, but this is used
|
||||
as the facet kind for modules.
|
||||
-/
|
||||
@[reducible] def Module.keyword : Name := `module
|
||||
|
||||
/-- The kind identifier for facets of a (Lean) module. -/
|
||||
@[match_pattern] abbrev Module.facetKind : Name := keyword
|
||||
|
||||
/-- The keyword for Lean library declarations. -/
|
||||
@[reducible] def LeanLib.keyword : Name := `lean_lib
|
||||
|
||||
/-- The kind identifier for facets of a Lean library. -/
|
||||
@[match_pattern] abbrev LeanLib.facetKind : Name := `lean_lib
|
||||
|
||||
/-- The type kind for Lean library configurations. -/
|
||||
@[match_pattern] abbrev LeanLib.configKind := facetKind
|
||||
|
||||
/-- The keyword for Lean executable declarations. -/
|
||||
@[reducible] def LeanExe.keyword : Name := `lean_exe
|
||||
|
||||
/-- The kind identifier for facets of a Lean executable. -/
|
||||
@[match_pattern] abbrev LeanExe.facetKind : Name := keyword
|
||||
|
||||
/-- The type kind for Lean executable configurations. -/
|
||||
@[match_pattern] abbrev LeanExe.configKind := facetKind
|
||||
|
||||
/-- The keyword for external library declarations. -/
|
||||
@[reducible] def ExternLib.keyword : Name := `extern_lib
|
||||
|
||||
/-- The kind identifier for facets of an external library. -/
|
||||
@[match_pattern] abbrev ExternLib.facetKind : Name := keyword
|
||||
|
||||
/-- The type kind for external library configurations. -/
|
||||
@[match_pattern] abbrev ExternLib.configKind := facetKind
|
||||
|
||||
/-- The keyword for input file declarations. -/
|
||||
@[reducible] def InputFile.keyword : Name := `input_file
|
||||
|
||||
/-- The kind identifier for facets of an input file. -/
|
||||
@[match_pattern] abbrev InputFile.facetKind := keyword
|
||||
|
||||
/-- The type kind for input file configurations. -/
|
||||
@[match_pattern] abbrev InputFile.configKind := facetKind
|
||||
|
||||
/-- The keyword for input directory declarations. -/
|
||||
@[reducible] def InputDir.keyword : Name := `input_dir
|
||||
|
||||
/-- Tge kind identifier for facets of an input directory. -/
|
||||
@[match_pattern] abbrev InputDir.facetKind := keyword
|
||||
|
||||
/-- The type kind for input directory configurations. -/
|
||||
@[match_pattern] abbrev InputDir.configKind := facetKind
|
||||
|
||||
/--
|
||||
**Lake Internal.**
|
||||
Returns the facet kind for an Lake target namespace.
|
||||
Used by the `builtin_facet` macro.
|
||||
-/
|
||||
def facetKindForNamespace (ns : Name) : Name :=
|
||||
match ns with
|
||||
| `Lake.Package => Package.facetKind
|
||||
| `Lake.Module => Module.facetKind
|
||||
| `Lake.LeanLib => LeanLib.facetKind
|
||||
| `Lake.LeanExe => LeanExe.facetKind
|
||||
| `Lake.ExternLib => ExternLib.facetKind
|
||||
| `Lake.InputFile => InputFile.facetKind
|
||||
| `Lake.InputDir => InputDir.facetKind
|
||||
| _ => Name.anonymous
|
||||
|
|
@ -28,6 +28,7 @@ def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig n) : LeanLibConfig n whe
|
|||
srcDir := self.srcDir
|
||||
roots := #[]
|
||||
libName := self.exeName
|
||||
needs := self.needs
|
||||
extraDepTargets := self.extraDepTargets
|
||||
nativeFacets := self.nativeFacets
|
||||
toLeanConfig := self.toLeanConfig
|
||||
|
|
|
|||
|
|
@ -41,6 +41,9 @@ configuration LeanExeConfig (name : Name) extends LeanConfig where
|
|||
/-- An `Array` of target names to build before the executable's modules. -/
|
||||
extraDepTargets : Array Name := #[]
|
||||
|
||||
/-- An `Array` of targets to build before the executable's modules. -/
|
||||
needs : Array PartialBuildKey := #[]
|
||||
|
||||
/--
|
||||
Enables the executable to interpret Lean files (e.g., via
|
||||
`Lean.Elab.runFrontend`) by exposing symbols within the executable
|
||||
|
|
|
|||
|
|
@ -51,6 +51,9 @@ configuration LeanLibConfig (name : Name) extends LeanConfig where
|
|||
/-- An `Array` of target names to build before the library's modules. -/
|
||||
extraDepTargets : Array Name := #[]
|
||||
|
||||
/-- An `Array` of targets to build before the executable's modules. -/
|
||||
needs : Array PartialBuildKey := #[]
|
||||
|
||||
/--
|
||||
Whether to compile each of the library's modules into a native shared library
|
||||
that is loaded whenever the module is imported. This speeds up evaluation of
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ instance [parent : ConfigParent σ ρ] [field : ConfigField ρ name α] : Config
|
|||
modify f := parent.modify (field.modify f)
|
||||
|
||||
syntax configField :=
|
||||
atomic(nestedDeclModifiers ident,+) declSig " := " term
|
||||
atomic(nestedDeclModifiers ident,+) declSig (" := " term)?
|
||||
|
||||
/--
|
||||
An tailored `structure` command for producing Lake configuration data types.
|
||||
|
|
@ -141,12 +141,15 @@ private def mkConfigAuxDecls
|
|||
return data.cmds.push fieldsDef |>.push fieldsInst |>.push infoInst
|
||||
|
||||
private def mkFieldView (stx : TSyntax ``configField) : MacroM FieldView := withRef stx do
|
||||
let `(configField|$mods:declModifiers $ids,* $bs* : $rty := $val) := stx
|
||||
let `(configField|$mods:declModifiers $ids,* $bs* : $rty $[:= $val?]?) := stx
|
||||
| Macro.throwError "ill-formed configuration field declaration"
|
||||
let bvs ← expandBinders bs
|
||||
let type := mkDepArrow bvs rty
|
||||
let some id := ids.getElems[0]?
|
||||
| Macro.throwError "expected a least one field name"
|
||||
withRef id.raw do
|
||||
let some val := val?
|
||||
| Macro.throwError "expected a default value"
|
||||
let defVal ← `(fun $(bvs.map (·.id))* => $val)
|
||||
let decl ← `(structSimpleBinder|$mods:declModifiers $id : $type := $defVal)
|
||||
return {ref := stx, mods, id, ids, type, defVal, decl? := decl}
|
||||
|
|
|
|||
|
|
@ -23,56 +23,6 @@ namespace Lake
|
|||
@[inline] def defaultBuildArchive (name : Name) : String :=
|
||||
s!"{name.toString false}-{System.Platform.target}.tar.gz"
|
||||
|
||||
/-- A `String` pattern. Matches some subset of strings. -/
|
||||
inductive StrPat
|
||||
/--
|
||||
Matches a string that satisfies an arbitrary predicate
|
||||
(optionally identified by a `Name`).
|
||||
-/
|
||||
| satisfies (f : String → Bool) (name := Name.anonymous)
|
||||
/-- Matches a string that is a member of the array -/
|
||||
| mem (xs : Array String)
|
||||
/-- Matches a string that starts with this prefix. -/
|
||||
| startsWith (pre : String)
|
||||
deriving Inhabited
|
||||
|
||||
instance : Coe (Array String) StrPat := ⟨.mem⟩
|
||||
instance : Coe (String → Bool) StrPat := ⟨.satisfies⟩
|
||||
|
||||
/-- Matches nothing. -/
|
||||
def StrPat.none : StrPat := .mem #[]
|
||||
|
||||
instance : EmptyCollection StrPat := ⟨.none⟩
|
||||
|
||||
/--
|
||||
Whether a string is "version-like".
|
||||
That is, a `v` followed by a digit.
|
||||
-/
|
||||
def isVerLike (s : String) : Bool :=
|
||||
if h : s.utf8ByteSize ≥ 2 then
|
||||
s.get' 0 (by simp [String.atEnd]; omega) == 'v' &&
|
||||
(s.get' ⟨1⟩ (by simp [String.atEnd]; omega)).isDigit
|
||||
else
|
||||
false
|
||||
|
||||
/-- Matches a "version-like" string: a `v` followed by a digit. -/
|
||||
def StrPat.verLike : StrPat := .satisfies isVerLike `verLike
|
||||
|
||||
/-- Default string pattern for a Package's `versionTags`. -/
|
||||
def defaultVersionTags := StrPat.satisfies isVerLike `default
|
||||
|
||||
/-- Builtin `StrPat` presets available to TOML for `versionTags`. -/
|
||||
def versionTagPresets :=
|
||||
NameMap.empty
|
||||
|>.insert `verLike .verLike
|
||||
|>.insert `default defaultVersionTags
|
||||
|
||||
/-- Returns whether the string `s` matches the pattern. -/
|
||||
def StrPat.matches (s : String) : (self : StrPat) → Bool
|
||||
| .satisfies f _ => f s
|
||||
| .mem xs => xs.contains s
|
||||
| .startsWith p => p.isPrefixOf s
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! # PackageConfig -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
|
|||
241
src/lake/Lake/Config/Pattern.lean
Normal file
241
src/lake/Lake/Config/Pattern.lean
Normal file
|
|
@ -0,0 +1,241 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Util.Name
|
||||
|
||||
open System Lean
|
||||
|
||||
namespace Lake
|
||||
|
||||
/-! ## Match Notation -/
|
||||
|
||||
class IsPattern (α : Type u) (β : outParam $ Type v) where
|
||||
/-- Returns whether the value matches the pattern. -/
|
||||
satisfies (pat : α) (val : β) : Bool
|
||||
|
||||
@[inherit_doc] scoped infix:50 " =~ " => IsPattern.satisfies
|
||||
|
||||
/-! ## Abstract Patterns -/
|
||||
|
||||
mutual
|
||||
|
||||
/--
|
||||
A pattern. Matches some subset of the values of a type.
|
||||
May also include a declarative description.
|
||||
-/
|
||||
structure Pattern (α : Type u) (β : Type v) where
|
||||
/-- Returns whether the value matches the pattern. -/
|
||||
filter : α → Bool
|
||||
/-- An optional name for the filter. -/
|
||||
name := Name.anonymous
|
||||
/-- A optional declarative description of the filter. -/
|
||||
descr? : Option (PatternDescr α β) := none
|
||||
deriving Inhabited
|
||||
|
||||
/--
|
||||
An abstract declarative pattern.
|
||||
Augments another pattern description `β` with logical connectives.
|
||||
-/
|
||||
inductive PatternDescr (α : Type u) (β : Type v)
|
||||
/-- Matches a value that does not satisfy the pattern. -/
|
||||
| not (p : Pattern α β)
|
||||
/-- Matches a value that satisfies every pattern. Short-circuits. -/
|
||||
| all (ps : Array (Pattern α β))
|
||||
/-- Matches a value that satisfies any one of the patterns. Short-circuits. -/
|
||||
| any (ps : Array (Pattern α β))
|
||||
/-- Matches a value that statisfies the underlying pattern description. -/
|
||||
| coe (p : β)
|
||||
deriving Inhabited
|
||||
|
||||
end
|
||||
|
||||
instance : Coe β (PatternDescr α β) := ⟨.coe⟩
|
||||
|
||||
/-- Returns whether the value matches the pattern. Alias for `filter`. -/
|
||||
abbrev Pattern.matches (a : α) (self : Pattern α β) : Bool :=
|
||||
self.filter a
|
||||
|
||||
instance : IsPattern (Pattern α β) α := ⟨Pattern.filter⟩
|
||||
|
||||
/-- Returns whether the value matches the pattern. -/
|
||||
@[specialize] def PatternDescr.matches
|
||||
[IsPattern β α] (val : α) (self : PatternDescr α β)
|
||||
: Bool :=
|
||||
match self with
|
||||
| .not p => !(p =~ val)
|
||||
| .all ps => ps.all (· =~ val)
|
||||
| .any ps => ps.any (· =~ val)
|
||||
| .coe p => p =~ val
|
||||
|
||||
instance [IsPattern β α] : IsPattern (PatternDescr α β) α := ⟨flip PatternDescr.matches⟩
|
||||
|
||||
/--
|
||||
Matches a value that satisfies an arbitrary predicate
|
||||
(optionally identified by a `Name`).
|
||||
-/
|
||||
@[inline] def Pattern.ofFn (f : α → Bool) (name := Name.anonymous) : Pattern α β :=
|
||||
{filter := f, name}
|
||||
|
||||
instance : Coe (α → Bool) (Pattern α β) := ⟨.ofFn⟩
|
||||
|
||||
/--
|
||||
Matches a string that satisfies the declarative pattern.
|
||||
(optionally identified by a `Name`).
|
||||
-/
|
||||
@[inline] def Pattern.ofDescr [IsPattern β α] (descr : PatternDescr α β) (name := Name.anonymous) : Pattern α β :=
|
||||
{filter := (descr =~ ·), descr? := descr, name}
|
||||
|
||||
instance [IsPattern β α] : Coe (PatternDescr α β) (Pattern α β) := ⟨(.ofDescr ·)⟩
|
||||
|
||||
@[inherit_doc PatternDescr.all, inline]
|
||||
def Pattern.not [IsPattern β α] (p : Pattern α β) : Pattern α β :=
|
||||
PatternDescr.not p
|
||||
|
||||
@[inherit_doc PatternDescr.all, inline]
|
||||
def Pattern.all [IsPattern β α] (ps : Array (Pattern α β)) : Pattern α β :=
|
||||
PatternDescr.all ps
|
||||
|
||||
@[inherit_doc PatternDescr.all, inline]
|
||||
def Pattern.any [IsPattern β α] (ps : Array (Pattern α β)) : Pattern α β :=
|
||||
PatternDescr.any ps
|
||||
|
||||
/-- Matches nothing. -/
|
||||
def PatternDescr.empty : PatternDescr α β := .any #[]
|
||||
|
||||
@[inherit_doc PatternDescr.empty]
|
||||
def Pattern.empty : Pattern α β :=
|
||||
{filter := fun _ => false, descr? := some .empty, name := `empty}
|
||||
|
||||
instance : EmptyCollection (PatternDescr α β) := ⟨.empty⟩
|
||||
instance : EmptyCollection (Pattern α β) := ⟨.empty⟩
|
||||
|
||||
/-- Matches eveything. -/
|
||||
def PatternDescr.star : PatternDescr α β := .all #[]
|
||||
|
||||
@[inherit_doc PatternDescr.star]
|
||||
def Pattern.star : Pattern α β :=
|
||||
{filter := fun _ => true, descr? := some .star, name := `star}
|
||||
|
||||
/-! ## String Patterns -/
|
||||
|
||||
/-- A declarative `String` pattern. Matches some subset of strings. -/
|
||||
inductive StrPatDescr
|
||||
/-- Matches a string that is a member of the array -/
|
||||
| mem (xs : Array String)
|
||||
/-- Matches a string that starts with this prefix. -/
|
||||
| startsWith (affix : String)
|
||||
/-- Matches a string that ends with this suffix. -/
|
||||
| endsWith (affix : String)
|
||||
deriving Inhabited
|
||||
|
||||
/-- Returns whether the string matches the pattern. -/
|
||||
def StrPatDescr.matches (s : String) (self : StrPatDescr) : Bool :=
|
||||
match self with
|
||||
| .mem xs => xs.contains s
|
||||
| .startsWith x => s.startsWith x
|
||||
| .endsWith x => s.endsWith x
|
||||
|
||||
instance : IsPattern StrPatDescr String := ⟨flip StrPatDescr.matches⟩
|
||||
|
||||
/-- A `String` pattern. Matches some subset of strings. -/
|
||||
abbrev StrPat := Pattern String StrPatDescr
|
||||
|
||||
@[inherit_doc Pattern.empty, deprecated Pattern.empty (since := "2025-03-27")]
|
||||
abbrev StrPat.none : StrPat := Pattern.empty
|
||||
|
||||
@[inherit_doc Pattern.ofFn, deprecated Pattern.ofFn (since := "2025-03-27")]
|
||||
abbrev StrPat.satisfies (f : String → Bool) (name := Name.anonymous) : StrPat :=
|
||||
Pattern.ofFn f name
|
||||
|
||||
@[inherit_doc StrPatDescr.mem, inline]
|
||||
def StrPat.mem (xs : Array String) : StrPat :=
|
||||
StrPatDescr.mem xs
|
||||
|
||||
instance : Coe (Array String) StrPatDescr := ⟨.mem⟩
|
||||
instance : Coe (Array String) StrPat := ⟨.mem⟩
|
||||
|
||||
@[inherit_doc StrPatDescr.startsWith, inline]
|
||||
def StrPat.startsWith (affix : String) : StrPat :=
|
||||
StrPatDescr.startsWith affix
|
||||
|
||||
@[inherit_doc StrPatDescr.endsWith, inline]
|
||||
def StrPat.endsWith (affix : String) : StrPat :=
|
||||
StrPatDescr.endsWith affix
|
||||
|
||||
/-- Matches a string that is equal to this one. -/
|
||||
def StrPatDescr.beq (s : String) : StrPatDescr := .mem #[s]
|
||||
|
||||
@[inherit_doc StrPatDescr.mem, inline]
|
||||
def StrPat.beq (s : String) : StrPat :=
|
||||
{filter := (· == s), descr? := some <| StrPatDescr.beq s}
|
||||
|
||||
instance : Coe String StrPatDescr := ⟨.beq⟩
|
||||
instance : Coe String StrPat := ⟨.beq⟩
|
||||
|
||||
/-! ## File Path Patterns -/
|
||||
|
||||
/-- A declarative `FilePath` pattern. Matches some subset of file paths. -/
|
||||
inductive PathPatDescr
|
||||
/-- Matches a file path whose normalized string representation satisfies the pattern. -/
|
||||
| path (p : StrPat)
|
||||
/-- Matches a file path whose extension satisfies the pattern. -/
|
||||
| extension (p : StrPat)
|
||||
/-- Matches a file path whose name satisfies the pattern. -/
|
||||
| fileName (p : StrPat)
|
||||
deriving Inhabited
|
||||
|
||||
/-- Matches a file path that is equal to this one (when both are normalized). -/
|
||||
@[inline] def PathPatDescr.eq (p : FilePath) : PathPatDescr :=
|
||||
.path p.toString
|
||||
|
||||
/-- Returns whether the string matches the pattern. -/
|
||||
def PathPatDescr.matches (path : FilePath) (self : PathPatDescr) : Bool :=
|
||||
match self with
|
||||
| .path p => p =~ path.normalize.toString
|
||||
| .extension p => path.extension.any (p =~ ·)
|
||||
| .fileName p => path.fileName.any (p =~ ·)
|
||||
|
||||
instance : IsPattern PathPatDescr FilePath := ⟨flip PathPatDescr.matches⟩
|
||||
|
||||
/-- A `FilePath` pattern. Matches some subset of file paths. -/
|
||||
abbrev PathPat := Pattern FilePath PathPatDescr
|
||||
|
||||
@[inherit_doc PathPatDescr.path, inline]
|
||||
def PathPat.path (p : StrPat) : PathPat :=
|
||||
PathPatDescr.path p
|
||||
|
||||
@[inherit_doc PathPatDescr.extension, inline]
|
||||
def PathPat.extension (p : StrPat) : PathPat :=
|
||||
PathPatDescr.extension p
|
||||
|
||||
@[inherit_doc PathPatDescr.fileName, inline]
|
||||
def PathPat.fileName (p : StrPat) : PathPat :=
|
||||
PathPatDescr.fileName p
|
||||
|
||||
/-! ## Version-specific Patterns -/
|
||||
|
||||
/--
|
||||
Whether a string is "version-like".
|
||||
That is, a `v` followed by a digit.
|
||||
-/
|
||||
def isVerLike (s : String) : Bool :=
|
||||
if h : s.utf8ByteSize ≥ 2 then
|
||||
s.get' 0 (by simp [String.atEnd]; omega) == 'v' &&
|
||||
(s.get' ⟨1⟩ (by simp [String.atEnd]; omega)).isDigit
|
||||
else
|
||||
false
|
||||
|
||||
/-- Matches a "version-like" string: a `v` followed by a digit. -/
|
||||
def StrPat.verLike : StrPat := .ofFn isVerLike `verLike
|
||||
|
||||
/-- Default string pattern for a Package's `versionTags`. -/
|
||||
def defaultVersionTags : StrPat := .ofFn isVerLike `default
|
||||
|
||||
/-- Builtin `StrPat` presets available to TOML for `versionTags`. -/
|
||||
def versionTagPresets :=
|
||||
NameMap.empty
|
||||
|>.insert `verLike .verLike
|
||||
|>.insert `default defaultVersionTags
|
||||
|
|
@ -13,3 +13,4 @@ import Lake.DSL.Script
|
|||
import Lake.DSL.Require
|
||||
import Lake.DSL.Targets
|
||||
import Lake.DSL.Meta
|
||||
import Lake.DSL.Key
|
||||
|
|
|
|||
|
|
@ -36,6 +36,12 @@ initialize leanExeAttr : OrderedTagAttribute ←
|
|||
initialize externLibAttr : OrderedTagAttribute ←
|
||||
registerOrderedTagAttribute `extern_lib "mark a definition as a Lake external library target"
|
||||
|
||||
initialize inputFileAttr : OrderedTagAttribute ←
|
||||
registerOrderedTagAttribute `input_file "mark a definition as a Lake input file target"
|
||||
|
||||
initialize inputDirAttr : OrderedTagAttribute ←
|
||||
registerOrderedTagAttribute `input_dir "mark a definition as a Lake input directory target"
|
||||
|
||||
initialize targetAttr : OrderedTagAttribute ←
|
||||
registerOrderedTagAttribute `target "mark a definition as a Lake target"
|
||||
|
||||
|
|
|
|||
56
src/lake/Lake/DSL/Key.lean
Normal file
56
src/lake/Lake/DSL/Key.lean
Normal file
|
|
@ -0,0 +1,56 @@
|
|||
/-
|
||||
Copyright (c) 2025 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
prelude
|
||||
import Lake.Build.Key
|
||||
|
||||
/-! # DSL for Build Key
|
||||
Notation for specifying build keys in a package.
|
||||
-/
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Lake.DSL
|
||||
|
||||
syntax facetSuffix := ":" noWs ident
|
||||
syntax packageTargetLit := ("+" noWs)? ident
|
||||
|
||||
scoped syntax:max "`+" noWs ident facetSuffix* : term
|
||||
scoped syntax:max "`@" noWs (ident)? (noWs "/" noWs packageTargetLit)? facetSuffix* : term
|
||||
|
||||
private def expandFacets (tgt : Term) (facets : Array Ident) : MacroM Term := do
|
||||
let facetLits := facets.map fun facet => Name.quoteFrom facet facet.getId
|
||||
facetLits.foldlM (init := tgt) fun tgt lit => `(BuildKey.facet $tgt $lit)
|
||||
|
||||
private def expandPackageTargetLit
|
||||
(pkg : Term) (stx : TSyntax ``packageTargetLit)
|
||||
: MacroM Term := withRef stx do
|
||||
let `(packageTargetLit|$[+%$mod?]?$tgt) := stx
|
||||
| Macro.throwError "ill-formed package target literal"
|
||||
let tgtName :=
|
||||
if mod?.isSome then
|
||||
tgt.getId ++ PartialBuildKey.moduleTargetIndicator
|
||||
else
|
||||
tgt.getId
|
||||
let tgtLit := Name.quoteFrom tgt tgtName
|
||||
`(BuildKey.packageTarget $pkg $tgtLit)
|
||||
|
||||
macro_rules
|
||||
| `(`+%$tk$mod$[:$facets]*) => withRef tk do
|
||||
let modLit := Name.quoteFrom mod mod.getId
|
||||
let tgt ← `(BuildKey.module $modLit)
|
||||
expandFacets tgt facets
|
||||
| `(`@%$tk$(pkg?)?$[/$tgt?]?$[:$facets]*) => withRef tk do
|
||||
let pkgLit :=
|
||||
if let some pkg := pkg? then
|
||||
Name.quoteFrom pkg pkg.getId
|
||||
else
|
||||
Name.quoteFrom tk Name.anonymous
|
||||
let tgt ←
|
||||
if let some tgt := tgt? then
|
||||
expandPackageTargetLit pkgLit tgt
|
||||
else
|
||||
`(BuildKey.package $pkgLit)
|
||||
expandFacets tgt facets
|
||||
|
|
@ -280,6 +280,46 @@ def elabLeanExeCommand : CommandElab := fun stx => do
|
|||
instance : Coe LeanExeCommand Command where
|
||||
coe x := ⟨x.raw⟩
|
||||
|
||||
/--
|
||||
Define a new input file target for the package.
|
||||
Can optionally be provided with a configuration of type `InputFileConfig`.
|
||||
-/
|
||||
scoped syntax (name := inputFileCommand)
|
||||
(docComment)? (Term.attributes)? "input_file " (identOrStr)? optConfig : command
|
||||
|
||||
@[command_elab inputFileCommand]
|
||||
def elabInputfileCommand : CommandElab := fun stx => do
|
||||
let `(inputFileCommand|$(doc?)? $(attrs?)? input_file%$kw $(nameStx?)? $cfg) := stx
|
||||
| throwErrorAt stx "ill-formed input_file declaration"
|
||||
withRef kw do
|
||||
let cmd ← mkConfigDeclDef ``InputFileConfig InputFile.keyword InputFile.configKind doc? attrs? nameStx? cfg
|
||||
withMacroExpansion stx cmd <| elabCommand cmd
|
||||
|
||||
@[inherit_doc inputFileCommand] abbrev InputFileCommand := TSyntax ``inputFileCommand
|
||||
|
||||
instance : Coe InputFileCommand Command where
|
||||
coe x := ⟨x.raw⟩
|
||||
|
||||
/--
|
||||
Define a new input directory target for the package.
|
||||
Can optionally be provided with a configuration of type `InputDirConfig`.
|
||||
-/
|
||||
scoped syntax (name := inputDirCommand)
|
||||
(docComment)? (Term.attributes)? "input_dir " (identOrStr)? optConfig : command
|
||||
|
||||
@[command_elab inputDirCommand]
|
||||
def elabInputDirCommand : CommandElab := fun stx => do
|
||||
let `(inputDirCommand|$(doc?)? $(attrs?)? input_dir%$kw $(nameStx?)? $cfg) := stx
|
||||
| throwErrorAt stx "ill-formed input_dir declaration"
|
||||
withRef kw do
|
||||
let cmd ← mkConfigDeclDef ``InputDirConfig InputDir.keyword InputDir.configKind doc? attrs? nameStx? cfg
|
||||
withMacroExpansion stx cmd <| elabCommand cmd
|
||||
|
||||
@[inherit_doc inputDirCommand] abbrev InputDirCommand := TSyntax ``inputDirCommand
|
||||
|
||||
instance : Coe InputDirCommand Command where
|
||||
coe x := ⟨x.raw⟩
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
/-! ## External Library Target Declaration -/
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -193,25 +193,80 @@ protected def StdVer.decodeToml (v : Value) : EDecodeM LeanVer := do
|
|||
|
||||
instance : DecodeToml StdVer := ⟨StdVer.decodeToml⟩
|
||||
|
||||
protected def StrPat.decodeToml (v : Value) (presets : NameMap StrPat := {}) : EDecodeM StrPat :=
|
||||
mutual
|
||||
|
||||
partial def Pattern.decodeToml
|
||||
[IsPattern β α] [DecodeToml β] (v : Value) (presets : NameMap (Pattern α β) := {})
|
||||
: EDecodeM (Pattern α β) :=
|
||||
have : DecodeToml (PatternDescr α β) := ⟨PatternDescr.decodeToml⟩
|
||||
match v with
|
||||
| .array _ vs => .mem <$> decodeArray vs
|
||||
| .string _ s =>
|
||||
if s == "*" then
|
||||
return .star
|
||||
else
|
||||
.ofDescr <$> decodeToml v
|
||||
| .table r t => do
|
||||
if let some pre ← t.decode? `startsWith then
|
||||
return .startsWith pre
|
||||
else if let some name ← t.decode? `preset then
|
||||
if let some name ← t.decode? `preset then
|
||||
if let some preset := presets.find? name then
|
||||
return preset
|
||||
else
|
||||
throwDecodeErrorAt r s!"unknown preset '{name}'"
|
||||
else
|
||||
throwDecodeErrorAt r "expected 'startsWith' or 'preset'"
|
||||
| v => throwDecodeErrorAt v.ref "expected array or table"
|
||||
.ofDescr <$> decodeToml v
|
||||
| v => .ofDescr <$> decodeToml v
|
||||
|
||||
instance : DecodeToml StrPat := ⟨StrPat.decodeToml⟩
|
||||
partial def PatternDescr.decodeToml
|
||||
[IsPattern β α] [DecodeToml β] (v : Value)
|
||||
: EDecodeM (PatternDescr α β) :=
|
||||
have : DecodeToml (Pattern α β) := ⟨Pattern.decodeToml⟩
|
||||
match v with
|
||||
| .table _ t => do
|
||||
if let some p ← t.decode? `not then
|
||||
return .not p
|
||||
if let some p ← t.decode? `any then
|
||||
return .any p
|
||||
else if let some p ← t.decode? `all then
|
||||
return .all p
|
||||
else
|
||||
.coe <$> decodeToml v
|
||||
| v => .coe <$> decodeToml v
|
||||
|
||||
end
|
||||
|
||||
instance [IsPattern β α] [DecodeToml β] : DecodeToml (Pattern α β) := ⟨Pattern.decodeToml⟩
|
||||
instance [IsPattern β α] [DecodeToml β] : DecodeToml (PatternDescr α β) := ⟨PatternDescr.decodeToml⟩
|
||||
|
||||
protected def StrPatDescr.decodeToml (v : Value) : EDecodeM StrPatDescr :=
|
||||
match v with
|
||||
| .array _ vs => .mem <$> decodeArray vs
|
||||
| .table r t => do
|
||||
if let some affix ← t.decode? `startsWith then
|
||||
return .startsWith affix
|
||||
else if let some affix ← t.decode? `endsWith then
|
||||
return .endsWith affix
|
||||
else
|
||||
throwDecodeErrorAt r "expected string pattern"
|
||||
| v => throwDecodeErrorAt v.ref "expected string pattern"
|
||||
|
||||
instance : DecodeToml StrPatDescr := ⟨StrPatDescr.decodeToml⟩
|
||||
|
||||
protected def PathPatDescr.decodeToml (v : Value) : EDecodeM PathPatDescr :=
|
||||
match v with
|
||||
| .table r t => do
|
||||
if let some p ← t.decode? `path then
|
||||
return .path p
|
||||
else if let some p ← t.decode? `extension then
|
||||
return .extension p
|
||||
else if let some p ← t.decode? `fileName then
|
||||
return .fileName p
|
||||
else
|
||||
throwDecodeErrorAt r "expected file path pattern"
|
||||
| v => throwDecodeErrorAt v.ref "expected file path pattern"
|
||||
|
||||
instance : DecodeToml PathPatDescr := ⟨PathPatDescr.decodeToml⟩
|
||||
|
||||
def decodeVersionTags (v : Value) : EDecodeM StrPat :=
|
||||
StrPat.decodeToml (presets := versionTagPresets) v
|
||||
inline <| Pattern.decodeToml (presets := versionTagPresets) v
|
||||
|
||||
instance : DecodeField (PackageConfig n) `versionTags where
|
||||
decodeField := decodeFieldCore `versionTags decodeVersionTags
|
||||
|
|
@ -222,6 +277,16 @@ instance [DecodeToml α] : DecodeToml (Option α) := ⟨(some <$> decodeToml ·)
|
|||
def decodeFacets (kind : Name) (val : Value) : EDecodeM (Array Name) := do
|
||||
return (← val.decodeArray).map (kind ++ ·)
|
||||
|
||||
instance : DecodeField (LeanLibConfig n) `defaultFacets where
|
||||
decodeField := decodeFieldCore `defaultFacets (decodeFacets LeanLib.facetKind)
|
||||
|
||||
def PartialBuildKey.decodeToml (v : Value) : EDecodeM PartialBuildKey := do
|
||||
match PartialBuildKey.parse (← v.decodeString) with
|
||||
| .ok k => return k
|
||||
| .error e => throwDecodeErrorAt v.ref e
|
||||
|
||||
instance : DecodeToml PartialBuildKey := ⟨PartialBuildKey.decodeToml⟩
|
||||
|
||||
instance : DecodeField (LeanLibConfig n) `defaultFacets where
|
||||
decodeField := decodeFieldCore `defaultFacets (decodeFacets LeanLib.facetKind)
|
||||
|
||||
|
|
@ -300,6 +365,8 @@ local macro "gen_toml_decoders%" : command => do
|
|||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genDecodeToml cmds ``LeanExeConfig true
|
||||
(exclude := #[`nativeFacets, `dynlibs, `plugins])
|
||||
let cmds ← genDecodeToml cmds ``InputFileConfig true
|
||||
let cmds ← genDecodeToml cmds ``InputDirConfig true
|
||||
-- Package
|
||||
let cmds ← genDecodeToml cmds ``WorkspaceConfig false
|
||||
let cmds ← genDecodeToml cmds ``PackageConfig true
|
||||
|
|
@ -314,6 +381,8 @@ def decodeTargetDecls
|
|||
let r := (#[], {})
|
||||
let r ← go r LeanLib.keyword LeanLib.configKind LeanLibConfig.decodeToml
|
||||
let r ← go r LeanExe.keyword LeanExe.configKind LeanExeConfig.decodeToml
|
||||
let r ← go r InputFile.keyword InputFile.configKind InputFileConfig.decodeToml
|
||||
let r ← go r InputDir.keyword InputDir.configKind InputDirConfig.decodeToml
|
||||
return r
|
||||
where
|
||||
go r kw kind (decode : {n : Name} → Table → DecodeM (ConfigType kind pkg n)) := do
|
||||
|
|
|
|||
|
|
@ -35,11 +35,45 @@ instance [ToToml α] : ToToml (Array α) := ⟨(.array .missing <| ·.map toToml
|
|||
instance : ToToml (Array Value) := ⟨(.array .missing <| ·)⟩
|
||||
instance : ToToml Table := ⟨.table .missing⟩
|
||||
|
||||
class ToToml? (α : Type u) where
|
||||
toToml? : α → Option Value
|
||||
|
||||
export ToToml? (toToml?)
|
||||
|
||||
instance(priority := high) [ToToml α] : ToToml? α where
|
||||
toToml? v := some (toToml v)
|
||||
|
||||
def Toml.encodeArray? [ToToml? α] (as : Array α) : Option (Array Value) :=
|
||||
as.foldl (init := some #[]) fun vs? a => do
|
||||
let vs ← vs?
|
||||
let v ← toToml? a
|
||||
return vs.push v
|
||||
|
||||
instance [ToToml? α] : ToToml? (Array α) where
|
||||
toToml? as := toToml <$> Toml.encodeArray? as
|
||||
|
||||
instance [ToToml? α] : ToToml? (Option α) := ⟨(·.bind toToml?)⟩
|
||||
instance [ToToml α] : ToToml? (Option α) := ⟨(·.map toToml)⟩
|
||||
|
||||
namespace Toml
|
||||
|
||||
/-- Insert a value into a table unless it represents a nullish value. -/
|
||||
class SmartInsert (α : Type u) where
|
||||
smartInsert (k : Name) : α → Table → Table
|
||||
|
||||
namespace Toml.Table
|
||||
instance (priority := low) [ToToml? α] : SmartInsert α where
|
||||
smartInsert k v t := t.insertSome k (toToml? v)
|
||||
|
||||
instance : SmartInsert Table where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
instance [ToToml (Array α)] : SmartInsert (Array α) where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
instance : SmartInsert String where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
namespace Table
|
||||
|
||||
/-- Inserts the encoded value into the table. -/
|
||||
@[inline] nonrec def insert [enc : ToToml α] (k : Name) (v : α) (t : Table) : Table :=
|
||||
|
|
@ -55,15 +89,6 @@ instance [ToToml α] : SmartInsert (Option α) := ⟨Table.insertSome⟩
|
|||
@[inline] nonrec def smartInsert [SmartInsert α] (k : Name) (v : α) (t : Table) : Table :=
|
||||
SmartInsert.smartInsert k v t
|
||||
|
||||
instance : SmartInsert Table where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
instance [ToToml (Array α)] : SmartInsert (Array α) where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
instance : SmartInsert String where
|
||||
smartInsert k v t := t.insertUnless v.isEmpty k (toToml v)
|
||||
|
||||
/-- Insert a value into the table if `p` is `true`. -/
|
||||
@[inline] nonrec def insertIf [enc : ToToml α] (p : Bool) (k : Name) (v : α) (t : Table) : Table :=
|
||||
t.insertIf p k (enc.toToml v)
|
||||
|
|
|
|||
1
src/lake/tests/inputFile/.gitignore
vendored
Normal file
1
src/lake/tests/inputFile/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
inputs
|
||||
2
src/lake/tests/inputFile/clean.sh
Executable file
2
src/lake/tests/inputFile/clean.sh
Executable file
|
|
@ -0,0 +1,2 @@
|
|||
rm -rf .lake lake-manifest.json
|
||||
rm -rf inputs lakefile.produced.lean lakefileAlt.produced.toml
|
||||
16
src/lake/tests/inputFile/lakefile.expected.lean
Normal file
16
src/lake/tests/inputFile/lakefile.expected.lean
Normal file
|
|
@ -0,0 +1,16 @@
|
|||
import Lake
|
||||
|
||||
open System Lake DSL
|
||||
|
||||
package test
|
||||
|
||||
@[default_target] lean_exe test where needs := #[`@/foo, `@/barz]
|
||||
|
||||
input_file foo where
|
||||
path := "inputs/foo.txt"
|
||||
text := true
|
||||
|
||||
input_dir barz where
|
||||
path := "inputs/barz"
|
||||
text := true
|
||||
filter := .fileName (.startsWith "b")
|
||||
17
src/lake/tests/inputFile/lakefile.toml
Normal file
17
src/lake/tests/inputFile/lakefile.toml
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
name = "test"
|
||||
defaultTargets = ["test"]
|
||||
|
||||
[[input_file]]
|
||||
name = "foo"
|
||||
path = "inputs/foo.txt"
|
||||
text = true
|
||||
|
||||
[[input_dir]]
|
||||
name = "barz"
|
||||
path = "inputs/barz"
|
||||
text = true
|
||||
filter.fileName.startsWith = "b"
|
||||
|
||||
[[lean_exe]]
|
||||
name = "test"
|
||||
needs = ["foo", "barz"]
|
||||
17
src/lake/tests/inputFile/lakefileAlt.expected.toml
Normal file
17
src/lake/tests/inputFile/lakefileAlt.expected.toml
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
name = "test"
|
||||
defaultTargets = ["test"]
|
||||
|
||||
[[lean_exe]]
|
||||
name = "test"
|
||||
needs = ["foo", "barz"]
|
||||
|
||||
[[input_file]]
|
||||
name = "foo"
|
||||
path = "inputs/foo.txt"
|
||||
text = true
|
||||
|
||||
[[input_dir]]
|
||||
name = "barz"
|
||||
path = "inputs/barz"
|
||||
text = true
|
||||
filter = {fileName = {startsWith = "b"}}
|
||||
18
src/lake/tests/inputFile/lakefileAlt.lean
Normal file
18
src/lake/tests/inputFile/lakefileAlt.lean
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
import Lake
|
||||
|
||||
open System Lake DSL
|
||||
|
||||
package test
|
||||
|
||||
input_file foo where
|
||||
path := "inputs/foo.txt"
|
||||
text := true
|
||||
|
||||
input_dir barz where
|
||||
path := "inputs/barz"
|
||||
text := true
|
||||
filter := .fileName (.startsWith "b")
|
||||
|
||||
@[default_target]
|
||||
lean_exe test where
|
||||
needs := #[foo, barz]
|
||||
12
src/lake/tests/inputFile/setup.sh
Executable file
12
src/lake/tests/inputFile/setup.sh
Executable file
|
|
@ -0,0 +1,12 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
./clean.sh
|
||||
|
||||
# Setup directory
|
||||
mkdir -p inputs/barz
|
||||
echo foo > inputs/foo.txt
|
||||
echo bar > inputs/barz/bar.txt
|
||||
echo baz > inputs/barz/baz.txt
|
||||
echo untraced > inputs/untraced.txt
|
||||
echo untraced > inputs/barz/untraced.txt
|
||||
29
src/lake/tests/inputFile/test.lean
Normal file
29
src/lake/tests/inputFile/test.lean
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
import Std.Data.HashMap
|
||||
|
||||
def foo := include_str "inputs" / "foo.txt"
|
||||
def bar := include_str "inputs" / "barz" / "bar.txt"
|
||||
def baz := include_str "inputs" / "barz" / "baz.txt"
|
||||
def untraced := include_str "inputs" / "untraced.txt"
|
||||
def untracedBarz := include_str "inputs" / "barz" / "untraced.txt"
|
||||
|
||||
def inputs : Std.HashMap String String :=
|
||||
(∅ : Std.HashMap ..)
|
||||
|>.insert "foo" foo
|
||||
|>.insert "bar" bar
|
||||
|>.insert "baz" baz
|
||||
|>.insert "untraced" untraced
|
||||
|>.insert "untracedBarz" untracedBarz
|
||||
|
||||
def main (args : List String) : IO Unit := do
|
||||
if args.isEmpty then
|
||||
IO.print foo
|
||||
IO.print bar
|
||||
IO.print baz
|
||||
IO.print untraced
|
||||
IO.print untracedBarz
|
||||
else
|
||||
let input :: [] := args
|
||||
| throw <| .userError "USAGE: lake exe test [input]"
|
||||
let some value := inputs[input]?
|
||||
| throw <| .userError s!"error: unknown input '{input}'"
|
||||
IO.print value
|
||||
61
src/lake/tests/inputFile/test.sh
Executable file
61
src/lake/tests/inputFile/test.sh
Executable file
|
|
@ -0,0 +1,61 @@
|
|||
#!/usr/bin/env bash
|
||||
set -euxo pipefail
|
||||
|
||||
LAKE=${LAKE:-../../.lake/build/bin/lake}
|
||||
|
||||
./setup.sh
|
||||
|
||||
# Validate configuration
|
||||
$LAKE -q resolve-deps 2>&1 | diff - /dev/null
|
||||
|
||||
# Test initial directory structure
|
||||
$LAKE exe test | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
foo
|
||||
bar
|
||||
baz
|
||||
untraced
|
||||
untraced
|
||||
EOF
|
||||
) -
|
||||
|
||||
# Validate Lean configuration
|
||||
$LAKE -f lakefileAlt.lean translate-config toml lakefileAlt.produced.toml 2>&1 | diff - /dev/null
|
||||
diff -u --strip-trailing-cr lakefileAlt.expected.toml lakefileAlt.produced.toml
|
||||
$LAKE -f lakefileAlt.lean -q build --no-build 2>&1 | diff - /dev/null
|
||||
|
||||
# Validate TOML->Lean translation
|
||||
$LAKE translate-config lean lakefile.produced.lean 2>&1 | diff - /dev/null
|
||||
diff -u --strip-trailing-cr lakefile.expected.lean lakefile.produced.lean
|
||||
$LAKE -f lakefile.expected.lean -q build --no-build 2>&1 | diff - /dev/null
|
||||
|
||||
# Test input file target
|
||||
cat "`$LAKE query foo`" | diff -u --strip-trailing-cr <(echo foo) -
|
||||
|
||||
# Test input directory target
|
||||
cat `$LAKE query barz` | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
bar
|
||||
baz
|
||||
EOF
|
||||
) -
|
||||
|
||||
# Test input file dependency
|
||||
echo traced > inputs/foo.txt
|
||||
$LAKE exe test foo | diff -u --strip-trailing-cr <(echo traced) -
|
||||
|
||||
# Test input directory dependency
|
||||
echo traced > inputs/barz/bar.txt
|
||||
$LAKE exe test bar | diff -u --strip-trailing-cr <(echo traced) -
|
||||
echo traced > inputs/barz/baz.txt
|
||||
$LAKE exe test baz | diff -u --strip-trailing-cr <(echo traced) -
|
||||
|
||||
# Test untraced dependencies
|
||||
echo traced > inputs/untraced.txt
|
||||
echo traced > inputs/barz/untraced.txt
|
||||
$LAKE exe test | diff -u --strip-trailing-cr <(cat << 'EOF'
|
||||
traced
|
||||
traced
|
||||
traced
|
||||
untraced
|
||||
untraced
|
||||
EOF
|
||||
) -
|
||||
Loading…
Add table
Reference in a new issue