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 a pre-built x64 tarball; pick cake-x64-64.tar.gz for compiling to 64-bit architectures, otherwise cake-x64-32.tar.gz.
  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 CakeML how-to.md (part of the latest tarballs above) explains how to use the CakeML compiler. We summarise the building of an example here:

If you have print "Hello!\n"; in a file called hello.cml, then you can compile it using make hello.cake. To run the code, simply type ./hello.cake on the command line. The supplied Makefile has a pattern that builds name.cake from a name.cml file, for any name.

The CakeML compiler accepts command-line arguments and the Makefile passes these to the CakeML compiler using the CAKEFLAGS environment variable. One can, for example, adjust the register allocator with --reg_alg=0 (naive graph colouring) or --reg_alg=3 (advanced: iterated register coalescing); or choose to compile to a non-x64 target, e.g. --target=arm8.

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 RISC-V. 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 (64 GB might be a 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.