use abbreviations in spec files (#152)

- xlp.ml: use abbreviations in spec files, use more informative names for decl constructors, do not create useless .lpo.mk files for temporary lp files - xlib.ml: separate concat and remove - README.md: reduce table width - every where: replace Printf.sprintf by string concatenations
Deducteam · Dec 15, 2024 · 14ba906 · 14ba906
1 parent 8b8947b
commit 14ba906
Show file tree

Hide file tree

Showing 5 changed files with 52 additions and 42 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,38 +645,38 @@ 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;
      string oc " : Prf "; term oc t; string oc ";\n"
 ;;
 
 (* [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
@@ -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