Support native compilation of HOL Light, add unit tests #114
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
aqjune
force-pushed
the
nativecomp
branch
4 times, most recently
from
bea0979
to
a19eac8
Compare
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.