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.

The compiler supports five target architectures (x86-64, RISC-V, ARMv8, ARMv6, MIPS), however, we currently only have the build process worked out for x86-64. Pre-built bootstrapped CakeML compilers for the other architectures will become available soon.

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 step includes obtaining Poly/ML and HOL. The only other dependency is a C compiler, to compile and link our I/O primitives.
  2. Run Holmake in the compiler/bootstrap/evaluation/x64 directory. This will eventually produce an executable, cake. (It also produces cake.S and basis_ffi.c, which are linked together to form cake.)
  3. Run it as described below.

Running CakeML

  1. Write a CakeML program. For example, echo 'print "Hello!\n";'>input.cml.
  2. ./cake <input.cml >result.S. Optionally provide additional arguments to the compiler, like --inline_size=20.
  3. gcc -o result basis_ffi.c result.S to produce the result executable
  4. Run the result! ./result

Downloading bootstrap results

Download the latest pre-built tarball (Jun 26 2017). To use it, unpack it (tar -xvzf cake-latest.tar.gz), then run make (or make cake) to obtain a cake executable that can be used as above. The provided Makefile can also automate the steps above: make result will compile input.cml.

Builds of previous revisions

These are cake.S files generated by bootstrapping (for x64) at earlier revisions of the frequently changing CakeML repository. They are probably only of interest for performance or feature comparisons. To use them, unpack, rename the cake.xxxxxx.S file to cake.S, and link them with the basis_ffi.c from the appropriate revision: gcc -o cake basis_ffi.c cake.S.