@[reducible, inline]

abbrev Lake.LeanExe : Type

A Lean executable -- its package plus its configuration.

Equations

• Lake.LeanExe = Lake.ConfigTarget Lake.LeanExe.configKind

@[inline]

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

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

Equations

• self.leanExes = Lake.Package.configTargets Lake.LeanExe.configKind self

@[inline]

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

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

Equations

• Lake.Package.findLeanExe? name self = Lake.Package.findConfigTarget? Lake.LeanExe.configKind name self

def Lake.LeanExeConfig.toLeanLibConfig {n : Lean.Name} (self : LeanExeConfig n) : LeanLibConfig n

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.config (self : LeanExe) : LeanExeConfig self.name

The executable's user-defined configuration.

Equations

• self.config = self.config

@[inline]

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

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

Equations

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

@[inline]

def Lake.LeanExe.root (self : LeanExe) : 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 : LeanExe) : Option 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

def Lake.LeanExe.isRootSrc? (path : System.FilePath) (self : LeanExe) : Option Module

Return the root module if the file stem of the path matches the source file. Otherwise, returns none.

Equations

• Lake.LeanExe.isRootSrc? path self = if (path.withExtension "" == Lake.Module.srcPath "" self.root) = true then some self.root else none

@[inline]

def Lake.LeanExe.fileName (self : 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 : 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 : LeanExe) : Bool

The executable's supportInterpreter configuration.

Equations

• self.supportInterpreter = self.config.supportInterpreter

def Lake.LeanExe.linkArgs (self : 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 prepends -rdynamic on non-Windows systems.

Equations

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

@[inline]

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

Whether the Lean shared library should be dynamically linked to the executable.

If supportInterpreter := true, Lean symbols must be visible to the interpreter. On Windows, it is not possible to statically include these symbols in the executable due to symbol limits, so Lake dynamically links to the Lean shared library. Otherwise, Lean is linked statically.

Equations

• self.sharedLean = strictAnd System.Platform.isWindows self.config.supportInterpreter

@[inline]

def Lake.LeanExe.weakLinkArgs (self : 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 : Package) : Option Module

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

Equations

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

def Lake.Package.findModuleBySrc? (path : System.FilePath) (self : Package) : Option Module

Returns the buildable module in the package whose source file is path.

Equations

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