This examplifies how to build the CakeML stack for translation without in-logic compilation. Functions defined in the theory listrevTheory get translated in listrevProgTheory to an s-expression. The Makefile compiles the previous into an executable program and runs simple tests.

A continuous integration (CI) performs these steps and finally produces the s-expression as a release artefact. The CI leverages the nix package manager so that compilation of both HOL4 and CakeML is a function of a git commit. The outputs are cached, and reused supposedly as long as the respective compilation function in flake.nix and its call arguments remain unchanged.

• flake.nix defines three compilation functions (hol4, cakeml, cakemlbin) and their commit hash input arguments.
• Makefile defines how the code of this repository shall be compiled, and is run by make with HOLDIR, CAKEMLDIR and CAKEDIR environment variables.
• .github/workflows/nix.yml defines the Github action workflow with caching and releasing an s-expression.