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
Download a pre-built x64 tarball; pick
cake-x64-64.tar.gzfor compiling to 64-bit architectures, otherwise
- To use it, first unpack it: tar -xvzf cake-x64-64.tar.gz && cd cake-x64-64.
- 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.
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 locallyBootstrapping the compiler in the logic takes several hours and works better with more RAM (64 GB might be a minimum).
- 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.
- 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.
- Run it as described above.