diff --git a/Makefile b/Makefile index 0ca6150d..a5c05f86 100644 --- a/Makefile +++ b/Makefile @@ -59,12 +59,20 @@ switch:; \ opam install -y zarith ledit ; \ opam pin -y add camlp5 8.03.00 +switch-5:; \ + opam update ; \ + opam switch create . ocaml-base-compiler.5.2.0 ; \ + eval $(opam env) ; \ + opam install -y zarith ledit ; \ + opam pin -y add camlp5 8.03.00 + # Choose an appropriate "update_database.ml" file -update_database.ml:; if [ ${OCAML_VERSION} = "4.14" ] ; \ - then cp update_database_4.14.ml update_database.ml ; \ - else cp update_database_${OCAML_UNARY_VERSION}.ml update_database.ml ; \ - fi +update_database.ml:; \ + if [ ${OCAML_VERSION} = "4.14" ] ; \ + then cp update_database/update_database_4.14.ml update_database.ml ; \ + else cp update_database/update_database_${OCAML_UNARY_VERSION}.ml update_database.ml ; \ + fi # Build the camlp4 syntax extension file (camlp5 for OCaml >= 3.10) @@ -174,7 +182,7 @@ 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 +default: hol_lib.cma hol_lib.cmxa unit_tests.byte unit_tests.native endif # TODO: update this and hol.* commands to use one of checkpointing tools diff --git a/Mizarlight/make.ml b/Mizarlight/make.ml index b904ae0c..1e32f8d8 100644 --- a/Mizarlight/make.ml +++ b/Mizarlight/make.ml @@ -21,7 +21,7 @@ let e tac = Topdirs.dir_directory (!hol_dir);; -Topdirs.load_file Format.std_formatter +Toploop.load_file Format.std_formatter (Filename.concat (!hol_dir) "Mizarlight/pa_f.cmo");; List.iter (fun s -> Hashtbl.add (Pa_j.ht) s true) diff --git a/README b/README index 1fd2ef8f..d18342b1 100644 --- a/README +++ b/README @@ -27,7 +27,7 @@ Refer to the reference manual for more details of individual functions: The Objective CAML (OCaml) implementation is a prerequisite for running HOL Light. HOL Light should work with any recent version of OCaml; I've tried it on at least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2, -4.00, 4.05 and 4.14. +4.00, 4.05 and 4.14 and 5.2.0. 1. OCaml: there are packages for many Linux distributions. For example, on a debian derivative like Ubuntu, you may just need @@ -142,21 +142,18 @@ have installed. As of 2024, there are three programs you can use. HOL Light does not have convenient commands or scripts to exploit DMTCP, but you can proceed as follows: - 1. Start ocaml running under the DMTCP coordinator: + 1. Start hol.sh running under the DMTCP coordinator and wait until + HOL Light is loaded: - dmtcp_launch ocaml + dmtcp_launch ./hol.sh - 2. Use ocaml to load HOL Light as usual, for example: - - #use "hol.ml";; - - 3. From another terminal, issue the checkpoint command: + 2. From another terminal, issue the checkpoint command: dmtcp_command -kc - This will kill the ocaml process once checkpointing is done. + This will kill the process once checkpointing is done. - 4. Step 3 created a checkpoint of the OCaml process and + 3. Step 2 created a checkpoint of the OCaml process and a shell script to invoke it, both in the directory in which ocaml was started. Running that should restore the OCaml process with all your state and bindings: @@ -206,7 +203,7 @@ checkpointing programs. DEPENDENCIES 1. zarith or num: The HOL Light system uses the OCaml "Num" library - or "Zarith" library for rational arithmetic. If OCaml 4.14 is used, + or "Zarith" library for rational arithmetic. If OCaml 4.14 or above is used, HOL Light will use Zarith. You can install it using the OCaml package manager "opam" by @@ -234,8 +231,8 @@ checkpointing programs. 2. camlp5: this is needed to run HOL Light under any OCaml >= 3.10. Somtimes you need a recent version of camlp5 to be compatible with your OCaml. For example, OCaml 4.05 is compatible with camlp5 7.10 and - OCaml 4.14 is compatible with camlp5 8.02 and 8.03. I recommend downloading - the sources for a recent version from + OCaml 4.14 and above is compatible with camlp5 8.02 and 8.03. I recommend + downloading the sources for a recent version from https://github.com/camlp5/camlp5/releases ('tags' tab has full series) @@ -269,7 +266,7 @@ HOL Light will only work on OCaml 4.14 or above. 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. +ocamlopt and .cmo with .cmx. ocamlfind ocamlc -package zarith -linkpkg -pp "`./hol.sh -pp`" \ -I (HOL dir) (HOL dir)/bignum.cmo (HOL dir)/hol_loader.cmo \ diff --git a/update_database_3.ml b/update_database/update_database_3.ml similarity index 100% rename from update_database_3.ml rename to update_database/update_database_3.ml diff --git a/update_database_4.14.ml b/update_database/update_database_4.14.ml similarity index 90% rename from update_database_4.14.ml rename to update_database/update_database_4.14.ml index f84769b5..9a2cad91 100755 --- a/update_database_4.14.ml +++ b/update_database/update_database_4.14.ml @@ -26,14 +26,16 @@ let rec get_simple_type = function (* Execute any OCaml expression given as a string. *) -let exec = ignore o Toploop.execute_phrase false Format.std_formatter - o !Toploop.parse_toplevel_phrase o Lexing.from_string +let exec s = (ignore o Toploop.execute_phrase false Format.std_formatter + o !Toploop.parse_toplevel_phrase o Lexing.from_string) s (* Evaluate any OCaml expression given as a string. *) let eval n = - exec ("let buf__ = ( " ^ n ^ " );;"); - Obj.magic (Toploop.getvalue "buf__") + if String.contains n '.' then begin + exec ("let buf__ = ( " ^ n ^ " );;"); + Obj.magic (Toploop.getvalue "buf__") + end else Obj.magic (Toploop.getvalue n) (* Register all theorems added since the last update. *) end @@ -75,10 +77,13 @@ let string_of_longident lid = String.concat "." (Longident.flatten lid) let all_theorems () = - enum1 None [] - |> List.map (fun lid -> - let s = string_of_longident lid in - (s, (Ocaml_typing.eval s : thm))) + let _ = Ocaml_typing.exec ("unset_jrh_lexer;;") in + let res = enum1 None [] + |> List.map (fun lid -> + let s = string_of_longident lid in + (s, (Ocaml_typing.eval s : thm))) in + let _ = Ocaml_typing.exec ("set_jrh_lexer;;") in + res end diff --git a/update_database_4.ml b/update_database/update_database_4.ml similarity index 100% rename from update_database_4.ml rename to update_database/update_database_4.ml diff --git a/update_database/update_database_5.ml b/update_database/update_database_5.ml new file mode 100755 index 00000000..9a2cad91 --- /dev/null +++ b/update_database/update_database_5.ml @@ -0,0 +1,152 @@ +(* ========================================================================= *) +(* Create search database from OCaml / modify search database dynamically. *) +(* *) +(* This file assigns to "theorems", which is a list of name-theorem pairs. *) +(* The core system already has such a database set up. Use this file if you *) +(* want to update the database beyond the core, so you can search it. *) +(* *) +(* The trickery to get at the OCaml environment is due to Roland Zumkeller *) +(* and Michael Farber. It works by copying some internal data structures and *) +(* casting into the copy using Obj.magic. *) +(* ========================================================================= *) + +module Ocaml_typing = struct + +open Types + +(* If the given type is simple return its name, otherwise None. *) + +let rec get_simple_type = function + | Tlink texpr -> + (match get_desc texpr with + | Tconstr (Pident p,[],_) -> Some (Ident.name p) + | d -> get_simple_type d) + | Tconstr (Path.Pident p, [], _) -> Some (Ident.name p) + | _ -> None;; + +(* Execute any OCaml expression given as a string. *) + +let exec s = (ignore o Toploop.execute_phrase false Format.std_formatter + o !Toploop.parse_toplevel_phrase o Lexing.from_string) s + +(* Evaluate any OCaml expression given as a string. *) + +let eval n = + if String.contains n '.' then begin + exec ("let buf__ = ( " ^ n ^ " );;"); + Obj.magic (Toploop.getvalue "buf__") + end else Obj.magic (Toploop.getvalue n) + +(* Register all theorems added since the last update. *) +end + +module Lookuptheorems = struct +open Types + +let lid_cons lidopt id = + match lidopt with + None -> Longident.Lident id + | Some li -> Longident.Ldot(li, id) + +let it_val_1 lidopt s p vd acc = + if (Some "thm") = Ocaml_typing.get_simple_type (get_desc vd.Types.val_type) then + (lid_cons lidopt s)::acc else acc + +let it_mod_1 lidopt s p md acc = (lid_cons lidopt s)::acc + +let enum0 lidopt = + try + let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in + let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in + (vl, ml) + with Not_found -> + (* Looking for (Longident.Lident "Stream") raises Not_found. + Stream is a deprecated alias module of "Stdlib.Stream", and the camlp-streams + package that is used by pa_hol_syntax redefines Stream, which seems to + confuse Env.fold_values and Env.fold_modules. *) + ([], []) + +let rec enum1 lidopt acc = + match enum0 lidopt with + (vl, []) -> vl@acc + | (vl, ml) -> + List.fold_left (fun acc mlid -> + enum1 (Some mlid) acc) (vl@acc) ml + +let string_of_longident lid = + String.concat "." (Longident.flatten lid) + +let all_theorems () = + let _ = Ocaml_typing.exec ("unset_jrh_lexer;;") in + let res = enum1 None [] + |> List.map (fun lid -> + let s = string_of_longident lid in + (s, (Ocaml_typing.eval s : thm))) in + let _ = Ocaml_typing.exec ("set_jrh_lexer;;") in + res +end + + +let update_database () = + theorems := Lookuptheorems.all_theorems() + +(* ------------------------------------------------------------------------- *) +(* Put an assignment of a theorem database in the named file. *) +(* ------------------------------------------------------------------------- *) + +let make_database_assignment filename = + update_database(); + (let allnames = uniq(sort (<) (map fst (!theorems))) in + let names = subtract allnames ["it"] in + let entries = map (fun n -> "\""^n^"\","^n) names in + let text = "needs \"help.ml\";;\n\n"^ + "theorems :=\n[\n"^ + end_itlist (fun a b -> a^";\n"^b) entries^"\n];;\n" in + file_of_string filename text);; + +(* ------------------------------------------------------------------------- *) +(* Search (automatically updates) *) +(* ------------------------------------------------------------------------- *) + +let search = + let rec immediatesublist l1 l2 = + match (l1,l2) with + [],_ -> true + | _,[] -> false + | (h1::t1,h2::t2) -> h1 = h2 && immediatesublist t1 t2 in + let rec sublist l1 l2 = + match (l1,l2) with + [],_ -> true + | _,[] -> false + | (h1::t1,h2::t2) -> immediatesublist l1 l2 || sublist l1 t2 in + let exists_subterm_satisfying p (n,th) = can (find_term p) (concl th) + and name_contains s (n,th) = sublist (explode s) (explode n) in + let rec filterpred tm = + match tm with + Comb(Var("",_),t) -> not o filterpred t + | Comb(Var("",_),Var(pat,_)) -> name_contains pat + | Comb(Var("",_),pat) -> exists_subterm_satisfying (aconv pat) + | pat -> exists_subterm_satisfying (can (term_match [] pat)) in + fun pats -> + update_database(); + let triv,nontriv = partition is_var pats in + (if triv <> [] then + warn true + ("Ignoring plain variables in search: "^ + end_itlist (fun s t -> s^", "^t) (map (fst o dest_var) triv)) + else ()); + (if nontriv = [] && triv <> [] then [] + else sort (increasing fst) + (itlist (filter o filterpred) pats (!theorems)));; + +(* ------------------------------------------------------------------------- *) +(* Update to bring things back to current state. *) +(* ------------------------------------------------------------------------- *) + +update_database();; + +(* This printf checks whether standard modules like Printf are still alive + after update_database. + See also: https://github.com/ocaml/ocaml/issues/12271 *) +Printf.printf "update_database.ml loaded! # theorems: %d\n" + (List.length !theorems);; diff --git a/update_database_5.ml b/update_database_5.ml deleted file mode 100755 index 14b99128..00000000 --- a/update_database_5.ml +++ /dev/null @@ -1,21 +0,0 @@ -(* ========================================================================= *) -(* Create search database from OCaml / modify search database dynamically. *) -(* *) -(* This file assigns to "theorems", which is a list of name-theorem pairs. *) -(* The core system already has such a database set up. Use this file if you *) -(* want to update the database beyond the core, so you can search it. *) -(* *) -(* The trickery to get at the OCaml environment is due to Roland Zumkeller *) -(* and Michael Farber. It works by copying some internal data structures and *) -(* casting into the copy using Obj.magic. *) -(* ========================================================================= *) - -Format.print_string - ("**** WARNING: Dynamic updating does not yet work in OCaml version 5.xx\n" ^ - "**** FOR NOW update_database() HAS NO EFFECT ***\n");; - -let update_database() = - Format.print_string("*** NOT YET SUPPORTED IN Ocaml >= 5\n");; - -let make_database_assignment (s:string) = - Format.print_string("*** NOT YET SUPPORTED IN Ocaml >= 5\n");;