cakeml - Compile CakeML programs

This repository is an Isabelle component that is supposed to work together with the CakeML AFP entry. It provides a Makefile to build the bootstrapped CakeML compiler from the official release. The etc/settings file is used to tell Isabelle about the location of the compiler.

Installation

1. Obtain a recent development version of Isabelle.
2. Enable $ISABELLE_HOME/Admin/components/cakeml as component list in ~/.isabelle/etc/settings.
3. Set the ISABELLE_CC variable to gcc or clang.
4. Obtain a recent development version of AFP.
5. Import the theory CakeML.CakeML_Compiler.

Examples

See the test theory.

Packaging

1. Make sure the compiler works as expected by running make clean test.
2. Build the compiler on Linux and macOS and copy the resulting binaries to the respective folder in bin/.
3. git tag a release.
4. Run isabelle env ./package.sh.
5. Upload the resulting .tar.gz to the component repository.

Sources

This README is part of the repository isabelle-prover/cakeml-component.