Build Target Specifiers

structure Lake.BuildSpec : Type

• info : BuildInfo
• buildable : Bool
• format : OutFormat → BuildData self.info.key → String

@[inline]

def Lake.mkConfigBuildSpec {facet : Lean.Name} (info : BuildInfo) (config : FacetConfig facet) (h : BuildData info.key = FacetOut facet) : BuildSpec

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.BuildSpec.fetch (self : BuildSpec) : FetchM (Job (BuildData self.info.key))

Equations

• self.fetch = do let __do_lift ← self.info.fetch Lake.maybeRegisterJob self.info.key.toSimpleString __do_lift

@[inline]

def Lake.BuildSpec.build (self : BuildSpec) : FetchM OpaqueJob

Equations

• self.build = do let __do_lift ← self.fetch pure __do_lift.toOpaque

@[inline]

def Lake.BuildSpec.query (self : BuildSpec) (fmt : OutFormat) : FetchM (Job String)

Equations

• self.query fmt = Lake.maybeRegisterJob self.info.key.toSimpleString =<< do let __do_lift ← self.info.fetch pure (Lake.Job.map (self.format fmt) __do_lift)

def Lake.buildSpecs (specs : Array BuildSpec) : FetchM (Job Unit)

Equations

• Lake.buildSpecs specs = do let __do_lift ← Array.mapM (fun (x : Lake.BuildSpec) => x.build) specs pure (Lake.Job.mixArray __do_lift)

def Lake.querySpecs (specs : Array BuildSpec) (fmt : OutFormat) : FetchM (Job (Array String))

Equations

• Lake.querySpecs specs fmt = do let __do_lift ← Array.mapM (fun (x : Lake.BuildSpec) => x.query fmt) specs pure (Lake.Job.collectArray __do_lift)

Parsing CLI Build Target Specifiers

def Lake.parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package

Equations

• One or more equations did not get rendered due to their size.

def Lake.resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Lean.Name := Lean.Name.anonymous) : Except CliError (Array BuildSpec)

For internal use only.

Equations

• One or more equations did not get rendered due to their size.

def Lake.parseExeTargetSpec (ws : Workspace) (spec : String) : Except CliError LeanExe

Equations

• One or more equations did not get rendered due to their size.

def Lake.parseTargetSpec (ws : Workspace) (spec : String) : EIO CliError (Array BuildSpec)

Equations

• One or more equations did not get rendered due to their size.

def Lake.parseTargetSpecs (ws : Workspace) (specs : List String) : EIO CliError (Array BuildSpec)

Equations

• One or more equations did not get rendered due to their size.