Obtaining CakeML

Here we explain how to build and run the bootstrapped CakeML compiler. You can run the bootstrapping process yourself, or download the result of one of our recent builds.

Bootstrapping locally

Bootstrapping the compiler in the logic takes several hours and works better with more RAM (16GB is a probable minimum). Example timings for the final phase (evaluation in the logic) can be found here. The pre-built section has downloads so you can avoid doing it yourself.
  1. Set up the CakeML repository (this includes obtaining Poly/ML and HOL).
  2. Run Holmake in the compiler/bootstrap/evaluation directory. This will produce the file cake.S.
  3. Build and run as described below.

Building and running CakeML

  1. Obtain basis/basis_ffi.c for the correct revision
  2. gcc -o cake basis_ffi.c cake.S to produce cake executable
Run, supposing input.cml contains CakeML source:
  1. ./cake <input.cml >result.S
  2. gcc -o result basis_ffi.c result.S to produce result executable

Downloading bootstrap results

Here are some pre-built cake.S files, named according to their repository revision. To use them above, unpack and rename the cake.xxxxxx.S file to cake.S.