Optimized semantics example program scripts and misc, new import script

Author: didriklundberg

hol/cake_sem/programs/build_cake.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+if [ $# -ne 1 ]; then
+    echo "Usage: $0 <program_name>"
+    echo "Example: $0 my_program"
+    exit 1
+fi
+
+PROGRAM_NAME=$1
+
+Holmake ${PROGRAM_NAME}Theory
+
+cp ${PROGRAM_NAME}.sexp compilation/
+
+cd compilation
+
+./compile_cake.sh ${PROGRAM_NAME}
+
+cd ..

hol/cake_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.