[isabelle-dev] CakeML compiler in the AFP
hupel at in.tum.de
Thu Sep 20 11:02:25 CEST 2018
I'm considering putting the entire CakeML compiler somewhere so that it
is accessible in the AFP. This includes a pretty-printer of (a small
subset of) the abstract syntax; together with some ML code that allows
one to invoke the compiler, not unlike "export_code ... checking".
Note that this is not yet the full compilation toolchain from
Isabelle/HOL to CakeML! It's just the tiny backend part where a CakeML
AST can be compiled by the official CakeML compiler.
I would do so without writing this to the list, but there are some
obstacles. The major obstacle being that the CakeML compiler is not in
fact a piece of ML code, but a large assembly artifact (65 MB
uncompressed) that needs to be linked to some FFI code . Hence, it
requires a C compilation toolchain including "make" .
I see two ways forward:
1) It becomes a component.
a) ... in Isabelle (optional)
b) ... in the AFP (optional?)
2) The compressed artifact (~ 2 MB with xz) is committed to the AFP and
I don't have a strong opinion either way. Thoughts?
 The original download can be found here:
 Luckily the "Makefile" is so simple that I am attaching it below in
cake: cake.o basis_ffi.o
rm -f cake.o basis_ffi.o cake
More information about the isabelle-dev