diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean index 289a94a7dd..d7f7485961 100644 --- a/src/lake/Lake/Build/Data.lean +++ b/src/lake/Lake/Build/Data.lean @@ -46,6 +46,8 @@ def OptDataKind.anonymous : OptDataKind α where name := .anonymous wf h := by simp [Name.isAnonymous] at h +instance : Inhabited (OptDataKind α) := ⟨OptDataKind.anonymous⟩ + @[inline] def OptDataKind.isAnonymous (self : OptDataKind α) : Bool := self.name.isAnonymous @@ -183,7 +185,7 @@ scoped macro (name := dataTypeDecl) data_type unit : Unit data_type bool : Bool -data_type file_path : System.FilePath +data_type filepath : System.FilePath data_type dynlib : Dynlib /-- Internal macro for declaring new facet within Lake. -/ diff --git a/src/lake/Lake/Build/Job/Monad.lean b/src/lake/Lake/Build/Job/Monad.lean index d503fe76e2..a694c966f1 100644 --- a/src/lake/Lake/Build/Job/Monad.lean +++ b/src/lake/Lake/Build/Job/Monad.lean @@ -134,7 +134,7 @@ Logs the job's log and throws if there was an error. /-- Apply `f` asynchronously to the job's output. -/ protected def mapM - [OptDataKind β] (self : Job α) (f : α → JobM β) + [kind : OptDataKind β] (self : Job α) (f : α → JobM β) (prio := Task.Priority.default) (sync := false) : SpawnM (Job β) := fun fetch stack store ctx trace => do @@ -156,7 +156,7 @@ Apply `f` asynchronously to the job's output and asynchronously await the resulting job. -/ def bindM - [OptDataKind β] (self : Job α) (f : α → JobM (Job β)) + [kind : OptDataKind β] (self : Job α) (f : α → JobM (Job β)) (prio := Task.Priority.default) (sync := false) : SpawnM (Job β) := fun fetch stack store ctx trace => do diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index a3f936ec14..ea6b8c14ee 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -31,6 +31,9 @@ A build key with some missing info. -/ def PartialBuildKey := BuildKey +/-- Cast a `BuildKey` to a `PartialBuildKey`. -/ +@[inline] def PartialBuildKey.mk (key : BuildKey) : PartialBuildKey := key + /-- Parses a `PartialBuildKey` from a `String`. Uses the same syntax as the `lake build` / `lake query` CLI. diff --git a/src/lake/Lake/Build/Target/Fetch.lean b/src/lake/Lake/Build/Target/Fetch.lean index 13b427a325..13cf2e050d 100644 --- a/src/lake/Lake/Build/Target/Fetch.lean +++ b/src/lake/Lake/Build/Target/Fetch.lean @@ -55,7 +55,9 @@ private def PartialBuildKey.fetchInCoreAux else let shortFacet := if shortFacet.isAnonymous then `default else shortFacet have facet := kind ++ shortFacet - let job ← (job.cast h).bindM fun data => + let some cfg := (← getWorkspace).findFacetConfig? facet + | error s!"invalid target '{root}': unknown facet '{facet}'" + let job ← (job.cast h).bindM (kind := cfg.outKind) fun data => fetch (.facet target kind data facet) return ⟨.facet target facet, cast (by simp) job⟩ where @@ -67,7 +69,8 @@ where | error s!"invalid target '{root}': package '{name}' not found in workspace" return pkg -@[inline] private def PartialBuildKey.fetchInCore +/-- **For internal use only.** -/ +@[inline] def PartialBuildKey.fetchInCore (defaultPkg : Package) (self : PartialBuildKey) : FetchM ((key : BuildKey) × Job (BuildData key)) := fetchInCoreAux defaultPkg self self true @@ -108,7 +111,10 @@ private def BuildKey.fetchCore if h : kind.isAnonymous then error s!"invalid target '{self}': targets of opaque data kinds do not support facets" else - (job.cast h).bindM fun data => fetch (.facet target kind data facetName) + let some cfg := (← getWorkspace).findFacetConfig? facetName + | error s!"invalid target '{root}': unknown facet '{facetName}'" + (job.cast h).bindM (kind := cfg.outKind) fun data => + fetch (.facet target kind data facetName) @[inline] protected def BuildKey.fetch (self : BuildKey) [FamilyOut BuildData self α] : FetchM (Job α) diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 06fbafff31..b961dbe62c 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -381,6 +381,26 @@ protected def query : CliM PUnit := do let results ← ws.runBuild (querySpecs specs fmt) buildConfig results.forM (IO.println ·) +protected def queryKind : CliM PUnit := do + processOptions lakeOption + let opts ← getThe LakeOptions + let config ← mkLoadConfig opts + let ws ← loadWorkspace config + let targetSpecs ← takeArgs + let keys ← targetSpecs.toArray.mapM fun spec => + IO.ofExcept <| PartialBuildKey.parse spec + let buildConfig := mkBuildConfig opts + let r ← ws.runFetchM (cfg := buildConfig) <| keys.mapM fun key => do + let ⟨_, job⟩ ← key.fetchInCore ws.root + let kind := job.kind + let job ← maybeRegisterJob key.toString job.toOpaque + return (kind.name, job) + r.forM (IO.println ·.1) + r.forM fun (_, job) => do + match (← job.wait?) with + | some _ => pure () + | none => error "build failed" + protected def resolveDeps : CliM PUnit := do processOptions lakeOption let opts ← getThe LakeOptions @@ -622,6 +642,7 @@ def lakeCli : (cmd : String) → CliM PUnit | "build" => lake.build | "check-build" => lake.checkBuild | "query" => lake.query +| "query-kind" => lake.queryKind | "update" | "upgrade" => lake.update | "resolve-deps" => lake.resolveDeps | "pack" => lake.pack diff --git a/src/lake/Lake/Config/FacetConfig.lean b/src/lake/Lake/Config/FacetConfig.lean index b4349127f2..10a46d721b 100644 --- a/src/lake/Lake/Config/FacetConfig.lean +++ b/src/lake/Lake/Config/FacetConfig.lean @@ -16,6 +16,8 @@ structure FacetConfig (name : Name) : Type where kind : Name /-- The facet's fetch function. -/ fetchFn : DataType kind → FetchM (Job (FacetOut name)) + /-- The optional data kind of the facet's output. -/ + [outKind : OptDataKind (FacetOut name)] /-- Is this facet compatible with the `lake build` CLI? -/ buildable : Bool := true /-- Format this facet's output (e.g., for `lake query`). -/ @@ -49,11 +51,13 @@ def FacetConfig.toKind? (kind : Name) (self : FacetConfig name) : Option (KFacet /-- A smart constructor for facet configurations that generate jobs for the CLI. -/ @[inline] def mkFacetJobConfig [FormatQuery β] + [outKind : OptDataKind β] [i : FamilyOut DataType kind α] [o : FamilyOut FacetOut facet β] (build : α → FetchM (Job β)) (buildable := true) : KFacetConfig kind facet where buildable + outKind := o.fam_eq ▸ outKind fetchFn := i.fam_eq ▸ o.fam_eq ▸ build format := o.fam_eq ▸ formatQuery diff --git a/src/lake/Lake/DSL/Key.lean b/src/lake/Lake/DSL/Key.lean index ba1af8a90b..94db9257ae 100644 --- a/src/lake/Lake/DSL/Key.lean +++ b/src/lake/Lake/DSL/Key.lean @@ -14,11 +14,15 @@ open Lean namespace Lake.DSL -syntax facetSuffix := ":" noWs ident -syntax packageTargetLit := ("+" noWs)? ident +syntax facetSuffix := atomic(":" noWs) ident +syntax packageTargetLit := atomic("+" noWs)? ident +/-- A module target key literal (with optional facet). -/ scoped syntax:max "`+" noWs ident facetSuffix* : term -scoped syntax:max "`@" noWs (ident)? (noWs "/" noWs packageTargetLit)? facetSuffix* : term + +/-- A package target key literal (with optional facet). -/ +scoped syntax:max "`@" (noWs ident)? + (atomic(noWs "/" noWs) packageTargetLit)? (noWs facetSuffix)* : term private def expandFacets (tgt : Term) (facets : Array Ident) : MacroM Term := do let facetLits := facets.map fun facet => Name.quoteFrom facet facet.getId @@ -41,7 +45,8 @@ macro_rules | `(`+%$tk$mod$[:$facets]*) => withRef tk do let modLit := Name.quoteFrom mod mod.getId let tgt ← `(BuildKey.module $modLit) - expandFacets tgt facets + let key ← expandFacets tgt facets + `(PartialBuildKey.mk $key) | `(`@%$tk$(pkg?)?$[/$tgt?]?$[:$facets]*) => withRef tk do let pkgLit := if let some pkg := pkg? then @@ -53,4 +58,5 @@ macro_rules expandPackageTargetLit pkgLit tgt else `(BuildKey.package $pkgLit) - expandFacets tgt facets + let key ← expandFacets tgt facets + `(PartialBuildKey.mk $key) diff --git a/src/lake/tests/api/keys.lean b/src/lake/tests/api/keys.lean new file mode 100644 index 0000000000..32d84bcd61 --- /dev/null +++ b/src/lake/tests/api/keys.lean @@ -0,0 +1,56 @@ +import Lake.DSL.Key +import Lake.Build.Data +import Lake.Build.Target.Basic +open Lake DSL + +/-! ## Test Key Literal Representations -/ + +/-- info: Lake.BuildKey.module `mod -/ +#guard_msgs in #eval `+mod + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.module `mod) `facet -/ +#guard_msgs in #eval `+mod:facet + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.facet (Lake.BuildKey.module `mod) `f1) `f2 -/ +#guard_msgs in #eval `+mod:f1:f2 + +/-- info: Lake.BuildKey.package Lean.Name.anonymous -/ +#guard_msgs in #eval `@ + +/-- info: Lake.BuildKey.package `pkg -/ +#guard_msgs in #eval `@pkg + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.package `pkg) `facet -/ +#guard_msgs in #eval `@pkg:facet + +/-- info: Lake.BuildKey.packageTarget `pkg `target -/ +#guard_msgs in #eval `@pkg/target + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target) `facet -/ +#guard_msgs in #eval `@pkg/target:facet + +/-- info: Lake.BuildKey.packageTarget `pkg `target.«_+» -/ +#guard_msgs in #eval `@pkg/+target + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget `pkg `target.«_+») `facet -/ +#guard_msgs in #eval `@pkg/+target:facet + +/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `target -/ +#guard_msgs in #eval `@/target + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `target) `facet -/ +#guard_msgs in #eval `@/target:facet + +/-- info: Lake.BuildKey.packageTarget Lean.Name.anonymous `mod.«_+» -/ +#guard_msgs in #eval `@/+mod + +/-- info: Lake.BuildKey.facet (Lake.BuildKey.packageTarget Lean.Name.anonymous `mod.«_+») `facet -/ +#guard_msgs in #eval `@/+mod:facet + +/-! ## Other Tests -/ + +-- Test syntax does not conflict with a type ascription +def stx := (`@pkg : PartialBuildKey) + +-- Test coercion to a target +def coe : Array (Target Dynlib) := #[`@pkg/target:facet] diff --git a/src/lake/tests/api/test.sh b/src/lake/tests/api/test.sh new file mode 100755 index 0000000000..66784be855 --- /dev/null +++ b/src/lake/tests/api/test.sh @@ -0,0 +1,7 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LEAN=${LEAN:-lean} + +# Run Lean tests +$LEAN keys.lean diff --git a/src/lake/tests/kinds/.gitignore b/src/lake/tests/kinds/.gitignore new file mode 100644 index 0000000000..2c8afebd8e --- /dev/null +++ b/src/lake/tests/kinds/.gitignore @@ -0,0 +1 @@ +/files diff --git a/src/lake/tests/kinds/clean.sh b/src/lake/tests/kinds/clean.sh new file mode 100755 index 0000000000..75c70324c9 --- /dev/null +++ b/src/lake/tests/kinds/clean.sh @@ -0,0 +1 @@ +rm -rf .lake lake-manifest.json files diff --git a/src/lake/tests/kinds/lakefile.lean b/src/lake/tests/kinds/lakefile.lean new file mode 100644 index 0000000000..39d75be961 --- /dev/null +++ b/src/lake/tests/kinds/lakefile.lean @@ -0,0 +1,20 @@ +import Lake +open System Lake DSL + +package test where + srcDir := "files" + +lean_lib Lib +lean_exe exe + +input_file inFile where + path := "files" / "test.txt" + +input_dir inDir where + path := "files" + +target pathTarget : FilePath := + return Job.pure "files" + +target dynlibTarget : Dynlib := + return Job.pure {name := "test", path := "test.lib"} diff --git a/src/lake/tests/kinds/test.sh b/src/lake/tests/kinds/test.sh new file mode 100755 index 0000000000..3da791ec01 --- /dev/null +++ b/src/lake/tests/kinds/test.sh @@ -0,0 +1,21 @@ +#!/usr/bin/env bash +set -euxo pipefail + +LAKE=${LAKE:-../../.lake/build/bin/lake} + +./clean.sh + +# setup directory structure +mkdir -p files +touch files/Lib.lean +echo "def main : IO Unit := pure ()" > files/exe.lean +touch files/test.txt + +# Test that targets have their expected data kinds +$LAKE query-kind exe | diff -u --strip-trailing-cr <(echo filepath) - +$LAKE query-kind Lib:static | diff -u --strip-trailing-cr <(echo filepath) - +$LAKE query-kind Lib:shared | diff -u --strip-trailing-cr <(echo dynlib) - +$LAKE query-kind inFile | diff -u --strip-trailing-cr <(echo filepath) - +$LAKE query-kind inDir | diff -u --strip-trailing-cr <(echo [anonymous]) - +$LAKE query-kind pathTarget | diff -u --strip-trailing-cr <(echo filepath) - +$LAKE query-kind dynlibTarget | diff -u --strip-trailing-cr <(echo dynlib) -