A Lean executable -- its package plus its configuration.
- pkg : Package
The package the executable belongs to.
- config : LeanExeConfig
The executable's user-defined configuration.
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
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)
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.
Converts the executable into a library with a single module (the root).
Equations
- self.toLeanLib = { pkg := self.pkg, config := self.config.toLeanLibConfig }
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
The path to the executable in the package's binDir
.
The executable's supportInterpreter
configuration.
Equations
- self.supportInterpreter = self.config.supportInterpreter
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.
The arguments to weakly pass to leanc
when linking the binary executable.
That is, the package's weakLinkArgs
plus the executable's weakLinkArgs
.
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)