Module 6 · Lesson 3

Compiling Executables

Build standalone executables from your Lean code. Lean compiles to efficient native code through C.

The Main Function

Every executable needs a main function:

lean

1-- Simplest main
2def main : IO Unit :=
3  IO.println "Hello, World!"
4
5-- Main with arguments
6def main (args : List String) : IO Unit := do
7  IO.println s!"Arguments: {args}"
8
9-- Main with exit code
10def main : IO UInt32 := do
11  IO.println "Running..."
12  return 0  -- 0 = success, non-zero = failure
13
14-- (These are three ALTERNATIVES. A module defines main exactly once.)
15-- Note: args does NOT include the program name, unlike C's argv[0].

Building with Lake

Define an executable in your lakefile:

lean

1-- lakefile.toml (the default format)
2-- name = "myapp"
3-- defaultTargets = ["myapp"]
4--
5-- [[lean_exe]]
6-- name = "myapp"
7-- root = "Main"
8
9-- The same thing in lakefile.lean:
10import Lake
11open Lake DSL
12
13package myapp
14
15@[default_target]
16lean_exe myapp where
17  root := `Main

bash

1# Build the executable
2lake build
3
4# Run it
5lake exe myapp
6
7# Or run directly
8./.lake/build/bin/myapp

Build Types

Lake's optimisation level is the package's buildType, set in the lakefile rather than on the command line. The options are debug, relWithDebInfo (the default), minSizeRel, and release; they control the flags passed to the C compiler.

toml|lakefile.toml

1name = "myapp"
2buildType = "release"
3
4[[lean_exe]]
5name = "myapp"
6root = "Main"

lean|lakefile.lean

1package myapp where
2  buildType := .release

⚠

You may see lake build -Krelease in older material. That does not enable optimisations — -K sets an arbitrary configuration key, and Lake has no built-in key called release. The command succeeds and changes nothing, which is why the myth survives. Set buildType instead.

In practice the default relWithDebInfois fine for almost everything: Lean's own optimiser does most of the work before the C compiler ever sees the code. Reach for release when you are shipping a binary, and debug only when you need to step through the generated C in a debugger.

Command Line Argument Parsing

Pattern matching on the args list provides a simple way to handle command-line options. For complex CLIs, consider a dedicated parsing library.

lean

1def main (args : List String) : IO UInt32 := do
2  match args with
3  | [] =>
4    IO.println "Usage: myapp <command> [options]"
5    return 1
6  | ["--help"] =>
7    IO.println "myapp - A sample application"
8    IO.println ""
9    IO.println "Commands:"
10    IO.println "  run     Run the main task"
11    IO.println "  check   Check configuration"
12    return 0
13  | ["run"] =>
14    IO.println "Running..."
15    return 0
16  | ["check"] =>
17    IO.println "Checking configuration..."
18    return 0
19  | cmd :: _ =>
20    IO.println s!"Unknown command: {cmd}"
21    return 1

Multiple Executables

A single Lake project can produce multiple executables. Each one has its ownmain function in a separate root module, but they can all share library code.

lean

1-- lakefile.lean
2import Lake
3open Lake DSL
4
5package myproject
6
7-- Library with shared code
8lean_lib MyProject
9
10-- Main CLI
11lean_exe myapp where
12  root := `Main
13
14-- Additional tool
15lean_exe mytool where
16  root := `Tool.Main
17
18-- Test runner
19lean_exe tests where
20  root := `Tests.Main

bash

1# Build all
2lake build
3
4# Build specific executable
5lake build myapp
6lake build mytool
7
8# Run specific executable
9lake exe myapp
10lake exe mytool

Key Takeaway

Each executable has its own root file with a main function. They can share code through library targets.

Cross-Platform Considerations

lean

1def main : IO Unit := do
2  -- Check platform
3  if System.Platform.isWindows then
4    IO.println "Running on Windows"
5  else if System.Platform.isOSX then
6    IO.println "Running on macOS"
7  else
8    IO.println "Running on Linux/Unix"
9
10  -- Platform-specific paths
11  let sep := if System.Platform.isWindows then "\\" else "/"
12  IO.println s!"Path separator: {sep}"

Environment Variables

Environment variables let you configure your program without changing code. Read them with IO.getEnv and set them for child processes.

lean

1def main : IO Unit := do
2  -- Read environment variable
3  let home ← IO.getEnv "HOME"
4  match home with
5  | none => IO.println "HOME not set"
6  | some path => IO.println s!"Home: {path}"
7
8  -- Set environment variable (for child processes)
9  -- Note: This affects the current process
10  IO.Process.run {
11    cmd := "echo"
12    args := #["$MY_VAR"]
13    env := #[("MY_VAR", some "hello")]
14  }

Running External Commands

Lean can invoke external programs and capture their output. This is useful for integrating with existing tools or shell scripts.

lean

1def main : IO Unit := do
2  -- Run a command and get output
3  let output ← IO.Process.output {
4    cmd := "ls"
5    args := #["-la"]
6  }
7  IO.println s!"Exit code: {output.exitCode}"
8  IO.println s!"Output: {output.stdout}"
9
10  -- Run interactively (inherits stdin/stdout)
11  let exitCode ← IO.Process.spawn {
12    cmd := "vim"
13    args := #["file.txt"]
14    stdin := .inherit
15    stdout := .inherit
16    stderr := .inherit
17  } >>= (·.wait)
18  IO.println s!"Editor exited with: {exitCode}"

Deep Dive: Compilation Pipeline

Lean compilation works in stages:

Lean → IR: Lean code to internal representation
IR → C: IR to C code (in .lake/build/ir/)
C → Object: C to object files via system C compiler
Link: Object files linked to final executable

The generated C is heavily optimized and uses reference counting for memory management.

Distribution

For distributing your executable:

bash

1# Build (with buildType = "release" set in the lakefile)
2lake build
3
4# The binary lands here:
5#   .lake/build/bin/myapp        (Linux, macOS)
6#   .lake/build/bin/myapp.exe    (Windows)
7
8# Check what it links against before you ship it:
9ldd .lake/build/bin/myapp        # Linux
10otool -L .lake/build/bin/myapp   # macOS

ℹ

Lean statically links the Lean runtime and your compiled code, but dynamically links the system C library (and, on Linux, libgmp for arbitrary-precision Nat/Int). So a binary is portable across machines with the same OS and architecture and a compatible glibc — but it is not a fully static executable you can drop into a scratch container without checking. Run ldd and see.

Exercise: Minimal CLI

Create a main that prints the number of arguments and exits.

lean

1def main (args : List String) : IO UInt32 := do
2  IO.println s!"args: {args.length}"
3  return 0

Example: Complete CLI Application

lean

1def version := "1.0.0"
2
3def printHelp : IO Unit := do
4  IO.println "myapp - A command line tool"
5  IO.println ""
6  IO.println "Usage: myapp [options] <command>"
7  IO.println ""
8  IO.println "Options:"
9  IO.println "  --help, -h     Show this help"
10  IO.println "  --version, -v  Show version"
11  IO.println ""
12  IO.println "Commands:"
13  IO.println "  init           Initialize a new project"
14  IO.println "  build          Build the project"
15  IO.println "  run            Run the project"
16
17def doInit : IO UInt32 := do
18  IO.println "Initializing..."
19  IO.FS.writeFile "config.json" "{}"
20  IO.println "Created config.json"
21  return 0
22
23def doBuild : IO UInt32 := do
24  IO.println "Building..."
25  -- Build logic here
26  IO.println "Done!"
27  return 0
28
29def main (args : List String) : IO UInt32 := do
30  match args with
31  | [] | ["--help"] | ["-h"] =>
32    printHelp
33    return 0
34  | ["--version"] | ["-v"] =>
35    IO.println s!"myapp version {version}"
36    return 0
37  | ["init"] => doInit
38  | ["build"] => doBuild
39  | ["run"] =>
40    IO.println "Running..."
41    return 0
42  | cmd :: _ =>
43    IO.println s!"Error: Unknown command '{cmd}'"
44    IO.println "Run 'myapp --help' for usage"
45    return 1

Modules & Imports Next: Best Practices