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