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 locallyBootstrapping 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.
- 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/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.)
- Run it as described below.
- Write a CakeML program. For example, echo 'print "Hello!\n";'>input.cml.
- ./cake <input.cml >result.S. Optionally provide additional arguments to the compiler, like --inline_size=20.
- gcc -o result basis_ffi.c result.S to produce the result executable
- Run the result! ./result
Downloading bootstrap resultsDownload 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 revisionsThese 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.
- cake-7d578ce.S.tar.gz (Jun 26 2017)
- cake-76757d2.S.tar.gz (Jun 08 2017)
- cake-fc29389.S.tar.gz (May 30 2017)
- cake-ca86d10.S.tar.gz (May 25 2017)
- cake-308eac6f2.S.tar.gz (May 22 2017)
- cake-6cccca6d2.S.tar.gz (May 13 2017)
- cake-ccc56c2.S.tar.gz (Apr 28 2017)
- cake-66f9b66.S.tar.gz (Apr 25 2017)
- cake-8f1ac5b86.S.tar.gz (Apr 21 2017)
- cake-e4d38e7b8.S.tar.gz (Apr 15 2017)
- cake-f193e590d.S.tar.gz (Apr 12 2017)
- cake-32b749c3.S.tar.gz (Mar 24 2017)
- cake-a95f62c3.S.tar.gz (Mar 17 2017)
- cake-bf676999.S.tar.gz (Mar 12 2017)
- cake-389d340f.S.tar.gz (Mar 04 2017)
- cake-3684c1cd.S.tar.gz (Mar 02 2017)