Lean 4 Documentation

The Lean Language Server uses a decoupled architecture to ensure stability:

• Watchdog Process: A single process that manages per-file worker processes, maintains minimal persistent state (like open file contents), and coordinates communication with the LSP client.
• Worker Processes: Per-file processes where the actual computation (elaboration, #eval, autocompletion, etc.) occurs.

Key Benefits:

• Fault Isolation: If a user's metaprogram or #eval statement causes a crash (e.g., a stack overflow) in one file, only that specific worker process dies. The watchdog remains active, and other open files remain unaffected.
• Memory Management: Workers can be restarted to safely free memory used by imported modules' compacted regions, which cannot be safely managed by the standard GC.

Use elan to manage Lean toolchains and switch between build stages (like stage0 and stage1) automatically based on your directory. To install elan without setting a default Lean version, use the following commands depending on your OS:

# Unix
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none

# Windows (PowerShell)
curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -f elan-init.ps1 --default-toolchain none
del elan-init.ps1

Lake can fetch and unpack pre-built artifacts from GitHub releases to avoid rebuilding packages from source.

To use this, configure the following package options in your lakefile.lean:

• releaseRepo?: The GitHub repository hosting the release.
• buildArchive?: The name of the correct artifact within the release.
• preferReleaseBuild := true: Tells Lake to fetch and unpack the artifact as an extra package dependency.

Note: Lake only fetches release builds automatically if the package is a dependency. To manually fetch a release for a root package, use lake build :release.

Requirements:

• curl and tar must be installed on your system.

Standard library documentation follows these rules:

• Linter: Use set_option linter.missingDocs true to ensure declarations are documented.
• Single-line comments: Use /-- ... -/ on a single line.
• Multi-line comments: Use delimiters on their own lines, with the text unindented.
• Style: Use the indicative mood and American orthography.

Examples:

/-- Single line doc. -/
@[inline] def forM ...

/--
Multi-line
doc string.
--/
@[inline] def foldM ...

Dependencies can be added via Lean configuration (require) or TOML configuration ([[require]]).

Lean require Syntax

require ["<scope>" /] <pkg-name> [@ <version>] [from <source>] [with <options>]

• from <path>: Loads a package from a local directory.
• from git <url> [@ <rev>] [/ <subDir>]: Clones a Git repository. <rev> can be a hash, branch, or tag. Defaults to master.
• with <options>: Passes configuration options (equivalent to -K).

Mathlib Dependency Best Practice

When using mathlib as a dependency, run lake exe cache get before lake build to avoid rebuilding mathlib from scratch.

To generate a package configuration pre-configured for mathlib, use: lake new <package-name> math.

package hello

require "leanprover-community" / "mathlib"

Lean 4 documentation (docstrings, manuals, guides, and examples) follows a consistent voice designed for a diverse audience of mathematicians, software developers, computer scientists, and students. The primary goal is accessibility and clarity for readers with various linguistic and cultural backgrounds.

Key Principles:

• Readers First: If a style rule makes text harder to understand, break the rule.
• Audience: Assume knowledge common to both math and CS (e.g., monads), but do not assume a full undergraduate curriculum unless specified.
• Standard: Use US English and the Chicago Manual of Style (18th Edition, Part II) as the default arbiter for style disputes.

When naming functions that return specific types, use the following suffixes to clarify behavior:

• ? suffix: Use when the function returns an Option (e.g., List.head?).
• ! suffix: Use when the function may panic (e.g., List.head!).

When writing code for the Lean standard library, follow these whitespace conventions:

• Syntactic elements: Surround :, :=, |, and :: with single spaces.
• Delimiters: Do not put spaces inside () or {} (except for subtype or structure instance notation).
• Commas and Semicolons: Follow , and ; with a space, but do not precede them with one.

Examples:

• Correct parameters: {α : Type u}, [BEq α], (cmp : α → α → Ordering)
• Correct terms: 1 :: [2, 3], (⟨2, 3⟩ : Nat × Nat)

Before building Lean 4 from source on Ubuntu, you must install the required build tools and development libraries. Ensure you have git, libgmp-dev, libuv1-dev, libssl-dev, cmake, ccache, clang, and pkgconf installed via apt-get.

sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf

On Linux, you can profile lean using the perf tool. To collect profile data, run perf record with the --call-graph dwarf flag, pointing to the lean binary in your release build directory and specifying the source file you wish to profile as an argument.

Note: If you use elan, the lean command executes the elan binary which selects the appropriate Lean version. For profiling, ensure you point directly to the specific lean binary in your build path (e.g., build/release/stage1/bin/lean).

perf record --call-graph dwarf build/release/stage1/bin/lean src/Lean/Elab/Term.lean

Simp sets

Name simp sets centered around a conversion function using the source_to_target pattern. Example: A simp set for BitVec.toNat should be named bitvec_to_nat.

Variable Naming Recommendations

• Hypotheses: h, h', or numerical sequences h₁, h₂. Also w (for "witness").
• Lists: l, l', l₁, or as, bs (use as/bs for different types). Avoid xs/ys for lists if possible.
• Arrays: xs, ys, zs. Use as/bs for different types.
• Vectors: xs, ys, zs. Use as/bs for different types.
• Indices: i, j, k. Descriptive names like start, stop, lo, hi are encouraged.
• Sizes: n, m.
• BitVec Width: w.
• Accumulators: acc in recursive functions.