structure Lake.LeanExe : Type

A Lean executable -- its package plus its configuration.

• pkg : Lake.Package

  The package the executable belongs to.

• config : Lake.LeanExeConfig

  The executable's user-defined configuration.

@[inline]

def Lake.Package.leanExes (self : Lake.Package) : Array Lake.LeanExe

The Lean executables of the package (as an Array).

Equations

• Lake.Package.leanExes self = Lake.RBArray.foldl (fun (a : Array Lake.LeanExe) (v : Lake.LeanExeConfig) => Array.push a { pkg := self, config := v }) #[] self.leanExeConfigs

@[inline]

def Lake.Package.findLeanExe? (name : Lake.Name) (self : Lake.Package) : Option Lake.LeanExe

Try to find a Lean executable in the package with the given name.

Equations

• Lake.Package.findLeanExe? name self = Option.map (fun (x : Lake.LeanExeConfig) => { pkg := self, config := x }) (Lake.RBArray.find? self.leanExeConfigs name)

def Lake.LeanExeConfig.toLeanLibConfig (self : Lake.LeanExeConfig) : Lake.LeanLibConfig

Converts the executable configuration into a library with a single module (the root).

Equations

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

@[inline]

def Lake.LeanExe.name (self : Lake.LeanExe) : Lake.Name

The executable's well-formed name.

Equations

• Lake.LeanExe.name self = self.config.name

@[inline]

def Lake.LeanExe.toLeanLib (self : Lake.LeanExe) : Lake.LeanLib

Converts the executable into a library with a single module (the root).

Equations

• Lake.LeanExe.toLeanLib self = { pkg := self.pkg, config := Lake.LeanExeConfig.toLeanLibConfig self.config }

@[inline]

def Lake.LeanExe.root (self : Lake.LeanExe) : Lake.Module

The executable's root module.

Equations

• Lake.LeanExe.root self = { lib := Lake.LeanExe.toLeanLib self, name := self.config.root, keyName := Lake.Package.name self.pkg ++ self.config.root }

def Lake.LeanExe.isRoot? (name : Lake.Name) (self : Lake.LeanExe) : Option Lake.Module

Return the the root module if the name matches, otherwise return none.

Equations

• Lake.LeanExe.isRoot? name self = if (name == self.config.root) = true then some (Lake.LeanExe.root self) else none

@[inline]

def Lake.LeanExe.fileName (self : Lake.LeanExe) : Lake.FilePath

The file name of binary executable (i.e., exeName plus the platform's exeExtension).

Equations

• Lake.LeanExe.fileName self = System.FilePath.addExtension { toString := self.config.exeName } System.FilePath.exeExtension

@[inline]

def Lake.LeanExe.file (self : Lake.LeanExe) : Lake.FilePath

The path to the executable in the package's binDir.

Equations

• Lake.LeanExe.file self = Lake.Package.binDir self.pkg / Lake.LeanExe.fileName self

def Lake.LeanExe.linkArgs (self : Lake.LeanExe) : Array String

The arguments to pass to leanc when linking the binary executable.

That is, -rdynamic (if non-Windows and supportInterpreter) plus the package's and then the executable's moreLinkArgs.

Equations

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

@[inline]

def Lake.LeanExe.weakLinkArgs (self : Lake.LeanExe) : Array String

The arguments to weakly pass to leanc when linking the binary executable. That is, the package's weakLinkArgs plus the executable's weakLinkArgs.

Equations

• Lake.LeanExe.weakLinkArgs self = Lake.Package.weakLinkArgs self.pkg ++ self.config.weakLinkArgs

def Lake.Package.findTargetModule? (mod : Lake.Name) (self : Lake.Package) : Option Lake.Module

Locate the named, buildable, but not necessarily importable, module in the package.

Equations

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