Add update_database for OCaml 5, fix a bug in search, add make switch-5

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

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)

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 \

update_database_4.14.ml → 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
 
 

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("<omit this pattern>",_),t) -> not o filterpred t
+    | Comb(Var("<match theorem name>",_),Var(pat,_)) -> name_contains pat
+    | Comb(Var("<match aconv>",_),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);;