# Icing

A new, nondeterministic floating-point source semantics and a proof-of-concept
connection to the CakeML verified compiler.

The development is known to compile with HOL4 running on commit
`30c14988fa7ce031bc99f6828e07df9529e6c3a9`.

The folder `cakeml` contains the CakeML verified compiler as a git submodule.
To checkout the latest revision which compiles with Icing run

    git submodule update --init cakeml

Afterwards the `cakeml` folder should be up-to-date.

To compile the development run `Holmake` after initializing the CakeML submodule.
All of the files, apart from `CakeMLconnScript.sml` can be build without
the CakeML compiler being initialized and do not depend on CakeML internals,
however it is necessary to initialize the submodule because HOL4 wants to
compile CakeML dependencies first.