Define Lean Libraries and Binary Executables in Lake

Lake packages can expose one or more Lean libraries (collections of importable modules) and binary executables (programs users can run without Lean). Both are declared as targets in the lakefile; Lake builds them on demand or as part of the default build.

Lean Libraries

A Lean library target defines a collection of Lean modules that other packages — or other targets within the same package — can import. Lake compiles each module in the library to a set of binary artefacts: .olean, .ilean, and optionally a compiled C file and native object.

Declaration Syntax

TOML
Lean DSL

[[lean_lib]]
name = "MyLib"

# With additional options:
[[lean_lib]]
name = "MyLib"
roots = ["MyLib", "MyLib.Extra"]
globs = ["MyLib.*"]
srcDir = "lib"
precompileModules = false

Each [[lean_lib]] block declares one library. The name field is required; all other fields are optional.

-- Minimal declaration (name defaults to target identifier)
lean_lib MyLib

-- With options
lean_lib MyLib where
  roots := #[`MyLib, `MyLib.Extra]
  globs := #[.submodules `MyLib]
  srcDir := "lib"
  precompileModules := false

In the Lean DSL, the identifier after lean_lib becomes the target name. The where clause is optional.

Library Configuration Fields

name

string

required

The name of the library target. Used on the command line (lake build MyLib) and as the default module root.

[[lean_lib]]
name = "MyLib"

roots

string[]

default:"[name]"

An array of root module names. Submodules of these roots (e.g. MyLib.Foo is a submodule of MyLib) are considered part of the library. Defaults to a single root matching the target name.

[[lean_lib]]
name = "MyLib"
roots = ["MyLib", "MyLib.Compat"]

lean_lib MyLib where
  roots := #[`MyLib, `MyLib.Compat]

globs

string[]

default:"[Glob.one of each root]"

An array of module globs specifying which modules to build when the library is built. A glob can match a single module or all submodules of a root.Glob format:

MyLib — build only the MyLib module itself
MyLib.+ — build all submodules of MyLib (not MyLib itself)
MyLib.* — build MyLib and all its submodules

[[lean_lib]]
name = "MyLib"
globs = ["MyLib.*"]   # build MyLib and every submodule

lean_lib MyLib where
  globs := #[.andSubmodules `MyLib]  -- MyLib and all submodules

Local imports of glob-matched files are also recursively built.

srcDir

string

default:". (package srcDir)"

The subdirectory of the package’s source directory containing this library’s Lean source files. Passed to lean as the -R option.

[[lean_lib]]
name = "MyLib"
srcDir = "lib"

libName

string

default:"target name"

The base name for the library’s native binary files (.a, .so). Defaults to the mangled target name.

[[lean_lib]]
name = "MyLib"
libName = "my_lib"

precompileModules

boolean

default:"false"

When true, each module is compiled into a native shared library that is loaded at import time. This speeds up metaprogram evaluation and allows @[extern] functions to be called from the interpreter. Applies if either the package-level or library-level setting is true.

[[lean_lib]]
name = "MyLib"
precompileModules = true

lean_lib MyLib where
  precompileModules := true

needs

string[]

default:"[]"

An array of target specifiers to build before this library’s modules. Use this to declare dependencies on native libraries, generated files, or other custom targets.

[[lean_lib]]
name = "MyLib"
needs = ["NativeBindings:static"]

lean_lib MyLib where
  needs := #[`NativeBindings]

defaultFacets

string[]

default:"[\"leanArts\"]"

Library facets to build on a bare lake build of this library. The default builds only Lean artefacts (.olean, .ilean, .c). Set to ["shared"] to also produce a shared library.

[[lean_lib]]
name = "MyLib"
defaultFacets = ["leanArts", "shared"]

lean_lib MyLib where
  defaultFacets := #[LeanLib.leanArtsFacet, LeanLib.sharedFacet]

libPrefixOnWindows

boolean

default:"false"

Whether native library artefacts should be prefixed with lib on Windows (e.g. libMyLib.dll instead of MyLib.dll). On Unix, the lib prefix is always present.

[[lean_lib]]
name = "MyLib"
libPrefixOnWindows = true

allowImportAll

boolean

default:"false"

Whether downstream packages may use import all to access private internals of this library’s modules.

[[lean_lib]]
name = "MyLib"
allowImportAll = true

Library Build Artefacts

When you run lake build MyLib, Lake produces (in .lake/build/):

Artefact	Location	Description
`.olean`	`lib/lean/MyLib.olean`	Binary Lean data for importers
`.ilean`	`lib/lean/MyLib.ilean`	LSP metadata
`.c`	`ir/MyLib.c`	Generated C source
`.a`	`lib/libMyLib.a`	Static library (facet `static`)
`.so/.dll`	`lib/libMyLib.so`	Shared library (facet `shared`)

Marking a Library as a Default Target

TOML
Lean DSL

defaultTargets = ["MyLib"]

[[lean_lib]]
name = "MyLib"

@[default_target]
lean_lib MyLib

Binary Executables

A Lean executable target builds a binary program from a single Lean module (the root) that must contain a main definition. Lake recursively builds all of the root’s local imports.

Declaration Syntax

TOML
Lean DSL

[[lean_exe]]
name = "hello"

# With options:
[[lean_exe]]
name = "hello"
root = "Main"
srcDir = "."
supportInterpreter = false

-- Minimal: root defaults to the target name
lean_exe Hello

-- With options
lean_exe hello where
  root := `Main
  supportInterpreter := false

Executable Configuration Fields

name

string

required

The name of the executable target. Used with lake build hello and lake exe hello.

[[lean_exe]]
name = "hello"

root

string

default:"target name"

The root module Name of the executable. This module must define main. Defaults to the target name.

[[lean_exe]]
name = "hello"
root = "Main"

lean_exe hello where
  root := `Main

srcDir

string

default:". (package srcDir)"

Subdirectory of the package’s source directory containing the executable’s source file. Passed to lean as -R.

[[lean_exe]]
name = "hello"
srcDir = "app"

exeName

string

default:"target name with \".\" replaced by \"-\""

The file name of the produced binary. Defaults to the target name with . replaced by - (e.g. My.Exe → My-Exe).

[[lean_exe]]
name = "hello"
exeName = "hello-world"

lean_exe hello where
  exeName := "hello-world"

supportInterpreter

boolean

default:"false"

When true, symbols within the executable are exported so the Lean interpreter can access them (needed for executables that call Lean.Elab.runFrontend). On Unix this links with -rdynamic; on Windows it links against Lean’s shared DLLs.

Enabling supportInterpreter increases binary size on Linux. On Windows, libInit_shared.dll and libleanshared.dll must be co-located with the executable or on PATH. Enable only when necessary.

[[lean_exe]]
name = "elaborator"
supportInterpreter = true

lean_exe elaborator where
  supportInterpreter := true

needs

string[]

default:"[]"

Targets to build before this executable’s modules.

[[lean_exe]]
name = "hello"
needs = ["NativeLib:static"]

lean_exe hello where
  needs := #[`NativeLib]

Running an Executable

After building, the binary is in .lake/build/bin/. Use lake exe to build and run in one step:

lake exe hello
lake exe hello -- --flag arg1 arg2

External Libraries (`extern_lib`)

extern_lib targets are deprecated. Use a custom target in conjunction with moreLinkObjs or moreLinkLibs instead.

An extern_lib target declares a non-Lean static library that will be linked to the package’s binaries. In the Lean DSL:

extern_lib myNativeLib (pkg : NPackage _package.name) := do
  let name := nameToStaticLib "myNativeLib"
  let srcDir := pkg.dir / "native"
  -- build and return the path to the .a file
  buildFileAfterDep (srcDir / name) headerTarget fun _ => do
    proc { cmd := "cc", args := #["-c", "-o", (srcDir / name).toString,
                                   (srcDir / "mylib.c").toString] }

The static library produced by extern_lib must follow platform naming conventions: foo.a on Windows and libfoo.a on Unix. Use Lake.nameToStaticLib to compute the correct filename.

Custom Targets

A target declaration lets you build arbitrary artefacts that can be referenced by other targets or triggered by lake build <name>.

target generatedHeaders (pkg : NPackage _package.name) : System.FilePath := do
  let outDir := pkg.buildDir / "include"
  buildFileAfterDep (outDir / "generated.h") inputFile fun _ => do
    proc { cmd := "python3", args := #["scripts/gen_headers.py",
                                        "--out", (outDir / "generated.h").toString] }

Then reference it from a library:

lean_lib MyLib where
  needs := #[generatedHeaders]

Complete Example

A package with a library and two executables:

TOML
Lean DSL

name = "myproject"
version = "0.1.0"
defaultTargets = ["myproject"]

[[lean_lib]]
name = "MyLib"
roots = ["MyLib"]
globs = ["MyLib.*"]
precompileModules = false

[[lean_exe]]
name = "myproject"
root = "Main"

[[lean_exe]]
name = "test"
root = "Test.Main"

import Lake
open Lake DSL

package "myproject" where
  version := v!"0.1.0"

lean_lib MyLib where
  roots := #[`MyLib]
  globs := #[.andSubmodules `MyLib]
  precompileModules := false

@[default_target]
lean_exe myproject where
  root := `Main

@[test_driver]
lean_exe test where
  root := `Test.Main

Getting Started with Lake

Configuration

CLI Reference

Define Lean Libraries and Binary Executables in Lake

Lean Libraries

Declaration Syntax

Library Configuration Fields

Library Build Artefacts

Marking a Library as a Default Target

Binary Executables

Declaration Syntax

Executable Configuration Fields

Running an Executable

External Libraries (`extern_lib`)

Custom Targets

Complete Example

Build docs developers (and LLMs) love

Getting Started with Lake

Configuration

CLI Reference

Documentation Index

​Lean Libraries

​Declaration Syntax

​Library Configuration Fields

​Library Build Artefacts

​Marking a Library as a Default Target

​Binary Executables

​Declaration Syntax

​Executable Configuration Fields

​Running an Executable

​External Libraries (extern_lib)

​Custom Targets

​Complete Example

Build docs developers (and LLMs) love

Lean Libraries

Declaration Syntax

Library Configuration Fields

Library Build Artefacts

Marking a Library as a Default Target

Binary Executables

Declaration Syntax

Executable Configuration Fields

Running an Executable

External Libraries (`extern_lib`)

Custom Targets

Complete Example