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.

Command Line Argument Parsing

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

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

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

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.

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