Writing, Declaring, and Running Lake Scripts in Lean 4

Lake scripts are named Lean functions that can be run directly from the command line via lake run or lake script run. They are defined in the lakefile alongside libraries and executables, but unlike executables they do not produce a standalone binary — they run inside Lake’s own process with access to Lake’s configuration and environment. Scripts are ideal for one-off automation tasks: generating files, running checks, formatting source code, or any task that benefits from having access to the Lean toolchain or the package configuration.

Script Type Signature

A script is a function of type:

ScriptFn := (args : List String) → ScriptM ExitCode

where ScriptM is an IO monad extended with information about the Lake configuration:

abbrev ScriptM := LakeT IO

Every script receives the command-line arguments as a List String and returns a UInt32 exit code (via ExitCode). Return 0 for success and a non-zero value for failure.

Declaring a Script

Lean DSL

Scripts are declared with the script keyword in a lakefile.lean:

import Lake
open Lake DSL

package "mypkg"

script hello (args) do
  IO.println "Hello from a Lake script!"
  return 0

The parenthesised parameter name (args) binds the argument list. The body is a do-block in ScriptM. You can add a docstring immediately before the script declaration. Lake uses it for lake script doc:

/--
Display a greeting.

USAGE:
  lake run greet [name]

Greet the given name, or the whole world if no name is provided.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

TOML Lakefiles

Scripts cannot be defined in lakefile.toml because scripts are Lean code that must be evaluated by the Lean runtime. Lake only loads one configuration file per package: if both lakefile.lean and lakefile.toml are present, lakefile.lean takes precedence (with a warning).

Scripts are only supported in Lean DSL lakefiles (lakefile.lean). If your project currently uses lakefile.toml, convert it with lake translate-config lean to switch to a Lean DSL lakefile that supports scripts.

Running a Script

`lake run` (shorthand)

lake run <script> [<args>...]
lake run greet
lake run greet Alice
lake run greet -- Alice Bob   # '--' separates Lake options from script args

`lake script run`

lake script run <script> [<args>...]
lake script run greet
lake script run greet Alice

Both forms are equivalent. lake run is the shorthand alias. You can also target a script in a specific package within the workspace:

lake script run myPkg/greet Alice
lake run myPkg/greet Alice

A bare lake run (with no script name) runs the default script(s) of the root package (those decorated with @[default_target]):

@[default_target]
script build (args) do
  -- ...
  return 0

Listing Available Scripts

lake scripts          # shorthand
lake script list      # full form

Prints the names of all scripts defined in the workspace, one per line. Useful for discovering what automation is available in an unfamiliar project. Example output:

greet
generateDocs
runBenchmarks

Printing Script Documentation

lake script doc <script>
lake script doc greet

Prints the docstring of the named script. This is the text of the /-- ... -/ doc comment placed immediately before the script declaration. Example:

$ lake script doc greet
Display a greeting.

USAGE:
  lake run greet [name]

Greet the given name, or the whole world if no name is provided.

Write a docstring for every script. It is the primary way users discover how to use your scripts without reading the source code.

Working with Arguments

Script arguments arrive as a List String. Pattern match or use standard List functions to process them:

script echo (args) do
  match args with
  | [] => IO.eprintln "Usage: lake run echo <message>"; return 1
  | msg :: _ => IO.println msg; return 0

For scripts with multiple arguments:

script add (args) do
  match args with
  | [a, b] =>
    let x := a.toInt!
    let y := b.toInt!
    IO.println s!"{x} + {y} = {x + y}"
    return 0
  | _ =>
    IO.eprintln "Usage: lake run add <x> <y>"
    return 1

Accessing Lake Configuration from a Script

Inside a script, ScriptM gives access to the workspace configuration through Lake.getLakeEnv:

script info (args) do
  let env ← getLakeEnv
  IO.println s!"Package: {env.rootPackage.name}"
  IO.println s!"Build dir: {env.rootPackage.buildDir}"
  return 0

Example: A Script That Generates a File

A common use case for scripts is code generation. This script writes a Lean source file containing build metadata:

import Lake
open Lake DSL

package "mypkg" where
  version := v!"1.0.0"

/--
Generate BuildInfo.lean with the current timestamp.

USAGE:
  lake run genBuildInfo

Creates `src/BuildInfo.lean` with the build date and package version.
-/
script genBuildInfo (args) do
  let env ← getLakeEnv
  let pkgName := env.rootPackage.name
  let version := env.rootPackage.config.version
  let timestamp ← IO.Process.run {
    cmd := "date", args := #["-u", "+%Y-%m-%dT%H:%M:%SZ"]
  }
  let content := s!"-- Auto-generated by `lake run genBuildInfo`. Do not edit.\n" ++
                 s!"def buildTimestamp : String := \"{timestamp.trim}\"\n" ++
                 s!"def packageVersion : String := \"{version}\"\n"
  IO.FS.writeFile "src/BuildInfo.lean" content
  IO.println s!"Generated src/BuildInfo.lean"
  return 0

Run it with:

lake run genBuildInfo

Test and Lint Driver Scripts

Scripts can be designated as the package’s test driver or lint driver by applying the @[test_driver] or @[lint_driver] attribute:

/-- Run the full test suite. -/
@[test_driver]
script test (args) do
  -- run tests and return the appropriate exit code
  let result ← IO.Process.spawn {
    cmd := "python3", args := #["scripts/run_tests.py"] ++ args
  }
  let code ← result.wait
  return code.toUInt32

/-- Run the linter on all source files. -/
@[lint_driver]
script lint (args) do
  let result ← IO.Process.spawn {
    cmd := "python3", args := #["scripts/lint.py"] ++ args
  }
  let code ← result.wait
  return code.toUInt32

These scripts are invoked automatically by lake test and lake lint:

lake test                  # runs the @[test_driver] script
lake test -- --only Foo    # passes '--only Foo' to the script
lake lint                  # runs the @[lint_driver] script

Complete Example

A lakefile.lean with two scripts:

import Lake
open Lake DSL

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

lean_lib MyProject

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

/--
Greet someone by name.

USAGE:
  lake run greet [name]

If no name is given, greets the world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

/--
Print the workspace root package name and version.
-/
script version (_args) do
  let env ← getLakeEnv
  let cfg := env.rootPackage.config
  IO.println s!"{cfg.name} v{cfg.version}"
  return 0

Run the scripts:

$ lake scripts
greet
version

$ lake run greet
Hello, world!

$ lake run greet Alice
Hello, Alice!

$ lake script doc greet
Greet someone by name.

USAGE:
  lake run greet [name]

If no name is given, greets the world.

$ lake run version
myproject v0.1.0

Getting Started with Lake

Configuration

CLI Reference

Writing, Declaring, and Running Lake Scripts in Lean 4

Script Type Signature

Declaring a Script

Lean DSL

TOML Lakefiles

Running a Script

`lake run` (shorthand)

`lake script run`

Listing Available Scripts

Printing Script Documentation

Working with Arguments

Accessing Lake Configuration from a Script

Example: A Script That Generates a File

Test and Lint Driver Scripts

Complete Example

Build docs developers (and LLMs) love

Getting Started with Lake

Configuration

CLI Reference

Documentation Index

​Script Type Signature

​Declaring a Script

​Lean DSL

​TOML Lakefiles

​Running a Script

​lake run (shorthand)

​lake script run

​Listing Available Scripts

​Printing Script Documentation

​Working with Arguments

​Accessing Lake Configuration from a Script

​Example: A Script That Generates a File

​Test and Lint Driver Scripts

​Complete Example

Build docs developers (and LLMs) love

Script Type Signature

Declaring a Script

Lean DSL

TOML Lakefiles

Running a Script

`lake run` (shorthand)

`lake script run`

Listing Available Scripts

Printing Script Documentation

Working with Arguments

Accessing Lake Configuration from a Script

Example: A Script That Generates a File

Test and Lint Driver Scripts

Complete Example