# Build Target Fetching #

Utilities for fetching package, library, module, and executable targets and facets.

source
@[inline]
def Lake.KConfigDecl.get {m : Type → Type u_1} {kind : Lean.Name} [Monad m] [MonadError m] [MonadLake m] (self : KConfigDecl kind) :
m (ConfigTarget kind)

Get the target in the workspace corresponding to this configuration.

Equations

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

Instances For

## Package Facets & Targets #

source
def Lake.Package.fetchTargetJob (self : Package) (target : Lean.Name) :
FetchM OpaqueJob

Fetch the build job of the specified package target.

Equations

- self.fetchTargetJob target = do let __do_lift ← (Lake.Package.target target self).fetch pure __do_lift.toOpaque

Instances For

source
def Lake.TargetDecl.fetch {α : Type} (self : TargetDecl) [FamilyOut (CustomData self.pkg) self.name α] :
FetchM (Job α)

Fetch the build result of a target.

Equations

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

Instances For

source
def Lake.TargetDecl.fetchJob (self : TargetDecl) :
FetchM OpaqueJob

Fetch the build job of the target.

Equations

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

Instances For

source
@[inline]
def Lake.PackageFacetDecl.fetch {α : Type} (pkg : Package) (self : PackageFacetDecl) [FamilyOut FacetOut self.name α] :
FetchM (Job α)

Fetch the build result of a package facet.

Equations

- Lake.PackageFacetDecl.fetch pkg self = (Lake.Package.facetCore self.name pkg).fetch

Instances For

source
@[deprecated "Deprecated without replacement." (since := "2025-03-17")]
def Lake.PackageFacetConfig.fetchJob {name : Lean.Name} (pkg : Package) (self : PackageFacetConfig name) :
FetchM OpaqueJob

Fetch the build job of a package facet.

Equations

- Lake.PackageFacetConfig.fetchJob pkg self = do let __do_lift ← (Lake.Package.facet self.name pkg).fetch pure __do_lift.toOpaque

Instances For

source
def Lake.Package.fetchFacetJob (name : Lean.Name) (self : Package) :
FetchM OpaqueJob

Fetch the build job of a library facet.

Equations

- Lake.Package.fetchFacetJob name self = do let __do_lift ← (Lake.Package.facet name self).fetch pure __do_lift.toOpaque

Instances For

## Module Facets #

source
@[inline]
def Lake.ModuleFacetDecl.fetch {α : Type} (mod : Module) (self : ModuleFacetDecl) [FamilyOut FacetOut self.name α] :
FetchM (Job α)

Fetch the build result of a module facet.

Equations

- Lake.ModuleFacetDecl.fetch mod self = (Lake.Module.facetCore self.name mod).fetch

Instances For

source
@[deprecated "Deprecated without replacement." (since := "2025-03-17")]
def Lake.ModuleFacetConfig.fetchJob {name : Lean.Name} (mod : Module) (self : ModuleFacetConfig name) :
FetchM OpaqueJob

Fetch the build job of a module facet.

Equations

- Lake.ModuleFacetConfig.fetchJob mod self = do let __do_lift ← (Lake.Module.facet self.name mod).fetch pure __do_lift.toOpaque

Instances For

source
def Lake.Module.fetchFacetJob (name : Lean.Name) (self : Module) :
FetchM OpaqueJob

Fetch the build job of a module facet.

Equations

- Lake.Module.fetchFacetJob name self = do let __do_lift ← (Lake.Module.facet name self).fetch pure __do_lift.toOpaque

Instances For

## Lean Library Facets #

source
@[inline]
def Lake.LeanLibDecl.get {m : Type → Type u_1} (self : LeanLibDecl) [Monad m] [MonadError m] [MonadLake m] :
m LeanLib

Get the Lean library in the workspace corresponding to this configuration.

Equations

- self.get = Lake.KConfigDecl.get self

Instances For

source
@[inline]
def Lake.LibraryFacetDecl.fetch {α : Type} (lib : LeanLib) (self : LibraryFacetDecl) [FamilyOut FacetOut self.name α] :
FetchM (Job α)

Fetch the build result of a library facet.

Equations

- Lake.LibraryFacetDecl.fetch lib self = (Lake.LeanLib.facetCore self.name lib).fetch

Instances For

source
@[deprecated "Deprecated without replacement," (since := "2025-03-17")]
def Lake.LibraryFacetConfig.fetchJob {name : Lean.Name} (lib : LeanLib) (self : LibraryFacetConfig name) :
FetchM OpaqueJob

Fetch the build job of a library facet.

Equations

- Lake.LibraryFacetConfig.fetchJob lib self = do let __do_lift ← (Lake.LeanLib.facet self.name lib).fetch pure __do_lift.toOpaque

Instances For

source
def Lake.LeanLib.fetchFacetJob (name : Lean.Name) (self : LeanLib) :
FetchM OpaqueJob

Fetch the build job of a library facet.

Equations

- Lake.LeanLib.fetchFacetJob name self = do let __do_lift ← (Lake.LeanLib.facet name self).fetch pure __do_lift.toOpaque

Instances For

## Lean Executable Target #

source
@[inline]
def Lake.LeanExeDecl.get {m : Type → Type u_1} (self : LeanExeDecl) [Monad m] [MonadError m] [MonadLake m] :
m LeanExe

Get the Lean executable in the workspace corresponding to this configuration.

Equations

- self.get = Lake.KConfigDecl.get self

Instances For

source
@[inline]
def Lake.LeanExe.fetch (self : LeanExe) :
FetchM (Job System.FilePath)

Fetch the build of the Lean executable.

Equations

- self.fetch = self.exe.fetch

Instances For

source
@[inline]
def Lake.LeanExeDecl.fetch (self : LeanExeDecl) :
FetchM (Job System.FilePath)

Fetch the build of the Lean executable.

Equations

- self.fetch = do let __do_lift ← self.get __do_lift.fetch

Instances For

## Input File / Directory Targets #

source
@[inline]
def Lake.InputFile.fetch (self : InputFile) :
FetchM (Job System.FilePath)

Fetch the input file.

Equations

- self.fetch = self.default.fetch

Instances For

source
@[inline]
def Lake.InputFileDecl.get {m : Type → Type u_1} (self : InputFileDecl) [Monad m] [MonadError m] [MonadLake m] :
m InputFile

Get the input file in the workspace corresponding to this configuration.

Equations

- self.get = Lake.KConfigDecl.get self

Instances For

source
@[inline]
def Lake.InputFileDecl.fetch (self : InputFileDecl) :
FetchM (Job System.FilePath)

Fetch the input file.

Equations

- self.fetch = do let __do_lift ← self.get __do_lift.default.fetch

Instances For

source
@[inline]
def Lake.InputDir.fetch (self : InputDir) :
FetchM (Job (Array System.FilePath))

Fetch the files in the input directory.

Equations

- self.fetch = self.default.fetch

Instances For

source
@[inline]
def Lake.InputDirDecl.get {m : Type → Type u_1} (self : InputDirDecl) [Monad m] [MonadError m] [MonadLake m] :
m InputDir

Get the input directory in the workspace corresponding to this configuration.

Equations

- self.get = Lake.KConfigDecl.get self

Instances For

source
@[inline]
def Lake.InputDirDecl.fetch (self : InputDirDecl) :
FetchM (Job (Array System.FilePath))

Fetch the files in the input directory.

Equations

- self.fetch = do let __do_lift ← self.get __do_lift.default.fetch

Instances For