Various unverified tools, e.g. tools for converting OCaml to CakeML and an SML version of the CakeML register allocator.
front-end: A CakeML front-end written in Haskell. It tries to give reasonable parse and type error messages that include source locations. It includes a rudimentary CakeML to OCaml and CakeML to SML translator, currently used for benchmarking.
hol-light-syntax: A work in progress attempt to translate the particular OCaml syntax used by HOL Light into Standard ML (as a step towards CakeML).
lem: A parking lot for the old Lem files that were used for defining the semantics
ocaml-syntax: An OCaml to CakeML translator. Attempts to translate type-correct OCaml files to equivalent CakeML files. Multi-file programs should be supported eventually, but are not currently.
reg_alloc: A snapshot of the register allocator from the CakeML compiler, translated from HOL to CakeML then pretty-printed in Standard ML syntax.
sexpr-bootstrap: An alternative bootstrapping process: The translated AST of the compiler is printed as an S-expression then fed into a previously built executable of the CakeML compiler.