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

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:

$ 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

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 FLARE monorepo. This is configured as its own Lean project to support compiling Lean files generated by 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.