[isabelle-dev] CakeML compiler in the AFP

[Lars Hupel]

Dear list,

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 [0]. Hence, it
requires a C compilation toolchain including "make" [1].

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
compiled on-the-fly.

I don't have a strong opinion either way. Thoughts?

Cheers
Lars


[0] The original download can be found here:
<https://github.com/CakeML/cakeml/releases/tag/v2.0>

[1] Luckily the "Makefile" is so simple that I am attaching it below in
full:

cake: cake.o basis_ffi.o

clean:
	rm -f cake.o basis_ffi.o cake

.PHONY: clean