Move Candle specific files to a new subdirectory

As explained in a comment in build-instructions.sh, this leads to a bit of
changing directories at the beginning.

The following mental model may be useful: all (relative) paths should be
relative to the project root. The main wrinkle here is that the cake binary
currently expects some files at hardcoded locations - so if we don't want those
files to be at the top-level directory, we need to start Candle in a different
location, and change directory right after booting.

To enable this, we also make use of the new "custom" FFI port - this will become
handy in the future for getting the time and calling external binaries.

Author: dnezam

basics.ml

@@ -8,7 +8,7 @@
 (*     (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018              *)
 (* ========================================================================= *)
 
-needs "candle_kernel.ml";;
+needs "candle/kernel.ml";;
 
 (* ------------------------------------------------------------------------- *)
 (* Create probably-fresh variable                                            *)

build-instructions.sh

@@ -1,32 +1,44 @@
 #!/bin/bash
+# Set up "strict mode" for bash
 set -euo pipefail
 
+# Create (if needed) + Change into the build directory
+mkdir -p candle/build
+cd candle/build
+
 # Get the 64-bit CakeML compiler from here:
-curl -OL https://cakeml.org/regression/artefacts/3276/cake-x64-64.tar.gz
-tar xvzf cake-x64-64.tar.gz
+curl -OL https://cakeml.org/regression/artefacts/3286/cake-x64-64.tar.gz
+tar xvzf cake-x64-64.tar.gz --strip-components=1
 
 # By default, the CakeML compiler reserves a few kilobytes for constants and
 # code produced by the dynamic compiler. Using Candle requires setting these
 # to some megabytes:
-patch cake-x64-64/cake.S cake.S.patch
+patch cake.S ../cake.S.patch
 
-# Build the compiler binary
-cd cake-x64-64 && make && cd ..
+# Patching in useful FFI calls
+patch basis_ffi.c ../basis_ffi.c.patch
 
-# Copy the compiler binary, the exported compiler state and candle_boot.ml into
-# this directory:
-cp cake-x64-64/cake cake-x64-64/config_enc_str.txt cake-x64-64/candle_boot.ml .
+# Build the compiler binary
+make
 
 # Create the types.txt file necessary for candle_insulate.py
 ./cake --types < /dev/null > types.txt 2>&1
 
 # Generate candle_insulate.ml
-python candle_insulate.py types.txt candle_insulate.ml
+python ../insulate.py types.txt insulate.ml
+
+#  The working directory of the binary will be CANDLE_ROOT/candle/build,
+#  so it needs to change directory to CANDLE_ROOT after booting..
+#
+#  Q: Why do we not start the cake binary from CANDLE_ROOT?
+#  A: The cake binary looks for config_enc_str.txt and candle_boot.ml relative
+#     to the current working directoy. I find it neater if these files are not
+#     copied to CANDLE_ROOT, but stay tucked away in the build folder.
+#
+cat ../chdir_to_root.ml >> candle_boot.ml
 
 # You can now run Candle by writing:
-#   $ ./cake --candle
-# or:
-#   $ ./candle
+#   $ ./candle.sh
 # (without the $) at your prompt. Load the HOL Light sources by writing:
 #   > #use "hol.ml";;
 # (without > and with double semicolons) in the REPL.

candle

@@ -0,0 +1,11 @@
+#!/bin/bash
+# Set up "strict mode" for bash
+set -euo pipefail
+
+# Change into correct directory - note that Candle must take care to change back
+# to script_dir (see build-instructions.sh for more information)
+script_dir=$(dirname -- "$(readlink -f -- "${BASH_SOURCE[0]}")")
+cd $script_dir/candle/build
+
+# Start Candle
+./cake --candle

candle.sh

@@ -0,0 +1 @@
+build/

candle/.gitignore

@@ -0,0 +1,20 @@
+--- basis_ffi.c
++++ basis_ffi.c
+@@ -294,6 +294,13 @@
+ }
+
+ void fficustom (unsigned char *c, long clen, unsigned char *a, long alen) {
+-  assert(0 <= alen);
+-  assert(0 <= clen);
++  if (strcmp(c, "chdir") == 0) {
++    assert(1 <= alen);
++    a[0] = chdir(a) != 0;
++  } else if (strcmp(c, "getcwd") == 0) {
++    assert(1 <= alen);
++    a[0] = getcwd(a + 1, alen - 1) == NULL;
++  } else {
++    return;
++  }
+ }
+
+ // ---------------------------------------------------------------------------

candle/basis_ffi.c.patch

@@ -0,0 +1,18 @@
+
+exception Sys_error of string;;
+let pp_exn e =
+  match e with
+  | Sys_error s ->
+     Pretty_printer.app_block "Sys_error" [Pretty_printer.pp_string s]
+  | _ -> pp_exn e;;
+
+let chdir dir =
+  let len = String.size dir in
+  let _ = if len = 0 then raise (Sys_error "Sys.chdir: empty input") else () in
+  let bytes = Word8_array.array (len + 1) (Word8.fromInt 0) in
+  let _ = Word8_array.copyVec dir 0 len bytes 0 in
+  let _ = Runtime.customFFI "chdir" bytes in
+  let ret = Word8.toInt (Word8_array.sub bytes 0) in
+  if ret <> 0 then raise (Sys_error "Sys.chdir: unsuccessful FFI") else ();;
+
+let _ = chdir "../..";;