update wrt master version of hol-light (#128)

.github/workflows/main.yml

@@ -32,7 +32,7 @@ jobs:
       - name: Install hol-light dependencies, dedukti
         run: |
           sudo apt-get install -y libipc-system-simple-perl libstring-shellquote-perl
-          opam install -y camlp5.${{ matrix.camlp5-version }} num ocamlfind dedukti.${{ matrix.dedukti-version }} #lambdapi.${{ matrix.lambdapi-version }}
+          opam install -y camlp5.${{ matrix.camlp5-version }} zarith ocamlfind dedukti.${{ matrix.dedukti-version }} #lambdapi.${{ matrix.lambdapi-version }}
       - name: Install lambdapi
         run: |
           git clone --depth 1 -b ${{ matrix.lambdapi-version }} https://github.com/Deducteam/lambdapi
@@ -46,7 +46,7 @@ jobs:
           export HOLLIGHT_DIR=`pwd`/hol-light
           git clone https://github.com/jrh13/hol-light
           cd hol-light
-          git checkout c153f40da8deb3bcc7aaef39126ad15e4713e68c
+          git checkout
           make
           hol2dk patch
       - name: Dump proofs

README.md

@@ -67,7 +67,7 @@ Installing HOL-Light sources
 ----------------------------
 
 **Requirements:**
-- hol-light >= af186e9f3c685f5acab16097b05717c10ebb030d (28/01/23) <= c153f40da8deb3bcc7aaef39126ad15e4713e68c (20/03/24)
+- hol-light >= bfb2ea95cf4b20f40136d5f08102875400c8cba7 (04/04/24)
 - libipc-system-simple-perl
 - libstring-shellquote
 - ocaml 4.14.1
@@ -419,7 +419,7 @@ On a machine with 32 processors i9-13950HX and 64G RAM:
 
 | HOL-Light file       | dump-simp | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo |
 |----------------------|-----------|-----------|-------------|-------------|--------------|-------------|--------------|--------------|
-| hol.ml               | 2m36s     | 3 Go      | 8 M         | 5679        | 36s          | 25s         | 0.4 Go       | 16m22s       |
+| hol.ml               | 3m57s     | 3 Go      | 8 M         | 5679        | 36s          | 25s         | 0.4 Go       | 16m22s       |
 | Multivariate/make.ml | 1h55m     | 52 Go     | 89 M        | 18866       | 18m11s       | 18m43s      | 2.3 Go       | 8h (*)       |
 
 (*) make -j32 vo; make -j8 vo

equal.ml

@@ -247,7 +247,7 @@ let (ONCE_DEPTH_CONV: conv->conv),
 
 let rec DEPTH_BINOP_CONV op conv tm =
   match tm with
-    Comb(Comb(op',l),r) when Pervasives.compare op' op = 0 ->
+    Comb(Comb(op',l),r) when Stdlib.compare op' op = 0 ->
       let l,r = dest_binop op tm in
       let lth = DEPTH_BINOP_CONV op conv l
       and rth = DEPTH_BINOP_CONV op conv r in

main.ml

@@ -8,7 +8,7 @@ open Xfiles
 open Xnames
 
 let usage() =
-  log
+  print_string
 "hol2dk uses
 ------------
 
@@ -160,13 +160,13 @@ hol2dk name upto file.(ml|hl)
 hol2dk name
   print on stdout the named theorems proved in all HOL-Light files
   in the working directory and all its subdirectories recursively
-%!"
+"
 
 let is_dk f =
   match Filename.extension f with
   | ".dk"  -> true
   | ".lp" -> false
-  | _ -> err "\"%s\" does not end with \".dk\" or \".lp\"\n%!" f; exit 1
+  | _ -> err "\"%s\" does not end with \".dk\" or \".lp\"\n" f; exit 1
 ;;
 
 let read_sig b =
@@ -186,7 +186,7 @@ let read_sig b =
 let integer s =
   try int_of_string s
   with Failure _ ->
-    Printf.eprintf "\"%s\" is not a valid integer\n%!" s; exit 1
+    Printf.eprintf "\"%s\" is not a valid integer\n" s; exit 1
 ;;
 
 (* [make nb_proofs dg b] generates a makefile for translating the
@@ -322,15 +322,15 @@ let range args =
   | [] -> All
   | [x] ->
      let x = integer x in
-     if x < 0 then (err "%d is negative\n%!" x; exit 1);
+     if x < 0 then (err "%d is negative\n" x; exit 1);
      Only x
   | [x;y] ->
      let x = integer x in
-     if x < 0 then (err "%d is negative\n%!" x; exit 1);
+     if x < 0 then (err "%d is negative\n" x; exit 1);
      let y = integer y in
-     if y < x then (err "%d is smaller than %d\n%!" y x; exit 1);
+     if y < x then (err "%d is smaller than %d\n" y x; exit 1);
      if x=0 then Upto y else Inter(x,y)
-  | _ -> (err "too many arguments\n%!"; exit 1)
+  | _ -> (err "too many arguments\n"; exit 1)
 ;;
 
 let dump after_hol f b =
@@ -366,7 +366,7 @@ dump_map_thid_name "%s.thm" %a;;
 let basename_ml f =
   match Filename.extension f with
   | ".ml" | ".hl" -> Filename.chop_extension f
-  | _ -> err "\"%s\" does not end with \".ml\" or \".hl\"\n%!" f; exit 1
+  | _ -> err "\"%s\" does not end with \".ml\" or \".hl\"\n" f; exit 1
 ;;
 
 let print_hstats() =
@@ -401,7 +401,8 @@ let wrong_nb_args() = err "wrong number of arguments\n"; 1;;
 let rec log_command l =
   print_string "\nhol2dk";
   List.iter (fun s -> print_char ' '; print_string s) l;
-  print_string " ...\n%!";
+  print_string " ...\n";
+  flush stdout;
   command l
 
 and dump_and_simp after_hol f =

xci.ml

@@ -1,4 +1,3 @@
-(* Truncated version of hol.ml used for testing. *)
 (* ========================================================================= *)
 (*                               HOL LIGHT                                   *)
 (*                                                                           *)
@@ -25,27 +24,24 @@ let hol_dir = ref
 
 let temp_path = ref "/tmp";;
 
-(* ------------------------------------------------------------------------- *)
-(* Load in parsing extensions.                                               *)
-(* For Ocaml < 3.10, use the built-in camlp4                                 *)
-(* and for Ocaml >= 3.10, use camlp5 instead.                                *)
-(* ------------------------------------------------------------------------- *)
-
-if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
-then (Topdirs.dir_directory "+camlp5";
-      Topdirs.dir_load Format.std_formatter "camlp5o.cma")
-else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
-
-Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
-
 (* ------------------------------------------------------------------------- *)
 (* Load files from system and/or user-settable directories.                  *)
 (* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual  *)
 (* $ character at the start of a directory.                                  *)
 (* ------------------------------------------------------------------------- *)
 
+(* A flag that sets whether use_file must raise Failure if loading the file  *)
+(* did not succeed. If set to true, this helps (nested) loading of files fail*)
+(* early. However, propagation of the failure will cause Toplevel to forget  *)
+(* bindings ('let .. = ..;;') that have been made before the erroneous       *)
+(* statement in the file. This leads to an inconsistent state between        *)
+(* variable and defined constants in HOL Light.                              *)
+let use_file_raise_failure = ref false;;
+
 let use_file s =
   if Toploop.use_file Format.std_formatter s then ()
+  else if !use_file_raise_failure
+  then failwith("Error in included file "^s)
   else (Format.print_string("Error in included file "^s);
         Format.print_newline());;
 
@@ -83,6 +79,37 @@ let needs s =
   if List.mem fileid (!loaded_files)
   then Format.print_string("File \""^s^"\" already loaded\n") else loadt s;;
 
+(* ------------------------------------------------------------------------- *)
+(* Load in parsing extensions.                                               *)
+(* For Ocaml < 3.10, use the built-in camlp4                                 *)
+(* and for Ocaml >= 3.10, use camlp5 instead.                                *)
+(* For Ocaml >= 4.14, use ocamlfind to locate camlp5.                        *)
+(* ------------------------------------------------------------------------- *)
+
+let ocaml_version = String.sub Sys.ocaml_version 0 4;;
+let version_ge_3_10 = ocaml_version >= "3.10";;
+let version_ge_4_14 = ocaml_version >= "4.14";;
+
+if version_ge_4_14
+then loads "load_camlp5_topfind.ml"
+else if version_ge_3_10
+then loads "load_camlp5.ml"
+else loads "load_camlp4.ml";;
+
+Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir) "pa_j.cmo");;
+
+if version_ge_4_14
+then loads "bignum_zarith.ml"
+else loads "bignum_num.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Bind this to a name that is independent of OCaml versions before it       *)
+(* is potentially overwritten by a theorem of the same name. On older        *)
+(* OCaml versions it is "Pervasives.sqrt", and on newer ones "Float.sqrt".   *)
+(* ------------------------------------------------------------------------- *)
+
+let float_sqrt = sqrt;;
+
 (* ------------------------------------------------------------------------- *)
 (* Various tweaks to OCaml and general library functions.                    *)
 (* ------------------------------------------------------------------------- *)