From f566904ade2b086da8fccc06287eebef48bd8440 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Tue, 8 Oct 2024 20:56:35 +0000 Subject: [PATCH] Support native compilation of HOL Light, add unit tests 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=` 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. --- .github/workflows/main.yml | 26 ++++++++++++++++---- .gitignore | 5 ++++ Makefile | 50 ++++++++++++++++++++++++++++++++------ README | 18 ++++++++------ hol_4.14.sh | 5 ++++ hol_4.sh | 5 ++++ inline_load.ml | 28 +++++++++++++++++---- unit_tests.ml | 13 ++++++++++ 8 files changed, 125 insertions(+), 25 deletions(-) create mode 100644 unit_tests.ml diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 603ebfe2..f7e4db4b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -18,14 +18,14 @@ jobs: test1: runs-on: ubuntu-22.04 name: OCaml 4.05, Camlp5 7.10 - + steps: - name: Install dependency run: | sudo apt update && sudo apt install -y opam opam init --disable-sandboxing --compiler=4.05.0 opam pin -y add camlp5 7.10 - opam install -y num + opam install -y num ledit - name: Checkout this repo uses: actions/checkout@v2 @@ -37,13 +37,14 @@ jobs: cd hol-light eval $(opam env) make - ./hol.sh | tee log.txt + ./hol.sh 2>&1 | tee log.txt ! grep "Error" log.txt + grep "Camlp5 parsing version" log.txt test2: runs-on: ubuntu-22.04 name: OCaml 4.14, Camlp5 8.03 (make switch) - + steps: - name: Install dependency run: | @@ -61,5 +62,20 @@ jobs: make switch eval $(opam env) make - ./hol.sh | tee log.txt + ./hol.sh 2>&1 | tee log.txt + ! grep "Error" log.txt + grep "Camlp5 parsing version (HOL-Light)" log.txt + cd .. + + - name: Run (HOLLIGHT_USE_MODULE=1) + run: | + cd hol-light + eval $(opam env) + make clean + export HOLLIGHT_USE_MODULE=1 + make + ./hol.sh 2>&1 | tee log.txt ! grep "Error" log.txt + grep "Camlp5 parsing version (HOL-Light)" log.txt + ./unit_tests.byte + ./unit_tests.native diff --git a/.gitignore b/.gitignore index f2dceb5a..c453df60 100644 --- a/.gitignore +++ b/.gitignore @@ -1,13 +1,18 @@ .DS_Store .vscode _opam +*.a *.cma *.cmi *.cmo *.o *.cmx +*.cmxa pa_j.ml update_database.ml ocaml-hol hol.sh hol_lib_inlined.ml +unit_tests_inlined.ml +unit_tests.byte +unit_tests.native \ No newline at end of file diff --git a/Makefile b/Makefile index 4ed12e4a..0ca6150d 100644 --- a/Makefile +++ b/Makefile @@ -37,7 +37,7 @@ CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' # If set to 1, build hol_lib.cmo and make hol.sh to use it. # NOTE: This extends the trusted base of HOL Light to include the inliner -# script, inline_loads.ml. inline_loads.ml is an OCaml program that receives +# script, inline_load.ml. inline_load.ml is an OCaml program that receives # an HOL Light proof and replaces the loads/loadt/needs function invocations # with their actual contents. Please turn this flag on only if having this # additional trusted base is considered okay. @@ -53,7 +53,7 @@ default: update_database.ml pa_j.cmo hol.sh; # HOL Light. # ledit is installed for line editing of OCaml REPL switch:; \ - opam update ; \ + opam update ; \ opam switch create . ocaml-base-compiler.4.14.0 ; \ eval $(opam env) ; \ opam install -y zarith ledit ; \ @@ -115,14 +115,35 @@ bignum.cmo: bignum_zarith.ml bignum_num.ml ; \ else ocamlc -c -o bignum.cmo bignum_num.ml ; \ fi +bignum.cmx: bignum_zarith.ml bignum_num.ml ; \ + if test ${OCAML_VERSION} = "4.14" -o ${OCAML_UNARY_VERSION} = "5" ; \ + then ocamlfind ocamlopt -package zarith -c -o bignum.cmx bignum_zarith.ml ; \ + else ocamlopt -c -o bignum.cmx bignum_num.ml ; \ + fi + hol_loader.cmo: hol_loader.ml ; \ ocamlc -verbose -c hol_loader.ml -o hol_loader.cmo -hol_lib.cmo: inline_load.ml hol_lib.ml hol_loader.cmo ; \ - ocaml inline_load.ml hol_lib.ml hol_lib_inlined.ml ; \ - ocamlc -verbose -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" hol_loader.cmo hol_lib_inlined.ml bignum.cmo -o hol_lib.cmo ; \ +hol_loader.cmx: hol_loader.ml ; \ + ocamlopt -verbose -c hol_loader.ml -o hol_loader.cmx + +hol_lib_inlined.ml: hol_lib.ml inline_load.ml ; \ + HOLLIGHT_DIR="`pwd`" ocaml inline_load.ml hol_lib.ml hol_lib_inlined.ml -omit-prelude + +hol_lib.cmo: pa_j.cmo hol_lib_inlined.ml hol_loader.cmo bignum.cmo ; \ + ocamlc -verbose -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" hol_loader.cmo hol_lib_inlined.ml bignum.cmo -o hol_lib.cmo + +hol_lib.cma: hol_lib.cmo bignum.cmo hol_loader.cmo ; \ ocamlfind ocamlc -package zarith -linkpkg -a -o hol_lib.cma bignum.cmo hol_loader.cmo hol_lib.cmo +hol_lib.cmx: pa_j.cmo hol_lib_inlined.ml hol_loader.cmx bignum.cmx ; \ + OCAMLRUNPARAM=l=1000000000 ocamlopt.byte -verbose -c \ + -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . pa_j.cmo" \ + hol_lib_inlined.ml hol_loader.cmx bignum.cmx -o hol_lib.cmx + +hol_lib.cmxa: hol_lib.cmx hol_loader.cmx bignum.cmx ; \ + ocamlfind ocamlopt -package zarith -a -o hol_lib.cmxa bignum.cmx hol_loader.cmx hol_lib.cmx + # Create a bash script 'hol.sh' that loads 'hol.ml' in OCaml REPL. hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo hol_loader.cmo update_database.ml @@ -140,9 +161,20 @@ hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo hol_loader.cmo update_database.ml fi # If HOLLIGHT_USE_MODULE is set, add hol_lib.cmo to dependency of hol.sh +# Also, build unit_tests using OCaml bytecode compiler as well as OCaml native compiler. ifeq ($(HOLLIGHT_USE_MODULE),1) hol.sh: hol_lib.cmo +unit_tests_inlined.ml: unit_tests.ml inline_load.ml ; \ + HOLLIGHT_DIR="`pwd`" ocaml inline_load.ml unit_tests.ml unit_tests_inlined.ml +unit_tests.byte: unit_tests_inlined.ml hol_lib.cmo inline_load.ml hol.sh ; \ + ocamlfind ocamlc -package zarith -linkpkg -pp "`./hol.sh -pp`" \ + -I . bignum.cmo hol_loader.cmo hol_lib.cmo unit_tests_inlined.ml -o unit_tests.byte +unit_tests.native: unit_tests_inlined.ml hol_lib.cmx inline_load.ml hol.sh ; \ + ocamlfind ocamlopt -package zarith -linkpkg -pp "`./hol.sh -pp`" \ + -I . bignum.cmx hol_loader.cmx hol_lib.cmx unit_tests_inlined.ml -o unit_tests.native + +default: hol_lib.cma unit_tests.byte unit_tests.native endif # TODO: update this and hol.* commands to use one of checkpointing tools @@ -205,7 +237,9 @@ install: hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.m # Clean up all compiled files clean:; \ - rm -f bignum.cmo update_database.ml pa_j.ml pa_j.cmi pa_j.cmo \ - hol_lib.cmo hol_lib.cmi hol_lib.cma hol_lib_inlined.ml \ - hol_loader.cmo hol_loader.cmi \ + rm -f bignum.c* bignum.o \ + update_database.ml pa_j.ml pa_j.cmi pa_j.cmo \ + hol_lib.a hol_lib.c* hol_lib.o hol_lib_inlined.ml \ + hol_loader.c* hol_loader.o \ + unit_tests_inlined.* unit_tests.native unit_tests.byte \ ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex diff --git a/README b/README index 83aabdb2..1fd2ef8f 100644 --- a/README +++ b/README @@ -263,20 +263,24 @@ checkpointing programs. COMPILING HOL LIGHT Running 'HOLLIGHT_USE_MODULE=1 make' will compile hol_lib.ml and generate -hol_lib.cmo. This will also create hol.sh which will configure hol.ml to use -the compiled hol_lib.cmo. Compiling HOL Light will only work on OCaml 4.14 -or above. +hol_lib.cmo/hol_lib.cmx. This will also create hol.sh which will configure +hol.ml to use the compiled hol_lib.cmo (but not hol_lib.cmx). Compiling +HOL Light will only work on OCaml 4.14 or above. -To compile an OCaml file that opens Hol_lib, use the following command. +To compile an OCaml file that opens Hol_lib using OCaml bytecode compiler, +use the following command. For OCaml native compiler, replace ocamlc with +ocamlopt. - ocamlfind ocamlc -package zarith -linkpkg -pp \ - "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . (HOL dir)pa_j.cmo" \ + ocamlfind ocamlc -package zarith -linkpkg -pp "`./hol.sh -pp`" \ -I (HOL dir) (HOL dir)/bignum.cmo (HOL dir)/hol_loader.cmo \ - (HOL dir)/hol_lib.cmo (input.ml) -o (output.ml) + (HOL dir)/hol_lib.cmo (input.ml) -o (output) The load functions (loads/loadt/needs) are not available anymore in this approach. Please use 'ocaml inline_loads.ml ' to inline their invocations. +For native compilation, if it raises the stack overflow error, either (1) +try ocamlopt.byte with OCAMLRUNPARAM=l=(some large number), or (2) increase +the stack size using `ulimit`. NOTE: Compiling HOL Light with 'HOLLIGHT_USE_MODULE=1' extends the trusted base of HOL Light to include the inliner script, inline_loads.ml. inline_loads.ml is diff --git a/hol_4.14.sh b/hol_4.14.sh index a24eb721..c807ed5c 100755 --- a/hol_4.14.sh +++ b/hol_4.14.sh @@ -1,5 +1,10 @@ #!/bin/bash +if [ "$#" -eq 1 ] && [ "$1" == "-pp" ]; then + echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo" + exit 0 +fi + # The default ocaml REPL does not accept arrow keys. # Export LINE_EDITOR to a proper program to enable this before invoking this # script. If not set, ledit will be used. diff --git a/hol_4.sh b/hol_4.sh index a05210fd..3c8feb4a 100755 --- a/hol_4.sh +++ b/hol_4.sh @@ -1,5 +1,10 @@ #!/bin/bash +if [ "$#" -eq 1 ] && [ "$1" == "-pp" ]; then + echo "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I "__DIR__" pa_j.cmo" + exit 0 +fi + # The default ocaml REPL does not accept arrow keys. # Export LINE_EDITOR to a proper program to enable this before invoking this # script. If not set, ledit will be used. diff --git a/inline_load.ml b/inline_load.ml index 7298c7d9..734764d4 100644 --- a/inline_load.ml +++ b/inline_load.ml @@ -10,12 +10,24 @@ (* (c) Copyright, Juneyoung Lee 2024 *) (* ========================================================================= *) -if Array.length Sys.argv <> 3 then - let _ = Printf.eprintf "inline_load.ml \n" in +let argn = Array.length Sys.argv;; + +if argn < 3 || argn > 4 then + let _ = Printf.eprintf "inline_load.ml [-omit-prelude]\n" in + let _ = Printf.eprintf " -omit-prelude: omit 'open Hol_lib;;' and 'open Hol_loader;;'.\n" in exit 1;; +try + let v = Sys.getenv "HOLLIGHT_DIR" in + if v = "" then Printf.printf "Warning: HOLLIGHT_DIR is not set\n%!" +with Not_found -> Printf.printf "Warning: HOLLIGHT_DIR is not set\n%!";; + let filename = Sys.argv.(1);; let fout = open_out (Sys.argv.(2));; +let omit_prelude = argn >= 4 && Sys.argv.(3) = "-omit-prelude";; + +if not omit_prelude then + Printf.fprintf fout "open Hol_lib;;\nopen Hol_loader;;\n";; #use "hol_loader.ml";; @@ -50,14 +62,20 @@ file_loader := fun filename -> let open Printf in fprintf fout "(* %s *)\n" filename; let lines = strings_of_file filename in + let fail_if_nonexistent f x = try f x with _ -> failwith x in List.iter (fun line -> match parse_load_statement "loadt" line with - | Some (path,line') -> loadt path; fprintf fout "%s\n" line' | None -> + | Some (path,line') -> fail_if_nonexistent loadt path; fprintf fout "%s\n" line' | None -> (match parse_load_statement "loads" line with - | Some (path,line') -> loads path; fprintf fout "%s\n" line' | None -> + | Some (path,line') -> begin + if path = "update_database.ml" + then Printf.printf "Warning: 'loads \"update_database.ml\";;' is omitted\n" + else (fail_if_nonexistent loads path; fprintf fout "%s\n" line') + end + | None -> (match parse_load_statement "needs" line with - | Some (path,line') -> needs path; fprintf fout "%s\n" line' + | Some (path,line') -> fail_if_nonexistent needs path; fprintf fout "%s\n" line' | None -> fprintf fout "%s\n" line (* no linebreak needed! *)))) lines; (* add digest *) diff --git a/unit_tests.ml b/unit_tests.ml new file mode 100644 index 00000000..0a87a30e --- /dev/null +++ b/unit_tests.ml @@ -0,0 +1,13 @@ +(* ========================================================================= *) +(* HOL LIGHT unit tests *) +(* ========================================================================= *) + +(* ------------------------------------------------------------------------- *) +(* Test verbose descriptive names for quantifiers/logical consts. *) +(* ------------------------------------------------------------------------- *) + +assert (`T` = `true`);; +assert (`F` = `false`);; +assert (`!(x:A). P x` = `forall (x:A). P x`);; +assert (`?(x:A). P x` = `exists (x:A). P x`);; +assert (`?!(x:A). P x` = `existsunique (x:A). P x`);;