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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev