structure Lake.LeanExeConfig (name : Lean.Name) extends Lake.LeanConfig : Type

A Lean executable's declarative configuration.

• buildType : BuildType
• leanOptions : Array LeanOption
• moreLeanArgs : Array String
• weakLeanArgs : Array String
• moreLeancArgs : Array String
• moreServerOptions : Array LeanOption
• weakLeancArgs : Array String
• moreLinkObjs : TargetArray System.FilePath
• moreLinkLibs : TargetArray Dynlib
• moreLinkArgs : Array String
• weakLinkArgs : Array String
• backend : Backend
• platformIndependent : Option Bool
• dynlibs : TargetArray Dynlib
• plugins : TargetArray Dynlib
• srcDir : System.FilePath

  The subdirectory of the package's source directory containing the executable's Lean source file. Defaults simply to said srcDir.

  (This will be passed to lean as the -R option.)

• root : Lean.Name

  The root module of the binary executable. Should include a main definition that will serve as the entry point of the program.

  The root is built by recursively building its local imports (i.e., fellow modules of the workspace).

  Defaults to the name of the target.

• exeName : String

  The name of the binary executable. Defaults to the target name with any . replaced with a -.

• needs : Array PartialBuildKey

  An Array of targets to build before the executable's modules.

• extraDepTargets : Array Lean.Name

  Deprecated. Use needs instead. An Array of target names to build before the executable's modules.

• supportInterpreter : Bool

  Enables the executable to interpret Lean files (e.g., via Lean.Elab.runFrontend) by exposing symbols within the executable to the Lean interpreter.

  Implementation-wise, on Windows, the Lean shared libraries are linked to the executable and, on other systems, the executable is linked with -rdynamic. This increases the size of the binary on Linux and, on Windows, requires libInit_shared.dll and libleanshared.dll to be co-located with the executable or part of PATH (e.g., via lake exe). Thus, this feature should only be enabled when necessary.

  Defaults to false.

• nativeFacets (shouldExport : Bool) : Array (ModuleFacet System.FilePath)

  The module facets to build and combine into the executable. If shouldExport is true, the module facets should export any symbols a user may expect to lookup in the executable. For example, the Lean interpreter will use exported symbols in the executable. Thus, shouldExport will be true if supportInterpreter := true.

  Defaults to a singleton of Module.oExportFacet (if shouldExport) or Module.oFacet. That is, the object file compiled from the Lean source, potentially with exported Lean symbols.

instance Lake.LeanExeConfig.extraDepTargets.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `extraDepTargets (Array Lean.Name)

Equations

• Lake.LeanExeConfig.extraDepTargets.instConfigField = { toConfigProj := Lake.LeanExeConfig.extraDepTargets._proj }

instance Lake.LeanExeConfig.exeName.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `exeName String

Equations

• Lake.LeanExeConfig.exeName.instConfigField = { toConfigProj := Lake.LeanExeConfig.exeName._proj }

instance Lake.LeanExeConfig.toLeanConfig.instConfigParent {name : Lean.Name} : ConfigParent (LeanExeConfig name) LeanConfig

Equations

• Lake.LeanExeConfig.toLeanConfig.instConfigParent = { toConfigProj := Lake.LeanExeConfig.toLeanConfig._proj }

instance Lake.LeanExeConfig.root.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `root Lean.Name

Equations

• Lake.LeanExeConfig.root.instConfigField = { toConfigProj := Lake.LeanExeConfig.root._proj }

instance Lake.LeanExeConfig.srcDir.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `srcDir System.FilePath

Equations

• Lake.LeanExeConfig.srcDir.instConfigField = { toConfigProj := Lake.LeanExeConfig.srcDir._proj }

instance Lake.LeanExeConfig.supportInterpreter.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `supportInterpreter Bool

Equations

• Lake.LeanExeConfig.supportInterpreter.instConfigField = { toConfigProj := Lake.LeanExeConfig.supportInterpreter._proj }

instance Lake.LeanExeConfig.needs.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `needs (Array PartialBuildKey)

Equations

• Lake.LeanExeConfig.needs.instConfigField = { toConfigProj := Lake.LeanExeConfig.needs._proj }

instance Lake.LeanExeConfig.nativeFacets.instConfigField {name : Lean.Name} : ConfigField (LeanExeConfig name) `nativeFacets (Bool → Array (ModuleFacet System.FilePath))

Equations

• Lake.LeanExeConfig.nativeFacets.instConfigField = { toConfigProj := Lake.LeanExeConfig.nativeFacets._proj }

instance Lake.LeanExeConfig.instConfigMeta : ConfigInfo `Lake.LeanExeConfig

Equations

• Lake.LeanExeConfig.instConfigMeta = { fields := Lake.LeanExeConfig._fields }

instance Lake.LeanExeConfig.instConfigFields {name : Lean.Name} : ConfigFields (LeanExeConfig name)

Equations

• Lake.LeanExeConfig.instConfigFields = { fields := Lake.LeanExeConfig._fields }

instance Lake.instInhabitedLeanExeConfig {a✝ : Lean.Name} : Inhabited (LeanExeConfig a✝)

Equations

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

instance Lake.instEmptyCollectionLeanExeConfig {n : Lean.Name} : EmptyCollection (LeanExeConfig n)

Equations

• Lake.instEmptyCollectionLeanExeConfig = { emptyCollection := { } }

@[reducible, inline]

abbrev Lake.LeanExeConfig.name {n : Lean.Name} : LeanExeConfig n → Lean.Name

The executable's name.

Equations

• x✝.name = n