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.

Package Facets & Targets

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

Fetch the build job of the specified package target.

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

Fetch the build result of a target.

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

Fetch the build job of the target.

@[inline]

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

Fetch the build result of a package facet.

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

Fetch the build job of a library facet.

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.

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

Fetch the build job of a module facet.

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.

@[inline]

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

Fetch the build result of a library facet.

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

Fetch the build job of a library facet.

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.

@[inline]

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

Fetch the build of the Lean executable.

@[inline]

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

Fetch the build of the Lean executable.

Input File / Directory Targets

@[inline]

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

Fetch the input file.

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

@[inline]

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

Fetch the input file.

@[inline]

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

Fetch the files in the input directory.

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

@[inline]

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

Fetch the files in the input directory.