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). We currently have the build process worked out for x86-64 and RISC-V. 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 or .../riscv directory (depending on the desired target). This will eventually produce an executable, cake. It also produces cake.S and basis_ffi.c, which are linked together to form cake. Note: for RISC-V, you need to have a cross compiler (e.g., riscv64-unknown-elf-gcc) set up for the last step to work. You may need to link the generated cake.S file manually, depending on your setup.
  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. Note: for RISC-V if you are not running on native hardware, you may need to invoke an emulator, for example spike pk cake.
  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 for x86-64. 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.

For RISC-V, we provide the latest pre-built tarball for RISC-V. It can be used as described above, however you may need to set your CC environment variable to the appropriate cross compiler, for example CC=riscv64-unknown-elf-gcc make cake.