Documentation

Lake.Config.LeanExe

structure Lake.LeanExe :

A Lean executable -- its package plus its configuration.

  • pkg : Package

    The package the executable belongs to.

  • config : LeanExeConfig

    The executable's user-defined configuration.

@[inline]

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

Equations
@[inline]

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

Equations

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]

The executable's well-formed name.

Equations
  • self.name = self.config.name
@[inline]

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

Equations
  • self.toLeanLib = { pkg := self.pkg, config := self.config.toLeanLibConfig }
@[inline]

The executable's root module.

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

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

Equations
@[inline]

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

Equations
@[inline]

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

Equations
  • self.file = self.pkg.binDir / self.fileName
@[inline]

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.
@[inline]

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
@[inline]

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

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

Equations