README updates, CakeML FFI C code

Author: didriklundberg

hol/cake_sem/README.md

@@ -1,9 +1,5 @@
-NOTE: This directory uses HOL4 commit `718b3aa`, and is not guaranteed to function properly with the Trindemossen-1 release.
+Please set identifier (32-bit, 64-bit word) for your compilation target in `p4_cake_auxLib.sml`, as well as optimization flags.
 
-The CakeML release used in this directory is `v2882`.
+`p4_exec_sem_cakeScript.sml` contains an optimized reformulation of the regular executable semantics (found in `p4_exec_semScript.sml`).
 
-Please set identifier (23-bit, 64-bit word) for your compilation target in `p4_cake_auxLib.sml`.
-
-`p4_exec_sem_cakeScript.sml` contains a more CakeML-friendly reformulation of the regular executable semantics (found in `p4_exec_semScript.sml`).
-
-`p4_cake_transformScript.sml` contains HOL4 functions to transform the actx and astate of the regular semantics to those of the CakeML-adjusted version. The SML functions are found in `p4_cake_transformLib.sml`.
+`p4_cake_transformScript.sml` contains HOL4 functions to transform the actx and astate of the regular semantics to those of the optimized version. The SML functions are found in `p4_cake_transformLib.sml`.

hol/retrofit_sem/programs/compilation/README.md

@@ -0,0 +1 @@
+The easiest way to compile to CakeML is to download and extract a suitable release (e.g. for (Trindemossen-2)[https://github.com/CakeML/cakeml/releases/tag/vHOL-Trindemossen-2]) here and keep the existing version of `basis_ffi.c`, which enables you to use `build_cake.sh` in the directory below. If you have already compiled the entire CakeML repository, you may just edit `compile_cake.sh` to use the compiler from there instead.