A Lean executable -- its package plus its configuration.
Equations
Instances For
The Lean executables of the package (as an Array).
Equations
Instances For
Converts the executable configuration into a library with a single module (the root).
Equations
Instances For
The executable's user-defined configuration.
Equations
Instances For
Converts the executable into a library with a single module (the root).
Equations
Instances For
The executable's root module.
Equations
Instances For
Return the root module if the file stem of the path
matches the source file. Otherwise, returns none
.
Equations
Instances For
The file name of binary executable
(i.e., exeName
plus the platform's exeExtension
).
Equations
Instances For
The path to the executable in the package's binDir
.
Equations
Instances For
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
Instances For
The arguments to weakly pass to leanc
when linking the binary executable.
That is, the package's weakLinkArgs
plus the executable's weakLinkArgs
.
Equations
Instances For
Returns the buildable module in the package whose source file is path
.