[isabelle-dev] NEWS: CakeML compiler

[Lars Hupel]

This refers to AFP/c245a746483a and Isabelle/337b8ce5ff8d.

The CakeML compiler is now available from within Isabelle/ML.

Steps to use:

1) echo 'init_components "$HOME/.isabelle/contrib" 
"$ISABELLE_HOME/Admin/components/cakeml"' >> ~/.isabelle/etc/settings
2) echo 'ISABELLE_CC=gcc' >> ~/.isabelle/etc/settings
    (or clang, if you like)
3) isabelle components -a
4) import "CakeML.CakeML_Compiler" [*]
5) the command "cakeml" with the flags "literal" and "prog" is available

Examples:

cakeml (literal) ‹print "hi1";› (* prints "hi1" *)
cakeml (literal) ‹print "hi2";› (* prints "hi2" *)

(* this defines a HOL term that corresponds to a CakeML AST *)
definition simple_print :: Ast.prog where
"simple_print =
   [Ast.Tdec (Ast.Dlet default_loc Ast.Pany (Ast.App Ast.Opapp [Ast.Var 
(Short ''print''), Ast.Lit (Ast.StrLit ''hi'')]))]"

cakeml (prog) ‹simple_print› (* prints "hi" *)

How it works:

The bootstrapped CakeML compiler is available as a component that 
provides binaries for Linux and macOS. The steps to compile a CakeML 
program are as follows:

1) use "cake" to produce an assembly file "foo.S" from some input 
"foo.ml"
2) use "ISABELLE_CC" to compile the "basis_ffi.c" file to "basis_ffi.o" 
(provided by the CakeML component)
3) use "ISABELLE_CC" to link "basis_ffi.o" and "foo.S"

"cakeml (literal)" will take a cartouche that contains a literal CakeML 
program and invokes those steps.

"cakeml (prog)" will take a term. That term is evaluated through the 
code generator -- expecting a CakeML AST --, and then converted into a 
string. It will then do the same as above. The conversion into a string 
is very rudimentary at the moment. It only supports a tiny fraction of 
the CakeML abstract syntax.

Let me know if you run into any problems.

[*] Note that that theory is _not_ built when building the AFP unless 
the CakeML component is enabled and "ISABELLE_CC" is set. In a way, it's 
similar to the various "export_code ... checking" theories.