From d7ef6f3f25d2f7c7c740bdeb5f89d651d4d79977 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 15 Apr 2024 17:56:07 +0200 Subject: [PATCH] update wrt master version of hol-light (#128) --- .github/workflows/main.yml | 4 +-- README.md | 4 +-- equal.ml | 2 +- main.ml | 21 ++++++++------- xci.ml | 55 ++++++++++++++++++++++++++++---------- 5 files changed, 57 insertions(+), 29 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f71eec5..f0e14e1 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/README.md b/README.md index 2c0f062..bc05ba3 100644 --- a/README.md +++ b/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 diff --git a/equal.ml b/equal.ml index 8b01d3b..8cf9b0e 100644 --- a/equal.ml +++ b/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 diff --git a/main.ml b/main.ml index d8bddfc..c2e55c7 100644 --- a/main.ml +++ b/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 = diff --git a/xci.ml b/xci.ml index 7345be4..dd07321 100644 --- a/xci.ml +++ b/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. *) (* ------------------------------------------------------------------------- *)