Fix make_complex.ml dependencies (#13)

* Fix crash while loading make_complex.ml

CODE_BUFFER_SIZE 5242880 is not enough.

* Fix Multivariate/canal.ml

* Fix Multivariate/clifford.ml

* Fix Multivariate/realanalysis.ml

Author: dnezam

Multivariate/canal.ml

@@ -2391,7 +2391,7 @@ let HOLOMORPHIC_CONSTANT_IM = prove
 (* Differentiation conversion.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-let complex_differentiation_theorems = ref [];;
+let complex_differentiation_theorems = ref ([]: thm list);;
 
 let add_complex_differentiation_theorems =
   let ETA_THM = prove

Multivariate/clifford.ml

@@ -761,7 +761,7 @@ let SETENUM_NORM_CONV =
     GEN_REWRITE_CONV I [FORALL_SIMP] in
   fun tm ->
     let nums = dest_setenum tm in
-    let nums' = map mk_numeral (sort (</) (map dest_numeral (setify nums))) in
+    let nums' = map mk_numeral (sort (</) (map dest_numeral (setify Term.(<) nums))) in
     if nums' = nums then REFL tm else
     let eq = mk_eq(tm,mk_setenum(nums',fst(dest_fun_ty(type_of tm)))) in
     EQT_ELIM(conv eq);;
@@ -829,7 +829,7 @@ let MBASIS_GROUP_CONV tm =
   let vadd_tm = rator(rator tm) in
   let mk_vadd = mk_binop vadd_tm in
   let mbs = map (snd o dest_binary "%") tms in
-  let tmbs = zip mbs tms and mset = setify mbs in
+  let tmbs = zip mbs tms and mset = setify Term.(<) mbs in
   let grps = map (fun x -> map snd (filter (fun (x',_) -> x' = x) tmbs))
                  mset in
   let tm' = end_itlist mk_vadd (map (end_itlist mk_vadd) grps) in

Multivariate/realanalysis.ml

@@ -4326,7 +4326,7 @@ let REAL_CONTINUOUS_ON_ACS = prove
 (* Differentiation conversion.                                               *)
 (* ------------------------------------------------------------------------- *)
 
-let real_differentiation_theorems = ref [];;
+let real_differentiation_theorems = ref ([]: thm list);;
 
 let add_real_differentiation_theorems =
   let ETA_THM = prove

build-instructions.sh

@@ -12,7 +12,8 @@ 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:
+# to some megabytes (or hundreds of megabytes for some of the more heavier
+# files in HOL Light, such as make_complex.ml).
 patch cake.S ../cake.S.patch
 
 # Patching in useful FFI calls

candle/cake.S.patch

@@ -2,5 +2,5 @@
 < #define DATA_BUFFER_SIZE    65536
 < #define CODE_BUFFER_SIZE  5242880
 ---
-> #define DATA_BUFFER_SIZE  65536000
-> #define CODE_BUFFER_SIZE  52428800
+> #define DATA_BUFFER_SIZE  655360000
+> #define CODE_BUFFER_SIZE  524288000