From 2d28331cb663ece501db099325364c12b5024425 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 28 Mar 2025 15:47:58 -0400 Subject: [PATCH] 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. --- src/lake/Lake/Build/Common.lean | 22 ++ src/lake/Lake/Build/Data.lean | 23 +- src/lake/Lake/Build/Facets.lean | 9 + src/lake/Lake/Build/Info.lean | 100 ++++++-- src/lake/Lake/Build/InitFacets.lean | 3 + src/lake/Lake/Build/InputFile.lean | 52 ++++ src/lake/Lake/Build/Key.lean | 82 +++++- src/lake/Lake/Build/Library.lean | 11 +- src/lake/Lake/Build/Target/Fetch.lean | 88 ++++++- src/lake/Lake/Build/Targets.lean | 61 +++-- src/lake/Lake/CLI/Translate/Lean.lean | 112 +++++++- src/lake/Lake/CLI/Translate/Toml.lean | 62 ++++- src/lake/Lake/Config/ConfigDecl.lean | 38 ++- src/lake/Lake/Config/InputFile.lean | 16 ++ src/lake/Lake/Config/InputFileConfig.lean | 57 +++++ src/lake/Lake/Config/Kinds.lean | 89 +++++++ src/lake/Lake/Config/LeanExe.lean | 1 + src/lake/Lake/Config/LeanExeConfig.lean | 3 + src/lake/Lake/Config/LeanLibConfig.lean | 3 + src/lake/Lake/Config/Meta.lean | 7 +- src/lake/Lake/Config/Package.lean | 50 ---- src/lake/Lake/Config/Pattern.lean | 241 ++++++++++++++++++ src/lake/Lake/DSL.lean | 1 + src/lake/Lake/DSL/AttributesCore.lean | 6 + src/lake/Lake/DSL/Key.lean | 56 ++++ src/lake/Lake/DSL/Targets.lean | 40 +++ src/lake/Lake/Load/Toml.lean | 87 ++++++- src/lake/Lake/Toml/Encode.lean | 45 +++- src/lake/tests/inputFile/.gitignore | 1 + src/lake/tests/inputFile/clean.sh | 2 + .../tests/inputFile/lakefile.expected.lean | 16 ++ src/lake/tests/inputFile/lakefile.toml | 17 ++ .../tests/inputFile/lakefileAlt.expected.toml | 17 ++ src/lake/tests/inputFile/lakefileAlt.lean | 18 ++ src/lake/tests/inputFile/setup.sh | 12 + src/lake/tests/inputFile/test.lean | 29 +++ src/lake/tests/inputFile/test.sh | 61 +++++ 37 files changed, 1357 insertions(+), 181 deletions(-) create mode 100644 src/lake/Lake/Build/InputFile.lean create mode 100644 src/lake/Lake/Config/InputFile.lean create mode 100644 src/lake/Lake/Config/InputFileConfig.lean create mode 100644 src/lake/Lake/Config/Kinds.lean create mode 100644 src/lake/Lake/Config/Pattern.lean create mode 100644 src/lake/Lake/DSL/Key.lean create mode 100644 src/lake/tests/inputFile/.gitignore create mode 100755 src/lake/tests/inputFile/clean.sh create mode 100644 src/lake/tests/inputFile/lakefile.expected.lean create mode 100644 src/lake/tests/inputFile/lakefile.toml create mode 100644 src/lake/tests/inputFile/lakefileAlt.expected.toml create mode 100644 src/lake/tests/inputFile/lakefileAlt.lean create mode 100755 src/lake/tests/inputFile/setup.sh create mode 100644 src/lake/tests/inputFile/test.lean create mode 100755 src/lake/tests/inputFile/test.sh diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 031707bc38..305d63c2df 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -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: diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean index 0a53f4b43b..cee9f040f4 100644 --- a/src/lake/Lake/Build/Data.lean +++ b/src/lake/Lake/Build/Data.lean @@ -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) diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean index 2c9f2f76c2..bcd502b326 100644 --- a/src/lake/Lake/Build/Facets.lean +++ b/src/lake/Lake/Build/Facets.lean @@ -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 diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean index 33ac477003..2a057d7a57 100644 --- a/src/lake/Lake/Build/Info.lean +++ b/src/lake/Lake/Build/Info.lean @@ -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 diff --git a/src/lake/Lake/Build/InitFacets.lean b/src/lake/Lake/Build/InitFacets.lean index 8dbdd3d21b..7c9cd2e36f 100644 --- a/src/lake/Lake/Build/InitFacets.lean +++ b/src/lake/Lake/Build/InitFacets.lean @@ -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 diff --git a/src/lake/Lake/Build/InputFile.lean b/src/lake/Lake/Build/InputFile.lean new file mode 100644 index 0000000000..a0891eceea --- /dev/null +++ b/src/lake/Lake/Build/InputFile.lean @@ -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 diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index 7d8f4eec15..a8d48a856a 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -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 diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean index 46dc47ed9a..029b1bbbbc 100644 --- a/src/lake/Lake/Build/Library.lean +++ b/src/lake/Lake/Build/Library.lean @@ -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 := diff --git a/src/lake/Lake/Build/Target/Fetch.lean b/src/lake/Lake/Build/Target/Fetch.lean index 23b6b7aff1..ec1e5f9579 100644 --- a/src/lake/Lake/Build/Target/Fetch.lean +++ b/src/lake/Lake/Build/Target/Fetch.lean @@ -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 diff --git a/src/lake/Lake/Build/Targets.lean b/src/lake/Lake/Build/Targets.lean index f690f477be..43ae04f5db 100644 --- a/src/lake/Lake/Build/Targets.lean +++ b/src/lake/Lake/Build/Targets.lean @@ -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 diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 9abc2bd2c9..a8bfe50181 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -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]* ) diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean index ae2eba5993..9ab8f66a95 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/src/lake/Lake/CLI/Translate/Toml.lean @@ -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) diff --git a/src/lake/Lake/Config/ConfigDecl.lean b/src/lake/Lake/Config/ConfigDecl.lean index 5aad70c170..7d53ae3766 100644 --- a/src/lake/Lake/Config/ConfigDecl.lean +++ b/src/lake/Lake/Config/ConfigDecl.lean @@ -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 diff --git a/src/lake/Lake/Config/InputFile.lean b/src/lake/Lake/Config/InputFile.lean new file mode 100644 index 0000000000..855e425193 --- /dev/null +++ b/src/lake/Lake/Config/InputFile.lean @@ -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 diff --git a/src/lake/Lake/Config/InputFileConfig.lean b/src/lake/Lake/Config/InputFileConfig.lean new file mode 100644 index 0000000000..13daadcd7a --- /dev/null +++ b/src/lake/Lake/Config/InputFileConfig.lean @@ -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) := ⟨{}⟩ diff --git a/src/lake/Lake/Config/Kinds.lean b/src/lake/Lake/Config/Kinds.lean new file mode 100644 index 0000000000..90d9e8ceb7 --- /dev/null +++ b/src/lake/Lake/Config/Kinds.lean @@ -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 diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean index eece5a2e3b..7c98c2d24a 100644 --- a/src/lake/Lake/Config/LeanExe.lean +++ b/src/lake/Lake/Config/LeanExe.lean @@ -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 diff --git a/src/lake/Lake/Config/LeanExeConfig.lean b/src/lake/Lake/Config/LeanExeConfig.lean index b7bab0e558..43615472c0 100644 --- a/src/lake/Lake/Config/LeanExeConfig.lean +++ b/src/lake/Lake/Config/LeanExeConfig.lean @@ -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 diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean index 523cec48d1..8e10aba7dd 100644 --- a/src/lake/Lake/Config/LeanLibConfig.lean +++ b/src/lake/Lake/Config/LeanLibConfig.lean @@ -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 diff --git a/src/lake/Lake/Config/Meta.lean b/src/lake/Lake/Config/Meta.lean index 455614e8d8..160f172bc1 100644 --- a/src/lake/Lake/Config/Meta.lean +++ b/src/lake/Lake/Config/Meta.lean @@ -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} diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 45e72e1d4a..54fb39d0fb 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -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 -/ -------------------------------------------------------------------------------- diff --git a/src/lake/Lake/Config/Pattern.lean b/src/lake/Lake/Config/Pattern.lean new file mode 100644 index 0000000000..09962da4b1 --- /dev/null +++ b/src/lake/Lake/Config/Pattern.lean @@ -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 diff --git a/src/lake/Lake/DSL.lean b/src/lake/Lake/DSL.lean index 4240392b19..36f1d956f0 100644 --- a/src/lake/Lake/DSL.lean +++ b/src/lake/Lake/DSL.lean @@ -13,3 +13,4 @@ import Lake.DSL.Script import Lake.DSL.Require import Lake.DSL.Targets import Lake.DSL.Meta +import Lake.DSL.Key diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean index bcba9949a5..1b5408da6b 100644 --- a/src/lake/Lake/DSL/AttributesCore.lean +++ b/src/lake/Lake/DSL/AttributesCore.lean @@ -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" diff --git a/src/lake/Lake/DSL/Key.lean b/src/lake/Lake/DSL/Key.lean new file mode 100644 index 0000000000..ba1af8a90b --- /dev/null +++ b/src/lake/Lake/DSL/Key.lean @@ -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 diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean index 58fbdb11f5..9a9f89edd3 100644 --- a/src/lake/Lake/DSL/Targets.lean +++ b/src/lake/Lake/DSL/Targets.lean @@ -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 -/ -------------------------------------------------------------------------------- diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index c1a565c76b..10907c8ba1 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -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 diff --git a/src/lake/Lake/Toml/Encode.lean b/src/lake/Lake/Toml/Encode.lean index e874e79f74..5f6db91638 100644 --- a/src/lake/Lake/Toml/Encode.lean +++ b/src/lake/Lake/Toml/Encode.lean @@ -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) diff --git a/src/lake/tests/inputFile/.gitignore b/src/lake/tests/inputFile/.gitignore new file mode 100644 index 0000000000..15d7aef969 --- /dev/null +++ b/src/lake/tests/inputFile/.gitignore @@ -0,0 +1 @@ +inputs diff --git a/src/lake/tests/inputFile/clean.sh b/src/lake/tests/inputFile/clean.sh new file mode 100755 index 0000000000..2787f30c33 --- /dev/null +++ b/src/lake/tests/inputFile/clean.sh @@ -0,0 +1,2 @@ +rm -rf .lake lake-manifest.json +rm -rf inputs lakefile.produced.lean lakefileAlt.produced.toml diff --git a/src/lake/tests/inputFile/lakefile.expected.lean b/src/lake/tests/inputFile/lakefile.expected.lean new file mode 100644 index 0000000000..d48ed1f46d --- /dev/null +++ b/src/lake/tests/inputFile/lakefile.expected.lean @@ -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") diff --git a/src/lake/tests/inputFile/lakefile.toml b/src/lake/tests/inputFile/lakefile.toml new file mode 100644 index 0000000000..27dac8d9e0 --- /dev/null +++ b/src/lake/tests/inputFile/lakefile.toml @@ -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"] diff --git a/src/lake/tests/inputFile/lakefileAlt.expected.toml b/src/lake/tests/inputFile/lakefileAlt.expected.toml new file mode 100644 index 0000000000..e90e3a65c0 --- /dev/null +++ b/src/lake/tests/inputFile/lakefileAlt.expected.toml @@ -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"}} diff --git a/src/lake/tests/inputFile/lakefileAlt.lean b/src/lake/tests/inputFile/lakefileAlt.lean new file mode 100644 index 0000000000..9223a7390f --- /dev/null +++ b/src/lake/tests/inputFile/lakefileAlt.lean @@ -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] diff --git a/src/lake/tests/inputFile/setup.sh b/src/lake/tests/inputFile/setup.sh new file mode 100755 index 0000000000..3cd26d2156 --- /dev/null +++ b/src/lake/tests/inputFile/setup.sh @@ -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 diff --git a/src/lake/tests/inputFile/test.lean b/src/lake/tests/inputFile/test.lean new file mode 100644 index 0000000000..e4c75fc49c --- /dev/null +++ b/src/lake/tests/inputFile/test.lean @@ -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 diff --git a/src/lake/tests/inputFile/test.sh b/src/lake/tests/inputFile/test.sh new file mode 100755 index 0000000000..ad05c51828 --- /dev/null +++ b/src/lake/tests/inputFile/test.sh @@ -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 +) -