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

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

@[inline]

def Lake.Package.findLeanExe? (name : Lean.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) : Lean.Name

The executable's well-formed name.

Equations

• self.name = 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

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

@[inline]

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

The executable's root module.

Equations

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

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

• self.file = self.pkg.binDir / self.fileName

@[inline]

def Lake.LeanExe.supportInterpreter (self : Lake.LeanExe) : Bool

The executable's supportInterpreter configuration.

Equations

• self.supportInterpreter = self.config.supportInterpreter

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

The arguments to pass to leanc when linking the binary executable. By default, the package's plus the executable's moreLinkArgs.

If supportInterpreter := true, Lake links directly to the Lean shared libraries on Windows by prepending -leanshared and adds -rdynamic on other systems.

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

• self.weakLinkArgs = self.pkg.weakLinkArgs ++ self.config.weakLinkArgs

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

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

Equations

• Lake.Package.findTargetModule? mod self = ((self.leanExes.findSomeRev? fun (x : Lake.LeanExe) => Lake.LeanExe.isRoot? mod x) <|> Lake.Package.findModule? mod self)