From d6e8ede7fa7f6768c8ad7924c0e845d656c1249c Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sun, 10 May 2026 15:27:55 +0800
Subject: [PATCH 1/4] Fix crash while loading make_complex.ml

CODE_BUFFER_SIZE 5242880 is not enough.
---
 build-instructions.sh | 3 ++-
 candle/cake.S.patch   | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/build-instructions.sh b/build-instructions.sh
index cc071efc..ade35db3 100755
--- a/build-instructions.sh
+++ b/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
diff --git a/candle/cake.S.patch b/candle/cake.S.patch
index ba2e9cde..d0fe686a 100644
--- a/candle/cake.S.patch
+++ b/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

From fc57d79414f83513d77dd0595f7ca5ced6807aa5 Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sun, 10 May 2026 15:29:06 +0800
Subject: [PATCH 2/4] Fix Multivariate/canal.ml

---
 Multivariate/canal.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Multivariate/canal.ml b/Multivariate/canal.ml
index ef5cc02d..be30c21d 100644
--- a/Multivariate/canal.ml
+++ b/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

From 90e8ecceb63afe465c993b839ccc04bf1a767c7a Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sun, 10 May 2026 15:29:11 +0800
Subject: [PATCH 3/4] Fix Multivariate/clifford.ml

---
 Multivariate/clifford.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Multivariate/clifford.ml b/Multivariate/clifford.ml
index 8da82a7f..3664d52d 100644
--- a/Multivariate/clifford.ml
+++ b/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

From 6a89d0b624a5a557c081a55614f9b4345af3296f Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sun, 10 May 2026 17:09:15 +0800
Subject: [PATCH 4/4] Fix Multivariate/realanalysis.ml

---
 Multivariate/realanalysis.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Multivariate/realanalysis.ml b/Multivariate/realanalysis.ml
index 766daae6..ee6eddcb 100644
--- a/Multivariate/realanalysis.ml
+++ b/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