Projects and Structure in Lean

Project setup
- Build targets
- Organizing in files and directories
  - Simple
  - Multiple source directories
Libraries and dependencies
Modules
Naming Conventions
Project Organization
- Directory Structure
- Import Patterns
Learning Resources

Project setup

Lean comes with a project management tool called lake. To set up a new Lean project:

Create a new directory for the project and navigate into it:
```
mkdir my_lean_project
cd my_lean_project
```
Initialize the project with lake:
```
lake init
```
Build the project:
```
lake build
```

Build targets

Lean has two main types of build targets: libraries and executables. Libraries are collections of Lean code that can be reused across multiple projects, while executables are standalone programs that can be run directly. Usually a library project will also have an executable target for testing or demo purposes.

By default, lake build only builds library targets. To ensure executables are also built when running lake build without arguments, add a defaultTargets configuration to your lakefile.toml:

name = "myproject"
defaultTargets = ["MyLib", "myexe"]

[[lean_lib]]
name = "MyLib"
srcDir = "src"

[[lean_exe]]
name = "myexe"
root = "main.lean"

This ensures that both the library and executable are built when you run lake build.

Organizing in files and directories

As Lean projects grow, code should be organized across multiple files and directories. Lake supports several ways to structure projects:

Simple

For basic projects, files can be organized in subdirectories within the srcDir:

src/
├── MyProject.lean          # Main module
├── Basic/
│   ├── Numbers.lean        # src/Basic/Numbers.lean
│   └── Structures.lean     # src/Basic/Structures.lean
└── Advanced/
    └── Theorems.lean       # src/Advanced/Theorems.lean

Import these files using dot notation:

import Basic.Numbers        -- imports src/Basic/Numbers.lean
import Advanced.Theorems    -- imports src/Advanced/Theorems.lean

Multiple source directories

To include files from directories outside the main srcDir (like test files), configure additional library targets:

[[lean_lib]]
name = "MyProject"
srcDir = "src"

[[lean_lib]]
name = "Tests"
srcDir = "."
roots = ["test"]

[[lean_exe]]
name = "test_runner"
root = "test_runner.lean"

With this structure, test files can be imported:

import test.TestModule      -- imports test/TestModule.lean

Libraries and dependencies

Lean 4 uses lake as both a build system and package manager. Libraries are managed through dependencies in your project configuration.

Adding dependencies

Dependencies must be added manually by editing the lakefile.toml file:

Add to lakefile.toml: Edit the project’s lakefile.toml to include the dependency:
```
[[require]]
name = "mathlib"
scope = "leanprover-community"
```
Update dependencies: After editing the lakefile, run:
```
lake update
```
Build with new dependencies:
```
lake build
```

Common libraries

Mathlib: The comprehensive mathematics library

[[require]]
name = "mathlib"
scope = "leanprover-community"

Batteries: Standard library extensions (formerly std)

[[require]]
name = "batteries"
scope = "leanprover-community"

Aesop: Automated theorem proving tactic

[[require]]
name = "aesop"
git = "https://github.com/JLimperg/aesop"

Managing dependencies

Update all dependencies:
```
lake update
```
Clean and rebuild:
```
lake clean
lake build
```
Check dependency status:
```
lake deps
```

Working with local libraries

For local development, libraries can be referenced using relative paths in the lakefile.toml:

[[require]]
name = "mylib"
path = "../path/to/mylib"

Example: Complete lakefile.toml

Here’s an example of a mature lakefile.toml with multiple dependencies:

name = "MyMathProject"
version = "0.1.0"
keywords = ["math", "algebra", "category-theory"]
homepage = "https://github.com/user/MyMathProject"
repository = "https://github.com/user/MyMathProject.git"
authors = ["Author Name <email@example.com>"]
license = "Apache-2.0"
defaultTargets = ["MyMathProject", "main"]

[package]
buildType = "release"

[[lean_lib]]
name = "MyMathProject"
srcDir = "src"

[[lean_exe]]
name = "main"
root = "main.lean"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[[require]]
name = "batteries"
scope = "leanprover-community"

[[require]]
name = "aesop"
git = "https://github.com/JLimperg/aesop"

[[require]]
name = "batteries"
scope = "leanprover-community"

# Local dependency example
[[require]]
name = "MyUtilLib"
path = "../MyUtilLib"

Modules

Modules are a fundamental way to organize code in Lean, similar to other programming languages. They help to group related definitions, theorems, and proofs together, making it easier to manage large codebases.

File-based modules

In Lean, each file implicitly declares a module with the same name as the file (without the .lean extension). The file path determines the module name using dot notation:

src/Basic.lean → module Basic
src/Data/List.lean → module Data.List
test/TestBasic.lean → module test.TestBasic (if test directory is configured as a root in lakefile.toml)

Importing modules

Modules can be imported using absolute paths based on the project structure:

import Basic.Numbers            -- imports src/Basic/Numbers.lean
import Data.List.Lemmas         -- imports src/Data/List/Lemmas.lean
import test.TestNumbers         -- imports test/TestNumbers.lean
import TestNumbers              -- imports test/TestNumbers.lean

For all the direcories listed in the lakefile.toml as srcDir or root, the files inside them can be imported using their relative paths.

Explicit module declarations

You can also explicitly declare modules within a file:

module MyModule where
  -- Module contents here
  def myFunction := 42

module NestedModule where
  -- Nested module contents
  def nestedFunction := 24

This creates namespaces that can help organize code within a single file.

Naming Conventions

Lean has some common naming practices, though they’re more guidelines than strict rules:

Functions and variables: Use camelCase (e.g., addNumbers, totalCount)
Types and structures: Use PascalCase (e.g., NaturalNumber, BinaryTree)
Modules: Use PascalCase (e.g., Data.List, Logic.Propositional)
Constants and axioms: Often use PascalCase (e.g., Pi, ExcludedMiddle)
Unicode characters: Lean supports Unicode, so mathematical symbols are common (e.g., ∀, λ, →)
Notation: Lean has a powerful notation system for defining custom syntax

Project Organization

Directory Structure

Lean projects benefit from consistent organization. Here are common patterns:

Mathematical projects:

src/
├── Basic/
│   ├── Definitions.lean    # Core definitions
│   └── Properties.lean     # Basic properties
├── Algebra/
│   ├── Groups.lean         # Group theory
│   └── Rings.lean          # Ring theory
└── Logic/
    ├── Propositional.lean  # Propositional logic
    └── Predicate.lean      # Predicate logic

Software projects:

src/
├── Core/
│   ├── Types.lean          # Core data types
│   └── Utils.lean          # Utility functions
├── Parser/
│   ├── Lexer.lean          # Lexical analysis
│   └── Grammar.lean        # Grammar definitions
└── Compiler/
    ├── Frontend.lean       # Frontend processing
    └── Backend.lean        # Code generation

Import Patterns

Lean imports should be structured to minimize dependencies and improve clarity. Here are some stuff to remember:

Hierarchical imports: Lean imports should ideally be hierarchical, importing from more general to more specific modules.

import Basic.Definitions    -- General definitions first
import Basic.Properties     -- Then their properties
import Algebra.Groups       -- Then specialized structures

Avoiding circular imports: Circular dependencies can lead to complications and Lean may fail to compile. Ensure that modules do not depend on each other in a circular manner.

-- ✓ Good: Clear dependency chain
Basic.Definitions → Basic.Properties → Algebra.Groups → Algebra.Advanced

-- ✗ Bad: Circular dependency
Groups ↔ Rings  -- Groups imports Rings, Rings imports Groups

Selective imports: Importing broad modules can lead to namespace pollution, leading to stuff like naming conflicts to increasing compilation times. Import only what is needed.

import Basic.Definitions (MyType, myFunction)
import Algebra.Groups (Group, group_axioms)

Learning Resources

Here are recommended resources for learning Lean:

Lean’s official documentation: A great guide to get started with Lean 4.
Theorem Proving in Lean: An introduction to theorem proving using Lean.
Mathematics in Lean: A tutorial on formalizing mathematics in Lean.
Functional Programming in Lean: A guide to functional programming concepts in Lean.
Lean for the Curious Mathematician: An introduction to Lean for mathematicians.
Lean Zulip Chat: A community chat for Lean users and developers.
Lean Together: Materials from the Lean Together workshops.
Lean 4 Examples: A collection of example Lean 4 projects.
The Natural Number Game: An interactive tutorial for learning Lean through number theory.
Formal Abstractions: A YouTube channel with Lean tutorials and demonstrations.

Types