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.
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 includes obtaining Poly/ML and HOL).
- Run Holmake in the compiler/bootstrap/evaluation directory. This will produce the file cake.S.
- Build and run as described below.
Building and running CakeMLBuild:
- Obtain basis/basis_ffi.c for the correct revision
- gcc -o cake basis_ffi.c cake.S to produce cake executable
- ./cake <input.cml >result.S
- gcc -o result basis_ffi.c result.S to produce result executable
Downloading bootstrap resultsHere are some pre-built cake.S files, named according to their repository revision.
- 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)