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


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 "" 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.
isabelle-dev mailing list

Reply via email to