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 can produce code for four 64-bit target architectures (x86-64, RISC-V, ARMv8, MIPS), and one 32-bit target architecture (ARMv6). The compiler can be built to run on each of the above architectures. We currently have the build process in place for x86-64 only (producing code for all targets). Pre-built bootstrapped CakeML compilers to run on other architectures can be made on request.

Downloading bootstrap results

  1. Download the latest pre-built tarball for x86-64 producing all 64-bit targets, or the same producing the 32-bit target.
  2. To use it, first unpack it: tar -xvzf cake-x64-64.tar.gz && cd cake-x64-64.
  3. Then run make (or make cake) to obtain a cake executable that can be used as described below.

The pre-built tarballs above, as well as earlier versions, are available as build artefacts on our regression test server.

Running CakeML

The Makefile provided in the pre-built downloads above automates the process below: make result will compile input.cml producing code for x86-64.

If you prefer to do things manually, or need to specify compile-time options:

  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 or --target=arm8.
  3. cc -o result basis_ffi.c result.S to produce the result executable
  4. Run the result! ./result

For non-x64 targets, if you are not running on native hardware, you may need to invoke an emulator, for example spike pk result for RISCV. You may also need to set your CC environment variable to the appropriate cross compiler, for example CC=riscv64-unknown-elf-gcc make cake.

Bootstrapping locally

Bootstrapping the compiler in the logic takes several hours and works better with more RAM (16GB is a probable minimum).
  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/compilation/x64/64 or .../32 directory (depending on the desired target(s)). This will eventually produce the cake-x64-64.tar.gz tarball described above.
  3. Run it as described above.
For examples of timings for running the above, you can see builds logs on our regression test server here, and some older more detailed timing data here.