# 1.2 Project Structure with Lean and Lake

Lean development is organized around projects. A project defines a closed environment: it fixes the Lean version, declares dependencies, and specifies how code is compiled. The structure is simple, but small details determine whether imports resolve, builds succeed, and tooling behaves predictably.

## Problem

You want a project layout that supports reproducible builds, clear module boundaries, and predictable imports.

## Solution

Create and work inside a Lake project. The default layout produced by:

```sh
lake new myproj
```

has the following structure:

```text
myproj/
├── lakefile.lean
├── lean-toolchain
├── Myproj/
│   └── Basic.lean
├── Main.lean
└── lake-manifest.json
```

Each file has a precise role.

## File Roles

| File                 | Purpose                                   |
| -------------------- | ----------------------------------------- |
| `lean-toolchain`     | Pins the Lean version                     |
| `lakefile.lean`      | Declares packages, libraries, executables |
| `lake-manifest.json` | Resolved dependency graph                 |
| `Myproj/`            | Library source directory                  |
| `Main.lean`          | Entry point for executables               |

The directory `Myproj/` corresponds to a namespace. The file:

```lean
-- Myproj/Basic.lean
namespace Myproj

def hello : String :=
  "hello"

end Myproj
```

is imported using:

```lean
import Myproj.Basic
```

The mapping between file paths and module names is strict. A mismatch between directory names and namespaces leads to unresolved imports.

## Lake Configuration

The file `lakefile.lean` defines the build graph. A minimal configuration looks like:

```lean
import Lake
open Lake DSL

package «myproj» where

lean_lib Myproj

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

This declares:

* a package named `myproj`
* a library `Myproj`
* an executable whose root module is `Main`

The executable is built and run with:

```sh
lake build
lake exe myproj
```

## Module System

Lean uses a hierarchical module system. A file path:

```text
Myproj/Data/List.lean
```

corresponds to module:

```lean
import Myproj.Data.List
```

Within the file, you typically declare:

```lean
namespace Myproj.Data
```

Namespaces do not have to match directories exactly, but keeping them aligned avoids ambiguity and reduces the need for qualification.

## Imports and Visibility

Imports are explicit. A file only sees definitions from modules it imports.

```lean
import Myproj.Basic
```

brings all public declarations from `Myproj.Basic` into scope.

You can control visibility:

```lean
open Myproj
```

to avoid prefixing names.

Or keep names qualified:

```lean
Myproj.hello
```

This choice affects readability and conflict resolution in larger projects.

## Dependency Management

Dependencies are declared in `lakefile.lean`. For example, adding mathlib:

```lean
require mathlib from git
  "https://github.com/leanprover-community/mathlib4"
```

Then update:

```sh
lake update
lake build
```

The resolved versions are stored in `lake-manifest.json`. This file should be committed for reproducibility.

## Build Model

Lake compiles modules incrementally. A change in one file triggers recompilation of dependent modules only.

Key properties:

* compilation is deterministic under fixed toolchain and dependencies
* imports define the dependency graph
* build artifacts are cached

This model supports large developments without full rebuilds.

## Minimal Working Example

Library file:

```lean
-- Myproj/Math.lean
namespace Myproj

def double (n : Nat) : Nat :=
  n + n

end Myproj
```

Executable:

```lean
-- Main.lean
import Myproj.Math

def main : IO Unit := do
  IO.println (toString (Myproj.double 10))
```

Run:

```sh
lake exe myproj
```

Expected output:

```text
20
```

## Common Pitfalls

If `import Myproj.X` fails, check that the file path is `Myproj/X.lean`.

If the editor shows unresolved imports, ensure you opened the project root, not a subdirectory.

If builds use the wrong Lean version, inspect `lean-toolchain`.

If dependencies fail to fetch, run `lake update` explicitly.

If names collide, avoid `open` and use qualified names.

## Takeaway

A Lean project is a controlled environment defined by `lean-toolchain` and `lakefile.lean`. Files map directly to modules, and imports define all visibility. Keeping directory structure, module names, and namespaces aligned removes a large class of errors and makes larger systems manageable.