Build Target Fetching

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

Package Facets & Targets

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

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 : Lake.TargetDecl) [Lake.FamilyOut Lake.CustomData (self.pkg, self.name) α] : Lake.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 : Lake.TargetDecl) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.Package) (self : Lake.PackageFacetDecl) [Lake.FamilyOut Lake.PackageData self.name α] : Lake.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 : Lake.Package) (self : Lake.PackageFacetConfig name) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.Package) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.Module) (self : Lake.ModuleFacetDecl) [Lake.FamilyOut Lake.ModuleData self.name α] : Lake.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 : Lake.Module) (self : Lake.ModuleFacetConfig name) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.Module) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.LeanLibConfig) [Monad m] [Lake.MonadError m] [Lake.MonadLake m] : m Lake.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 : Lake.LeanLib) (self : Lake.LibraryFacetDecl) [Lake.FamilyOut Lake.LibraryData self.name α] : Lake.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 : Lake.LeanLib) (self : Lake.LibraryFacetConfig name) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.LeanLib) : Lake.FetchM (Lake.BuildJob Unit)

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 : Lake.LeanExeConfig) [Monad m] [Lake.MonadError m] [Lake.MonadLake m] : m Lake.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 : Lake.LeanExeConfig) : Lake.FetchM (Lake.BuildJob 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 : Lake.LeanExe) : Lake.FetchM (Lake.BuildJob System.FilePath)

Fetch the build of the Lean executable.

Equations

• self.fetch = self.exe.fetch