Skip to content

Fix make_complex.ml dependencies #13

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dnezam merged 4 commits into from
May 11, 2026
Merged

Fix make_complex.ml dependencies #13

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d6e8ede
Fix crash while loading make_complex.ml
dnezam May 10, 2026
fc57d79
Fix Multivariate/canal.ml
dnezam May 10, 2026
90e8ecc
Fix Multivariate/clifford.ml
dnezam May 10, 2026
6a89d0b
Fix Multivariate/realanalysis.ml
dnezam May 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Multivariate/canal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Multivariate/clifford.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);;
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Multivariate/realanalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion build-instructions.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions candle/cake.S.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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