# Compiling Lean files

The FormulationBench dataset includes many [Lean](https://lean-lang.org/) files. Each formulation and reformulation proof has a corresponding Lean file and `Common.lean` defines {ref}`formulation-definition` and {ref}`reformulation-definition`.

This guide provides minimal instructions for compiling Lean files. For extensive documentation and tutorials on Lean, we direct the curious reader to the [Lean Community](https://leanprover-community.github.io/) documentation.

## Install Lean

See the Lean [installation instructions](https://lean-lang.org/install/). The recommended way to install Lean is through VS Code. You can also install it [manually](https://lean-lang.org/install/manual/). This will install `elan`, the Lean version manager. `elan` will read `lean-toolchain` and fetch the right Lean version automatically.

## Initial Setup

The dataset is structured as a Lean project; it includes a `lakefile.toml` (see below) that specifies all dependency information and project structure. FormulationBench has one dependency: [Mathlib](https://mathlib-initiative.org/), Lean's comprehensive mathematical library.

:::{dropdown} `lakefile.toml`
:icon: code
```{literalinclude} ../../../../dataset/lakefile.toml
:language: lean
```
:::

Lean projects are managed by `lake`, the Lean package manager. After downloading the dataset (see {doc}`/user_guide/download`), run the following commands from the dataset root to download pre-compiled Mathlib files. This may take a few minutes.

```bash
lake update
lake exe cache get
```

## Building everything

Run `lake build` from the dataset root to compile every Lean file in the dataset. This is expected to take ~5-10 minutes on the first build. Subsequent builds are incremental. 

```bash
lake build
```

:::{warning}
If pre-compiled Mathlib files were not downloaded successfully, the initial build will take substantially longer than 10 minutes. When you run `lake build`, verify the initial output is consistent with Mathlib being pre-compiled successfully.

**[BAD] Mathlib is missing and is being compiled from source:**

```bash
$ lake build
[2/40] Running importGraph:optBarrel (+ 3 more)
```

**[GOOD] Mathlib was pre-compiled successfully:**

```bash
$ lake build
[3102/3289] Running Common (+ 0 more)
```
:::

## Building a single file

To compile just one formulation or proof, pass its module path:

```bash
# Build a single MILP formulation:
lake build problems.p1.formulations.a.Formulation

# Build a single reformulation proof:
lake build reformulations.p1.a_b
```

The module path mirrors the dataset path with `/` replaced by `.`
and the `.lean` extension dropped. Lake will pull in only the
files actually required by the target.

## FLARE Monorepo

The FormulationBench dataset is managed by the {github}`FLARE monorepo </>`. This is configured as its *own* Lean project to support compiling Lean files generated by {mf}`FLARE </>`, and the FormulationBench dataset is configured as a local dependency. From the root of the monorepo, run `lake build FormulationBench` to build everything. Use the same commands as above to build single files; the module paths are the same. If you did the initial setup inside the `dataset` directory, you'll need to re-run from the root of the monorepo.