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

Building with Lake

Define an executable in your lakefile:

lean

1-- lakefile.lean
2import Lake
3open Lake DSL
4
5package myapp
6
7@[default_target]
8lean_exe myapp where
9  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

Release Builds

For production, build with optimizations:

bash

1# Build with release optimizations
2lake build -Krelease
3
4# The executable is now optimized

💡

Release builds are significantly faster. Always use -Kreleasefor production executables.

Debug Builds

During development, use regular builds for faster compile times and better error messages. Switch to release mode only when you need performance.

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 release
2lake build -Krelease
3
4# The executable is self-contained
5# Copy from .lake/build/bin/myapp to wherever needed
6
7# On Windows, it's myapp.exe

ℹ

Lean executables link against the system C library. They're generally portable across machines with the same OS and architecture.

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: Theorem Proving