Build Target Fetching

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

@[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.

Package Facets & Targets

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

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.

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.

@[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

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

Module Facets

@[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

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

Lean Library Facets

@[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

@[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

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

Lean Executable Target

@[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

@[inline]

def Lake.LeanExe.fetch (self : LeanExe) : FetchM (Job System.FilePath)

Fetch the build of the Lean executable.

Equations

• self.fetch = self.exe.fetch

@[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

Input File / Directory Targets

@[inline]

def Lake.InputFile.fetch (self : InputFile) : FetchM (Job System.FilePath)

Fetch the input file.

Equations

• self.fetch = self.default.fetch

@[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

@[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

@[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

@[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

@[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