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

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

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

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

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 ModuleData self.name α] : FetchM (Job α)

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

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

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.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 (Job α)

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

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

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 ← (self.facet name).fetch pure __do_lift.toOpaque

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