diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 603ebfe2..cd611d6e 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 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 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..5b97a4fa 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 @@ -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 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`);;