structure Lake.LeanExe : Type

• pkg : Lake.Package

  The package the executable belongs to.

• config : Lake.LeanExeConfig

  The executable's user-defined configuration.

A Lean executable -- its package plus its configuration.

@[inline]

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

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

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

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

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

@[inline]

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

The executable's well-formed name.

@[inline]

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

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

@[inline]

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

The executable's root module.

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.

@[inline]

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

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

@[inline]

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

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

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.

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

Locate the named module in the package (if it is buildable and local to it).