diff --git a/README.md b/README.md index 6025aa0..50e296d 100644 --- a/README.md +++ b/README.md @@ -246,22 +246,22 @@ Remark: for the checking of generated Coq files to not fail because of lack of R Performance with the mapping of real numbers (master branch) ------------------------------------------------------------ -On a machine with 32 processors i9-13950HX and 64G RAM, with OCaml 5.2.1, Camlp5 8.02.01, Coq 8.20.0, or (1) OCaml 4.14.2, Camlp5 8.02.01: +On a machine with 32 processors i9-13950HX and 64G RAM with HOL-Light ea45176, Hol2dk master, OCaml 4.14.2, Camlp5 8.02.01, Lambdapi c24b28e2 and Coq 8.20.0: -| HOL-Light file | dump-simp(1) | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo | -|----------------|--------------|-----------|-------------|-------------|--------------|-------------|--------------|--------------| -| hol.ml | 3m57s | 3 Gb | 5 M | 5682 | 39s | 1m29s | 1 Gb | 50m13s | +| HOL-Light file | dump | size | steps | thms | lp | v | size | vo | +|----------------|-------|------|-------|------|-----|-----|------|--------| +| hol.ml | 3m57s | 3 Gb | 3 M | 5687 | 39s | 37s | 1 Gb | 56m23s | Performance without the mapping of real numbers (hol2dk 2.0) ------------------------------------------------------------ -On a machine with 32 processors i9-13950HX and 64G RAM, with Hol2dk 2.0, OCaml 5.1.1, Camlp5 8.02.01, Lambdapi 2.5.0 and Coq 8.19.1, or (1) OCaml 4.14.2, Camlp5 8.02.01: +On a machine with 32 processors i9-13950HX and 64G RAM, with HOL-Light ea45176, Hol2dk 2.0, OCaml 4.14.2, Camlp5 8.02.01, Lambdapi 2.5.0 and Coq 8.19.1: -| HOL-Light file | dump-simp(1) | dump size | proof steps | nb theorems | make -j32 lp | make -j32 v | v files size | make -j32 vo | -|------------------------------------|--------------|-----------|-------------|-------------|--------------|-------------|--------------|--------------| -| hol.ml | 3m57s | 3 Gb | 5 M | 5679 | 51s | 55s | 1 Gb | 18m4s | -| Multivariate/make_upto_topology.ml | 48m | 52 Gb | 52 M | 18866 | 22m22s | 20m16s | 68 Gb | 8h (*) | -| Multivariate/make_complex.ml | 2h48m | 158 Gb | 220 M | 41883 | 52m26s | 31m39s | 240 Gb | | +| HOL-Light file | simp | size | steps | thms | lp | v | size | vo | +|------------------------------------|-------|--------|-------|-------|--------|--------|--------|--------| +| hol.ml | 3m57s | 3 Gb | 3 M | 5687 | 51s | 55s | 1 Gb | 18m4s | +| Multivariate/make_upto_topology.ml | 48m | 52 Gb | 52 M | 18866 | 22m22s | 20m16s | 68 Gb | 8h (*) | +| Multivariate/make_complex.ml | 2h48m | 158 Gb | 220 M | 41883 | 52m26s | 31m39s | 240 Gb | | (*) with `make -j32 vo; make -j8 vo` diff --git a/main.ml b/main.ml index 1ffe7fb..89d6630 100644 --- a/main.ml +++ b/main.ml @@ -719,7 +719,7 @@ and command = function (* replace file.prf by file-simp.prf, and recompute file.pos and file.use *) log "replace %s.prf by %s-simp.prf ...\n" b b; - begin match Sys.command (Printf.sprintf "mv %s-simp.prf %s.prf" b b) with + begin match Sys.command ("mv "^b^"-simp.prf "^b^".prf") with | 0 -> begin match log_command ["pos";b] with | 0 -> log_command ["use";b] diff --git a/xlib.ml b/xlib.ml index 0e5b07a..337221c 100644 --- a/xlib.ml +++ b/xlib.ml @@ -62,11 +62,14 @@ let create_file_bin n f = let oc = log_open_out_bin n in f oc; close_out oc;; let read_file_bin n f = let ic = log_open_in_bin n in f ic; close_in ic;; let concat f1 f2 f3 = - log "generate %s ...\n%!" f3; - command (Printf.sprintf "cat %s %s > %s && rm -f %s %s" f1 f2 f3 f1 f2) + log "generate %s ...\n%!" f3; command ("cat "^f1^" "^f2^" > "^f3) ;; -let rename f1 f2 = log "rename %s into %s ...\n%!" f1 f2; Sys.rename f1 f2;; +let remove f = command ("rm -f "^f);; + +let copy f1 f2 = log "generate %s ...\n%!" f2; command ("cp -f "^f1^" "^f2);; + +let rename f1 f2 = log "generate %s ...\n%!" f2; command ("mv -f "^f1^" "^f2);; (* [string_of_file f] puts the contents of file [f] in a string. *) let string_of_file f = diff --git a/xlp.ml b/xlp.ml index 6714bad..223daad 100644 --- a/xlp.ml +++ b/xlp.ml @@ -622,10 +622,10 @@ let decl_axioms oc ths = (****************************************************************************) type decl = - | Unnamed_thm (* lemXXX : abbrev_type := proof *) - | Axiom (* lemXXX : unabbrev_type *) - | Named_thm of string (* name : unabbrev_type := lemXXX *) - | Named_axm of string (* name : unabbrev_type *) + | DefThmIdProof (* lemXXX : abbrev_type := proof *) + | DeclThmId of (*abbrev:*)bool (* lemXXX : [un]abbrev_type *) + | DefThmNameAsThmId of string (* name : unabbrev_type := lemXXX *) + | DeclThmName of string (* name : unabbrev_type *) ;; (* [!proof_part_max_idx] indicates the maximal index of the current part. *) @@ -645,26 +645,26 @@ let decl_theorem oc k p d = in let decl_hyps term = List.iteri (decl_hyp term) in match d with - | Unnamed_thm -> + | DefThmIdProof -> let term = term rmap in let prv = let l = get_use k in l > 0 && l <= !proof_part_max_idx in string oc (if prv then "private" else "opaque"); string oc " symbol lem"; int oc k; typ_vars oc tvs; list (decl_param rmap) oc xs; decl_hyps term ts; string oc " : Prf "; term oc t; string oc " ≔ "; proof tvs rmap oc p; string oc ";\n"; - | Axiom -> - let term = unabbrev_term rmap in + | DeclThmId abbrev -> + let term = if abbrev then term rmap else unabbrev_term rmap in string oc "symbol lem"; int oc k; typ_vars oc tvs; list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts; string oc " : Prf "; term oc t; string oc ";\n" - | Named_thm n -> + | DefThmNameAsThmId n -> let term = unabbrev_term rmap in string oc "opaque symbol "; string oc n; typ_vars oc tvs; list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts; string oc " ≔ @lem"; int oc k; list_prefix " " raw_typ oc tvs; list_prefix " " (var rmap) oc xs; List.iteri (fun i _ -> string oc " h"; int oc (i+1)) ts; string oc ";\n" - | Named_axm n -> + | DeclThmName n -> let term = unabbrev_term rmap in string oc "symbol thm_"; string oc n; typ_vars oc tvs; list (unabbrev_decl_param rmap) oc xs; decl_hyps term ts; @@ -672,11 +672,11 @@ let decl_theorem oc k p d = ;; (* [theorem oc k p] outputs on [oc] the proof [p] of index [k]. *) -let theorem oc k p = decl_theorem oc k p Unnamed_thm;; +let theorem oc k p = decl_theorem oc k p DefThmIdProof;; -(* [theorem_as_axiom oc k p] outputs on [oc] the proof [p] of index - [k] as an axiom. *) -let theorem_as_axiom oc k p = decl_theorem oc k p Axiom;; +(* [theorem_as_axiom abbrev oc k p] outputs on [oc] the proof [p] of index + [k] as an axiom, with abbreviated terms if [abbrev]. *) +let theorem_as_axiom abbrev oc k p = decl_theorem oc k p (DeclThmId abbrev);; (* [proofs_in_interval oc x y] outputs on [oc] the proofs in interval [x] .. [y]. *) @@ -691,7 +691,7 @@ let proofs_in_interval oc x y = let proofs_in_range oc = function | Only x -> let p = proof_at x in - List.iter (fun k -> theorem_as_axiom oc k (proof_at k)) (deps p); + List.iter (fun k -> theorem_as_axiom false oc k (proof_at k)) (deps p); theorem oc x p(*; out oc "flag \"print_implicits\" on; @@ -762,7 +762,8 @@ let export_theorem_term_abbrevs_part b n k = in create_file_with_deps (p^"_head") p iter_deps (fun _ -> ()); (* generate [p^".lp"] *) - concat (p^"_head.lp") (p^"_tail.lp") (p^".lp") + concat (p^"_head.lp") (p^"_tail.lp") (p^".lp"); + remove (p^"_head.lp "^p^"_tail.lp") ;; (****************************************************************************) @@ -856,7 +857,7 @@ let export_theorem_proof b n = Xlib.rename (n^part !proof_part^"_proofs.lp") (n^"_proofs.lp"); write_val (n^".typ") !map_typ_abbrev; export (n^"_spec") [b^"_types";b^"_terms"] - (fun oc -> theorem_as_axiom oc thid (proof_at thid)) + (fun oc -> theorem_as_axiom false oc thid (proof_at thid)) ;; (* 3rd step in command "theorem" when n is not in BIG_FILES. @@ -879,7 +880,8 @@ let export_theorem_deps b n = SetStr.iter (spec f) (Hashtbl.find htbl_thm_deps i); in create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ()); - concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp") + concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp"); + remove (p^"_deps.lp "^p^"_proofs.lp") done ;; @@ -915,19 +917,21 @@ let split_theorem_proof b n = let max_of = Array.init (Hashtbl.length ht_part_max) (Hashtbl.find ht_part_max) in write_val (n^".max") max_of; - (* generate [n^".lp"] and [n^"_spec.lp"]. *) + (* generate [n^".lp"] and [n^"_spec.lp"]. + Remark: these two files are identical. *) let iter_deps f = f (b^"_types"); f (b^"_terms"); spec f (n^part !proof_part); in let p = proof_at max in - let t = Named_thm ("lem"^string_of_int max) in + let t = DefThmNameAsThmId ("lem"^string_of_int max) in export_iter n iter_deps (fun oc -> decl_theorem oc max p t); export_iter (n^"_spec") iter_deps (fun oc -> decl_theorem oc max p t) ;; -(* Called in [export_theorem_proof_part]. +(* Called in [export_theorem_proof_part] which is + called by command "thmpart" in Makefile when n is in BIG_FILES. [split_theorem_abbrevs n] generates the files [n^".brv"], [n^".brp"] and [n^"_term_abbrevs"^part(k)^".min"]. *) let split_theorem_abbrevs n = @@ -995,9 +999,9 @@ let export_theorem_proof_part b n k = let p = part_of d in if p <> !proof_part then part_deps := SetInt.add p !part_deps in - export (p^"_proofs") [] + create_file (p^"_proofs.lp") (fun oc -> - export (p^"_spec") [b^"_types";b^"_terms"] + create_file (p^"_spec_body.lp") (fun oc_spec -> proof_part_max_idx := max - 1; for k = min to max do @@ -1007,7 +1011,7 @@ let export_theorem_proof_part b n k = let p = proof_at k in List.iter add_dep (deps p); theorem oc k p; - if l = 0 || l >= max then theorem_as_axiom oc_spec k p + if l = 0 || l >= max then theorem_as_axiom true oc_spec k p end done)); (* dump term abbreviations *) @@ -1028,8 +1032,11 @@ let export_theorem_proof_part b n k = for j = 1 to nb_parts do f (p^"_term_abbrevs"^part j) done in create_file_with_deps (p^"_deps") p iter_deps (fun _ -> ()); - (* generate [n^part(k)^".lp"] *) - concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp") + create_file_with_deps (p^"_deps") (p^"_spec") iter_deps (fun _ -> ()); + (* generate [n^part(k)^".lp"] and [n^part(k)^"_spec.lp"] *) + concat (p^"_deps.lp") (p^"_proofs.lp") (p^".lp"); + concat (p^"_deps.lp") (p^"_spec_body.lp") (p^"_spec.lp"); + remove (p^"_deps.lp "^p^"_proofs.lp "^p^"_spec_body.lp") ;; (****************************************************************************) @@ -1079,14 +1086,14 @@ let export_proofs b r = (* Generate a declaration of the form "thm_name : type" for each named theorem. *) let out_map_thid_name_as_axioms map_thid_name oc = - MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (Named_axm n)) + MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (DeclThmName n)) map_thid_name ;; (* Generate a declaration of the form "name : type := lemXXX" for each named theorem. *) let out_map_thid_name map_thid_name oc = - MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (Named_thm n)) + MapInt.iter (fun k n -> decl_theorem oc k (proof_at k) (DefThmNameAsThmId n)) map_thid_name ;; diff --git a/xnames.ml b/xnames.ml index da002be..e56b8f2 100644 --- a/xnames.ml +++ b/xnames.ml @@ -37,7 +37,7 @@ let idx = Stdlib.ref (-1);; index. *) let map_thid_name = (* OCaml code for setting [idx] to the index of theorem [name]. *) - let cmd_set_idx = Printf.sprintf "idx := index_of %s;;" in + let cmd_set_idx s = "idx := index_of "^s^";;" in List.fold_left (fun map tname -> (*if tname = "_" then map