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=<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.

.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 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 | tee log.txt
           ! grep "Error" log.txt
+          grep "Camlp5 parsing version (HOL-Light)" log.txt
+          ./unit_tests.byte
+          ./unit_tests.native

.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

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
@@ -207,5 +239,7 @@ install: hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; cp hol hol.m
 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 \
+        hol_lib.cmx hol_lib.cmxa \
+        hol_loader.cmo hol_loader.cmi \
+        hol_loader.cmx bignum.cmx \
         ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex

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 <input.ml> <output.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

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.

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.

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 <input.ml> <output.ml>\n" in
+let argn = Array.length Sys.argv;;
+
+if argn < 3 || argn > 4 then
+  let _ = Printf.eprintf "inline_load.ml <input.ml> <output.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 *)

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`);;