This patch adds support for native compilation of HOL Light. If HOLLIGHT_USE_MODULE is set to 1, make inlines loads in hol_lib.ml and compiles into hol_lib.cmx and hol_lib.cmxa.
The stack overflow error is a hurdle when compiling the code using ocamlopt. To avoid this error, make uses ocamlopt.byte which is a bytecode version of ocamlopt and distributed by the current OPAM switch. Combined with OCAMLRUNPARAM=l=<some large number> which sets the maximum stack size for OCaml bytecode runners, this successfully compiles hol_lib. However, it could not still compile a significantly large project such as Multivariate. One possible approach is to chop the inlined .ml file into multiple smaller .ml files and compile each of them, but this makes the inliner script complicated which could be a concern...
This patch also adds unit_tests.ml, and when HOLLIGHT_USE_MODULE is set, compiles it into a bytecode and native executable.
It currently contains simple checks of the verbose quantifiers and constants, but it can contain more interesting sanity checks in the future.
The CI check is also updated to make with HOLLIGHT_USE_MODULE set to 1 and run the unit tests.
OCaml 4.05 CI check had been broken, and this is fixed too.
This patch adds support for native compilation of HOL Light. If
HOLLIGHT_USE_MODULEis set to 1,makeinlines loads in hol_lib.ml and compiles into hol_lib.cmx and hol_lib.cmxa.The stack overflow error is a hurdle when compiling the code using
ocamlopt. To avoid this error,makeusesocamlopt.bytewhich is a bytecode version ofocamloptand distributed by the current OPAM switch. Combined withOCAMLRUNPARAM=l=<some large number>which sets the maximum stack size for OCaml bytecode runners, this successfully compiles hol_lib. However, it could not still compile a significantly large project such as Multivariate. One possible approach is to chop the inlined .ml file into multiple smaller .ml files and compile each of them, but this makes the inliner script complicated which could be a concern...This patch also adds unit_tests.ml, and when
HOLLIGHT_USE_MODULEis set, compiles it into a bytecode and native executable. It currently contains simple checks of the verbose quantifiers and constants, but it can contain more interesting sanity checks in the future.The CI check is also updated to make with
HOLLIGHT_USE_MODULEset to 1 and run the unit tests. OCaml 4.05 CI check had been broken, and this is fixed too.