From 074eec3d79cf6cb1a1d0f5d16962084aabb7ee85 Mon Sep 17 00:00:00 2001 From: Juneyoung Lee Date: Mon, 2 Sep 2024 22:16:15 -0500 Subject: [PATCH] Support compilation of HOL Light This patch supports compilation of HOL Light. If the `HOLLIGHT_USE_MODULE` environment variable is set to 1, Makefile builds `hol_lib.cmo` and makes `hol.sh` to use it. It first generates `hol_lib_inlined.ml` which is the output of the new `inline_load.ml` script which inlines all `loads`/`loadt`/`needs` invocations of the input file. Then, it compiles the inlined file with ocmal compiler. 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 an OCaml program that receives an HOL Light proof and replaces the loads/loadt/needs function invocations with their actual contents. The README file newly explains that this flag should be turned of only if having this additional trusted base is considered okay. --- .gitignore | 2 ++ Makefile | 53 +++++++++++++++++++++------- README | 26 ++++++++++++++ hol.ml | 13 +++++-- hol_4.14.sh | 1 + hol_4.sh | 1 + hol_lib.ml | 1 + hol_lib_use_module.ml | 15 ++++++++ inline_load.ml | 82 +++++++++++++++++++++++++++++++++++++++++++ 9 files changed, 180 insertions(+), 14 deletions(-) create mode 100644 hol_lib_use_module.ml create mode 100644 inline_load.ml diff --git a/.gitignore b/.gitignore index 8d13c150..f2dceb5a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,7 @@ .DS_Store .vscode _opam +*.cma *.cmi *.cmo *.o @@ -9,3 +10,4 @@ pa_j.ml update_database.ml ocaml-hol hol.sh +hol_lib_inlined.ml diff --git a/Makefile b/Makefile index adcfa0f9..4ed12e4a 100644 --- a/Makefile +++ b/Makefile @@ -35,6 +35,15 @@ CAMLP5_BINARY_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1-4` CAMLP5_UNARY_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -c1` CAMLP5_VERSION=`camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -f1 -d'-' | cut -c1-6` +# 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 +# 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. + +HOLLIGHT_USE_MODULE?=0 + # Main target default: update_database.ml pa_j.cmo hol.sh; @@ -106,19 +115,35 @@ bignum.cmo: bignum_zarith.ml bignum_num.ml ; \ else ocamlc -c -o bignum.cmo 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 ; \ + ocamlfind ocamlc -package zarith -linkpkg -a -o hol_lib.cma bignum.cmo hol_loader.cmo hol_lib.cmo + # Create a bash script 'hol.sh' that loads 'hol.ml' in OCaml REPL. -hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo update_database.ml ; \ - if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ - if [ ${OCAML_UNARY_VERSION} = "5" ] || [ ${OCAML_VERSION} = "4.14" ] ; \ - then ocamlfind ocamlmktop -package zarith -o ocaml-hol zarith.cma bignum.cmo ; \ - sed "s^__DIR__^`pwd`^g" hol_4.14.sh > hol.sh ; \ - else ocamlmktop -o ocaml-hol nums.cma bignum.cmo ; sed "s^__DIR__^`pwd`^g" hol_4.sh > hol.sh ; \ - fi ; \ - chmod +x hol.sh ; \ - else \ - echo 'FAILURE: hol.sh assumes Linux' ; \ - fi +hol.sh: pa_j.cmo ${HOLSRC} bignum.cmo hol_loader.cmo update_database.ml + if [ `uname` = "Linux" ] || [ `uname` = "Darwin" ] ; then \ + if [ ${OCAML_UNARY_VERSION} = "5" ] || [ ${OCAML_VERSION} = "4.14" ] ; then \ + ocamlfind ocamlmktop -package zarith -o ocaml-hol zarith.cma bignum.cmo hol_loader.cmo ; \ + sed "s^__DIR__^`pwd`^g; s^__USE_MODULE__^$(HOLLIGHT_USE_MODULE)^g" hol_4.14.sh > hol.sh ; \ + else \ + ocamlmktop -o ocaml-hol nums.cma bignum.cmo hol_loader.cmo ; \ + sed "s^__DIR__^`pwd`^g; s^__USE_MODULE__^$(HOLLIGHT_USE_MODULE)^g" hol_4.sh > hol.sh ; \ + fi ; \ + chmod +x hol.sh ; \ + else \ + echo 'FAILURE: hol.sh assumes Linux' ; \ + fi + +# If HOLLIGHT_USE_MODULE is set, add hol_lib.cmo to dependency of hol.sh + +ifeq ($(HOLLIGHT_USE_MODULE),1) +hol.sh: hol_lib.cmo +endif # TODO: update this and hol.* commands to use one of checkpointing tools # other than ckpt. @@ -179,4 +204,8 @@ 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 ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex; +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 \ + ocaml-hol hol.sh hol hol.multivariate hol.sosa hol.card hol.complex diff --git a/README b/README index 84bd5569..83aabdb2 100644 --- a/README +++ b/README @@ -258,6 +258,32 @@ checkpointing programs. However, you may get a version in "transitional" instead of "strict" mode (do "camlp5 -pmode" to check which you have). + * * * * * * * * + + 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. + +To compile an OCaml file that opens Hol_lib, use the following command. + + ocamlfind ocamlc -package zarith -linkpkg -pp \ + "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo -I . (HOL dir)pa_j.cmo" \ + -I (HOL dir) (HOL dir)/bignum.cmo (HOL dir)/hol_loader.cmo \ + (HOL dir)/hol_lib.cmo (input.ml) -o (output.ml) + +The load functions (loads/loadt/needs) are not available anymore in this +approach. Please use 'ocaml inline_loads.ml ' to inline +their invocations. + +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 +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. + * * * * * * * * [*] HOL Light uses the OCaml 'num' library for multiple-precision diff --git a/hol.ml b/hol.ml index df1c9e2d..15e68063 100644 --- a/hol.ml +++ b/hol.ml @@ -21,7 +21,12 @@ let hol_version = "2.20++";; let temp_path = ref "/tmp";; -#use "hol_loader.ml";; +(* ------------------------------------------------------------------------- *) +(* Load the load/need functions. *) +(* ------------------------------------------------------------------------- *) + +#load "hol_loader.cmo";; +include Hol_loader;; file_loader := fun s -> Toploop.use_file Format.std_formatter s;; (* Hide the definition of file_loader of hol_loader.ml. *) @@ -50,7 +55,11 @@ Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");; (* Load the core files. *) (* ------------------------------------------------------------------------- *) -loads "hol_lib.ml";; +let use_module = + try Sys.getenv "HOLLIGHT_USE_MODULE" = "1" with Not_found -> false;; +if use_module +then loads "hol_lib_use_module.ml" +else loads "hol_lib.ml";; (* ------------------------------------------------------------------------- *) (* Install printers. *) diff --git a/hol_4.14.sh b/hol_4.14.sh index c81fb3e6..a24eb721 100755 --- a/hol_4.14.sh +++ b/hol_4.14.sh @@ -9,6 +9,7 @@ fi # Makefile will replace __DIR__ with the path export HOLLIGHT_DIR=__DIR__ +export HOLLIGHT_USE_MODULE=__USE_MODULE__ # If a local OPAM is installed, use it if [ -d "${HOLLIGHT_DIR}/_opam" ]; then diff --git a/hol_4.sh b/hol_4.sh index ef8dec4c..a05210fd 100755 --- a/hol_4.sh +++ b/hol_4.sh @@ -9,6 +9,7 @@ fi # Makefile will replace __DIR__ with the path export HOLLIGHT_DIR=__DIR__ +export HOLLIGHT_USE_MODULE=__USE_MODULE__ # If a local OPAM is installed, use it if [ -d "${HOLLIGHT_DIR}/_opam" ]; then diff --git a/hol_lib.ml b/hol_lib.ml index 6a056963..10f24525 100644 --- a/hol_lib.ml +++ b/hol_lib.ml @@ -11,6 +11,7 @@ (* ========================================================================= *) include Bignum;; +open Hol_loader;; (* ------------------------------------------------------------------------- *) (* Bind these to names that are independent of OCaml versions before they *) diff --git a/hol_lib_use_module.ml b/hol_lib_use_module.ml new file mode 100644 index 00000000..c1af2d4a --- /dev/null +++ b/hol_lib_use_module.ml @@ -0,0 +1,15 @@ +(* ========================================================================= *) +(* HOL LIGHT *) +(* *) +(* Modern OCaml version of the HOL theorem prover *) +(* *) +(* John Harrison *) +(* *) +(* (c) Copyright, University of Cambridge 1998 *) +(* (c) Copyright, John Harrison 1998-2024 *) +(* (c) Copyright, Juneyoung Lee 2024 *) +(* ========================================================================= *) + +Topdirs.dir_load Format.std_formatter + (Filename.concat (!hol_dir) "hol_lib.cmo");; +include Hol_lib;; \ No newline at end of file diff --git a/inline_load.ml b/inline_load.ml new file mode 100644 index 00000000..7298c7d9 --- /dev/null +++ b/inline_load.ml @@ -0,0 +1,82 @@ +(* ========================================================================= *) +(* HOL LIGHT *) +(* *) +(* Modern OCaml version of the HOL theorem prover *) +(* *) +(* John Harrison *) +(* *) +(* (c) Copyright, University of Cambridge 1998 *) +(* (c) Copyright, John Harrison 1998-2024 *) +(* (c) Copyright, Juneyoung Lee 2024 *) +(* ========================================================================= *) + +if Array.length Sys.argv <> 3 then + let _ = Printf.eprintf "inline_load.ml \n" in + exit 1;; + +let filename = Sys.argv.(1);; +let fout = open_out (Sys.argv.(2));; + +#use "hol_loader.ml";; + +let parse_load_statement fnname stmt: (string * string) option = + let stmt = String.trim stmt in + if not (String.starts_with ~prefix:fnname stmt) then None else + let n = String.length fnname in + let stmt = String.trim (String.sub stmt n (String.length stmt - n)) in + if not (stmt.[0] = '"') then None else + let stmt = String.sub stmt 1 (String.length stmt - 1) in + let idx = String.index stmt '"' in + if idx = -1 then None else + let path = String.sub stmt 0 idx in + let stmt = String.sub stmt (idx + 1) (String.length stmt - idx - 1) in + let stmt = String.trim stmt in + if not (String.starts_with ~prefix:";;" stmt) then None else + let stmt = String.sub stmt 2 (String.length stmt - 2) in + Some (path,stmt);; + + +let strings_of_file filename = + let fd = + try open_in filename + with Sys_error _ -> failwith("strings_of_file: can't open "^filename) in + let rec suck_lines acc = + let l = try [input_line fd] with End_of_file -> [] in + if l = [] then List.rev acc else suck_lines(List.hd l::acc) in + let data = suck_lines [] in + (close_in fd; data);; + +file_loader := fun filename -> + let open Printf in + fprintf fout "(* %s *)\n" filename; + let lines = strings_of_file filename in + List.iter + (fun line -> + match parse_load_statement "loadt" line with + | Some (path,line') -> 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 -> + (match parse_load_statement "needs" line with + | Some (path,line') -> needs path; fprintf fout "%s\n" line' + | None -> fprintf fout "%s\n" line (* no linebreak needed! *)))) + lines; + (* add digest *) + let digest_str = Digest.file filename in + let digest = Bytes.of_string digest_str in + let the_str = ref "" in + Bytes.iter (fun c -> + let i = Char.code c in + if !the_str = "" + then the_str := string_of_int i + else the_str := !the_str ^ "; " ^ (string_of_int i)) + digest; + fprintf fout "(* update digest *)\n"; + fprintf fout "loaded_files := \n"; + fprintf fout " let digest_bytes = [|%s|] in\n" !the_str; + fprintf fout " let digest = Bytes.init (Array.length digest_bytes) (fun i -> Char.chr digest_bytes.(i)) in\n"; + fprintf fout " (\"%s\", Bytes.to_string digest)::!loaded_files;;\n\n" (Filename.basename filename); + true;; + +loadt filename;; + +close_out fout;;