Compiling Lean files

The FormulationBench dataset includes many Lean files. Each formulation and reformulation proof has a corresponding Lean file and Common.lean defines MILP Formulation and Reformulation.

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 documentation.

Install Lean

See the Lean installation instructions. The recommended way to install Lean is through VS Code. You can also install it manually. 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, Lean’s comprehensive mathematical library.

lakefile.toml

name = "FormulationBench"
version = "0.1.0"
defaultTargets = ["Common", "Dataset"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4"
rev = "v4.28.0"

[[lean_lib]]
name = "Common"

[[lean_lib]]
name = "Dataset"
srcDir = "."
globs = ["problems.+", "reformulations.+"]

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

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.

lake build

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:

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

[GOOD] Mathlib was pre-compiled successfully:

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

Building a single file

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

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

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

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.