Support native compilation of HOL Light, add unit tests

.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

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

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