Build Target Fetching

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

Package Facets & Targets

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

Fetch the build job of the specified package target.

Equations

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

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

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 PackageData self.name α] : FetchM α

Fetch the build result of a package facet.

Equations

• Lake.PackageFacetDecl.fetch pkg self = (Lake.Package.facet self.name pkg).fetch

def Lake.PackageFacetConfig.fetchJob {name : Lean.Name} (pkg : Package) (self : PackageFacetConfig name) : FetchM OpaqueJob

Fetch the build job of a package facet.

Equations

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

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

Fetch the build job of a library facet.

Equations

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

Module Facets

@[inline]

def Lake.ModuleFacetDecl.fetch {α : Type} (mod : Module) (self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : FetchM α

Fetch the build result of a module facet.

Equations

• Lake.ModuleFacetDecl.fetch mod self = (Lake.Module.facet self.name mod).fetch

def Lake.ModuleFacetConfig.fetchJob {name : Lean.Name} (mod : Module) (self : ModuleFacetConfig name) : FetchM OpaqueJob

Fetch the build job of a module facet.

Equations

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

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

Fetch the build job of a module facet.

Equations

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

Lean Library Facets

@[inline]

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

Get the Lean library in the workspace with the configuration's name.

Equations

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

@[inline]

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

Fetch the build result of a library facet.

Equations

• Lake.LibraryFacetDecl.fetch lib self = (lib.facet self.name).fetch

def Lake.LibraryFacetConfig.fetchJob {name : Lean.Name} (lib : LeanLib) (self : LibraryFacetConfig name) : FetchM OpaqueJob

Fetch the build job of a library facet.

Equations

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

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

Fetch the build job of a library facet.

Equations

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

Lean Executable Target

@[inline]

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

Get the Lean executable in the workspace with the configuration's name.

Equations

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

@[inline]

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

Fetch the build of the Lean executable.

Equations

• self.fetch = do let __do_lift ← self.get __do_lift.exe.fetch

@[inline]

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

Fetch the build of the Lean executable.

Equations

• self.fetch = self.exe.fetch